When we defining a Functor
instance in Haskell, it should satisfy the following two laws:
fmap id = id
fmap f . fmap g = fmap (f . g)
But I found these two articles that say the second Functor law can be derived form the first:
The proof in these articles uses the free theorem for fmap
. For example, the second article says that:
Free Theorem:
The free theorem for
fmap :: (a -> b) -> F a -> F b
is that given functionsf
,g
,k
, andh
such thatg . h = k . f
then
$map g . fmap h = fmap k . $map f
where
$map
is the "natural map" for the type constructorF
.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
!
I cannot find Bartosz's comment, so I found and read Philip Wadler's “Theorems for Free”.
Philip Wadler's “Theorems for Free” basically says that for each type $T$, there is a corresponding relation $\mathcal{T}$, and every closed term $t$ of type $T$ satisfies $(t,t)\in\mathcal{T}$.
The type constructor $F$ of the Functor would also give a function $\mathcal{F}$ from relations to relations. This is the "natural map" $map
in the article. But the problem is, this $map
does not always map functions to functions.
When I tried to derive fmap
's free theorem by hand, I got this:
For given functions
f :: A -> B
,g :: C -> D
,k :: B -> D
,h :: A -> C
such thatg . h = k . f
then for every
x :: F A
andy :: F C
, if(x, y)
is in the relation$map h
, then(fmap f x, fmap g y)
is in the relation$map g
.
If we can show that $map
actually maps functions to functions, this result would be the same as that in the article.
But there are some type constructors that $map
doesn't maps functions to functions. For example, for F a = a -> ()
, $map
would map functions to functions in the inverse direction.
How do I fill this gap of the proof?