The free theorem for fmap

When we write down the definition of Functor we carefully state two laws:

fmap id = id
fmap f . fmap g = fmap (f . g)

These are pretty well known in the Haskell community.

What is less well known is that the second actually follows from the first and parametricity, so you only need to sit down and prove one Functor law when you go to supply a Functor!

This is a “folklore” result, which I've used in conversation many times before, but it continues to surprise folks, so I decided to write up a slow, step by step proof of this result as it is a fun little exercise in equational reasoning.

To prove this we're going to need the free theorem for fmap and a few lemmas.

Free Theorem:
The free theorem for fmap :: (a -> b) -> F a -> F b is that given functions f, g, k, and h such that
g . h = k . f
then
$map g . fmap h = fmap k . $map f
where $map is the "natural map" for the type constructor F.
Proof:
This is a free theorem, so it holds for any function with the same type signature as fmap, regardless of implementation.
You can obtain this theorem employing Philip Wadler's “Theorems for Free” laboriously by hand as is done by Bartosz in the comments below, but we can also obtain this result just by asking lambdabot to do it for us on IRC.
<edwardk> @free fmap :: (a -> b) -> (F a -> F b)
<lambdabot> g . h = k . f => $map_F g . fmap h = fmap k . $map_F f
Thanks, lambdabot!

The natural map has the properties we're looking for, so what we need to do is use the above theorem to prove fmap f = $map f, and borrow them.

Note: There are some caveats about precisely when such a natural map exists in the comments below, but in any case where fmap can be given with fmap id = id, it can also exist with this variance.

To do that we start with

Lemma 1:

Given fmap id = id, then

fmap f = $map f

Proof:

fmap f 
= {- by $map id = id -}
$map id . fmap f
= {- by free theorem, using g = k = id, h = f -} 
fmap id . $map f
= {- by fmap id = id -}
$map f

Now we know that fmap f = $map f pointwise, and if we assume functional extensionality, we can even show fmap = $map.

Lemma 1 is sufficient to show that any two definitions fmap1 and fmap2 for fmap that each satisfy fmap id = id, are equivalent up to functional extensionality, as of course fmap1 f = $map f = fmap2 f.

Therefore the observable behavior of fmap is uniquely determined.

Next we'll, need another precondition:

Lemma 2:
f . g = id . (f . g)
Proof:
Naively, id is the unit for (.). In reality it results in it eta-expanded.

Now we're finally ready to proceed to the real proof:

Theorem:
Given fmap id = id, we can show that
fmap f . fmap g = fmap (f . g)
Proof:
We can read this off of the properties of the free theorem several ways.
The easiest one which does not use the same shaped property on $map is to just play with $map id = id
fmap f . fmap g 
= {- by lemma 1, fmap f = $map f -}
$map f . fmap g
= {- by the free theorem for fmap using lemma 2 for the precondition -}
fmap id . $map (f . g)
= {- by fmap id = id -}
$map (f . g)
= {- by fmap _ = $map _ -}
fmap (f . g)

(We could have also employed the fact that $map f . $map g = $map (f . g) more directly.)

There is definitely room to improve this proof. It would be more satisfying to start with two definitions of fmap such that they both satisfy fmap_1 id = id and fmap_2 id = id, and show that they must be equivalent up to functional extensionality, rather than appeal to the existence of a "natural map", which is a bit hand wavy. Russell O'Connor took a similar approach to concisely show that fmap is uniquely determined, if it exists, on the libraries mailing list.

But there you have it. Next time you go to write a Functor, you can rest assured that you only need to prove fmap id = id, and you can get the other result for free!

-Edward Kmett

February 15, 2015

Sections