Janis Voigtlaender wrote:
A free theorem can be used to prove that any
f :: (a -> b) -> [a] -> [b]
which satisfies
f id = id
also satisfies
f = map (for the Haskell standard map).
Here comes the full proof. Feed http://linux.tcs.inf.tu-dresden.de/~voigt/ft/ with the type of f. The output is: For every f :: forall a b . (a -> b) -> [a] -> [b] holds: forall t1,t2 in TYPES, g :: t1 -> t2. forall t3,t4 in TYPES, h :: t3 -> t4. forall p :: t1 -> t3. forall q :: t2 -> t4. (forall x :: t1. h (p x) = q (g x)) ==> (forall y :: [t1]. map h (f p y) = f q (map g y)) Set p = id and g = id. It results: forall t3,t4 in TYPES, h :: t3 -> t4. forall q :: t3 -> t4. (forall x :: t3. h (id x) = q (id x)) ==> (forall y :: [t3]. map h (f id y) = f q (map id y)) The precondition is obviously fulfilled whenever h = q. So we get, for every h, forall y :: [t3]. map h (f id y) = f h (map id y) Now note that we assume f id = id, and also know map id = id. This gives: forall y :: [t3]. map h y = f h y This is the desired extensional equivalence of map and f. All we needed was a free theorem and the identity law. The same kind of proof works for the Tree type, and friends. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de