haskell - 添加类型级自然数

Question

我认为，不可能只在 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) (???))

Answer 1

您不需要添加 HZero 的案例和 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第二种情况下的约束。它们被类的父类(super class)约束所暗示。

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

 data Nat = Zero | Succ Nat

然后您可以使用 Nat不仅作为一种类型，而且作为一种类型。然后，您可以定义一个类型族以对两个自然数进行加法，如下所示:

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

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