如果你打破monad法则,你会怎么样？

Question

编译器或库中更"本机"的部分(IO或能够访问黑魔法和实现的函数)是否对这些定律做出假设？打破它们会导致不可能发生的事吗？

或者他们只是表达一种编程模式 - 也就是说,你唯一能够惹恼他们的人就是那些使用你的代码并且不希望你如此粗心的人？

Answer 1

monad法则只是实例预期遵循的附加规则,超出了类型系统中可以表达的范围.就Monad表达编程模式而言,法律是该模式的一部分.这些法律也适用于其他类型的类别:Monoid具有非常相似的规则Monad,并且通常期望这些实例Eq将遵循平等关系所期望的规则,以及其他示例.

因为这些定律在某种意义上是"类型"的一部分,所以其他代码期望它们能够持有并且相应地采取行动应该是合理的.因此,行为不当的实例可能会违反客户端代码逻辑所做的假设,从而导致错误,其中的错误适当地放在实例上,而不是使用它的代码.

简而言之,"打破monad法则"通常应该被理解为"编写错误代码".

我将通过一个涉及另一个类型类的示例来说明这一点,该类由Daniel Fischer在haskell-cafe邮件列表中给出的类修改.它是(希望)众所周知,标准库包括一些行为不当的情况下,即Eq与Ord用于浮点类型.正如您所猜测的那样,当涉及NaN时,会发生不当行为.考虑以下数据结构:

> let x = fromList  [0, -1, 0/0, -5, -6, -3] :: Set Float

当0/0产生NaN的,违反有关的假设Ord所作的实例Data.Set.Set.这Set包含0吗？

> member 0 x
True

是的,当然它确实如此,它就在那里!现在,我们在以下内容中插入一个值Set:

> let x' = insert (0/0) x

这Set仍然包含0,对吗？毕竟,我们没有删除任何东西.

> member 0 x'
False

... 哦.噢亲爱的.

对不起,我只接受一个答案 - 这是一个非常酷的例子.谢谢你. (3认同)
@Sjoerd Visscher:实际上,我认为我们真正想要的是一种"毫无意义的排序"类型.在许多情况下,我们不关心*Set'使用什么,只要它是一致的总排序.在订购中任意给NaN一个语义无意义的地方会使`Set`按原样工作,而部分订单类型类将在浮点数上提供正确的语义顺序.根据IEEE规范,当前情况既不提供正确的任意排序也不提供正确的比较实现. (3认同)

Answer 2

编译器不会对法律做出任何假设,但是,如果您的实例不遵守法律,它将不会像monad一样 - 它会做出奇怪的事情,否则会让您的用户看起来不能正常工作(例如掉线)价值观,或以错误的顺序评估事物).

此外,假设monad法则保持不变,用户可能会进行重构.

Owen,是的,但在某种意义上,许多函数只有法律和类型才具有规范意义 - 无论实现的选择如何.liftM和fmap*有*由monad定律做同样的事情,甚至没有看他们的身体.丢失这些并且不保证它是有效的默认定义. (2认同)
丹尼尔:鉴于类型和法律.你不能同时遵守monad和functor法则以及做不同事情的实例.liftMWrong意味着如果将'fmap id = id law'用作fmap或'fmap f xs == xs >> = return,则会破坏它.如果不这样做,f'就会被打破. (2认同)
尽管如此,向GHC讲授一些monad法律并不是特别困难.{ - #RULES"返回/绑定"forall fx.例如,返回x >> = f = fx# - }可能很有用.也许它应该在标准库中. (2认同)

Answer 3

对于使用更多"主流"语言的人来说,这就像实现一个接口,但这样做不正确.例如,假设您正在使用提供IShape接口的框架,并实现它.但是,您的draw()方法的实现根本不会绘制,而只是实例化您的类的1000多个实例.

该框架将尝试使用您的IShape并使用它做合理的事情,并且上帝知道会发生什么.这是一个有趣的火车残骸值得关注.

如果你说你是一个Monad,你就是"声明"你遵守其合同和法律.其他代码将相信您的声明并采取相应行动.既然你撒谎,事情会以不可预见的方式出错.