What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)? 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 &gt;&gt;= k = mplus (a &gt;&gt;= k) (b &gt;&gt;= k)



see MonadPlus on HaskellWiki.)



My current knowledge + intuition is that:


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.
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 - likely false - I believe that MaybeT (Either e) (or basically anything MaybeT m') should serve as a counterexample. The reason is that

((pure x) &lt;|&gt; g) &lt;*&gt; a =    -- LeftCatch
    (pure x) &lt;*&gt; a
-- which in general cannot be equal to
((pure x) &lt;*&gt; a) &lt;|&gt; (g &lt;*&gt; 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.)
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 [].)
MonadPlusDist $\rightarrow$ MonadPlusCatch - false - [] is a known counter-example.
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)

Assumed: MonadPlusDist Laws

-- (mplus,mzero) is a monoid
mzero &gt;&gt;= k = mzero`                             -- left identity &gt;&gt;=
(a `mplus` b) &gt;&gt;= k  =  (a &gt;&gt;=k) `mplus` (b&gt;&gt;=k) -- left dist mplus


To prove: Alternative Laws

-- ((&lt;|&gt;),empty) is a monoid
(f &lt;|&gt; g) &lt;*&gt; a = (f &lt;*&gt; a) &lt;|&gt; (g &lt;*&gt; a) -- right dist &lt;*&gt;
empty &lt;*&gt; a = empty                       -- left identity &lt;*&gt;
f &lt;$&gt; (a &lt;|&gt; b) = (f &lt;$&gt; a) &lt;|&gt; (f &lt;$&gt; b) -- left dist &lt;$&gt;
f &lt;$&gt; empty = empty                       -- empty fmap


&lt;*&gt; expansion lemma
Assume we use the standard derivation of an applicative from a monad, namely (&lt;*&gt;) = ap and pure = return. Then

mf &lt;*&gt; mx = mf &gt;&gt;= \f -&gt; mx &gt;&gt;= \x -&gt; return (f x)


because

mf &lt;*&gt; mx = ap mf mx                                  -- premise
          = liftM2 id mf mx                           -- def(ap)
          = do { f &lt;- mf; x &lt;- mx; return (id f x) }  -- def(liftM2)
          = mf &gt;&gt;= \f -&gt; mx &gt;&gt;= \x -&gt; return (id f x) -- desugaring
          = mf &gt;&gt;= \f -&gt; mx &gt;&gt;= \x -&gt; return (f x)    -- def(id)


&lt;$&gt; expansion lemma
Assume we use the standard derivation of a functor from a monad, namely (&lt;$&gt;) = liftM. Then

f &lt;$&gt; mx = mx &gt;&gt;= return . f


because

f &lt;$&gt; mx = liftM f mx                    -- premise
         = do { x &lt;- mx; return (f x) }  -- def(liftM)
         = mx &gt;&gt;= \x -&gt; return (f x)     -- desugaring
         = mx &gt;&gt;= \x -&gt; (return.f) x     -- def((.))
         = mx &gt;&gt;= return.f               -- eta-reduction 


Proof

Assume (&lt;+&gt;,m0) satisfy the MonadPlus laws. Trivially then it's a monoid.

Right Dist &lt;*&gt;

I'll prove

(mf &lt;+&gt; mg) &lt;*&gt; ma = (mf &lt;*&gt; ma) &lt;+&gt; (mg &lt;*&gt; ma) -- right dist &lt;*&gt;


because it's easier on the notation.

(mf &lt;+&gt; mg) &lt;*&gt; ma = (mf &lt;+&gt; mg) &gt;&gt;= \forg -&gt; mx &gt;&gt;= \x -&gt; return (forg x) -- &lt;*&gt; expansion
                   =     (mf &gt;&gt;= \f_g -&gt; mx &gt;&gt;= \x -&gt; return (f_g x))
                     &lt;+&gt; (mg &gt;&gt;= \f_g -&gt; mx &gt;&gt;= \x -&gt; return (f_g x))      -- left dist mplus
                   = (mf &lt;*&gt; mx) &lt;+&gt; (mg &lt;*&gt; mx)                           -- &lt;*&gt; expansion


Left Identity &lt;*&gt;

mzero &lt;*&gt; mx = mzero &gt;&gt;= \f -&gt; mx &gt;&gt;= \x -&gt; return (f x) -- &lt;*&gt; expansion
             = mzero                                     -- left identity &gt;&gt;=


as required.

Left Dist &lt;$&gt;

f &lt;$&gt; (a &lt;|&gt; b) = (f &lt;$&gt; a) &lt;|&gt; (f &lt;$&gt; b) -- left dist &lt;$&gt;

f &lt;$&gt; (a &lt;+&gt; b) = (a &lt;+&gt; b) &gt;&gt;= return . f              -- &lt;$&gt; expansion
                = (a &gt;&gt;= return.f) &lt;+&gt; (b &gt;&gt;= return.f) -- left dist mplus
                = (f &lt;$&gt; a) &lt;+&gt; (f &lt;$&gt; b)               -- &lt;$&gt; expansion


empty fmap

f &lt;$&gt; mzero = mzero &gt;&gt;= return.f   -- &lt;$&gt; expansion
            = mzero                -- left identity &gt;&gt;=


as required