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.
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? Pat