3
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ Two arbitrary monads do not satisfy the distributive law in general. What do you mean by the general case in the last sentence? $\endgroup$ – Tsuyoshi Ito Dec 20 '14 at 1:55
  • $\begingroup$ 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. $\endgroup$ – Bob Dec 20 '14 at 18:20
  • $\begingroup$ 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. $\endgroup$ – Tsuyoshi Ito Dec 21 '14 at 1:10
  • $\begingroup$ @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? $\endgroup$ – Bob Dec 21 '14 at 9:24
  • $\begingroup$ 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? $\endgroup$ – Tsuyoshi Ito Dec 21 '14 at 11:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.