10

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

我想不通的是如何在类型类的规范中表达操作必须通勤的合同。

举个简单的例子：

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

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

4

4 回答 4

11

你想要的是一个包含证明负担的类型类，类似于下面的伪 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 的类型类，但快速搜索是有成效的，例如：

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

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

于 2010-12-23T20:45:08.197 回答
7

除了 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

这表示关于两种类型相等的定理。ega等价于bis 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 中。它通过从类型世界中的值世界复制数据来做到这一点。我认为它还不能处理重复的值级函数，如果是这样，我的直觉是这可能太复杂而无法处理。

于 2010-12-23T21:18:48.853 回答
3

如前所述，没有办法直接在 Haskell 中使用类型系统强制执行此操作。但是，如果仅在注释中指定约束还不够令人满意，作为中间立场，您可以为所需的代数属性提供 QuickCheck 测试。

类似的东西已经可以在checkers 包中找到；您可能想咨询它以获取灵感。

于 2010-12-23T21:18:09.620 回答
2

我想不通的是如何在类型类的规范中表达操作必须通勤的合同。

你想不通的原因是不可能。你不能在类型中编码这种属性——至少在 Haskell 中是这样。

于 2010-12-23T20:06:40.423 回答