Monad是一个替代但不是MonadPlus的例子是什么？

Question

在他的回答这个问题"类型类之间的区别MonadPlus,Alternative以及Monoid？",爱德华Kmett说,

而且,即使Applicative是超级课程Monad,你最终还是需要MonadPlus上课,因为顺从

empty <*> m = empty

并不足以证明这一点

empty >>= f = empty

因此声称某事物是一件事,MonadPlus比宣称事情要强Alternative.

很明显,任何适用函子是不是一个单子是自动的一个例子Alternative是不是MonadPlus,但爱德华Kmett的回答意味着存在一个单子这是一个Alternative,但不是一个MonadPlus:它empty和<|>将满足Alternative法律,¹而不是MonadPlus法律.² 我自己无法想出这样的例子; 有人知道吗？

---

¹我无法找到一套规则的规范参考Alternative,但是我将我认为它们的内容大概放在我对" 类型类的含义及其与其他类型的关系的混淆"这一问题的答案的中间.类"(搜索短语"正确的分配").我认为应该遵守的四项法律是:Alternative

1. 正确的分配性<*>:  (f <|> g) <*> a = (f <*> a) <|> (g <*> a)
2. 正确吸收(for <*>):  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. 正确吸收(for <*>): 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!".

你可以看一下这是我用>>=打破的左偏mplus了Maybe.

我的证明的有效性:

万一你觉得我做得不够繁琐,我会证明我用过的身份:

首先

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)