为什么必须手动验证 Haskell 的类型类定律？

Question

为什么需要为 Haskell 中的类型类法则明确编写检查（可能使用快速检查）？

例如用于测试字符串幺半群的结合性：

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

quickCheck (leftIdcheck :: String -> Bool)

但这工作量太大了！为什么 Haskell 编译器不能在默认情况下自行检查所有这些并告诉我我的类型上的幺半群实例不满足恒等律？

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

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

Answer 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 属性要费力得多。当然，如果你已经成功地做到这一点，它是多一点安慰，但在实践中快速检查通常足以捕获> 90％的错误。适当的形式验证很棒，但仅对真正重要/安全关键的代码才值得，即使如此，首先让 QuickCheck 确认甚至有任何希望证明您要证明的内容也是一个好主意。