Writing the coherence conditions for a monad in a functional laguage

Question

i recently asked a related question about the relationship between monads in category theory and Haskell. The answerer showed me the following classes and instances:

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 m = m >>== (ret . f)
  eta     = ret
  mu m    = m >>== id

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

And told me I should show that the rules for each class are equivalent. I've finally gotten around to this exercise but I've already run into some confusion.

I know that the "laws" for a Kleisli Triple are as follows:

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

And I know that the coherence conditions for a monad can be written $$\mu \circ \eta T = \mu \circ T \eta = id_C$$ $$\mu \circ \mu T = \mu \circ T \mu$$ Where $T$ is the endofunctor, fun in the Haskell class.

I know $(\eta T)_x = \eta_{T\, x}$ and $(T\eta)_x=T(\eta_x)$, so I think the rules for MyMonad could be written as follows:

mu . eta . (fun f) = f
mu . (fun eta) = id
mu . mu . (fun id) = mu . (fun mu)

Writing any of these expressions as a function with the desired type signatures loads in GHCI, but I don't think I'm right.

It's mainly associativity that I'm not confident about. Unwrapping associativity for the Kleisli triple yields

mu (fun g (mu (fun f m))) = mu (fun (\x -> mu (fun g (f x))) m)

Which seems over-complicated, but unlike my attempt to express the category-theoretic constraints, this equation universally quantifies over the functions

f :: a -> m b 
g :: b -> m c`

How close am I to coming to the correct conclusion? Hints would be appreciated.

Answer 1

First off, you've confused $\nu$ and $\eta$ in your class. I'm going to go with $\eta$.

The coherency law:

$$\mu \circ T \eta = \mu \circ \eta T = 1_T$$

translates to:

mu . fun eta = mu . eta = id

And the other coherency law:

$$\mu \circ T\mu = \mu \circ \mu T$$

translates to:

mu . fmap mu = mu . mu

Intuitively, the reason why the $T$ "disappears" when translating $\mu T$ to mu is the same reason why it "disappears" when translating $1_T$ into id: in Haskell, types are passed implicitly. If you translate this into System $F_\omega$ (or GHC Core!) the types are passed explicitly and the correspondence is more obvious. I'm going to leave you that one as an exercise.

One more thing. Don't forget the other conditions on mu and eta: they have to be natural transformations! The coherency conditions in category theory are:

$$\forall f : X \rightarrow Y, \eta_Y \circ f = T(f) \circ \eta_X$$ $$\forall f : X \rightarrow Y, \nu_Y \circ T^2(f) = T(f) \circ \nu_X$$

In Haskell:

∀ f, eta . f = fun f . eta
∀ f, nu . fun (fun f) = fun f . nu

In category theory, you might need to prove these, but in Haskell you don't because they are the free theorems for those functions. This is a very nice property of Haskell: Ignoring bottom values and general recursion, any function with the type of a natural transformation must be a natural transformation.

(This is also a good piece of intuition as to what is so "natural" about natural transformations. It means that the "forall" in a polymorphic type is a real "forall"; it's true for any type with no exceptions.)