(Note: I'm phrasing the question using Haskell terminology; answers are welcome to use the same terminology and/or the mathematical language of category theory, including proper mathematical definitions and axioms where I speak of functor and monad laws.)
It is well known that every monad is also a functor, with the functor's fmap
equivalent to the monad's liftM
. This makes sense, and of course holds for all common/reasonable monad instances.
My question is whether this equivalence of fmap
and liftM
provably follows from the functor and monad laws. If so it will be nice to see how, and if not it will be nice to see a counterexample.
To clarify, the functor and monad laws I know are the following:
fmap id
≡id
fmap f . fmap g
≡fmap (f . g)
return x >>= f
≡f x
x >>= return
≡x
(x >>= f) >>= g
≡x >>= (\x -> f x >>= g)
I don't see anything in these laws which relates the functor functionality (fmap
) to the monad functionality (return
and >>=
), and so I find it hard to see how the equivalence of fmap
and liftM
(defined as liftM f x = x >>= (return . f)
) can be derived from them. Maybe there is an argument for it which is just not straightforward enough for me to spot? Or maybe I'm missing some laws?
What you have missed is the parametericity law, otherwise known as the free theorem. One of the consequences of parametricity is that all polymorphic functions are natural transformations. Naturality says that any polymorphic function of the form
where
F
andG
are functors, commutes withfmap
:If we can make something involving
liftM
that has the form of a natural transformation, then we will have an equation relatingliftM
andfmap
.liftM
itself doesn't produce a natural transformation:But here's an idea, since
(a ->)
is a functor:Let's try using parametericity on
flip liftM m
:The former
fmap
is on the(a ->)
functor, wherefmap = (.)
, soEta expand
This is promising. Take
g = id
:It would suffice to show
liftM id = id
. That probably follows from its definition:Yep! Qed.
For this exercise, I found it easier to work with
join
rather than>>=
. A monad can be equivalently defined throughreturn
andjoin
, satisfyingIndeed,
join
and>>=
are inter-definable:And the laws you mentioned correspond to those above (I won't prove this).
Then, we have: