45

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

Darren
  • 2,888
  • 1
  • 23
  • 34
  • 2
    my suggestion to you would have been phantom types as well, but you are correct that they do not 'compose' as you desire. The first situation you mention (the error in comparison) and the last (the conversion functions) could be handled by phantom types though. – nlucaroni Feb 03 '14 at 22:26
  • 4
    it really would make sense to have that in every language doing anything remotely physically interpretable....! – nicolas Feb 04 '14 at 13:25
  • 1
    This may be possible as a plugin at the typechecker level. There has been some talk about allowing plugins for the typechecker. I don't know what the current state of the compiler is in this case. – hcarty Feb 04 '14 at 14:10
  • seems like a good idea to have compile time units of measure support to OCaml, as an aside I've created an F# runtime units of measure library which you could easily port & potentially use for a little inspiration: http://trelford.com/blog/post/Runtime-Units-of-Measure-for-F.aspx – Phillip Trelford Feb 04 '14 at 15:02
  • 6
    you can write composition functions for the types (for example having `type ('a,'b) per` and `type 'a measure = { v : float };` and `let (>) (a : 'a measure) (b : 'b measure) : (('a,'b) per) measure = {a.v /. b.v}` But you'll have issues with multiplication and associativity, that I assume F# takes care of. – nlucaroni Feb 04 '14 at 15:13
  • For runtime units in OCaml I wrote bindings to the UDUNITS library - https://github.com/hcarty/ocaml-udunits – hcarty Feb 11 '14 at 11:59
  • I would answer "probably yes" to the Haskell question, as I have toyed with a rudimentary form of this. But I don't know enough about type-level computations in OCaml. – n. m. could be an AI Jun 10 '14 at 15:39
  • There is something like this for C++ (compile time checking of units). You can do run time checking in any Turing complete language. – ctrl-alt-delor Jul 01 '14 at 12:04
  • @richard runtime checking is not enough: you would want to spot mismatched unit of measure checking _before_ you run the actual code. You can accomplish this by associating different types to different units of measure: the problem is whether there is an easy way to extend the operation on the original types to the types with unit of measure. – pqnet Aug 06 '14 at 13:36

2 Answers2

8

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

Baggers
  • 3,183
  • 20
  • 31
Tom Primozic
  • 191
  • 1
  • 3
  • 2
    Good answer. Note that with a little nudge, F# will generalize measures at lets; adding the annotation `:float<_>` to either `x` or `z`'s binding will result in `y` having the type you expect. – kvb Aug 20 '14 at 15:39
8

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>
Pierre Chambart
  • 1,469
  • 12
  • 17