haskell - Haskell 实例的适用律证明

Question

我们通过 Haskell 平台获得的 Applicative 类型类的所有 Haskell 实例是否都已被证明满足所有 Applicative 定律？如果是，我们在哪里可以找到这些证据？

Control.Applicative的源代码似乎没有包含任何证据证明各种情况下的适用法律确实成立。它只是提到了

-- | A functor with application.
--
--Instances should satisfy the following laws:

然后它只是在评论中陈述法律。

我也发现了其他类型类(Alternative 和 Monad)的实例的类似情况。

这些图书馆的用户是否应该自行验证这些法律？

但我想知道开发者是否在其他地方给出了这些定律的严格证明？

我再次意识到，IO Monad 的 Applicate(或 Monad)定律的严格证明(通常涉及与外界对话)可能非常复杂。

谢谢。

Answer 1

是的，举证责任完全由库作者承担。有一些违反这些法律的实现示例。违反法律的典型示例是 ListT，它不遵守大多数基本 monad 的 monad 法则(请参阅 examples )。这会产生非常错误的行为，因此没有人真正使用 ListT。

我很确定大多数此类证据都没有刻在标准位置的石头上。大多数证明只是被社区中各种好奇的成员重复和检查到死，所以过了一段时间我们就知道哪些实现满足和不满足他们的法律。

举一个具体的例子，当我编写我的pipes库时，我必须证明我的pipes满足Category法则，但是我只是将这些证明保存在文本文件或粘贴中，以便将来有人要求时记录。将它们包含在源代码中实际上并不可行，因为它们可能会变得很长，尤其是对于结合律而言。

但是，我认为一个好的做法可能是在可能的情况下在原始存储库中包含机器检查的证明，以便用户可以在必要时引用它们。