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.

Answer 3

Your example makes me think you are trying to do prolog style logic numbers which would be something like

type fancyInt = Zero | Succ of fancyInt ;;

then add would be

let rec add a b = match a with Zero -> b | Succ c -> add c (Succ b);;

Your background story hints at a different solution, create a class that represents distances. Internally store the value however you need to then provide an interface that allows you to get and set the distance in the units necessary at the time. Or if you are wanting to stay with a functional approach just create the types for your units then have of functions the same way Ocaml itself handles such things, i.e. meters_of_km.