Janis Voigtlaender voigt at tcs.inf.tu-dresden.de
Tue Nov 25 08:49:58 EST 2008

```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 at tcs.inf.tu-dresden.de

```