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.

Answer 2

You might be able to use one of Oleg's many amazing constructions: http://caml.inria.fr/pub/ml-archives/caml-list/2009/07/2984f23799f442d0579faacbf4e6e904.en.html

Jane Street has another suggestion using first-class modules.

http://ocaml.janestreet.com/?q=node/81

Disclaimer: I mostly admire this kind of programming from afar.