Can F# units of measure be implemented in OCaml?

Question

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').

Answer 1

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

Answer 2

It cannot be directly expressed in the syntax of the type system, but some encoding are possible. One have been proposed for instance in this message on the caml-list https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00069.html . Here is the formated content of the answer. By the way, I can't see any reason why this wouldn't be applicable to Haskell.

module Unit : sig
  type +'a suc
  type (+'a, +'b) quantity

  val of_float : float -> ('a, 'a) quantity
  val metre : ('a, 'a suc) quantity
  val mul : ('a, 'b) quantity -> ('b, 'c) quantity -> ('a, 'c) quantity
  val add : ('a, 'b) quantity -> ('a, 'b) quantity -> ('a, 'b) quantity
  val neg : ('a, 'b) quantity -> ('a, 'b) quantity
  val inv : ('a, 'b) quantity -> ('b, 'a) quantity
end = struct
  type 'a suc = unit
  type ('a, 'b) quantity = float
  let of_float x = x
  let metre = 1.
  let mul x y = x *. y
  let add x y = x +. y
  let neg x = 0. -. x
  let inv x = 1. /. x
end

This successfully tracks the dimension of quatities:

# open Unit;;

# let m10 = mul (of_float 10.) metre;;
val m10 : ('a, 'a Unit.suc) Unit.quantity = <abstr>

# let sum = add m10 m10;;
val sum : ('a, 'a Unit.suc) Unit.quantity = <abstr>

# let sq = mul m10 m10;;
val sq : ('a, 'a Unit.suc Unit.suc) Unit.quantity = <abstr>

# let cube = mul m10 (mul m10 m10);;
val cube : ('a, 'a Unit.suc Unit.suc Unit.suc) Unit.quantity = <abstr>

# let _ = add (mul sq (inv cube)) (inv m10);;
- : ('a Unit.suc, 'a) Unit.quantity = <abstr>

and it will give errors if they are used incorrectly:

# let _ = add sq cube;;
Characters 15-19:
let _ = add sq cube;;
^^^^
Error: This expression has type
('a, 'a Unit.suc Unit.suc Unit.suc) Unit.quantity
but an expression was expected of type
('a, 'a Unit.suc Unit.suc) Unit.quantity
The type variable 'a occurs inside 'a Unit.suc

# let _ = add m10 (mul m10 m10);;
Characters 16-29:
let _ = add m10 (mul m10 m10);;
^^^^^^^^^^^^^
Error: This expression has type ('a, 'a Unit.suc Unit.suc) Unit.quantity
but an expression was expected of type ('a, 'a Unit.suc)
Unit.quantity
The type variable 'a occurs inside 'a Unit.suc

However, it will infer too restrictive types for some things:

# let sq x = mul x x;;
val sq : ('a, 'a) Unit.quantity -> ('a, 'a) Unit.quantity = <fun>