gpt4 book ai didi

haskell - mplus 必须始终是关联的吗? Haskell wiki vs. Oleg Kiselyov

转载 作者:行者123 更新时间:2023-12-03 11:07:01 25 4
gpt4 key购买 nike

Haskell wikibook断言

Instances of MonadPlus are required to fulfill several rules, just as instances of Monad are required to fulfill the three monad laws. ... The most essential are that mzero and mplus form a monoid.



其结果是 mplus必须是关联的。 Haskell wiki同意。

然而,奥列格,在 one of his many backtracking search implementations , 写道
-- Generally speaking, mplus is not associative. It better not be,
-- since associative and non-commutative mplus makes the search
-- strategy incomplete.

定义非关联 mplus 是否符合规定? ?前两个链接非常清楚地表明您没有真正的 MonadPlus例如 mplus不是关联的。但是,如果 Oleg 这样做了……(另一方面,在该文件中,他只是定义了一个名为 mplus 的函数,并没有声称 mplusmplusMonadPlus。他选择了相当困惑的名字,如果这是正确的解释。)

最佳答案

以下是奥列格本人的意见,以及我的评论和他的澄清。

好的。 首先,我想说明我与加布里埃尔的分歧
冈萨雷斯。不是每个人都同意 MonadPlus应该是幺半群
关于 mplusmzero .报告对此只字未提。那里
当情况并非如此时,有许多令人信服的案例(见下文)。一般来说,
代数结构应该适合任务。这就是为什么我们有
群,以及较弱的半群或类群(岩浆)。它似乎MonadPlus通常被视为搜索/非确定性单子(monad)。如果是这样,
那么 MonadPlus 的属性应该是那些促进
搜索和关于搜索的推理——而不是一些理想的临时
某人出于任何原因喜欢的属性。让我举个例子:
制定法律很诱人

m >> mzero === mzero

然而,支持搜索并且可以做其他效果的单子(monad)(想想 NonDeT m )不能满足该法律。例如,
print "OK" >> mzero  =/==  mzero

因为左边打印了一些东西,但右边
没有。同理, mplus不能对称: mplus m1 m2通常不同于 mplus m2 m1 , 在同一模型中。

让我们来 mplus .不需要 mplus 的主要原因有两个
具有关联性。首先是搜索的完整性。考虑
ones = return 1 `mplus` ones

foo = ones `mplus` return 2
=== {- inlining ones -}
(return 1 `mplus` ones) `mplus` return 2
=== {- associativity -}
return 1 `mplus` (ones `mplus` return 2)
===
return 1 `mplus` foo

因此,看起来,和 foo 是相同的。那
意思是,我们永远不会从 foo 得到答案 2。

该结果适用于可以由 MonadPlus 表示的任何搜索。 , 所以
只要 mplus是结合的和不可交换的。因此,如果 MonadPlus是一个
monad 用于搜索,然后是 mplus 的关联性是不合理的要求。

这是第二个原因:有时我们希望概率
搜索——或者,一般来说,加权搜索,当一些替代品是
加权。显然,概率选择算子不是
联想的。出于这个原因,我们的 JFP 论文特别避免
mplus 上强加幺半群 ( mzero , MonadPlus ) 结构.

http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet
(参见论文图 1 的讨论)。

RC
我认为加布里埃尔和你同意搜索单子(monad)不
表现出幺半群结构。争论归结为是否 MonadPlus应该用于搜索单子(monad)或应该有另一个
类,我们称之为 MonadPlus' ,就像 MonadPlus但与
更宽松的法律。正如你所说,报告没有说明这一点
话题,没有决定权。

出于推理的目的,我认为这没有任何问题——一个
只需清楚说明她对 MonadPlus 的假设即可。实例。

至于重新关联 mplus的重写规则是的,单纯的存在 MonadPlus 的广泛使用非关联的实例,
不管它们是否“坏”,意味着一个应该可能
避免定义它。

好的。
我想我不同意加布里埃尔的说法

The monoid laws are the minimum requirement because without them the other laws are meaningless. For example, when you say mzero >>= f = mzero, you first need some sensible definition of mzero is, but without the identity laws you don't have that. The monoid laws are what keep the other proposed laws "honest". If you don't have the monoid laws then you have no sensible laws and what's the point of a theoretical type class that has no laws?



例如,LogicT 论文,尤其是 JFP 论文有很多
关于非确定性的等式推理的例子,没有 mplus 的关联性. JFP 论文省略了 mplus 的所有幺半群定律。
mzero (但使用 mzero >>= f === mzero )。好像可以有
“诚实”和“明智的法律”,用于非确定性和搜索 mplus 的幺半群定律和 mzero .

我也不确定我是否同意该主张

The two laws that everybody agrees that MonadPlus should obey are the identity and associativity laws (a.k.a. the monoid laws):



我不确定是否对此进行了民意调查。报告没有说明任何法律
对于 mplus (也许作者仍在辩论他们)。所以我
会说这个问题是开放的——这是要得到的主要信息
穿过。

关于haskell - mplus 必须始终是关联的吗? Haskell wiki vs. Oleg Kiselyov,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/15722906/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com