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

Question

我开始阅读关于CRDT的这篇论文,这是一种通过确保修改数据的操作是可交换的,同时共享可修改数据的方法.在我看来,这将是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的类型类,但快速搜索很有成效,例如:

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是依赖类型的语言,其中障碍不存在或允许事物跨越.所述斯特拉斯克莱德Haskell的增强(SHE)为Haskell代码可以欺骗一些DTP的影响成Haskell中的预处理器.它通过复制类型世界中值世界的数据来实现这一点.我不认为它处理重复的价值级功能,如果确实如此,我的预感是这可能太复杂了,无法处理.