如何在类型类型中指定两个操作通勤？

Question

我开始阅读 关于CRDT的本文, ，这是一种通过确保修改数据的操作是交换性的一种方式共享可修改数据的方法。在我看来，这将是在Haskell中抽象的良好候选者 - 为CRDT提供了类型，该crdts指定了该类型上通勤的数据类型和操作，然后致力于使库实际上共享并发过程之间的更新。

我不知道如何表达操作必须在类型类规范中上下班的合同。

对于一个简单的示例：

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

不能保证 turnLeft . turnRight 是相同的 turnRight . turnLeft. 。我想后备是指定同等法律 - 使用注释来指定类型系统未强制执行的约束。

Answer 1

您想要的是一个包括证明负担的类型类，类似于以下伪哈斯尔的类型：

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的类型类 以前，快速搜索是富有成果的，一个例子：

Class EqDec (A : Type) := {
   eqb : A -> A -> bool ;
   eqb_leibniz : forall x y, eqb x y = true -> x = y }.

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

Answer 2

除了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增强（她） 是Haskell代码的预处理器，可以将DTP的某些效果欺骗到Haskell中。它通过重复类型世界中价值世界的数据来做到这一点。我认为它还没有处理重复的值级功能，如果这样做，我的直觉是太复杂了，无法处理它。

Answer 3

如前所述，没有办法使用类型系统直接在Haskell中执行此操作。但是，如果仅在评论中指定约束不足以满足，则作为中间立场，您可以为所需的代数属性提供快速检查测试。

沿着这些线已经可以找到 跳棋包;您可能需要咨询它以获取灵感。

Answer 4

我不知道如何表达操作必须在类型类规范中上下班的合同。

您无法弄清楚的原因是不可能。您不能以类型编码这种属性 - 至少不是在Haskell中。