2

The laws for monoids in the category of endofunctors are:

monoid laws

And the Haskell monad laws are:

Left identity: return a >>= k = k a

Right identity: m >>= return = m

Associativity: m >>= (\x -> k x >>= h) = (m >>= k) >>= h

I'm assuming the latter is derived from the former, but how so? The diagrams basically say

join (join x) = join (fmap join x)
join (return x) = x
join (fmap return x) = x

How are these equivalent to the Haskell monad laws?

michid
  • 10,536
  • 3
  • 32
  • 59
Ziyang Liu
  • 810
  • 4
  • 10
  • 1
    See also [A monad is just a monoid in the category of endofunctors, what's the problem?](https://stackoverflow.com/questions/3870088/a-monad-is-just-a-monoid-in-the-category-of-endofunctors-whats-the-problem). Doesn't really answer your question, but there's some good reading there anyway. – Daniel Wagner Oct 21 '21 at 20:24

2 Answers2

4

To show the >>=-monad laws from the join-monad laws, one needs to define x >>= y in terms of multiplication (join), unity (return), and functoriality (fmap), so we need to let, by definition,

(x >>= y) = join (fmap y x)

Left identity law

The left identity law then becomes

return a >>= k = k a

By definition of >>=, it is equivalent to

join (fmap k (return a)) = k a

Now, return is a natural transformation I -> T (where I is the identity functor), so fmap_T k . return = return . fmap_I k = return . k. We reduce the law to:

join (return (k a)) = k a

And this follows by the join laws.

Right identity law

The right identity law

m >>= return = m

reduces to, by definition of >>=:

join (fmap return m) = m

which is exactly one of the join laws.

I'll leave the associativity law for you to prove. It should follow using the same tools (join laws, naturality, functoriality).

chi
  • 111,837
  • 3
  • 133
  • 218
2

Phrase the monad laws in terms of the Kleisli composition operator (>=>).

Assuming k :: a -> m b, k' :: b -> m c, k'' :: c -> m d (i.e. k, k', k'' are Kleisli arrows)

  • Left identity: return >=> k = k
  • Right identity: k >=> return = k
  • Associativity: (k >=> k') >=> k'' = k >=> (k' >=> k'')

It's relatively straightforward from the definition of (>=>) to show that these are equivalent to what you wrote. And you don't need any fancy diagrams or anything: these are literally the monoid laws, with return as the identity and (>=>) as your monoid operation.

The diagram you show in your picture is a different way of thinking about monads. You can equivalently define monads in terms of natural transformations (i.e. join and return) or in terms of composition (i.e. return and (>>=) / (>=>)). The latter approach lends itself to the monoid way of thinking that you're looking for.

Silvio Mayolo
  • 62,821
  • 6
  • 74
  • 116
  • 1
    Your last paragraph says that the diagram is a different way of thinking about monads. But the question *starts* with that assumption and asks how the two different ways of thinking are connected. This answer doesn't appear to talk about that at all. – Daniel Wagner Oct 21 '21 at 20:27
  • those are _literally_ the _category_ laws, not the monoid laws. Kleisli arrows form a [category](https://hackage.haskell.org/package/base-4.15.0.0/docs/Control-Category.html#t:Category), not a monoid. an arrow `Kleisli m a b` goes from `a` to `b`. those are two different objects in the Kleisli category. a monoid viewed as a category [has only one object](https://math.stackexchange.com/questions/1332690/monoid-as-a-single-object-category). In Haskell, `Monoid t`, like `Monoid (Sum Int)`. `(<>) :: a -> a -> a` but `Category.. :: cat b c -> cat a b -> cat a c`. – Will Ness Oct 23 '21 at 12:58
  • i.e. `(<=<) :: Kleisli m b c -> Kleisli m a b -> Kleisli m a c`. so a `Monad m` induces a category `Monad m => Category (Kleisli m)`. – Will Ness Oct 23 '21 at 13:22
  • @WillNess : A monoid can alternatively be defined as an object in a monoidal category. The category of endofunctors has monoidal structure with functor composition as multiplication and the identity functor as unit. – Bartosz Milewski Oct 24 '21 at 17:57
  • @BartoszMilewski of course. I was reacting to the answer that presents the Kleisli category as this monoid. – Will Ness Oct 24 '21 at 18:45