How can I add two numbers using type constraints?

Here I encode addition by 1 as wrapping in a tuple type and subtraction by 1 as extracting the second element of the tuple type:

type zero = unit * unit
type 'a minus1 = 'snd constraint 'a = unit * 'snd
type 'a plus1 = unit * 'a

So far, the encoding works:

type one = zero plus1
type two = one plus1
type two' = zero plus1 plus1
type two'' = unit * (unit * (unit * unit))

let minus1 ((), n) = n
let plus1 n = ((), n)
let zero = ((), ())
let one : one = plus1 zero
let two : two = plus1 one
let two : two = plus1 (plus1 zero)
let two : two' = two
let two : two'' = two

I'm trying to implement addition as subtracting the left-hand side by 1 and adding 1 to the right-hand side until the left-hand side is 0, but I don't know how to do such branching logic. If type-information had an or, this would express what I'm looking for:

type ('a, 'b) plus = 'res
                (constraint 'a = zero constraint 'res = 'b)
            or  (
                 constraint  ('a_pred, 'b_succ) plus = 'res
                 constraint 'a_pred = 'a minus1
                 constraint 'b_succ = 'b plus1
            )

Is there a way to implement plus along these lines?

Solution

This is not directly possible: you cannot encode unbounded computation in the type system using type constraints. However, you can use unification to transfer some computational work done in some part of the type to another part.

Mimicking the classical GADT encoding for natural numbers with additions, we can define:

type ('x,'y) nat = 'x * 'y

type 'a zero = ('a, 'a) nat
let zero (type a) (x:a): a zero = x, x

type 'nat s = (unit * 'a, 'b) nat
  constraint 'nat = ('a, 'b) nat

let succ (nat:'s -> 'n) (x:'s) : 'n s  =
  let x, y = nat x in
  ((), x), y

where the type ('res,'start) nat represent the result of the addition to the underlying integer of type nat to the natural number start (which is using itself the unary Peano encoding)

We can check that we can construct the encoding for 1, 2 and 3 with

type 'a one = 'a zero s
type 'a two = 'a one s
type 'a three = 'a two s
let one (x:'a): 'a one = succ zero x
let two (x:'a): 'a two = succ one x
let three (x:'a): 'a three = succ two x

Then defining addition is a matter of combining the computational work done on the type of each operand using type unification :

type ('x,'y) plus = ('sup,'inf) nat
  constraint 'x = ('sup, 'mid) nat
  constraint 'y = ('mid,'inf) nat

let (+) (nat1: _ -> 'nat1) (nat2: _ -> 'nat2)
    x : ('nat1,'nat2) plus =
  let mid, _ = nat2 x in
  let sup, _ = nat1 mid in
  sup, x

We can then use the typechecker to check that 1 + 2 = 3 with

let three' x = (one + two) x
let ok = [ three;  three' ]