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:[EMAIL PROTECTED]
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
