Naive and failed type-level theorem proving using GADT

Learning
1

Using GADT types to encode the facts:

  • zero is a natural number
  • successor of a natural number is a natural number
  • zero adds to whatever natural number is that number
  • if a and b sums to c, then succ. of a and b sums to succ. of c.

Then GADT values are just the proof terms of the facts encoded by their types.

But all these good wishes are suspended by the error message:

Error: In this definition, a type variable cannot be deduced
from the type parameters.

It refers to the type definition of nat. What are the problems with the code?

(* use toplevel to show the error *)
type 'a s;;
type z;;
type _ nat =
  | Zero : z nat
  | Succ : 'a nat -> 'a s nat;;

let two_is_nat : z s s nat = Succ (Succ Zero);;  

type (_ , _, _) add =
  | Monoid : (z nat, 'a nat , 'a nat) add
  | Step   : ('a nat, 'b nat, 'c nat) add -> ('a s nat, 'b nat, 'c s nat) add

let zero_plus_one_is_one : (z nat, z s nat , z s nat) add
  = Monoid

let one_plus_one_is_two : (z s nat, z s nat, z s s nat) add 
  = Step Monoid

let two_plus_one_is_three : (z s s nat, z s nat, z s s s nat) add 
  = Step (Step Monoid)
2

This abstract type might be implemented as

type 'a s = int

Then, it impossible to infer the type 'a on the left-hand side of the arrow from the type 'a s on the right hand side in your GADT definition:

type _ nat =
  | Zero : z nat
  | Succ : 'a nat -> 'a s nat

In general, nominal types (like variants or records) are better suited to be used as type-level function (because there are injective and have some form of distinct identity).
I would advise you to define s and z as:

type 'a s = S
type z = Z
type _ nat =
  | Zero : z nat
  | Succ : 'a nat -> 'a s nat

Note that your specific error could be fixed with an injectivity annotation

type !'a s
type z
type _ nat =
  | Zero : z nat
  | Succ : 'a nat -> 'a s nat

but there are still problem lurking around with this implementation because the typechecker cannot prove any inequalities involving 'a s and z (z might be int and !'a s might be 'a list for instance).

5 Likes