haskell实例的适用法律证明

Question

我们在Haskell平台上获得的所有Haskell应用类型类的实例是否都被证明满足所有的适用法律？如果是,我们在哪里找到这些证明？

Control.Applicative的源代码似乎不包含任何证据证明各种实例的适用法律确实存在.它只是提到了

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

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

我发现了其他类型类(Alternative和Monad)实例的类似案例.

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

但我想知道这些法律的严格证明是否已由开发商在其他地方提供过？

同样,我知道IO Monad的Applicate(或Monad)法律的严格证明,一般涉及与外界交谈,可能非常复杂.

谢谢.

Answer 1

是的,举证责任完全在于图书馆作家.有一些违反这些法律的实施例子.法律违规的典型例子是ListT,它不服从大多数基础单子的monad定律(见例子).这给出了非常错误的行为,没有人真正使用ListT它的结果.

我很确定大多数这类样张都没有在标准的地方蚀刻.大多数证据都被社会中的各种好奇的成员简单地重复和检查,所以过了一段时间我们知道哪些实施有和不满足他们的法律.

举一个具体的例子,当我写我的pipes图书馆时,我必须证明我pipes的Category法律满足,但我只是将这些证据保存在文本文件中,或者如果有人要求的话,将这些证据保存在未来的记录中.将它们包括在源中是不可行的,因为它们可能会变得很长,特别是对于相关性法则.

但是,我认为一个好的做法可能是在可能的情况下在原始存储库中包含机器检查的证据,以便用户可以根据需要参考它们.