# Writing the coherence conditions for a monad in a functional laguage

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.

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$$

∀ f, eta . f = fun f . eta
`