Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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:

  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.
share|improve this question
add comment

2 Answers 2

up vote 5 down vote accepted

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 >>= 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

share|improve this answer
    
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
add comment

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
share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.