我开始阅读this paper on CRDTs，这是一种通过确保修改数据的操作是可交换的同时共享可修改数据的方法。在我看来，这将是 Haskell 中抽象的一个很好的候选 - 为 CRDT 提供一个类型类，指定数据类型和在该类型上通勤的操作，然后致力于使库在并发进程之间实际共享更新。
我想不通的是如何在类型类的规范中表述操作必须通勤的契约。
举个简单的例子：
class Direction a where
turnLeft :: a -> a
turnRight :: a -> a
不保证turnLeft . turnRight 与turnRight . turnLeft 相同。我想后备是指定等效的 monad 法则 - 使用注释来指定类型系统未强制执行的约束。
【问题讨论】：
标签： haskell typeclass commutativity
你想要的是一个包含证明负担的类型类，类似于下面的伪 Haskell：
class Direction a where
turnLeft :: a -> a
turnRight :: a -> a
proofburden (forall a. turnLeft (turnRight a) === turnRight (turnLeft a))
这里所有实例都必须提供函数和证明供编译器进行类型检查。这是一厢情愿的想法（对于 Haskell），因为 Haskell 没有（嗯，有限的）证明概念。
OTOH，Coq 是可提取到 Haskell 的依赖类型语言的证明助手。虽然我以前从未使用过Coq's type classes，但快速搜索是很有成效的，例如：
Class EqDec (A : Type) := {
eqb : A -> A -> bool ;
eqb_leibniz : forall x y, eqb x y = true -> x = y }.
所以看起来高级语言可以做到这一点，但可以说在降低标准开发人员的学习曲线方面还有很多工作要做。
【讨论】：
对于 TomMD 的回答，您可以使用 Agda 达到同样的效果。虽然它没有类型类，但您可以从记录中获得大部分功能（动态调度除外）。
record Direction (a : Set) : Set₁ where
field
turnLeft : a → a
turnRight : a → a
commLaw : ∀ x → turnLeft (turnRight x) ≡ turnRight (turnLeft x)
我想我会编辑帖子并回答为什么不能在 Haskell 中执行此操作的问题。
在 Haskell（+ 扩展）中，您可以表示上面 Agda 代码中使用的等价。
{-# LANGUAGE GADTs, KindSignatures, TypeOperators #-}
data (:=:) a :: * -> * where
Refl :: a :=: a
这表示关于两种类型相等的定理。例如。 a 等价于b 是a :=: b。
在我们等价的地方，我们可以使用构造函数Refl。使用它，我们可以对定理（类型）的证明（值）执行函数。
-- symmetry
sym :: a :=: b -> b :=: a
sym Refl = Refl
-- transitivity
trans :: a :=: b -> b :=: c -> a :=: c
trans Refl Refl = Refl
这些都是类型正确的，因此是正确的。不过这个；
wrong :: a :=: b
wrong = Refl显然是错误的，并且确实在类型检查上失败了。
然而，通过这一切，值和类型之间的障碍并没有被打破。值、值级函数和证明仍然存在于冒号的一侧；类型、类型级函数和定理相互依赖。您的turnLeft 和turnRight 是值级函数，因此不能参与定理。
Agda 和 Coq 是依赖类型语言，其中不存在障碍或允许事物跨越。 Strathclyde Haskell Enhancement (SHE) 是 Haskell 代码的预处理器，可以将 DTP 的某些效果欺骗到 Haskell 中。它通过从类型世界中的值世界复制数据来做到这一点。我认为它还不能处理重复的值级函数，如果是这样，我的直觉是这可能太复杂而无法处理。
【讨论】：
如前所述，没有办法直接在 Haskell 中使用类型系统强制执行此操作。但是，如果仅在 cmets 中指定约束还不够令人满意，那么作为中间立场，您可以为所需的代数属性提供 QuickCheck 测试。
在checkers package 中已经可以找到类似的内容；您可能需要查阅它以获取灵感。
【讨论】：
我想不通的是如何在类型类的规范中表述操作必须通勤的契约。
你想不通的原因是不可能。你不能在类型中编码这种属性——至少在 Haskell 中是这样。
【讨论】：