haskell - Monad 是替代品但不是 MonadPlus 的例子是什么？

Question

在 his answer对于问题“Distinction between typeclasses MonadPlus , Alternative , and Monoid ?” ，爱德华·克梅特说

Moreover, even if Applicative was a superclass of Monad, you’d wind up needing the MonadPlus class anyways, because obeying

empty <*> m = empty

isn’t strictly enough to prove that

empty >>= f = empty

So claiming that something is a MonadPlus is stronger than claiming it is Alternative.

很明显，任何不是 monad 的应用仿函数都会自动成为 Alternative 的示例。这不是 MonadPlus ，但 Edward Kmett 的回答暗示存在一个 monad，它是 Alternative但不是MonadPlus :其empty和<|>会满足Alternative法律，¹ 但不是 MonadPlus ²我自己无法举出这样的例子；有人知道吗？

<小时/>

¹ 我无法找到一组 Alternative 的规范引用法律，但我列出了我认为大约一半的内容my answer对于问题“Confused by the meaning of the Alternative type class and its relationship to other type classes” (搜索短语“右分配性”)。我认为应该遵守的四项法则是:

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法律。

² 我知道 there’s some ambiguity about what the MonadPlus laws are ;我对使用左分布或左捕获的答案感到满意，尽管我不太喜欢前者。

Answer 1

答案的线索在 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.

所以根据你喜欢的选择，Maybe不是 MonadPlus (虽然有一个实例，但它不满足左分布)。让我们证明它满足Alternative。

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)并不总是成立。与以往一样，技巧是使用一些绑定(bind)来偷偷取出非常不同的值:

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

这里我使用了bind (>>=)从胜利的口中夺取失败(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，结果也是Nothing ，而如果 mf = Just f和mx = Just x ，结果是Just (f x)