Monad 是 Alternative 但不是 MonadPlus 的例子是什么? [英] What’s an example of a Monad which is an Alternative but not a MonadPlus?

查看:23
本文介绍了Monad 是 Alternative 但不是 MonadPlus 的例子是什么?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

他对问题的回答类型类 MonadPlusAlternativeMonoid 之间的区别?",Edward Kmett 说

<块引用>

此外,即使 ApplicativeMonad 的超类,你最终还是需要 MonadPlus 类,因为服从>

空<*>m = 空

不足以证明这一点

empty >>= f = 空

因此,声称某物是 MonadPlus 比声称它是 Alternative 更有说服力.

很明显,任何 not monad 的 applicative functor 自动成为 Alternative 的一个例子,它不是 MonadPlus,而是 EdwardKmett 的回答意味着存在一个 monad,它是一个 Alternative 但不是一个 MonadPlus:它的 empty<|> 将满足 Alternative 法则,1 但不满足 MonadPlus 法则.2 我自己想不出这样的例子;有人知道吗?

<小时>

1 我无法找到一组 Alternative 法律的规范参考,但我列出了我认为它们大约在 我对问题困惑于"的回答Alternative 类型类的含义及其与其他类型类的关系"(搜索短语正确的分配性").我认为应该遵守的四项法律是:

  1. 权利分配(<*>):  (f <|> g) <*>a = (f <*> a) <|>(g <*> a)
  2. 右吸收(对于<*>):  空<*>a = 空
  3. 左分配(fmap):  f <$>(a <|> b) = (f <$> a) <|>(f <$> b)
  4. 左吸收(对于fmap):  f <$>空 = 空

我也很乐意接受一组更有用的替代法律.

2 我知道关于MonadPlus 的内容有些含糊不清 法律是;我对使用左分布或左捕捉的答案感到满意,尽管我不太喜欢前者.

解决方案

您的答案的线索在 HaskellWiki 关于您链接的 MonadPlus 中到:

<块引用>

哪些规则?马丁&Gibbons 选择 Monoid、Left Zero 和 Left Distribution.这使得 [] 成为 MonadPlus,但不是 MaybeIO.

所以根据您的偏好,Maybe 不是 MonadPlus(虽然有一个实例,但它不满足左分布).让我们证明它满足 Alternative.

也许是另一种选择

  1. 权利分配(<*>): (f <|> g) <*>a = (f <*> a) <|>(g <*> a)

情况 1:f=Nothing:

(Nothing <|> g) <*>a=(g)*a -- 左身份 <|>= 没什么 <|>(g <*> a) -- 左身份 <|>= (什么都没有<*>a)<|>(g <*> a) -- 左失败 <*>

情况 2:a=Nothing:

(f <|> g) <*>没有 = 没有 - 正确的失败 <*>= 没什么 <|>什么都没有——留下身份 <|>= (f <*> 没有) <|>(g <*> Nothing) -- 正确失败 <*>

情况 3:f=Just h,a = Just x

(只是 h <|> g) <*>仅 x = 仅 h <*>只是 x -- 左偏差 <|>= Just (h x) -- 成功 <*>= 只是 (h x) <|>(g <*> Just x) -- 左偏置 <|>= (只是 h <*> 只是 x) <|>(g <*> Just x) -- 成功 <*>

  1. 右吸收(对于<*>): 空<*>a = 空

这很简单,因为

没什么<*>a = 无 - 留下失败 <*>

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

情况 1:a = Nothing

f <$>(没有<|> b) = f <$>b -- 左身份 <|>= 没什么 <|>(f <$> b) -- 左身份 <|>= (f <$> 没有) <|>(f <$> b) -- 失败 <$>

情况 2:a = Just x

f <$>(只是 x <|> b) = f <$>只是 x -- 左偏差 <|>= Just (f x) -- 成功 <$>= 只是 (f x) <|>(f <$> b) -- 左偏置 <|>= (f <$>只是 x) <|>(f <$> b) -- 成功 <$>

  1. 左吸收(对于fmap): f <$>空 = 空

另一个简单的:

f <$>无 = 无 - 失败 <$>

也许不是 MonadPlus

让我们证明 Maybe 不是 MonadPlus 的断言:我们需要证明 mplus ab >>= k = mplus (a >>= k) (b >>= k) 并不总是成立.与以往一样,诀窍是使用一些绑定来隐藏非常不同的值:

a = Just Falseb = 正确k True = 只是成功了!"k 假 = 没有

现在

mplus (Just False) (Just True) >>= k = Just False >>= k= k 错误= 没什么

这里我使用了 bind (>>=) 从胜利的口中抢夺失败 (Nothing) 因为 Just False 看起来很成功.

mplus (Just False >>= k) (Just True >>= k) = mplus (k False) (k True)= mplus 什么都没有(只是做到了!")= 只是成功了!"

这里的失败(k False)是提前计算出来的,所以被忽略了,我们成功了!".

所以,mplus ab >>= k = 没有 但是 mplus (a >>= k) (b >>= k) = 只是做到了"!".

你可以像我一样使用 >>= 来打破 mplus 对于 Maybe 的左偏差.>

我的证明的有效性:

以防万一你觉得我没有完成足够繁琐的推导,我将证明我使用的身份:

首先

什么都没有 <|>c = c -- 左身份 <|>只是 d <|>c = Just d -- 左偏置 <|>

来自实例声明

instance Alternative 也许在哪里空 = 没有什么都没有<|>r = r<|>_ = l

其次

f <$>无 = 无 - 失败 <$>f <$>Just x = Just (f x) -- 成功 <$>

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

instance Functor 也许在哪里fmap _ 无 = 无fmap f (Just a) = Just (f a)

第三,其他三个需要更多的工作:

没什么<*>c = 没有——留下失败 <*>c <*>没有 = 没有 - 正确的失败 <*>只是 f <*>Just x = Just (f x) -- 成功 <*>

来自定义

instance Applicative 也许在哪里纯 = 回报(<*>) = apap :: (Monad m) =>m (a -> b) ->m a ->米ap =liftM2 idLiftM2 :: (Monad m) =>(a1 -> a2 -> r) ->m a1 ->m a2 ->先生LiftM2 f m1 m2 = do { x1 <- m1;x2<-m2;返回 (f x1 x2) }实例 Monad 也许在哪里(只是 x) >>= k = k x什么都没有 >>= _ = 什么都没有返回 = 只是

所以

mf <*>mx = ap mf mx=liftM2 id mf mx= 做 { f <- mf;x <- mx;返回 (id f x) }= 做 { f <- mf;x <- mx;返回 (f x) }= 做 { f <- mf;x <- mx;只是 (f x) }= mf >>= f ->mx >>= x ->只是 (f x)

所以如果 mfmx 是 Nothing,结果也是 Nothing,而如果 mf = Just fmx = Just x,结果是 Just (fx)

In his answer to the question "Distinction between typeclasses MonadPlus, Alternative, and Monoid?", Edward Kmett says that

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.

It’s clear that any applicative functor which is not a monad is automatically an example of an Alternative which is not a MonadPlus, but Edward Kmett’s answer implies that there exists a monad which is an Alternative but not a MonadPlus: its empty and <|> would satisfy the Alternative laws,1 but not the MonadPlus laws.2 I can’t come up with an example of this by myself; does anybody know of one?


1 I wasn’t able to find a canonical reference for a set of Alternative laws, but I lay out what I believe them to be roughly halfway through my answer to the question "Confused by the meaning of the Alternative type class and its relationship to other type classes" (search for the phrase "right distributivity"). The four laws I believe ought to hold are:

  1. Right distributivity (of <*>):  (f <|> g) <*> a = (f <*> a) <|> (g <*> a)
  2. Right absorption (for <*>):  empty <*> a = empty
  3. Left distributivity (of fmap):  f <$> (a <|> b) = (f <$> a) <|> (f <$> b)
  4. Left absorption (for fmap):  f <$> empty = empty

I’d also happily accept being given a more useful set of Alternative laws.

2 I know that there’s some ambiguity about what the MonadPlus laws are; I’m happy with an answer that uses left distribution or left catch, although I would weakly prefer the former.

解决方案

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

  1. 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 <*>

  1. Right absorption (for <*>): empty <*> a = empty

That's easy, because

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

  1. 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 <$>

  1. 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)

这篇关于Monad 是 Alternative 但不是 MonadPlus 的例子是什么?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆