我们通过 Haskell 平台获得的 Applicative 类型类的所有 Haskell 实例是否已被证明满足所有 Applicative 定律？如果是，我们在哪里可以找到这些证据？
Control.Applicative的源代码似乎不包含任何证据证明适用于各种情况的法律确实成立。它只是提到
-- | A functor with application.
--
--Instances should satisfy the following laws:
然后它只是在评论中说明法律。
对于其他类型类（Alternative 和 Monad）的实例，我也发现了类似的情况。
这些图书馆的用户是否应该自己验证这些法律？
但我想知道这些法律的严格证明是否已经由开发商在其他地方给出？
同样，我知道对于 IO Monad 的应用（或 Monad）定律的严格证明，一般来说，它涉及与外部世界的对话，可能非常复杂。
谢谢。
是的，举证责任完全在图书馆作者身上。有一些违反这些法律的实施示例。违反法律的典型示例是ListT，它不遵守大多数基本单子的单子定律（请参阅示例）。这给出了非常错误的行为，ListT结果没有人真正使用。
我很确定大多数此类证明都没有在标准位置刻在石头上。大多数证明只是被社区中各种好奇的成员简单地重复和检查到死，所以一段时间后我们知道哪些实现符合他们的法律，哪些不符合他们的法律。
举一个具体的例子，当我编写我的pipes库时，我必须证明我pipes满足Category法律，但我只是将这些证明保存在文本文件或 hpaste 中以备将来记录，如果有人要求的话。将它们包含在源代码中实际上并不可行，因为它们可能会变得很长，尤其是对于结合律。
但是，我认为一个好的做法可能是在可能的情况下在原始存储库中包含机器检查的证明，以便用户可以在必要时参考它们。
有优秀的库检查器提供 QuickCheck 属性来检查法律。
实验库ghc-proofs允许您使用编译器为您验证这些规律：
app_law_2 a b (c :: Succs a) = pure (.) <*> a <*> b <*> c
=== a <*> (b <*> c)
它仅在少数情况下有效，例如我的博客文章中描述的情况，最好将其视为实验，而不是现成的工具。