<p></p>

<h2>A counter-example for <em>MonadPlusCatch</em> $\rightarrow$ <em>Alternative</em></h2>

<p>Indeed it's <code>MaybeT Either</code>:</p>

<pre><code>{-# LANGUAGE FlexibleInstances #-}
import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Maybe

instance (Show a, Show b) =&gt; Show (MaybeT (Either b) a) where
    showsPrec _ (MaybeT x) = shows x

main = print $
    let
        x = id :: Int -&gt; 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)
       )
</code></pre>

<p>The output is</p>

<pre><code>(Right Nothing, Left "something")
</code></pre>

<p>which means that <code>MaybeT Either</code> fails the left distribution law of <code>Applicative</code>.</p>

<hr>

<p>The reason is that</p>

<pre><code>(return x `mplus` g) `ap` a
</code></pre>

<p>ignores <code>g</code> (due to <em>LeftCatch</em>) and evaluates just to</p>

<pre><code>return x `ap` a
</code></pre>

<p>but this is different from what the other side evaluates to:</p>

<pre><code>g `ap` a
</code></pre>

CC BY-SA 3.0
2012-10-31T09:05:58.973Z
2012-10-31T12:22:40.593Z
2012-10-31T12:22:40.593Z
Petr
<h1><em>MonadPlusDist</em> $\rightarrow$ <em>Alternative</em> is true.</h1>

<h2>Corollary: <em>Alternative</em> $\rightarrow$ <em>MonadPlusCatch</em> is false</h2>

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

<h2>Assumed: MonadPlusDist Laws</h2>

<pre><code>-- (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
</code></pre>

<h2>To prove: Alternative Laws</h2>

<pre><code>-- ((&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
</code></pre>

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

<pre><code>mf &lt;*&gt; mx = mf &gt;&gt;= \f -&gt; mx &gt;&gt;= \x -&gt; return (f x)
</code></pre>

<p>because</p>

<pre><code>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)
</code></pre>

<p><strong><code>&lt;$&gt;</code> expansion lemma</strong><br>
Assume we use the standard derivation of a functor from a monad, namely <code>(&lt;$&gt;) = liftM</code>. Then</p>

<pre><code>f &lt;$&gt; mx = mx &gt;&gt;= return . f
</code></pre>

<p>because</p>

<pre><code>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 
</code></pre>

<h1>Proof</h1>

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

<h2>Right Dist <code>&lt;*&gt;</code></h2>

<p>I'll prove</p>

<pre><code>(mf &lt;+&gt; mg) &lt;*&gt; ma = (mf &lt;*&gt; ma) &lt;+&gt; (mg &lt;*&gt; ma) -- right dist &lt;*&gt;
</code></pre>

<p>because it's easier on the notation.</p>

<pre><code>(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
</code></pre>

<h2>Left Identity <code>&lt;*&gt;</code></h2>

<pre><code>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;=
</code></pre>

<p>as required.</p>

<h2>Left Dist <code>&lt;$&gt;</code></h2>

<pre><code>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
</code></pre>

<h2><code>empty fmap</code></h2>

<pre><code>f &lt;$&gt; mzero = mzero &gt;&gt;= return.f   -- &lt;$&gt; expansion
            = mzero                -- left identity &gt;&gt;=
</code></pre>

<p>as required</p>

CC BY-SA 3.0
2012-10-31T10:37:29.557Z
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
CC BY-SA 3.0
2012-10-31T10:40:12.883Z
@PetrPudlák Updated - finished proof and added your corollory about `[]`.
AndrewC
CC BY-SA 3.0
2012-10-31T10:45:15.253Z
@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
CC BY-SA 3.0
2012-10-31T11:39:48.943Z
I suppose you mean _MonadPlusDist_, don't you? I think we could, this would complete the proof of the corollary.
Petr
CC BY-SA 3.0
2012-10-31T11:59:25.387Z
@PetrPudlák Oh yes I do sorry. Will do.
AndrewC
CC BY-SA 3.0
2012-10-31T09:55:04.883Z
2012-10-31T10:35:41.403Z
2012-10-31T10:35:41.403Z
AndrewC
<p>
Following up <a href="https://stackoverflow.com/q/13122489/1333025">What’s an example of a Monad which is an Alternative but not a MonadPlus?</a>:</p>

<p><strong>Assume $m$ is a monad. What are the relations betweem $m$ being an <em>Alternative</em>, a <em>MonadPlusCatch</em> and a <em>MonadPlusDistr</em>?</strong> 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.</p>

<p>(I'm using</p>

<ul>
<li><p><em>MonadPlusCatch</em> to distinguish a <em>MonadPlus</em> that satisfies the <em>Left-Catch</em> rule:</p>

<pre><code>mplus (return a) b = return a
</code></pre></li>
<li><p><em>MonadPlusDistr</em> to distinguish a <em>MonadPlus</em> that satifies <em>Left-Distribution</em> rule:</p>

<pre><code>mplus a b &gt;&gt;= k = mplus (a &gt;&gt;= k) (b &gt;&gt;= k)
</code></pre></li>
</ul>

<p>see <a href="http://www.haskell.org/haskellwiki/MonadPlus" rel="nofollow noreferrer">MonadPlus on HaskellWiki</a>.)</p>

<hr>

<p>My current knowledge + intuition is that:</p>

<ol>
<li><em>MonadPlusDist</em> $\rightarrow$ <em>Alternative</em> - <strong><strike>likely</strike> true</strong> - <strike>it seems straightforward, I believe I have sketch of a proof, I'll check it and if it's correct, I'll post it</strike> AndrewC answered this part.</li>
<li><em>Alternative</em> $\rightarrow$ <em>MonadPlusDist</em> - <strong>false</strong> - as AndrewC showed in <a href="https://stackoverflow.com/a/13124491/1333025">his answer</a>: <code>Maybe</code> is an <em>Alternative</em>, but it's known it's not <em>MonadPlusDist</em> (it's <em>MonadPlusCatch</em>).</li>
<li><p><em>MonadPlusCatch</em> $\rightarrow$ <em>Alternative</em> - <strong><strike>likely</strike> false</strong> - I believe that <code>MaybeT (Either e)</code> (or basically anything <code>MaybeT m'</code>) should serve as a counterexample. The reason is that</p>

<pre><code>((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)
</code></pre>

<p>again I'll check and post. (Interestingly, for just <code>Maybe</code> it's provable, because we can analyze if <code>a</code> is <code>Just something</code> or <code>Nothing</code> - see the aforementioned AndrewC's answer.)</p></li>
<li><em>Alternative</em> $\rightarrow$ <em>MonadPlusCatch</em> - <strong><strike>likely</strike> false</strong> - if we prove that <em>MonadPlusDist</em> $\rightarrow$ <em>Alternative</em> then <code>[]</code> will server as a counter-example. (Or we could explicitly prove <em>Alternative</em> laws for <code>[]</code>.)</li>
<li><em>MonadPlusDist</em> $\rightarrow$ <em>MonadPlusCatch</em> - <strong>false</strong> - <code>[]</code> is a known counter-example.</li>
<li><em>MonadPlusCatch</em> $\rightarrow$ <em>MonadPlusDist</em> - <strong>false</strong> - <code>Maybe</code> is a known counter-example.</li>
</ol>

<pl.programming-languages><functional-programming><haskell><monad><applicative>
What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)?
Petr
# What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)?

(Asked by: username_0 on 2012-10-31)

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 - 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 username_1 answered this part.
Alternative $\rightarrow$ MonadPlusDist - false - as username_1 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) <|> 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 username_1'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.

**Tags:** pl.programming-languages, functional-programming, haskell, monad, applicative


---

## 2 answers

### Answer by username_1 on 2012-10-31. Score: 9 | Accepted answer

MonadPlusDist $\rightarrow$ Alternative is true.
Corollary: Alternative $\rightarrow$ MonadPlusCatch is false
(because as username_0 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 >>= 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

> **Comments:**
> **username_0**: 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".  
> **username_1**: @username_0Pudlák Updated - finished proof and added your corollory about `[]`.  
> **username_1**: @username_0Pudlá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)`  
> **username_0**: I suppose you mean _MonadPlusDist_, don't you? I think we could, this would complete the proof of the corollary.  
> **username_1**: @username_0Pudlák Oh yes I do sorry. Will do.  

---

### Answer by username_0 on 2012-10-31. Score: 6

A counter-example for MonadPlusCatch $\rightarrow$ Alternative
Indeed it's MaybeT Either:
{-# LANGUAGE FlexibleInstances #-}
import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Maybe

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


---

