[Haskell-cafe] Unique functor instance

[Janis Voigtlaender]

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