haskell - 一个简单的例子表明 IO 不满足单子(monad)定律？

Question

我见过提到 IO不满足单子(monad)定律，但我没有找到一个简单的例子来说明这一点。有人知道一个例子吗？谢谢。

编辑:如ertes和 n.m.指出，使用 seq有点非法，因为它可以使任何 monad 违反法律(结合 undefined )。由于undefined可能被视为非终止计算，使用它完全没问题。

所以修改后的问题是:任何人都知道一个例子表明 IO不满足单子(monad)定律，不使用 seq ? (或者，如果 IO 不被允许，也许可以证明 seq 确实满足法律？)

Answer 1

如果你排除了奇怪的 seq，Haskell 中的所有单子(monad)都是单子(monad)。组合器。 IO 也是如此.由于seq实际上不是常规函数，而是涉及魔法，您必须将其排除在检查单子(monad)定律之外，原因与您必须排除 unsafePerformIO 的原因相同。 .使用 seq您可以证明所有单子(monad)都是错误的，如下所示。

在 Kleisli 类别中，monad 产生，return是恒等态射和(<=<)是组成。所以return必须是 (<=<) 的标识:

return <=< x = x

使用 seq甚至 Identity 和 Maybe 都不是单子(monad):

seq (return <=< undefined :: a -> Identity b) () = ()
seq (undefined            :: a -> Identity b) () = undefined

seq (return <=< undefined :: a -> Maybe b) () = ()
seq (undefined            :: a -> Maybe b) () = undefined