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.


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.

| cite | improve this answer | |
  • $\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$ – Steven Shaw May 7 '16 at 2:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.