Type-level Peano arithmetics: the type constructor would escape its scope

Question

I tried to implement Peano arithmetic on the type-level in Ocaml and came through a problem:

module Nat = struct
  type zero = Z

  type 'a succ = S

  type 'a nat = Zero : zero nat | Succ : 'a nat -> 'a succ nat
end

Now, if I want to implement add, the two axioms regarding this operation are that:

I tried

let rec add : type n1 n2. n1 nat -> n2 nat -> 'a nat =
  fun a b -> match b with Zero -> a | Succ b' -> Succ (add a b')

But

9 |    fun a b -> match b with Zero -> a | Succ b' -> Succ (add a b')
                                       ^
Error: This expression has type n1 nat but an expression was expected of type
         'a nat
       The type constructor n1 would escape its scope

And I have an error for the second branch too:

let rec add : type n1 n2. n1 nat -> n2 nat -> 'a nat =
  fun a b -> match b with Succ b' -> Succ (add a b') | Zero -> a

9 |    fun a b -> match b with Succ b' -> Succ (add a b') | Zero -> a
                                               ^^^^^^^^^^
Error: This expression has type 'a succ nat
       but an expression was expected of type 'a nat
       The type variable 'a occurs inside 'a succ

If I put the Succ inside the recursive call:

let rec add : type n1 n2. n1 nat -> n2 nat -> 'a nat =
   fun a b -> match b with Succ b' -> add (Succ a) b' | Zero -> a

9 |    fun a b -> match b with Succ b' -> add (Succ a) b' | Zero -> a
                                                                    ^
Error: This expression has type n1 nat but an expression was expected of type
         'a nat
       The type constructor n1 would escape its scope

When I add another type variable, the error changes:

let rec add : type n1 n2 n3. n1 nat -> n2 nat -> n3 nat =
   fun a b -> match b with Succ b' -> add (Succ a) b' | Zero -> a

9 |    fun a b -> match b with Succ b' -> add (Succ a) b' | Zero -> a
                                                                    ^
Error: This expression has type n1 nat but an expression was expected of type
         n3 nat
       Type n1 is not compatible with type n3 

I'm not used to GADT so I'm kind of lost as how to solve this typing problem and if it can even be solved.

Answer 1

The root issue is that the type of the function add is not 'a nat -> 'b nat -> 'c nat.

Moreover, there are no non-diverging values of this type since the return type 'c. 'c nat is universally quantified. Thus a function of type _ nat -> _ nat -> 'c nat is promising to return all integers at once.

The fantasy type for add would be something like 'a nat -> 'b nat -> ('a + 'b) nat, where the type expression ('a + 'b) is computing the addition. However, with the direct encoding for unary integers, there is no way to perform this computation. This is not totally surprising, compared to the non-typed representation of unary integers

type u = Z | Succ of u

the GADTs version is more typed, and thus forbids some functions compared to the untyped version. The function add is one of this ill-typed function.

In other words, if we want to have an addition function, we need an encoding that allows to perform the computation 'a nat -> 'b nat -> ('a+'b) nat at the type level. Moreover, in HM type systems the only computations that are going on when typing are the unification of type variables. Thus, we need to choose an encoding in which addition can be computed by unification.

Fortunately, there is a geometric encoding that works. Consider one-dimensional vectors integer vectors with named end points:

0 = ||
    a b

1 = |-|
    a b

If I want to add a vector u and v, I can perform the addition with

|-----------|-------------|
a    u     b=c      v     d

Here, I have computed the vector u+v by taking the left end point of u, the right end point of v and unifying the right end point of u and the left end point of u. In other words, I have computed an addition by unification. And that encoding can be represented with GADTs:

type ('left,'right) nat =
| Z : ('p, 'p) nat
| S: ('left, 'right) nat -> ('left, 'right succ) nat

let rec add: type left mid right.
(left,mid) nat -> (mid,right) nat -> (left,right) nat =
fun x y -> match y with
| Z -> x
| S y -> S (add x y)

With this addition works. However, this encoding is hard to use due to the value restriction. In particular the values returned by the add function is not polymorphic, which creates issue when we are using unification to do type-level computation.