7

(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?

Tom
  • 4,910
  • 5
  • 33
  • 48

2 Answers2

11

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

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 doesn't produce a natural transformation:

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

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

as :: m a
flip liftM as :: (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.

Bartosz Milewski
  • 11,012
  • 5
  • 36
  • 45
luqui
  • 59,485
  • 12
  • 145
  • 204
  • 6
    Yup. Parametricity means that functions with the `fmap` type that take `id` to `id` are unique, and from the definition of `liftM` it follows that `liftM id = id`, therefore `liftM = fmap`. Cf. [my answer to a very similar question](https://stackoverflow.com/a/44106008/2751851). – duplode Oct 27 '18 at 15:22
  • 2
    So, just to clarify: You can define a monad as a type constructor `m`, with two polymorphic functions `>>=` and `return`; and it is automatically a functor, with the action on morphisms defined by `liftM`. The question is: What if I define another functor, whose action on objects (the type constructor `m`) is the same, but whose action on morphisms (`fmap`) is different? You are free to do that in category theory, but if you try to do it in Haskell, you're limited by parametricity, which tells you that `fmap` for a given type constructor is unique, as long as it maps identity to identity. – Bartosz Milewski Nov 10 '18 at 10:37
  • Thanks, @luqui. I was not aware of the law of parametricity, which is quite different in its nature to the laws I mentioned in the question: whereas those "laws" are axioms type constructors are expected to fulfil in order to be functors and monads, this one is actually a theorem, bound to hold regardless of how we define our specific types. I'm quite baffled by all this. – Tom Nov 15 '18 at 21:26
  • This was a bit too advanced for me at the time, as I was not really familiar with free theorems and parametricity back then, but looking back at it now I see it's a great answer, and I'll accept it :) (For anyone reading this who's in a similar state to my past self, just hang on in there, and learn about this stuff – it's fascinating! And @luqui, perhaps you can improve your answer with such readers in mind, by adding links to relevant resources suitable for the less initiated? I'd do it myself, but I have yet to come across good resources for beginners...) – Tom Aug 23 '22 at 20:24
6

For this exercise, I found it easier to work with join rather than >>=. A monad can be equivalently defined through return and join, satisfying

1) join . join = join . fmap join
2) join . return = join . fmap return = id

Indeed, join and >>= are inter-definable:

x >>= f = join (fmap f x)
join x = x >>= id

And the laws you mentioned correspond to those above (I won't prove this).

Then, we have:

liftM f x
= { def liftM }
x >>= return . f 
= { def >>= }
join (fmap (return . f) x)
= { def . and $ }
join . fmap (return . f) $ x
= { fmap law }
join . fmap return . fmap f $ x
= { join law 2 }
id . fmap f $ x
= { def id, ., $ }
fmap f x
chi
  • 111,837
  • 3
  • 133
  • 218
  • I am not sure I am satisfied with this, since `fmap` appears in the join laws. Imagine back in the days when `Functor` was not a superclass of `Monad`. That is, I suspect "the laws .. correspond to those above" elides some technical dragons which undermine this argument. – luqui Oct 27 '18 at 13:20
  • @luqui I used that to sweep parametricity under the rug :-P. The OP explicitly mentions "It is well known that every monad is also a functor", so I only focused on "real" monads, in the mathematical sense. I actually prefer your approach to mine since it clearly shows parametricity in action, and avoids passing through an equivalent axiomatization. – chi Oct 27 '18 at 13:25
  • 2
    You are answering a slightly different question. The definition of a monad using `join` and `return` also requires `fmap`. On the other hand, using those three you can define `liftM`. You're showing that this `liftM` is the same as the original `fmap`. This doesn't require parametricity. It is true in any category. – Bartosz Milewski Nov 10 '18 at 10:21
  • this answer answers the question exactly as asked, "how the equivalence of `fmap` and `liftM` (*defined* as `liftM f x = x >>= (return . f)`) can be derived from [the laws]". the other question answers a wider question, "is the function `liftM` with `fmap`'s type necessarily equivalent to `fmap`". – Will Ness Nov 10 '18 at 19:34
  • Thanks, @chi, for showing another useful way to look at it. As opposed to the rules for `>>=`, the rules for `join` do tie it to `fmap`, which makes reaching what we wanted more straightforward, but, as I think @luqui was trying to say, using the equivalence of the two representations here assumes the conclusion (or something equivalent or stronger, e.g. parametricity). Would be nice to see a proof of this equivalence :-) – Tom Nov 15 '18 at 21:13