添加类型级别自然数

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自然:

 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第二个实例中的约束.它们隐含在类的超类约束上.

这些天,我认为进行这种类型级编程的最好方法是使用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.