以下是奥列格本人的意见,以及我的评论和他的澄清。
好的首先,我想说明我与 Gabriel Gonzalez 的分歧。不是每个人都同意关于和MonadPlus
应该是幺半群。报告对此只字未提。有许多令人信服的案例并非如此(见下文)。一般来说,代数结构应该适合任务。这就是为什么我们有群体,还有更弱的半群体或群体(岩浆)。它似乎
通常被视为搜索/非确定性单子。如果是这样,那么 的属性应该是那些有助于搜索和推理搜索的属性——而不是某些人出于任何原因喜欢的理想的临时属性。让我举个例子:设定法律很诱人mplus
mzero
MonadPlus
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
因此,看起来,和 foo 是相同的。这意味着,我们永远不会从 foo 得到答案 2。
该结果适用于任何可以由 表示的搜索,MonadPlus
只要mplus
是关联的和不可交换的。因此,如果MonadPlus
是搜索的单子,那么的关联性mplus
是不合理的要求。
这是第二个原因:有时我们希望进行概率搜索——或者,一般来说,加权搜索,当一些备选方案被加权时。很明显,概率选择算子不是关联的。mplus
出于这个原因,我们的 JFP 论文特别避免mzero
在MonadPlus
.
http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet
(参见论文图 1 的讨论)。
R.C.
I think Gabriel and you agree on the fact that search monads do not
exhibit the monoid structure. The argument boils down to whether
MonadPlus
should be used for search monads or should there be another
class, let's call it MonadPlus'
, which is just like MonadPlus
but with
more lax laws. As you say, the report doesn't say anything on this
topic, and there's no authority to decide.
For the purpose of reasoning, I don't see any problem with that — one
just has to state clearly her assumptions about the MonadPlus
instances.
As for the rewrite rule that re-associates mplus
'es, the mere existence
and widespread use of MonadPlus
instances that are not associative,
regardless of whether they are "broken", means that one should probably
abstain from defining it.
O.K.
I guess I disagree with Gabriel's statement
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?
For example, LogicT paper and especially the JFP paper has lots of
examples of equational reasoning about non-determinism, without
associativity of mplus
. The JFP paper omits all monoid laws for mplus
and mzero
(but uses mzero >>= f === mzero
). It seems one can have
"honest" and "sensible laws" for non-determinism and search without
the monoid laws for mplus
and mzero
.
I'm also not sure I agree with the claim
The two laws that everybody agrees that MonadPlus
should obey are
the identity and associativity laws (a.k.a. the monoid laws):
I'm not sure a poll has been taken on this. The Report states no laws
for mplus
(perhaps the authors were still debating them). So, I
would say the issue is open — and this is the main message to get
across.