A 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 which seem to involve special cases of distributive law where one of the monad is fixed. However I am interested in the general case.

• 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 Dec 20 '14 at 1:55
• 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 Dec 20 '14 at 18:20
• 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 Dec 21 '14 at 1:10
• @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 Dec 21 '14 at 9:24
• 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 Dec 21 '14 at 11:11