Prove that all monads are functors

Question

It is often written that all monads are functors, but it is quite hard to find an actual mathematical proof of it.

A functor is defined as a higher level type defining the fmap function:

class Functor f where 
   fmap :: (a -> b) -> f a -> f b 

It must also preserve composition:

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

And follow the identity law:

fmap id == id

A monad is defined as:

class Monad m where
  (>>=)  :: m a -> (  a -> m b) -> m b
  return ::   a                 -> m a

And the bind function must follow the three laws: left identity, right identity and associativity.

fmap for a monad can be defined as:

fmap f xs  =  xs >>= return . f

In order to prove that all monads are functors, we must prove that such a fmap function follow the composition and identity laws of functors. It's easy enough to prove identity using the left identity law of monads, but I am struggling to show that such definition of fmap conserves composition.

Does someone know the proof for this?

Answer 1

An alternate to the usual definition of a monad (as a functor plus some structure) that's similar to your Haskell definition has three pieces of structure and three equations.

Let $\mathcal C$ be a category. A monad on $\mathcal C$ consists of a map on objects $T : Ob(\mathcal C) \to Ob(\mathcal C)$, for each object $x \in Ob(\mathcal C)$ a morphism $\eta_x : x \to T(x)$ and for each morphism $f : x \to T(y)$, a morphism $f^T : T(x) \to T(y)$.

This structure should satisfy the equations $(\eta_x)^T = id_{T(x)}$, $f^T \circ \eta_x = f$ and $(f^T \circ g)^T = f^T \circ g^T$.

$T$ corresponds to your type function m. $\eta_x$ is the same as return and $f^T$ corresponds to the function that takes x to x >>= f.

---

$T$ can then be extended to morphisms via $T(f) = (\eta_y \circ f)^T$ (where $f : x \to y$).

Then $T(id_x) = (\eta_x \circ id_x)^T = (\eta_x)^T = id_{T(x)}$. Moreover, for $f : y \to z$ and $g : x \to y$,

$$ \begin{align} T(f) \circ T(g) &= (\eta_z \circ f)^T \circ (\eta_y \circ g)^T\\ &= ((\eta_z \circ f)^T \circ \eta_y \circ g)^T\\ &= (\eta_z \circ f \circ g)^T\\ &= T(f \circ g). \end{align} $$

So $T$ is a functor.

Answer 2

I'm not convinced that this is a math question... Mathematically (as Zhen Lin points out), it's part of the definition of a monad that it also be a functor.

The question is really about the haskell typeclasses "Monad" and "Functor", and while these are obviously made to imitate their categorical namesakes, there's no way to guarantee that the monad/functor laws actually hold for your implementation. Moreover, it used to be the case that haskell Monads weren't required to be Functors, and some old tutorials still emphasize this fact. This was widely regarded to be a Bad Idea™, especially since any Monad instance which actually satisfies the monad laws will automatically be a functor!

Thankfully, as of GHC 7.10, it's explicitly required that a Monad be an Applicative (and thus a Functor) as part of the definition. See here for instance.

This is OK since, as I mentioned earlier, it's always been possible to derive the applicative data (pure and <*>) as well as the functor data (fmap) from the data of a monad instance (namely return and >>=). This all makes sense, since mathematically we know that every monad should be a functor. So if these typeclasses aren't badly named, it should be true for them too!

Now, for completeness, how do we actually derive Applicative and Functor instances from a Monad instance?

For applicatives, pure is defined to be return and <*> is defined to be

<*> :: m (a -> b) -> m a -> m b
mf <*> mx = do
  f <- mf
  x <- mx
  return $ f x

I'll leave it as an exercise to desugar this do notation into something using only return and >>=.

To get from applicatives to functors, you can check that

fmap :: (a -> b) -> m a -> m b
fmap f mx = pure f <*> mx

works. As another exercise, can you compose these in order to directly write fmap using return and >>=?

Lastly, as a more mathematical question, you might be interested in proving that the Functor laws hold for this definition, provided we assume that the Monad laws hold for the Monad we started with! With the definition of fmap in hand, this isn't so hard, and you should definitely try to do it yourself!

---

I hope this helps ^_^