Do the monadic liftM and the functorial fmap have to be equivalent?

  • A+
Category:Languages

(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 idid
  • fmap f . fmap gfmap (f . g)
  • return x >>= ff x
  • x >>= returnx
  • (x >>= f) >>= gx >>= (/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, which comes with any polymorphic function. Categorically, it says that polymorphic functions are natural transformations. It says that any polymorphic function of the form

t :: F a -> G a 

where F and G are functors, commutes with fmap:

t . fmap f = fmap f . t 

If we can make something involving liftM that has the form of a natural transformation, then we will have an equation relating liftM and fmap. liftM itself won't do:

liftM :: (a -> b) -> m a -> m b               --       ^______^               -- these need to be the same 

But here's an idea, since (a ->) is a functor:

m :: m a flip liftM m :: (a -> b) -> m b              --  F    b  -> G b 

Let's try using parametericity on flip liftM m:

flip liftM m . fmap f = fmap f . flip liftM m 

The former fmap is on the (a ->) functor, where fmap = (.), so

flip liftM m . (.) f = fmap f . flip liftM m 

Eta expand

(flip liftM m . (.) f) g = (fmap f . flip liftM m) g flip liftM m (f . g) = fmap f (flip liftM m g) liftM (f . g) m = fmap f (liftM g m) 

This is promising. Take g = id:

liftM (f . id) m = fmap f (liftM id m) liftM f m = fmap f (liftM id m) 

It would suffice to show liftM id = id. That probably follows from its definition:

liftM id m    = m >>= return . id    = m >>= return    = m 

Yep! Qed.

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: