Assume $m$ is a monad. What are the relations betweem $m$ being an Alternative, a MonadPlusCatch and a MonadPlusDistr? For each of the six possible pairs, I'd like to have either a proof that one implies another, or a counter-example that it doesn't.
MonadPlusCatch to distinguish a MonadPlus that satisfies the Left-Catch rule:
mplus (return a) b = return a
MonadPlusDistr to distinguish a MonadPlus that satifies Left-Distribution rule:
mplus a b >>= k = mplus (a >>= k) (b >>= k)
see MonadPlus on HaskellWiki.)
My current knowledge + intuition is that:
- MonadPlusDist $\rightarrow$ Alternative -
likelytrue - it seems straightforward, I believe I have sketch of a proof, I'll check it and if it's correct, I'll post itAndrewC answered this part.
- Alternative $\rightarrow$ MonadPlusDist - false - as AndrewC showed in his answer:
Maybeis an Alternative, but it's known it's not MonadPlusDist (it's MonadPlusCatch).
MonadPlusCatch $\rightarrow$ Alternative -
likelyfalse - I believe that
MaybeT (Either e)(or basically anything
MaybeT m') should serve as a counterexample. The reason is that
((pure x) <|> g) <*> a = -- LeftCatch (pure x) <*> a -- which in general cannot be equal to ((pure x) <*> a) <|> (g <*> a)
again I'll check and post. (Interestingly, for just
Maybeit's provable, because we can analyze if
Nothing- see the aforementioned AndrewC's answer.)
- Alternative $\rightarrow$ MonadPlusCatch -
likelyfalse - if we prove that MonadPlusDist $\rightarrow$ Alternative then
will server as a counter-example. (Or we could explicitly prove Alternative laws for
- MonadPlusDist $\rightarrow$ MonadPlusCatch - false -
is a known counter-example.
- MonadPlusCatch $\rightarrow$ MonadPlusDist - false -
Maybeis a known counter-example.