Following up What’s an example of a Monad which is an Alternative but not a MonadPlus?:
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.
(I'm using
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:
Maybe
is an Alternative, but it's known it's not MonadPlusDist (it's MonadPlusCatch). MonadPlusCatch $\rightarrow$ Alternative -
likelyfalse - I believe thatMaybeT (Either e)
(or basically anythingMaybeT 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
Maybe
it's provable, because we can analyze ifa
isJust something
orNothing
- 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 -
Maybe
is a known counter-example.