Add Type Level Natural Numbers

Question

I assume, that it is not possible to just add two type level natural numbers in haskell. Is this true?

Suppose the natural numbers are defined like so:

class HNat a

data HZero
instance HNat HZero

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

Is it pssible to define HAdd in a way similar to:

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

You don't need the case for adding HZero and HZero. This is already covered by the second case. Think how you'd add Peano naturals on the term level, by induction on the first argument:

 data Nat = Zero | Succ Nat

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

Now if you're using functional dependencies, you're writing a logic program. So instead of making a recursive call on the right hand side, you add a constraint for the result of the recursive call on the left:

 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)

You don't need the HNat constraints in the second instance. They're implied by the superclass constraints on the class.

These days, I think the nicest way of doing this sort of type-level programming is to use DataKinds and TypeFamilies. You define just as on the term level:

 data Nat = Zero | Succ Nat

You can then use Nat not only as a type, but also as a kind. You can then define a type family for addition on two natural numbers as follows:

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

This is much closer to the term-level definition of addition. Also, using the "promoted" kind Nat saves you from having to define a class such as HNat.

Answer 2

It is possible. Take a look at the packages type-level-natural-number and `type-level-natural-number-operations. Both are a bit old, but easy to use and the latter defines a Plus type family.

Anyway, I would change your last line to something like this (I didn't test if this compiles).

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

Basically, what you do is to define addition inductively and the additional constraint HAdd n1 x y adds the necessary inductive case.