Type-level shenanigans!

(* Dimensional analysis in OCaml, using only Hindley-Milner
   with variance annotations!
   The technique for representing typelevel integers that we use
   here is from the talk "Many Holes in Hindley-Milner", by
   Sam Lindley (http://www.kb.ecei.tohoku.ac.jp/ml2008/slides/lindley.pdf) *)

(* This type needs to be covariant so we can
   generalize one : ('_a, '_a suc) int to ('a, 'a suc) int *)
(* It is also necessary to make it concrete so we don't
   allow circular types such as ( 'a suc as 'a, 'a ) int *)
type +'a suc = 'a * 'a

(* not necessary, but illustrates the general principle of what we're doing *)
type ('a, 'b) int = unit
let zero : ('a, 'a) int = ()
let inc : ('a, 'b) int -> ('a, 'b suc) int = fun x -> x
let add : ('a, 'b) int -> ('b, 'c) int -> ('a, 'c) int = fun x y -> ()
let sub : ('a, 'b) int -> ('c, 'b) int -> ('a, 'c) int = fun x y -> ()

module Dim :
sig
  (* This also needs to be covariant *)
  type (+'a, +'b, +'c, +'d) dim

  val (+) : ('a, 'b, 'c, 'd) dim
	    -> ('a, 'b, 'c, 'd) dim
	    -> ('a, 'b, 'c, 'd) dim
  val (-) : ('a, 'b, 'c, 'd) dim
	    -> ('a, 'b, 'c, 'd) dim
	    -> ('a, 'b, 'c, 'd) dim

  val ( * ) : ('a0, 'b0, 'c0, 'd0) dim
	      -> ('b0, 'b1, 'd0, 'd1) dim
	      -> ('a0, 'b1, 'c0, 'd1) dim
  val ( / ) : ('a0, 'b0, 'c0, 'd0) dim
	      -> ('a1, 'b0, 'c1, 'd0) dim
	      -> ('a0, 'a1, 'c0, 'c1) dim

  val meters : float -> ('a, 'a suc, 'b, 'b) dim
  val seconds : float -> ('a, 'a, 'b, 'b suc) dim
		    
end = struct
  type ('a, 'b, 'c, 'd) dim = float

  let (+) = (+.)
  let (-) = (-.)
  let ( * ) = ( *.)
  let (/) = (/.)

  let meters x = x
  let seconds x = x
end

module Test = struct
  open Dim

  let z = zero
	 
  let test = meters 1.
  let x = seconds 1. * meters 1.

  (* This does not typecheck *)
  (* let y = x + seconds 1. *)

  (* This does *)
  let y = x + seconds 1. * meters 1.

  (* Also this *)
  let z = y / seconds 1. + meters 1.

  (* And this *)
  let h = y * meters 1. / meters 1. + seconds 1. * meters 1.
  
  (* But not this! *)
  (* let h' = h - meters 1. / seconds 1. *)

  (* Working as expected *)
  let test = 
    let x = meters 2. in
    let y = x * x in
    y
  let () =
    let x = meters 1. in
    let y = meters 2. in
    let w = x * y in
    let z = x + y in
    ()
end