How is the definition of monads in category theory equivalent to the definition in functional programming?

Question

In Haskell, Monad is a class of type constructors which act on types that have the following functions implemented:

(>>=)  :: m a -> (a -> m b) -> m b
(>>)   :: m a ->       m b  -> m b
return ::   a               -> m a

and they satisfy the following "laws:"

return a >>= f      = f a
m        >>= return = m
(m >>= f) >>= g = m >>= m >>= (\x -> f x >>= g)

I understand why a type with these functions implemented with those constraints is useful, because I've used them. But to be completely honest, I'm interested in pure mathematics over programming, so I want to understand the category theoretic origins of monads.

Monads in category theory seem very different, they are ordered triples $\langle T, \mu, \nu\rangle$. Where $T$ is an endofunctor on a given category $C$, $\mu : 1_C \rightarrow T$ is a natural transformation as is $\nu : T\circ T \rightarrow T$ such that they all satisfy conditions reminiscent of the one's for Haskell monads. It seems like return, which I understand to be the type constructor for an instance of monad, is the endofunctor $T$.

In essence I want to understand which functions are which natural transformations, and why, but I also want to understand why return is an endofunctor, acting on a category, even though it seems like most types in Haskell are treated as objects.

I was once watching Bartosz Milewski lecture and he said that monads can be thought of as "monoids on the category of endofunctors." I stopped watching because I didn't know what monoids were at the time. But now when I think "monoid on the category of endofunctors" I think "The set of endofunctors on a category under composition." But I don't see how an object like this could relate to the definition of a monad, so if someone could explain that as well it would be greatly appreciated.

Answer 1

The Haskell monads are known as Kleisli triples in mathematics. I am guessing you're coming from the Haskell land, so let me just put down the translations between the two formulations in Haskell (I define everything from scratch on purpose and avoid clashes with standard notation):

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}

class MyMonad t where
  fun :: (a -> b) -> (t a -> t b) -- functorial action, known as fmap
  eta :: a -> t a
  mu :: t (t a) -> t a

class KleisliTriple t where
  ret :: a -> t a
  (>>==) :: t a -> (a -> t b) -> t b

instance KleisliTriple t => MyMonad t where
  fun f x = (x >>== (ret . f))
  mu x = (x >>== id)
  eta = ret

instance MyMonad t => KleisliTriple t where
  ret = eta
  (>>==) x f = mu (fun f x)

There's a bunch of equations to be verified, but they all work out, which is not to say that you should trust me or anyone else, work them out, it's a good exercise. Actually, you should try to reconstruct things by yourself. Take the code above and delete the two instances. Then try to reconstruct their definitions.

As for your question about monads being monoids in the endofunctor category, you'll just have to unfold all the definitions in the privacy of your own mind. I can give you a roadmap, but until you pick up pencil and paper and go through it all by yourself, it's not going to click.

Recall that a monoid is given by a set $T$, a multiplication operation $\mu : T \times T \to T$, and an element $\eta \in T$ such that

1. $\mu (x, \eta) = x$
2. $\mu (\eta, x) = x$
3. $\mu (\mu (x, y), z) = \mu (x, \mu (y, z))$

$\newcommand{\CC}{\mathcal{C}}$ $\newcommand{\pair}[1]{\langle #1 \rangle}$ This can be generalized as follows. Consider a monoidal category $\mathcal{C}$. It has a tensor product $\otimes$ which behaves a little like ordinary binary products, and it has a special object $I$ which is a unit for the tensor. A monoid object in the monoidal category $\CC$ is given by the following data:

• an object $T \in \CC$
• an arrow $\mu : T \otimes T \to T$
• an arrow $\eta : I \to T$

subject to the laws that correspond to the three laws above. I am not going to reproduce the laws here, you can find them here.

If we take $\CC = \mathsf{Set}$, $A \otimes B = A \times B$, and $I = 1$ then we recover the usual notion of monoid.

Now let $\CC$ be any category (no monoidal structure required). The functor category $\CC^\CC$ is monoidal if we take the tensor to be composition of functors $F \otimes G = F \circ G$, and the unit the identity functor $I = \mathsf{Id}_{\CC}$. What is a monoid object in $\CC^\CC$? It is given by the following data:

• a functor $T : \CC \to \CC$
• a natural transformation $\mu : T \circ T \to T$
• a natural transformation $\eta : \mathsf{Id} \to T$

subject to some laws. When we unfold those laws we get, you guessed it, precisely the laws for a monad.