为什么哈斯克尔的类型类定律必须手动验证？

Question

为什么需要显式地为Haskell中的类型类定律编写检查(可能使用快速检查(？

例如，测试字符串monoid:的结合性

leftIdcheck :: Monoid a => a -> Bool
leftIdcheck a = a <> mempty == a
quickCheck (leftIdcheck :: String -> Bool)

但这是太多的工作了！为什么haskell编译器不能在默认情况下自行检查所有这些，并告诉我我的类型上的monoid实例不满足恒等定律？

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

与此相关的是，Agda是让我们免费获得这些支票/证明，还是我们也必须在那里手动书写？

Answer 1

Haskell是一种没有依赖类型的非完全语言，因此，如果你考虑Ş，你可能想证明a(的大多数属性甚至不能被精确地公式化。

在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确认是否有任何希望来证明你试图证明的东西也是一个不错的主意。