The clue to your answer is in the HaskellWiki about MonadPlus you linked to:
Which rules? Martin & Gibbons choose Monoid, Left Zero, and Left Distribution. This makes [] a MonadPlus, but not Maybe or IO.
So according to your favoured choice, Maybe isn't a MonadPlus (although there's an instance, it doesn't satisfy left distribution). Let's prove it satisfies Alternative.
Maybe is an Alternative
- Right distributivity (of
<*>): (f <|> g) <*> a = (f <*> a) <|> (g <*> a)
Case 1: f=Nothing:
(Nothing <|> g) <*> a = (g) <*> a -- left identity <|>
= Nothing <|> (g <*> a) -- left identity <|>
= (Nothing <*> a) <|> (g <*> a) -- left failure <*>
Case 2: a=Nothing:
(f <|> g) <*> Nothing = Nothing -- right failure <*>
= Nothing <|> Nothing -- left identity <|>
= (f <*> Nothing) <|> (g <*> Nothing) -- right failure <*>
Case 3: f=Just h, a = Just x
(Just h <|> g) <*> Just x = Just h <*> Just x -- left bias <|>
= Just (h x) -- success <*>
= Just (h x) <|> (g <*> Just x) -- left bias <|>
= (Just h <*> Just x) <|> (g <*> Just x) -- success <*>
- Right absorption (for
<*>): empty <*> a = empty
That's easy, because
Nothing <*> a = Nothing -- left failure <*>
- Left distributivity (of
fmap): f <$> (a <|> b) = (f <$> a) <|> (f <$> b)
Case 1: a = Nothing
f <$> (Nothing <|> b) = f <$> b -- left identity <|>
= Nothing <|> (f <$> b) -- left identity <|>
= (f <$> Nothing) <|> (f <$> b) -- failure <$>
Case 2: a = Just x
f <$> (Just x <|> b) = f <$> Just x -- left bias <|>
= Just (f x) -- success <$>
= Just (f x) <|> (f <$> b) -- left bias <|>
= (f <$> Just x) <|> (f <$> b) -- success <$>
- Left absorption (for
fmap): f <$> empty = empty
Another easy one:
f <$> Nothing = Nothing -- failure <$>
Maybe isn't a MonadPlus
Let's prove the assertion that Maybe isn't a MonadPlus: We need to show that mplus a b >>= k = mplus (a >>= k) (b >>= k) doesn't always hold. The trick is, as ever, to use some binding to sneak very different values out:
a = Just False
b = Just True
k True = Just "Made it!"
k False = Nothing
Now
mplus (Just False) (Just True) >>= k = Just False >>= k
= k False
= Nothing
here I've used bind (>>=) to snatch failure (Nothing) from the jaws of victory because Just False looked like success.
mplus (Just False >>= k) (Just True >>= k) = mplus (k False) (k True)
= mplus Nothing (Just "Made it!")
= Just "Made it!"
Here the failure (k False) was calculated early, so got ignored and we "Made it!".
So, mplus a b >>= k = Nothing but mplus (a >>= k) (b >>= k) = Just "Made it!".
You can look at this as me using >>= to break the left-bias of mplus for Maybe.
Validity of my proofs:
Just in case you felt I hadn't done enough tedious deriving, I'll prove the identities I used:
Firstly
Nothing <|> c = c -- left identity <|>
Just d <|> c = Just d -- left bias <|>
which come from the instance declaration
instance Alternative Maybe where
empty = Nothing
Nothing <|> r = r
l <|> _ = l
Secondly
f <$> Nothing = Nothing -- failure <$>
f <$> Just x = Just (f x) -- success <$>
which just come from (<$>) = fmap and
instance Functor Maybe where
fmap _ Nothing = Nothing
fmap f (Just a) = Just (f a)
Thirdly, the other three take a bit more work:
Nothing <*> c = Nothing -- left failure <*>
c <*> Nothing = Nothing -- right failure <*>
Just f <*> Just x = Just (f x) -- success <*>
Which comes from the definitions
instance Applicative Maybe where
pure = return
(<*>) = ap
ap :: (Monad m) => m (a -> b) -> m a -> m b
ap = liftM2 id
liftM2 :: (Monad m) => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 f m1 m2 = do { x1 <- m1; x2 <- m2; return (f x1 x2) }
instance Monad Maybe where
(Just x) >>= k = k x
Nothing >>= _ = Nothing
return = Just
so
mf <*> mx = ap mf mx
= liftM2 id mf mx
= do { f <- mf; x <- mx; return (id f x) }
= do { f <- mf; x <- mx; return (f x) }
= do { f <- mf; x <- mx; Just (f x) }
= mf >>= \f ->
mx >>= \x ->
Just (f x)
so if mf or mx are Nothing, the result is also Nothing, whereas if mf = Just f and mx = Just x, the result is Just (f x)
