在haskell中，用户不必证明他们的monad满足monad定律。
return a >>= k = k a
m >>= return = m
m >>= (x -> k x >>= h) = (m >>= k) >>= h
如果我理解正确，即使他们愿意，编译器也无法读取这样的证明。
问题
- haskell中缺少什么技术，可以通过编译器实现这种可检查的证明
- 哪种函数式语言支持这样的功能(即可以检查一个声明是否满足monad定律(
在实践中，法律通常不会在Haskell中得到验证，但它们很可能会经过测试。如果你对你的monad方程两边的表达式进行大量随机输入，结果总是一样的，这可能不能保证什么，但确实会让任何违法行为都很可能被抓住。也就是说，只要您以足够有代表性的方式生成输入。QuickCheck通常在这方面做得很好。
如果你真的想证明定律，那么，Haskell并不是真正合适的工具。您可能希望在编译时检查证明，但Haskell使得在类型级别表达复杂的值变得相当困难。如果您改为在运行时执行，那么首先：如果部署的可执行文件因错误而崩溃，那就没有好处。但更重要的是，由于Haskell不是total，你可以通过给出undefined作为结果来"证明"任何命题——或者其他一些值，更典型的是，这可能是一些微妙的无限循环。
正确的工具是依赖类型的语言。最受欢迎的是Coq和Lean，它们比Haskell更像ML，以及Agda。这些主要是为了证明辅助，而不是一般的编程语言，它们也允许你公式化定理；伊德里斯更倾向于这个方向。
尽管如此，现代Haskell现在也有一定的依赖类型编程能力。关键工具是将函数作为类型族，并使用singleton来获得类型级值的值级standins，然后使用GADT或约束CPS来传递证明。
用它来指定类型类的定律仍然很尴尬，但它可以很好地用于Curry Howard表达具体定理。singletons-base包包含许多类型提升形式的标准函数，因此适合于证明有关内容。例如，以下是如何公式化列表串联运算符是关联的：
{-# LANGUAGE TypeFamilies, DataKinds, KindSignatures, PolyKinds, TypeOperators #-}
import Data.List.Singletons
listConcatAssoc :: ∀ k l m ρ . Sing k -> Sing l -> Sing m
-> (((k++l)++m ~ k++(l++m)) => ρ) -> ρ
listConcatAssoc SNil SNil SNil φ = φ
...
完整的证明写起来会很烦人，但TBH证明即使在Coq中也很烦人，尽管这是它的工作。不过，Coq确实让用定律等真正表达类型类变得更好。