Can F# units of measure be implemented in OCaml?

Quick answer: No, that’s beyond the capabilities of current OCaml type inference.

To explain it a bit more: type inference in most functional languages is based on a concept called unification, which is really just a specific way of solving equations. For example, inferring the type of an expression like

let f l i j =
  (i, j) = List.nth l (i + j)

involves first creating a set of equations (where the types of l, i and j are 'a, 'b and 'c respectively, and List.nth : 'd list -> int -> 'd, (=) : 'e -> 'e -> bool, (+) : int -> int -> int):

'e ~ 'b * 'c
'a ~ 'd list
'b ~ int
'c ~ int
'd ~ 'e

and then solving these equations, which yields 'a ~ (int * int) list and f : (int * int) list -> int -> int -> bool. As you can see, these equations are not very hard to solve; in fact, the only theory underlying unification is syntactic equality, i.e. if two things are equal if and only if they are written in the same way (with special consideration for unbound variables).

The problem with units of measures is that the equations that are generated cannot be solved in a unique way using syntactic equality; the correct theory to use is the theory of Abelian groups (inverses, identity element, commutative operation). For example, the units of measure m * s * s⁻¹ should be equivalent to m. There is a further complication when it comes to principal types and let-generalization. For example, the following doesn’t type-check in F#:

fun x -> let y z = x / z in (y mass, y time)

because y is inferred to have type float<'_a> -> float<'b * '_a⁻¹>, instead of the more general type float<'a> -> float<'b * 'a⁻¹>

Anyhow, for more information, I recommend reading the chapter 3 of the following PhD thesis:

http://adam.gundry.co.uk/pub/thesis/thesis-2013-12-03.pdf

Leave a Comment