<p><a href="http://en.wikipedia.org/wiki/Distributive_law_between_monads" rel="nofollow">A distributive law between monads</a> must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are:</p>

<ul>
<li><p>$\mu^S T \circ S l \circ l S = l \circ T \mu^S$, and</p></li>
<li><p>$S \mu^T \circ l T \circ T l = l \circ \mu^T S$</p></li>
</ul>

<p>I would like to state those laws in Haskell in terms of <code>fmap</code>, <code>return</code> and <code>(&gt;&gt;=)</code>. By replacing $\mu$ in the above equation I respectively get:</p>

<ul>
<li><p><code>fmap l (l n) &gt;&gt;= id  ==  l (fmap (\m  -&gt; m &gt;&gt;= id) n)</code>, and</p></li>
<li><p><code>fmap (\m -&gt; m &gt;&gt;= id) (l (fmap l n))  ==  l (n &gt;&gt;= id)</code></p></li>
</ul>

<p>But those equations in this form are not very useful for making proofs by rewriting because such patterns never arise directly in practice and thus I cannot use them for rewriting.</p>

<p>Is there a nicer, smarter and equivalent way to define a distributive law for monads in Haskell terms of <code>fmap</code>, <code>return</code> and <code>(&gt;&gt;=)</code>? I searched the literature on Haskell but the closer I found were <a href="https://en.wikipedia.org/wiki/Monad_transformer" rel="nofollow">monad transformers</a> which seem to involve special cases of distributive law where one of the monad is fixed. However I am interested in the general case.</p>

CC BY-SA 3.0
2014-12-20T01:55:36.617Z
Two arbitrary monads do not satisfy the distributive law in general.  What do you mean by the general case in the last sentence?
Tsuyoshi Ito
CC BY-SA 3.0
2014-12-20T18:20:45.593Z
Thank you @TsuyoshiIto for trying to help but I am not so stupid (^O^)  The "general case" in the last sentence is with respect to the previous sentence.
Bob
CC BY-SA 3.0
2014-12-21T01:10:09.840Z
I know that it is with respect to the previous sentence, and that is why I am confused.  Because distributive law needs two monads (and function l), fixing one monad is not even a special case of it.
Tsuyoshi Ito
CC BY-SA 3.0
2014-12-21T09:24:26.683Z
@TsuyoshiIto: Take for example `MaybeT m a` that is equal to `m (Maybe a)`: there is a distributive law where the first monad $T$ is the variable `m` while the second monad $U$ is fixed to `Maybe`. Does it clarify?
Bob
CC BY-SA 3.0
2014-12-21T11:11:47.483Z
I think that you meant S is an arbitrary monad and T is `Maybe`.  Sure, I can believe that this particular choice satisfies the distributive law with l = `maybe (return Nothing) (fmap Just)`, but what is the more “general case” than this you are interested in?
Tsuyoshi Ito
CC BY-SA 3.0
2016-02-14T15:28:41.750Z
@TsuyoshiIto Bob asks for a Haskell definition of (the type of) distributive law where both monads are parameters; not for a theorem proving this type for two arbitrary monads.
Blaisorblade
<functional-programming><ct.category-theory><haskell><monad>
Distributive law between monads in Haskell
Bob
# Distributive law between monads in Haskell

(Asked by: username_0 on 2014-12-19)

[A distributive law between monads](http://en.wikipedia.org/wiki/Distributive_law_between_monads) must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are:

* $\mu^S T \circ S l \circ l S = l \circ T \mu^S$, and
* $S \mu^T \circ l T \circ T l = l \circ \mu^T S$

I would like to state those laws in Haskell in terms of `fmap`, `return` and `(>>=)`. By replacing $\mu$ in the above equation I respectively get:

* `fmap l (l n) >>= id == l (fmap (\m -> m >>= id) n)`, and
* `fmap (\m -> m >>= id) (l (fmap l n)) == l (n >>= id)`

But those equations in this form are not very useful for making proofs by rewriting because such patterns never arise directly in practice and thus I cannot use them for rewriting.

Is there a nicer, smarter and equivalent way to define a distributive law for monads in Haskell terms of `fmap`, `return` and `(>>=)`? I searched the literature on Haskell but the closer I found were [monad transformers](https://en.wikipedia.org/wiki/Monad_transformer) which seem to involve special cases of distributive law where one of the monad is fixed. However I am interested in the general case.

**Tags:** functional-programming, ct.category-theory, haskell, monad

> **Comments:**
> **username_1**: Two arbitrary monads do not satisfy the distributive law in general.  What do you mean by the general case in the last sentence?  
> **username_0**: Thank you @TsuyoshiIto for trying to help but I am not so stupid (^O^)  The "general case" in the last sentence is with respect to the previous sentence.  
> **username_1**: I know that it is with respect to the previous sentence, and that is why I am confused.  Because distributive law needs two monads (and function l), fixing one monad is not even a special case of it.  
> **username_0**: @TsuyoshiIto: Take for example `MaybeT m a` that is equal to `m (Maybe a)`: there is a distributive law where the first monad $T$ is the variable `m` while the second monad $U$ is fixed to `Maybe`. Does it clarify?  
> **username_1**: I think that you meant S is an arbitrary monad and T is `Maybe`.  Sure, I can believe that this particular choice satisfies the distributive law with l = `maybe (return Nothing) (fmap Just)`, but what is the more “general case” than this you are interested in?  
> **username_2**: @TsuyoshiIto username_0 asks for a Haskell definition of (the type of) distributive law where both monads are parameters; not for a theorem proving this type for two arbitrary monads.  

---

## 0 answers

