为什么必须手动验证 Haskell 的类型类法则？答案

【问题标题】：Why do Haskell's typeclass laws have to be verified manually?为什么必须手动验证 Haskell 的类型类法则？
【发布时间】：2020-08-22 01:31:19
【问题描述】：

为什么需要在 Haskell 中为类型类规则显式编写检查（可能使用快速检查）？

例如用于测试 String monoid 的关联性：

leftIdcheck :: Monoid a => a -> Bool
leftIdcheck a = a <> mempty == a

quickCheck (leftIdcheck :: String -> Bool)

但是这工作量太大了！为什么 haskell 编译器不能自己默认检查所有这些并告诉我我的类型上的 monoid 实例不满足恒等律？

是否有任何库或语言扩展允许我们在编写程序时内置这些检查，而不必单独编写它们？这似乎很容易出错。

在相关的说明中，Agda 是让我们免费获得这些检查/证明，还是我们也必须在那里手动编写它们？

【问题讨论】：

因为通常无法验证这一点。这是赖斯定理的结果。
QuickCheck 尝试通过一些随机值来查找错误。它不会尝试所有这些，因为通常有无限多的值。可计算性理论确实证明了对语义属性（例如法律）的完美自动验证是不可能的。然而，Haskell 可以做的是为所有类和法则提供 QuickCheck 属性，以便于测试。我不知道有任何图书馆提供此功能，但原则上可以编写。
好的，不可能有一个算法肯定成功地证明“一般”所需的属性。但是，是否不可能提供一种允许失败但在某些简单情况下成功的算法？就像，编译器应该能够在简单的情况下派生Eq 类的实例，因此编译器显然可以说服自己相信x == x 和/或x==y && y==z ⇒ x==z 等属性。这节省了很多样板代码。当然，对于newtype NTei = NTei (Int -> Int) deriving Eq之类的东西如果失败也完全没问题。
@jpmarinier 在派生Eq 实例时，编译器不会对x==x 之类的东西进行任何“思考”。它只是有一些关于A 和B 类型的相等性如何暗示(A,B) 和Either A B 上的相等性的硬编码规则，并且可以归纳地扩展到任何代数数据类型上的相等性。
@chi，有 Andrew Martin 的quickcheck-classes 和更早的checkers 和genvalidity-hspec。我不知道它们之间的权衡，除了 Martin 的可能更容易使用。

标签： haskell typeclass

【解决方案1】：

Haskell 是一种没有依赖类型的非完整语言，因此您可能想要证明的大多数属性 a) 甚至不能公式化 完全b) 不是真的严格来说是真的，如果你考虑 ⊥。

在 Coq 和 Agda 中，情况就不同了，实际上，一个 Coq 类通常不仅包含其 Haskell 挂件所具有的方法，还包含法律：

Class Monoid (m: Type) : Type :=
  { mempty : m
  ; mappend : m -> m -> m
  ; mempty_left : forall (p: m), mappend mempty p = p
  ; mempty_right : forall (p: m), mappend p mempty = p
  ; mappend_assoc : forall (p q r: m)
                  , mappend p (mappend q r) = mappend (mappend p q) r
  }.

但这并不意味着编译器会在您声明实例时自动为您证明这些。正如 Willem Van Onsem 评论的那样，这通常是不可能的。您需要自己编写证明，这比编写 QuickCheck 属性要费力很多。当然，如果您设法做到了，它会更让人放心，但在实践中，QuickCheck 通常足以捕获 >90% 的所有错误。适当的形式验证很棒，但它只对真正重要/安全至关重要的代码才值得，即使这样，首先让 QuickCheck 确认甚至有任何希望证明你正在尝试的东西也是一个好主意证明。

【讨论】：