我开始读书这篇关于 CRDT 的论文 http://pagesperso-systeme.lip6.fr/Marc.Shapiro/papers/RR-6956.pdf，这是一种通过确保修改数据的操作是可交换的来同时共享可修改数据的方法。在我看来，这将是 Haskell 中抽象的一个很好的候选者 - 为 CRDT 提供一个类型类，指定数据类型和在该类型上交换的操作，然后致力于使库能够在并发进程之间实际共享更新。
我不明白的是如何在类型类的规范中表达操作必须交换的契约。
举个简单的例子：
class Direction a where
turnLeft :: a -> a
turnRight :: a -> a
无法保证turnLeft . turnRight是相同的turnRight . turnLeft。我认为后备方法是指定 monad 法则的等效项 - 使用注释来指定类型系统未强制执行的约束。
你想要的是一个包含证明负担的类型类，类似于下面的伪 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 的类型类 http://coq.inria.fr/refman/Reference-Manual024.html之前，快速搜索是富有成效的，例如：
Class EqDec (A : Type) := {
eqb : A -> A -> bool ;
eqb_leibniz : forall x y, eqb x y = true -> x = y }.
所以它看起来像高级语言can这样做，但是在降低标准开发人员的学习曲线方面可以说还有很多工作要做。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
