haskell - 如何指定两个操作在类型类中交换？

Question

我开始阅读this paper on CRDTs ，这是一种通过确保修改数据的操作是可交换的来同时共享可修改数据的方法。在我看来，这将是 Haskell 中抽象的一个很好的候选者 - 为 CRDT 提供一个类型类，指定数据类型和在该类型上交换的操作，然后致力于使库在并发进程之间实际共享更新。

我不知道如何在类型类规范中表达操作必须交换的约定。

举个简单的例子:

class Direction a where
  turnLeft :: a -> a
  turnRight :: a -> a

无法保证 turnLeft . turnRight与 turnRight . turnLeft 相同。我认为后备方法是指定 monad 法则的等效项 - 使用注释来指定类型系统未强制执行的约束。

Answer 1

您想要的是一个包含证明负担的类型类，类似于下面的伪 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 }.

所以看起来高级语言可以做到这一点，但是在降低标准开发人员的学习曲线方面可以说还有很多工作要做。