什么是替代但不是MonadPlus的Monad的例子?

Question

在回答"类型类MonadPlus、Alternative和Monoid之间的区别？"时，爱德华·克米特说：

此外，即使Applicative是Monad的超阶级，你最终也需要MonadPlus类，因为服从

empty <*> m = empty

不足以严格证明这一点

empty >>= f = empty

因此，声称某物是MonadPlus比声称它是Alternative更强大。

很明显，任何不是monad 的应用函子都自动成为不是MonadPlus的Alternative的例子，但 Edward Kmett 的回答暗示存在一个monad是一个Alternative而不是一个MonadPlus：它的empty和<|>将满足Alternative定律，¹但不是MonadPlus法。^{阿拉伯数字}我自己想不出一个例子;有人知道吗？

---

¹我无法找到一组Alternative定律的规范参考，但我列出了我认为它们大致在回答问题"对Alternative类型类的含义及其与其他类型类的关系感到困惑"(搜索短语"右分配")的一半。 我认为应该成立的四条定律是：

1. 右分配(<*>  )：(f <|> g) <*> a = (f <*> a) <|> (g <*> a)
2. 正确吸收(<*>)：  empty <*> a = empty
3. 左分布(fmap  )：f <$> (a <|> b) = (f <$> a) <|> (f <$> b)
4. 左吸收(fmap  )：f <$> empty = empty

我也很乐意接受被赋予一套更有用的Alternative法律。

²我知道MonadPlus法有些含糊不清;我对使用左分布或左捕获的答案感到满意，尽管我弱弱地更喜欢前者。

Answer 1

你的答案的线索在HaskellWiki关于你链接到的MonadPlus：

哪些规则？Martin & Gibbons 選擇 Monoid、Left Zero 和 Left Distribution。这使得[]成为MonadPlus，但不是Maybe或IO。

因此，根据您喜欢的选择，Maybe不是MonadPlus(尽管有一个实例，但它不满足左分布)。让我们证明它满足替代。

Maybe是一种替代方案

1. 右分配(<*>)：(f <|> g) <*> a = (f <*> a) <|> (g <*> a)

案例 1：f=Nothing：

(Nothing <|> g) <*> a =                    (g) <*> a  -- left identity <|>
= Nothing         <|> (g <*> a) -- left identity <|>
= (Nothing <*> a) <|> (g <*> a) -- left failure <*>

案例2：a=Nothing：

(f <|> g) <*> Nothing = Nothing                             -- right failure <*>
= Nothing <|> Nothing                 -- left identity <|>
= (f <*> Nothing) <|> (g <*> Nothing) -- right failure <*>

案例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 <*>

1. 正确吸收(<*>)：empty <*> a = empty

这很容易，因为

Nothing <*> a = Nothing    -- left failure <*>

1. 左分配(fmap)：f <$> (a <|> b) = (f <$> a) <|> (f <$> b)

案例1：a = Nothing

f <$> (Nothing <|> b) = f <$> b                        -- left identity <|>
= Nothing <|> (f <$> b)          -- left identity <|>
= (f <$> Nothing) <|> (f <$> b)  -- failure <$>

案例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 <$>

1. 左吸收(fmap)：f <$> empty = empty

另一个简单的：

f <$> Nothing = Nothing   -- failure <$>

Maybe不是MonadPlus

让我们证明Maybe不是MonadPlus的断言：我们需要证明mplus a b >>= k = mplus (a >>= k) (b >>= k)并不总是成立。与以往一样，诀窍是使用一些绑定来偷偷取出非常不同的值：

a = Just False
b = Just True
k True = Just "Made it!"
k False = Nothing

现在

mplus (Just False) (Just True) >>= k = Just False >>= k
= k False
= Nothing

在这里，我使用绑定(>>=)从胜利的下巴中抢夺失败(Nothing)，因为Just False看起来像成功。

mplus (Just False >>= k) (Just True >>= k) = mplus (k False) (k True)
= mplus Nothing (Just "Made it!")
= Just "Made it!"

这里的失败(k False)是提前计算的，所以被忽略了，我们"Made it!"。

所以，mplus a b >>= k = Nothing但mplus (a >>= k) (b >>= k) = Just "Made it!".

你可以把这看作是我用>>=来打破mplusMaybe的左倾。

我的证明的有效性：

以防万一你觉得我做得不够乏味，我会证明我使用的身份：

首先

Nothing <|> c = c      -- left identity <|>
Just d <|> c = Just d  -- left bias <|>

来自实例声明

instance Alternative Maybe where
empty = Nothing
Nothing <|> r = r
l       <|> _ = l

其次

f <$> Nothing = Nothing    -- failure <$>
f <$> Just x = Just (f x)  -- success <$>

只是来自(<$>) = fmap和

instance  Functor Maybe  where
fmap _ Nothing       = Nothing
fmap f (Just a)      = Just (f a)

第三，其他三个需要做更多的工作：

Nothing <*> c = Nothing        -- left failure <*>
c <*> Nothing = Nothing        -- right failure <*>
Just f <*> Just x = Just (f x) -- success <*>

这来自定义

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

所以

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)

所以如果mf或mx为无，则结果也是Nothing，而如果mf = Just f和mx = Just x，则结果是Just (f x)