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