Monad 是 Alternative 但不是 MonadPlus 的例子是什么? [英] What’s an example of a Monad which is an Alternative but not a MonadPlus?
问题描述
在他对问题的回答中类型类 MonadPlus
、Alternative
和 Monoid
之间的区别?",Edward Kmett 说
此外,即使 Applicative
是 Monad
的超类,你最终还是需要 MonadPlus
类,因为服从>
空<*>m = 空
不足以证明这一点
empty >>= f = 空
因此,声称某物是 MonadPlus
比声称它是 Alternative
更有说服力.
很明显,任何 not monad 的 applicative functor 自动成为 Alternative
的一个例子,它不是 MonadPlus
,而是 EdwardKmett 的回答意味着存在一个 monad,它是一个 Alternative
但不是一个 MonadPlus
:它的 empty
和 <|>
将满足 Alternative
法则,1 但不满足 MonadPlus
法则.2 我自己想不出这样的例子;有人知道吗?
1 我无法找到一组 Alternative
法律的规范参考,但我列出了我认为它们大约在 Alternative
类型类的含义及其与其他类型类的关系"(搜索短语正确的分配性").我认为应该遵守的四项法律是:
- 权利分配(
<*>
):(f <|> g) <*>a = (f <*> a) <|>(g <*> a)
- 右吸收(对于
<*>
):空<*>a = 空
- 左分配(
fmap
):f <$>(a <|> b) = (f <$> a) <|>(f <$> b)
- 左吸收(对于
fmap
):f <$>空 = 空
我也很乐意接受一组更有用的替代
法律.
2 我知道关于MonadPlus 的内容有些含糊不清
法律是;我对使用左分布或左捕捉的答案感到满意,尽管我不太喜欢前者.
您的答案的线索在 HaskellWiki 关于您链接的 MonadPlus 中到:
<块引用>哪些规则?马丁&Gibbons 选择 Monoid、Left Zero 和 Left Distribution.这使得 []
成为 MonadPlus,但不是 Maybe
或 IO
.
所以根据您的偏好,Maybe
不是 MonadPlus(虽然有一个实例,但它不满足左分布).让我们证明它满足 Alternative.
也许
是另一种选择
- 权利分配(
<*>
):(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) -- 成功 <*>
- 右吸收(对于
<*>
):空<*>a = 空
这很简单,因为
没什么<*>a = 无 - 留下失败 <*>
- 左分配(
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) -- 成功 <$>
- 左吸收(对于
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)
所以如果 mf
或 mx
是 Nothing,结果也是 Nothing
,而如果 mf = Just f
和 mx = 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 ofMonad
, you’d wind up needing theMonadPlus
class anyways, because obeyingempty <*> m = empty
isn’t strictly enough to prove that
empty >>= f = empty
So claiming that something is a
MonadPlus
is stronger than claiming it isAlternative
.
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:
- Right distributivity (of
<*>
):(f <|> g) <*> a = (f <*> a) <|> (g <*> a)
- Right absorption (for
<*>
):empty <*> a = empty
- Left distributivity (of
fmap
):f <$> (a <|> b) = (f <$> a) <|> (f <$> b)
- 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 notMaybe
orIO
.
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)
这篇关于Monad 是 Alternative 但不是 MonadPlus 的例子是什么?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!