<p>You are missing the naturality laws. For every type parameter there is a separate naturality law.</p>
<p>As <code>oK :: (a -&gt; M b) -&gt; (b -&gt; M c) -&gt; a -&gt; M c</code> has 3 type parameters (<code>a</code>, <code>b</code>, <code>c</code>) the function <code>oK</code> will have 3 separate naturality laws.</p>
<p>As <code>bind :: M a -&gt; (a -&gt; M b) -&gt; M b</code> has 2 type parameters (<code>a</code>, <code>b</code>) the function <code>bind</code> will have 2 separate naturality laws.</p>
<p>The laws of <code>bind</code> are equivalent to the laws of the Kleisli composition: if one set of laws holds, then also the other holds, and vice versa.</p>
<p>As a consequence of the monad laws and naturality laws, <code>fmap</code> can be expressed via <code>bind</code> and <code>return</code> as:</p>
<pre><code>fmap f = λ m → bind m (return . f)
</code></pre>
<p>One can also express <code>bind</code> via <code>join</code> and <code>fmap</code>. Then the laws of <code>bind</code> will be equivalent to three laws of <code>join</code> and one naturality law of <code>join</code>.</p>
<p>The formulations of the laws via <code>join</code> is perhaps the simplest one, because <code>join</code> has only one type parameter:</p>
<pre><code> join :: M (M a) -&gt; M a
</code></pre>
<p>The laws of <code>join</code> can be written as:</p>
<pre><code> join . eta = id
 join . fmap eta = id
 join . fmap join = join . join
</code></pre>
<p>The naturality law of <code>join</code> is:</p>
<pre><code> join . fmap (fmap f) = fmap f . join
</code></pre>
<p>That's about it, if we are just looking at general monads.</p>
<p>Specific monads often have additional laws. For example, Haskell's <code>MonadPlus</code> has additional monoid-like methods, and there will be some compatibility laws for that.</p>
<p>There are a few &quot;commutative&quot; monads that have an additional law of &quot;commutativity&quot;. Commutativity means that the order of effects may be permuted without changing the results. The law is:</p>
<pre><code>do
  x &lt;- m1
  y &lt;- m2
  return (x, y)
</code></pre>
<p>must be equal to:</p>
<pre><code>do
  y &lt;- m2
  x &lt;- m1
  return (x, y)
</code></pre>
<p>But there are few commutative monads. <code>Reader</code> is commutative, for example.</p>
<p>If a monad has also a <code>filter</code> method, there should be a suitable compatibility law between <code>filter</code> and <code>join</code>.
The law is best formulated in terms of the <code>catMaybes</code> method instead of <code>filter</code>:</p>
<pre><code>catMaybes . join = join . fmap catMaybes
</code></pre>
<p>The method <code>catMaybes</code> is implemented by the <code>Witherable</code> typeclass: <a href="https://hackage.haskell.org/package/witherable-0.3/docs/Data-Witherable.html#t:Filterable" rel="nofollow noreferrer">https://hackage.haskell.org/package/witherable-0.3/docs/Data-Witherable.html#t:Filterable</a></p>
<p>If a monad has also a <code>fold</code> or <code>traverse</code> method, there should be a suitable compatibility law between <code>traverse</code> and <code>bind</code>.</p>

CC BY-SA 4.0
2024-03-11T21:33:14.460Z
The naturality laws follow from the monad laws automatically if the monad is presented in terms of return and bind.
Max New
CC BY-SA 4.0
2024-03-12T10:23:37.823Z
@MaxNew I don't think one can derive those naturality laws. I don't see how we could get, for example, the naturality law with respect to the type parameter `a` of `bind`: `bind . fmap f = `λ m g -> bind m (g . f)`. Even if you assume the naturality law for `return`, it doesn't seem to help.
winitzki
CC BY-SA 4.0
2024-03-12T12:55:31.387Z
You need to use the fact that fmap is defined in terms of bind then it follows from monad associativity and unit.
Max New
CC BY-SA 4.0
2024-03-13T09:35:13.790Z
@MaxNew Yes, this works if you _define_ `fmap` via `bind` and `return` as `fmap f = λ m → bind m (return . f)`. But any covariant type constructor `m` (and all monads are covariant) already has a standard `fmap` method derived from `m`'s type structure. Naturality laws _must_ use that standard `fmap` method (or else they cannot be derived from parametricity). The laws of `bind` never mention any `fmap`. So, we will not be able to prove that the new `fmap` is the same as the standard `fmap` for `m`. We'd need to postulate that as a new law. Only then we can prove the naturality laws of `bind`.
winitzki
CC BY-SA 4.0
2024-03-13T12:24:17.740Z
Then you can just add a new law that says fmap must be equal to the one defined in terms of return and bind which is much simpler than proving all those naturality properties. And bonus if you do this is that your fmap will be functorial for free from monad laws if you have not established this yet. It is a quirk of Haskell type classes to require me to have a functor instance before defining the monad instance.
Max New
CC BY-SA 4.0
2024-03-13T14:28:44.943Z
And if you really want to limit the discusssion to Haskell (which the original post specified nowhere explicitly) then naturality follows from parametricity anyway. If you are spending time verifying this naturality law you are wasting your time because it is always true.
Max New
CC BY-SA 4.0
2024-03-13T14:45:09.840Z
@MaxNew The original post asked "what are various interesting laws that hold in a monad" and gave some examples of such laws. I am answering the question as stated. Naturality laws are certainly important (even if they hold automatically due to parametricity). It's a different issue to figure out how to formulate monad laws so that verifying those laws for a given monad will take the least work. To that, my answer would be "use the laws of `join`", keeping in mind that for some monads (e.g., `Continuation` and `State`) the Kleisli composition laws are easier to check.
winitzki
CC BY-SA 4.0
2024-03-11T17:16:20.320Z
2024-03-13T11:00:16.330Z
2024-03-13T11:00:16.330Z
winitzki
<p>In a monad, one can prove that the Kleisli composition is associative, and eta is its right and left unit, this is the famous monoid in the endofunctor category:</p>
<pre><code>f oK (g oK h) = (f oK g) oK h

f oK eta = f

eta oK f = f
</code></pre>
<p>Similarly, if you define bind, it has a an associativity law and a left and right unit law, although these are not that algebraic as for the Kleisli composition:</p>
<pre><code>bind m (λa. bind  (k a) h) = bind (bind m k) h

bind m eta = m

bind (eta a) f = f a
</code></pre>
<p>Now, are there any other interesting laws that hold in a monad?</p>
<p>It can be practically interesting, for programming, or theoretically, for mathematics.</p>

<ct.category-theory><algebra><monad>
What theorems are interesting in a monad?
Gergely
# What theorems are interesting in a monad?

(Asked by: username_0 on 2024-03-11)

In a monad, one can prove that the Kleisli composition is associative, and eta is its right and left unit, this is the famous monoid in the endofunctor category:
f oK (g oK h) = (f oK g) oK h

f oK eta = f

eta oK f = f

Similarly, if you define bind, it has a an associativity law and a left and right unit law, although these are not that algebraic as for the Kleisli composition:
bind m (λa. bind  (k a) h) = bind (bind m k) h

bind m eta = m

bind (eta a) f = f a

Now, are there any other interesting laws that hold in a monad?
It can be practically interesting, for programming, or theoretically, for mathematics.

**Tags:** ct.category-theory, algebra, monad

---

## 1 answers

### Answer by username_1 on 2024-03-11. Score: 0 | Accepted answer

You are missing the naturality laws. For every type parameter there is a separate naturality law.
As oK :: (a -> M b) -> (b -> M c) -> a -> M c has 3 type parameters (a, b, c) the function oK will have 3 separate naturality laws.
As bind :: M a -> (a -> M b) -> M b has 2 type parameters (a, b) the function bind will have 2 separate naturality laws.
The laws of bind are equivalent to the laws of the Kleisli composition: if one set of laws holds, then also the other holds, and vice versa.
As a consequence of the monad laws and naturality laws, fmap can be expressed via bind and return as:
fmap f = λ m → bind m (return . f)

One can also express bind via join and fmap. Then the laws of bind will be equivalent to three laws of join and one naturality law of join.
The formulations of the laws via join is perhaps the simplest one, because join has only one type parameter:
 join :: M (M a) -> M a

The laws of join can be written as:
 join . eta = id
 join . fmap eta = id
 join . fmap join = join . join

The naturality law of join is:
 join . fmap (fmap f) = fmap f . join

That's about it, if we are just looking at general monads.
Specific monads often have additional laws. For example, Haskell's MonadPlus has additional monoid-like methods, and there will be some compatibility laws for that.
There are a few "commutative" monads that have an additional law of "commutativity". Commutativity means that the order of effects may be permuted without changing the results. The law is:
do
  x <- m1
  y <- m2
  return (x, y)

must be equal to:
do
  y <- m2
  x <- m1
  return (x, y)

But there are few commutative monads. Reader is commutative, for example.
If a monad has also a filter method, there should be a suitable compatibility law between filter and join.
The law is best formulated in terms of the catMaybes method instead of filter:
catMaybes . join = join . fmap catMaybes

The method catMaybes is implemented by the Witherable typeclass: https://hackage.haskell.org/package/witherable-0.3/docs/Data-Witherable.html#t:Filterable
If a monad has also a fold or traverse method, there should be a suitable compatibility law between traverse and bind.

> **Comments:**
> **username_2**: The naturality laws follow from the monad laws automatically if the monad is presented in terms of return and bind.  
> **username_1**: @MaxNew I don't think one can derive those naturality laws. I don't see how we could get, for example, the naturality law with respect to the type parameter `a` of `bind`: `bind . fmap f = `λ m g -> bind m (g . f)`. Even if you assume the naturality law for `return`, it doesn't seem to help.  
> **username_2**: You need to use the fact that fmap is defined in terms of bind then it follows from monad associativity and unit.  
> **username_1**: @MaxNew Yes, this works if you _define_ `fmap` via `bind` and `return` as `fmap f = λ m → bind m (return . f)`. But any covariant type constructor `m` (and all monads are covariant) already has a standard `fmap` method derived from `m`'s type structure. Naturality laws _must_ use that standard `fmap` method (or else they cannot be derived from parametricity). The laws of `bind` never mention any `fmap`. So, we will not be able to prove that the new `fmap` is the same as the standard `fmap` for `m`. We'd need to postulate that as a new law. Only then we can prove the naturality laws of `bind`.  
> **username_2**: Then you can just add a new law that says fmap must be equal to the one defined in terms of return and bind which is much simpler than proving all those naturality properties. And bonus if you do this is that your fmap will be functorial for free from monad laws if you have not established this yet. It is a quirk of Haskell type classes to require me to have a functor instance before defining the monad instance.  
> **username_2**: And if you really want to limit the discusssion to Haskell (which the original post specified nowhere explicitly) then naturality follows from parametricity anyway. If you are spending time verifying this naturality law you are wasting your time because it is always true.  
> **username_1**: @MaxNew The original post asked "what are various interesting laws that hold in a monad" and gave some examples of such laws. I am answering the question as stated. Naturality laws are certainly important (even if they hold automatically due to parametricity). It's a different issue to figure out how to formulate monad laws so that verifying those laws for a given monad will take the least work. To that, my answer would be "use the laws of `join`", keeping in mind that for some monads (e.g., `Continuation` and `State`) the Kleisli composition laws are easier to check.  

---

