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.