What's the relationship between free theorems and free objects from algebra. They seem quite similar. I'm wondering if there's an underlying principle here.
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
There is no relationship. They both use the word "free", but with different meanings of the word "free". It's just an accidental collision, which will happen when you have a language like English with a fixed number of words and the number of concepts we want to talk about exceeds the number of words in the language.
A free group is, roughly, a group that is about as generic as possible (it has no special structure). Here, the word free means "having no non-trivial strucutre", i.e., free of special equalities.
In contrast, a free theorem about some code (e.g., a function) is one that follows automatically from the type signature of that code. Here, the word free means "at no cost" or "with no extra reasoning about the code required"; it's an automatic consequence of the type signature, regardless of the implementation/code of the function.
-
$\begingroup$ and yet free objects are, in a sense, generated from the axioms. Free theorems are generated (as you say "follow automatically") from the type signature. $\endgroup$ Commented May 7, 2016 at 2:08