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

mplus (return a) b = return a


mplus a b >>= k = mplus (a >>= k) (b >>= k)


My current knowledge + intuition is that:

1. MonadPlusDist $\rightarrow$ Alternative - likely true - it seems straightforward, I believe I have sketch of a proof, I'll check it and if it's correct, I'll post it AndrewC answered this part.
2. 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).
3. MonadPlusCatch $\rightarrow$ Alternative - likely false - 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 Maybe it's provable, because we can analyze if a is Just something or Nothing - see the aforementioned AndrewC's answer.)

4. Alternative $\rightarrow$ MonadPlusCatch - likely false - if we prove that MonadPlusDist $\rightarrow$ Alternative then [] will server as a counter-example. (Or we could explicitly prove Alternative laws for [].)
5. MonadPlusDist $\rightarrow$ MonadPlusCatch - false - [] is a known counter-example.
6. MonadPlusCatch $\rightarrow$ MonadPlusDist - false - Maybe is a known counter-example.
-

# MonadPlusDist $\rightarrow$ Alternative is true.

## Corollary: Alternative $\rightarrow$ MonadPlusCatch is false

(because as Petr Pudlák pointed out, [] is a counterexample - it doesn't satisfy MonadPlusCatch but does satisfy MonadPlusDist, hence Applicative)

-- (mplus,mzero) is a monoid
mzero >>= k = mzero                             -- left identity >>=
(a mplus b) >>= k  =  (a >>=k) mplus (b>>=k) -- left dist mplus


## To prove: Alternative Laws

-- ((<|>),empty) is a monoid
(f <|> g) <*> a = (f <*> a) <|> (g <*> a) -- right dist <*>
empty <*> a = empty                       -- left identity <*>
f <$> (a <|> b) = (f <$> a) <|> (f <$> b) -- left dist <$>
f <$> empty = empty -- empty fmap  <*> expansion lemma Assume we use the standard derivation of an applicative from a monad, namely (<*>) = ap and pure = return. Then mf <*> mx = mf >>= \f -> mx >>= \x -> return (f x)  because mf <*> mx = ap mf mx -- premise = liftM2 id mf mx -- def(ap) = do { f <- mf; x <- mx; return (id f x) } -- def(liftM2) = mf >>= \f -> mx >>= \x -> return (id f x) -- desugaring = mf >>= \f -> mx >>= \x -> return (f x) -- def(id)  <$> expansion lemma
Assume we use the standard derivation of a functor from a monad, namely (<$>) = liftM. Then f <$> mx = mx >>= return . f


because

f <$> mx = liftM f mx -- premise = do { x <- mx; return (f x) } -- def(liftM) = mx >>= \x -> return (f x) -- desugaring = mx >>= \x -> (return.f) x -- def((.)) = mx >>= return.f -- eta-reduction  # Proof Assume (<+>,m0) satisfy the MonadPlus laws. Trivially then it's a monoid. ## Right Dist <*> I'll prove (mf <+> mg) <*> ma = (mf <*> ma) <+> (mg <*> ma) -- right dist <*>  because it's easier on the notation. (mf <+> mg) <*> ma = (mf <+> mg) >>= \forg -> mx >>= \x -> return (forg x) -- <*> expansion = (mf >>= \f_g -> mx >>= \x -> return (f_g x)) <+> (mg >>= \f_g -> mx >>= \x -> return (f_g x)) -- left dist mplus = (mf <*> mx) <+> (mg <*> mx) -- <*> expansion  ## Left Identity <*> mzero <*> mx = mzero >>= \f -> mx >>= \x -> return (f x) -- <*> expansion = mzero -- left identity >>=  as required. ## Left Dist <$>

f <$> (a <|> b) = (f <$> a) <|> (f <$> b) -- left dist <$>

f <$> (a <+> b) = (a <+> b) >>= return . f -- <$> expansion
= (a >>= return.f) <+> (b >>= return.f) -- left dist mplus
= (f <$> a) <+> (f <$> b)               -- <$> expansion  ## empty fmap f <$> mzero = mzero >>= return.f   -- <$> expansion = mzero -- left identity >>=  as required - Great. I even suspect that the left- laws are implied by the right- laws for any Applicative, but I have no proof so far. The intuition is that f <$> doesn't carry any idiomatic action, it's pure, so it might be possible to somehow "switch the sides". – Petr Pudlák Oct 31 '12 at 10:37
@PetrPudlák Updated - finished proof and added your corollory about []. – AndrewC Oct 31 '12 at 10:40
@PetrPudlák Do you think we should add a proof that [] satisfies MonadPlusCatch? At the moment it's just an assertion on the HaskellWiki. >>= k is defined explicitly using foldr ((++).k) – AndrewC Oct 31 '12 at 10:45
I suppose you mean MonadPlusDist, don't you? I think we could, this would complete the proof of the corollary. – Petr Pudlák Oct 31 '12 at 11:39
@PetrPudlák Oh yes I do sorry. Will do. – AndrewC Oct 31 '12 at 11:59

## A counter-example for MonadPlusCatch $\rightarrow$ Alternative

Indeed it's MaybeT Either:

{-# LANGUAGE FlexibleInstances #-}
import Control.Applicative

instance (Show a, Show b) => Show (MaybeT (Either b) a) where
showsPrec _ (MaybeT x) = shows x

main = print \$
let
x = id :: Int -> Int
g = MaybeT (Left "something")
a = MaybeT (Right Nothing)
-- print the left/right side of the left distribution law of Applicative:
in ( ((return x) mplus g) ap a
, ((return x) ap a) mplus (g ap a)
)


The output is

(Right Nothing, Left "something")


which means that MaybeT Either fails the left distribution law of Applicative.

The reason is that

(return x mplus g) ap a


ignores g (due to LeftCatch) and evaluates just to

return x ap a


but this is different from what the other side evaluates to:

g ap a
`
-