On Sun, Nov 22, 2009 at 04:12:29PM +0000, pbrowne wrote:
On Sun, Nov 22, 2009 at 03:32:07PM +0000, Brent Yorgey wrote:
A "free theorem" is a *property* which is satisfied by any function with a particular type. For example, any function with the type
foo :: [a] -> Maybe a
necessarily satisfies
foo (map f xs) = fmap f (foo xs)
A theorem is a statement which has been proved on the basis of previously established theorems or axiom. So, should the definition of the function not satisfy the signature? I may be confusing terminology here. I am coming of an OBJ2/Maude/CafeOBJ background to Haskell. In CafeOBJ a *property* of an operation could, for example, be associativity. I am having difficulty in adjusting to Haskells level of formality.
I'm not quite sure what you're asking here. My point is just that a "free theorem" will be of the form "Any function f of type T, *no matter how f is implemented*, will always satisfy the following property: blah blah f blah = blah f blah " This has nothing to do with whether or not there is only one possible implementation of f that does not involve undefined, which is a different phenomenon.
In Haskell the *theorems for free* means roughly that the definition of a class, instance or a function follows from the supplied types because they are the only types that don’t have undefined argumens or undefined return types.
Question: Is my generalization of applying the "free theorem" concept to classes and instances correct?
Classes don't have types, so I'm not sure what you mean by including classes. Generalizing to instances makes sense; type class instances are just composed of a list of functions. However, again, this notion of there sometimes being only one possible implementation of a particular type has nothing to do with the concept of "free theorems". (At least, it has not much to do with it that I am aware of.)