type level integers in ocaml

Question

Could anyone give me suggestions/advice on making type level integers in OCaml (3.12) supporting addition and subtraction operations on them?

For example, if I have numbers represented like this:

type zero
type 'a succ
type pos1 = zero succ
type pos2 =  zero succ succ
...

I need a way to define function on types like this:

val add: pos2 -> pos1 -> pos3

Little background: I'm trying to port some haskell code for operations on physical dimensions and i need the ability to define operations on dimension types (record of 7 type level ints representing exponents of 7 basic SI units). I need to do it this way to avoid dynamic binding (when using objects) and to enable compiler to evaluate and check all such expressions statically.

My current understanding is that I should make a GADT that implements operations as type constructors, but still I'm struggling with the idea, and any hint would be greatly appreciated.

Answer 1

You may also be interested in the article Many Holes in Hindley-Milner, by Sam Lindley, from the 2008 Workshop on ML.