mplus必须始终是联想的吗？Haskell wiki对阵Oleg Kiselyov

Question

该哈斯克尔维基断言

MonadPlus的实例需要满足几个规则,就像Monad的实例需要满足三个monad定律一样.......最重要的是mzero和mplus形成一个幺半群.

其结果是mplus必须是联想的.该哈斯克尔维基同意.

然而,Oleg在他的众多回溯搜索实现之一中写道

-- Generally speaking, mplus is not associative. It better not be,
-- since associative and non-commutative mplus makes the search
-- strategy incomplete.

定义非关联是否是犹太教mplus？MonadPlus如果mplus不是关联的话,前两个链接非常清楚地表明你没有真实的实例.但是,如果奥列格确实它...(在另一方面,在该文件中,他只是定义调用的函数mplus,而并没有说这 mplus是mplus的MonadPlus,他选择了一个非常令人迷惑的名字,如果这是正确的解释.)

Answer 1

以下是Oleg自己的意见,以及我的评论和澄清.

好的,首先,我想表达我与Gabriel Gonzalez的意见.不是每个人都同意,MonadPlus对于mplus和,应该是monoid mzero.报告对此一无所知.如果不是这样,有很多引人注目的案例(见下文).通常,代数结构应该适合任务.这就是为什么我们有团体,还有较弱的半群体或群体(岩浆).它似乎 MonadPlus通常被视为搜索/非决定论monad.如果是这样,那么属性MonadPlus应该是那些便于搜索和推理搜索的属性 - 而不是某些理想的特殊属性,无论出于何种原因.让我举一个例子:摆出法律很诱人

m >> mzero === mzero

但是,支持搜索并且可以做其他效果(想到NonDeT m)的monad 不能满足该法则.例如,

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

因此,似乎是coinductively和foo是相同的.这意味着,我们永远不会从foo得到答案2.

MonadPlus只要mplus是关联的和非交换的,那么结果就适用于任何可以表示的搜索.因此,如果MonadPlus是搜索的monad,那么关联性mplus是一个不合理的要求.

这是第二个原因:有时我们希望进行概率搜索 - 或者,一般来说,加权搜索,当一些替代方案被加权时.很明显,概率选择算子不是关联的.出于这个原因,我们的JFP论文特别避免强加monoid(mplus,mzero)结构MonadPlus.

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

RC 我认为加布里埃尔和你同意搜索单子不具有幺半群结构这一事实.这个论点归结为是否 MonadPlus应该用于搜索monad或者是否应该有另一个类,让我们称之为MonadPlus',这就像MonadPlus更宽松的法则.正如你所说,该报告没有就此主题发表任何意见,也无权决定.

出于推理的目的,我认为没有任何问题 - 只需要明确说明她对MonadPlus实例的假设.

至于重新关联的重写规则,mplus仅仅存在和广泛使用MonadPlus非关联的实例,无论它们是否"被破坏",都意味着人们应该放弃定义它.

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

幺半群法则是最低要求,因为没有它们,其他法则就没有意义.例如,当你说 mzero >>= f = mzero,你首先需要一些明智的定义 mzero,但没有身份法则你没有那个.幺半群法律使其他拟议法律"诚实".如果你没有幺半群定律,那么你就没有合理的定律,没有定律的理论类型有什么意义呢？

例如,LogicT论文,特别是JFP论文有很多关于非决定论的等式推理的例子,没有相关性mplus.该JFP纸忽略所有幺律mplus 和mzero(但使用mzero >>= f === mzero).对于非决定论和搜索而言,似乎人们可以拥有"诚实"和"明智的法则",而没有针对mplus和的幺半群定律mzero.

我也不确定我同意这个说法

每个人都同意MonadPlus应遵守的两条法律是身份和结社法(又称幺半群法):

我不确定是否对此进行了民意调查.报告没有提到任何法律mplus(也许作者仍然在辩论它们).所以,我想说这个问题是公开的 - 这是传达的主要信息.

Answer 2

每个人都同意MonadPlus应遵守的两条法律是身份和结社法(又称幺半群法):

mplus mempty a = a

mplus a mempty = a

mplus (mplus a b) c = mplus a (mplus b c)

我总是假设他们在MonadPlus我使用的所有情况下都持有并且认为违反这些法律的实例被"破坏",无论它们是否由奥列格撰写.

Oleg是正确的,关联性与广度优先搜索不能很好地匹配,但这只意味着它MonadPlus不是他正在寻找的抽象.

为了回答你在评论中提出的观点,我会一直认为你的重写规则听起来如此.