Type-level arithmetics in OCaml

Question

Ok, more type hackery failure. :) :P

In my week-long pursuit of getting rid of (runtime) assert(n > 0) and instead checking it statically, I've come up with this module:

module Nat : sig 
  type z
  type 'n s

  type ('a, 'n) nat = 
          Zero : ('a, z) nat 
        | Succ : ('a, 'n) nat -> ('a, 'n s) nat 

  val add : ('a, 'n) nat -> ('a, 'n s) nat

end = struct          
  type z
  type 'n s
  type ('a, 'n) nat = 
          Zero : ('a, z) nat 
        | Succ : ('a, 'n) nat -> ('a, 'n s) nat 

  let add n = Succ n

  (*  
  let rec to_int n = function 
        | Succ a -> 1 + (to_int a)
        | Zero -> 0
        *)
end

This gives Peano numbers where the number is encoded in it's own type:

# Zero;;
- : ('a, Nat.z) Nat.nat = Zero
# Succ (Zero);;
- : ('a, Nat.z Nat.s) Nat.nat = Succ Zero
# add (Succ Zero);;
- : ('_a, Nat.z Nat.s Nat.s) Nat.nat = Succ (Succ Zero) 

However, the last function to_int won't compile:

Error: This pattern [Zero -> 0] matches values of type ('a, z) nat
   but a pattern was expected which matches values of type
     ('a, ex#0 s) nat

This is, I think, because z and s is different types. Is it possible to make them the same type, and still have them as phantom types?

(Possible duplicate: type level integers in ocaml)

Answer 1

First, there is a genuine error in your code: it's let to_int = function, not let to_int n = function.

The real problem is that you are using a polymorphic recursive function: you are calling it recursively with different types for the second parameter of the nat type. As type inference of code using polymorphic recursion is undecidable in the general case, OCaml won't try to guess it for you, so you have to be explicit with a polymorphic recursion annotation:

let rec to_int : type n . ('a, n) nat -> int =
   ...

Another point that is not a problem right now but may become one in the future (and show that you still need a bit of training with GADTs): the fact that 'a s and z are distinct types is essential to your function working as you want. It tells you that if you have a value of type ('a, z) nat (note that the 'a parameter is useless in all this stuff), it can only be a Zero. You can write the following functions and they're total, you get no exhaustivity warning:

let is_zero : ('a, z) nat -> unit = function
  | Zero -> ()
  (* case Succ not considered *)

let equal : type n . ('a, n) nat * ('a, n) nat -> bool = function
  | Zero, Zero -> true
  | Succ n1, Succ n2 -> equal (n1, n2)
  (* cases (Zero, SUcc _) or (Succ _, Zero) not considered *)

If there was a possibility that the types z and 'a s overlap (for example if you define type 'a s = z), the type-checker could not reason on these cases being distinct, and you would have to handle the cases that I have omitted here.

The problem with your current definition is that the types 'a s and z are abstracted through a module interface. Inside the definition of the module, the definitions (as distinct abstract types) are visible, but outside the module you don't know anymore how they've been defined, and in fact maybe it was type 'a s = z. So when you are outside the module, you also won't be able to write those functions anymore. The solution is to pick concrete definitions for those types, and let them be visible through the module interface, so that the type-checker always know that they don't overlap:

module Nat : sig
  type z = Z
  type 'a s = S of 'a
  ...
end ...

It doesn't matter that you will never use those Z and S constructors, they're just here to let the type-checker know that z is never equal to 'a s. One could have used int and bool instead.