Can F# units of measure be implemented in OCaml?

f#, ocaml, units-of-measurement

Solution

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

Problem

F# has a units of measure capability (there's more detail in this research paper). ``` [<Measure>] type unit-name [ = measure ] ``` This allows units to be defined such as: ``` type [<Measure>] USD type [<Measure>] EUR ``` And code to be written as: ``` let dollars = 25.0<USD> let euros = 25.0<EUR> // Results in an error as the units differ if dollars > euros then printfn "Greater!" ``` It also handles conversions (I'm guessing that means Measure has some functions defined that let Measures be multiplied, divided and exponentiated): ``` // Mass, grams. [<Measure>] type g // Mass, kilograms. [<Measure>] type kg let gramsPerKilogram : float<g kg^-1> = 1000.0<g/kg> let convertGramsToKilograms (x : float<g>) = x / gramsPerKilogram ``` Could this capability be implemented in OCaml? Someone suggested I look at phantom types but they don't appear to compose in the same way as units. (Disclosure: I asked this question about Haskell a few months ago, got an interesting discussion but no definitive answer beyond 'probably not').

Original source