F# 度量单位可以在 OCaml 中实现吗？

Question

F# 有一个units of measure capability（research paper 中有更多详细信息）。

[<Measure>] type unit-name [ = measure ]

这允许定义单位，例如：

type [<Measure>] USD
type [<Measure>] EUR

而代码要写成：

let dollars = 25.0<USD>
let euros = 25.0<EUR>

// Results in an error as the units differ
if dollars > euros then printfn "Greater!"

它还处理转换（我猜这意味着 Measure 定义了一些函数，可以让Measures 进行乘法、除法和求幂）：

// 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

这个功能可以在 OCaml 中实现吗？有人建议我查看幻象类型，但它们的组成方式似乎与单位不同。

（披露：几个月前我问过这个关于 Haskell 的问题，得到了一个有趣的讨论，但除了“可能不是”之外没有明确的答案。

Answer 1

快速回答：不，这超出了当前 OCaml 类型推断的能力。

再解释一下：大多数函数式语言中的类型推断都是基于一个名为unification的概念，这实际上只是求解方程的一种特定方法。例如，推断表达式的类型，如

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

首先涉及创建一组方程（其中l、i和j的类型分别为'a、'b和'c，以及List.nth : 'd list -> int -> 'd、(=) : 'e -> 'e -> bool、@ 987654331@):

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

然后求解这些方程，得到'a ~ (int * int) list 和f : (int * int) list -> int -> int -> bool。如您所见，这些方程并不难求解；事实上，统一的唯一理论是句法相等，即如果两个事物相等当且仅当它们以相同的方式编写（特别考虑未绑定变量)。

度量单位的问题是生成的方程不能使用句法等式以独特的方式求解；使用的正确理论是阿贝尔群理论（逆、单位元、交换运算）。例如，度量单位m * s * s⁻¹ 应等于m。当涉及到主体类型和 let-generalization 时，还有一个更复杂的问题。例如，以下内容不会在 F# 中进行类型检查：

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

因为y 被推断为具有类型float<'_a> -> float<'b * '_a⁻¹>，而不是更一般的类型float<'a> -> float<'b * 'a⁻¹>

无论如何，我建议阅读以下博士论文的第 3 章：

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

Answer 2

它不能直接用类型系统的语法表示，但可以进行一些编码。例如，在 caml-list https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00069.html 上的这条消息中已经提出了一个建议。这是答案的格式化内容。顺便说一句，我看不出这不适用于 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

这成功地跟踪了数量的维度：

# 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>

如果使用不当会报错：

# 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

但是，对于某些事情，它会推断出过于严格的类型：

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