24

The monad laws are traditionally described in terms of >>= and pure:

pure a >>= k = k a
m >>= pure = m
m >>= (\x -> k x >>= h) = (m >>= k) >>= h

However, monads can also be defined in terms of join instead of >>=. I would like to come up with a formulation of the monad laws in terms of join.

Using x >>= f = join (fmap f x), it’s easy to rewrite the existing monad laws to eliminate >>=. Simplifying the results slightly with the help of the applicative laws, the first two laws are quite pleasantly expressed:

join . pure = id
join . fmap pure = id

The intuition for these laws is easy, too, since clearly, introducing an extra “layer” with pure should be a no-op when combined with join. The third law, however, is not nearly so nice. It ends up looking like this:

  join (fmap (\x -> join (fmap h (k x))) m)
= join (fmap h (join (fmap k m)))

This does not pleasantly reduce using the applicative laws, and it’s much harder to understand without staring at it for a while. It certainly doesn’t have the same easy intuition.

Is there an equivalent, alternative formulation of the monad laws in terms of join that is easier to understand? Alternatively, is there any way to simplify the above law, or to make it easier to grok? The version with >>= is already less nice than the one expressed with Kleisli composition, but the version with join is nearly unreadable.

1
  • 3
    If such terse mathematical language is accessible to you, I think this is a clear definition. Basically, the left-hand diagram corresponds to the first two laws you've stated (join . pure = join . fmap pure = id) and the right-hand diagram can be stated as join . join = join . fmap join. Note that (\h k m -> join (fmap h (join (fmap k m)))) id id = \m -> join (join m) - this follows from fmap id = id (and likewise for the other side of the two equalities). In other words, your law expresses both functor and monad laws in one statement. Commented Aug 23, 2017 at 1:52

1 Answer 1

28

Stolen straight from Wikipedia:

(The natural transformation η: 1 -> T is pure; the natural transformation µ: T^2 -> T is join)

µ . Tµ = µ . µT

In Haskell:

join . fmap join = join . join

In English: If you start with three layers of monad as mmma :: Monad m => m (m (m a)), it doesn't matter if you flatten it inner layer first and then outer, or flatten it outer layer first and then inner. This is the same law as what you listed as the third (associativity).

µ . Tη = µ . ηT = 1

In Haskell:

join . fmap pure = join . pure = id

In English: If you start with one layer of monad as ma :: Monad m => m a, it doesn't matter if you create a new layer inside it and then flatten it, or if you create a new layer outside it and then flatten it, and both are the same as doing nothing at all. This law is a combination of your first two.

Also, join being a natural transformation means that

join . fmap (fmap f) = fmap f . join

because of parametricity.

11
  • 6
    With your English explanation, I think I actually prefer these laws to the Kleisli composition version.
    – 4castle
    Commented Aug 23, 2017 at 4:14
  • You're missing one law: join . fmap (fmap f) ≡ fmap f . join
    – Shersh
    Commented Oct 28, 2017 at 20:16
  • 4
    @Shersh That's implied by join being a natural transformation. A natural transformation is f: F -> G must have f . F(m) = G(m) . f for all morphisms m.
    – HTNW
    Commented Oct 28, 2017 at 20:23
  • 1
    All this is really good... But I can't see how to derive this law from other two laws in your question. The origin question is about Monad laws in terms of join so it's quite reasonable to see all laws for Monad. It's just the fact that not every person knows Category Theory but this person may google "Monad laws in terms of join" and won't find all laws.
    – Shersh
    Commented Oct 28, 2017 at 20:49
  • 3
    join :: forall m a. Monad m => m (m a) -> m a (join is indexed by m and is parametric in a). Parametric types give rise to theorems. In particular, if Functor f, g, then for any r :: forall a. f a -> g a, the type tells you that r . fmap @f k = fmap @g k . r for all k. In the case of join, g = m and f = m . m, so fmap @f k = fmap @m (fmap @m k) and you get the law join . (fmap (fmap k)) = fmap k . join This law is therefore implied by the type of join and is checked by the typechecker. people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
    – HTNW
    Commented Oct 28, 2017 at 22:25

Not the answer you're looking for? Browse other questions tagged or ask your own question.