6

我认为，不可能只在 haskell 中添加两个类型级别的自然数。这是真的？

假设自然数定义如下：

class HNat a

data HZero
instance HNat HZero

data HSucc n
instance (HNat n) => HNat (HSucc n)

以类似于以下方式定义 HAdd 是否可行：

class (HNat n1, HNat n2, HNat ne) => HAdd n1 n2 ne | n1 n2 -> ne
instance             HAdd HZero HZero HZero
instance (HNat x) => HAdd HZero x     x
instance (HNat n1 
         ,HNat x) => HAdd (HSucc n1)  x (HAdd n1 (HSucc x) (???))
4

2 回答 2

20

您不需要添加HZeroand的案例HZero。第二种情况已经涵盖了这一点。通过对第一个参数的归纳，想想如何在术语级别添加 Peano naturals：

 data Nat = Zero | Succ Nat

 add :: Nat -> Nat -> Nat
 add Zero     y = y
 add (Succ x) y = Succ (add x y)

现在，如果您正在使用函数依赖项，那么您正在编写一个逻辑程序。因此，不是在右侧进行递归调用，而是在左侧为递归调用的结果添加一个约束：

 class (HNat x, HNat y, HNat r) => HAdd x y r | x y -> r
 instance (HNat y)     => HAdd HZero     y y
 instance (HAdd x y r) => HAdd (HSucc x) y (HSucc r)

在第二种情况下，您不需要HNat约束。它们被类的超类约束所暗示。

这些天来，我认为进行这种类型级编程的最好方法是使用DataKindsand TypeFamilies. 您就像在术语级别上定义的那样：

 data Nat = Zero | Succ Nat

然后，您Nat不仅可以将其用作 type ，还可以用作kind。然后，您可以定义一个类型族以对两个自然数进行加法，如下所示：

 type family Add (x :: Nat) (y :: Nat) :: Nat
 type instance Add Zero     y = y
 type instance Add (Succ x) y = Succ (Add x y)

这更接近于术语级别的加法定义。此外，使用“promoted”类型Nat可以让您不必定义一个类，例如HNat.

于 2013-01-28T13:10:14.317 回答
3

有可能的。看看包装type-level-natural-number和`type-level-natural-number-operations. 两者都有点老，但易于使用，后者定义了一个Plus类型族。

无论如何，我会将您的最后一行更改为这样的内容（我没有测试它是否可以编译）。

instance (HNat n1, HNat x, HAdd n1 x y) => HAdd (HSucc n1) x (HAdd n1 x (HSucc y))

基本上，您所做的就是以归纳方式定义加法，并且附加约束HAdd n1 x y添加必要的归纳情况。

于 2013-01-28T12:00:28.980 回答