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

Question

我开始阅读这篇关于CRDT的论文，它是一种通过确保修改数据的操作可交换来同时共享可修改数据的方法。在我看来，这将成为Haskell中抽象的好选择-提供一个CRDTs类型类，指定可交换的数据类型和操作，然后努力制作库以在并发进程之间实际共享更新。

我无法确定如何在类型类的规范中表达操作必须可交换的契约。

举个简单例子：

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

不能保证turnLeft . turnRight等同于turnRight . turnLeft。我想备选方案是指定单子律的等效方式 - 使用注释来指定类型系统未强制执行的约束条件。

- rampion

Answer 1

你需要的是一个包含“proof burden”的类型类，类似于下面的伪Haskell代码：

class Direction a where
    turnLeft  :: a -> a
    turnRight :: a -> a
    proofburden (forall a. turnLeft (turnRight a) === turnRight (turnLeft a))

所有实例必须提供函数和证明以供编译器进行类型检查。这对于Haskell来说是一种美好的愿望，因为Haskell没有（或者只有有限的）证明概念。

另一方面，Coq是一种依赖类型语言的证明助手，可以提取到Haskell中。虽然我从未使用过Coq 的类型类，但通过快速搜索可以找到如下示例：

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

看起来高级语言可以做到这一点，但要让普通开发人员更容易上手仍有相当多的工作要做。

- Thomas M. DuBuisson

---

有趣的是，C++0x概念（已被放弃的提案）具有这样的支持，它们被称为公理。 - snk_kid

@snk_kid：C++的公理不能静态地确保指定的不变量实际上是真的。 - sepp2k

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 Enhancement (SHE)是Haskell代码的预处理器，可以欺骗DTP的一些效果进入Haskell。它通过在类型世界中复制来自值世界的数据来实现这一点。我认为它还没有处理复制值级函数的能力，如果它这样做了，我的直觉是这可能对它来说太复杂了。

- Jason Reich

---

Agda在这种情况下还有一个小好处，就是更接近Haskell的风格，并且直接支持与Haskell的FFI——也就是说，对于一个新接触依赖类型语言的Haskell程序员来说，可能会有更小的学习曲线。 - C. A. McCann

我发现在编写Agda时感觉更像Haskell，而从Coq中提取的代码更像我会编写的Haskell。优劣势并存。 - Jason Reich

我想这取决于目标是提取一个小库以在Haskell中使用，还是在调用Haskell库的同时主要使用Agda编写。但是我很少使用Agda，从未使用过Coq,所以不能确定... - C. A. McCann

没错。我相信今年有人正在开发 Agda 到 Haskell 的编译器，以使其更加简洁。所有参与其中的人都做得非常出色。 - Jason Reich

我稍微尝试了一下She，我想澄清一下我的答案，因为你可能能够理解，但是She还没有完全到位，而且你可能还不想使用它。如果你有兴趣，可以查看我的博客文章以了解我的工作过程。你激发了我的灵感。谢谢。 - Jason Reich

大多数函数式程序员对使用依赖类型编程持犹豫态度。据说类型检查变得不可判定；类型检查器将始终循环；而且依赖类型非常、非常难。然而，这些程序员却非常乐意使用一堆复杂的类型系统扩展来编程。[...]为了避免使用依赖类型而不惜付出巨大的努力。--依赖类型 Lambda 演算的教程实现。注：请与 SHE 的罪犯名单进行比较。 :) - C. A. McCann

Answer 3

正如已经提到的那样，使用类型系统无法直接强制执行这一点。但是，如果仅在注释中指定约束条件不够满意，作为一个折衷方案，您可以为所需的代数属性提供QuickCheck测试。

类似这样的内容已经可以在checkers package中找到；您可能需要参考它以获得灵感。

- C. A. McCann

Answer 4

我无法确定如何在类型类的规范中表达操作必须交换的合同条款。

你无法确定的原因是这是不可能的。至少在Haskell中，你无法在类型中编码这种属性。

- sepp2k

---

我愿意相信 - 你能提供任何关于这个话题的讨论链接吗？ - rampion

我认为原因在于价值和它们的类型之间的分离。在Haskell的类型系统中，它们的世界之间存在着无法逾越的障碍。我非常喜欢Conor McBride在http://www.strictlypositive.org/winging-jpgs/和http://www.strictlypositive.org/a-case/中提到的“既定社会秩序”的比喻。 - Jason Reich

“已确立的社会秩序”幻灯片非常有趣（也很有启发性）。麦克布赖德还在Epigram上发表了论文《为什么依赖类型很重要》，该语言是依赖类型的。它的语法看起来与Haskell相似。 - emi