F#计量单位能否在OCaml中实施？

Question

F#具有度量单位能力(本研究报告中有更多细节).

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

它不能直接在类型系统的语法中表达,但可以进行某些编码.例如,在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>

Answer 2

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

进一步说明一下：大多数功能语言中的类型推断都是基于称为统一的概念，这实际上只是求解方程式的一种特定方式。例如，推断表达式的类型，例如

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，(+) : int -> int -> int）：

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

然后求解这些方程，得出'a ~ (int * int) list和f : (int * int) list -> int -> int -> bool。如您所见，这些方程式很难求解。实际上，统一的唯一理论是句法相等，即，当且仅当两个事物以相同的方式书写时（如果对未绑定变量有特殊考虑），两个事物相等。

度量单位的问题在于，生成的方程式无法使用句法等式以独特的方式求解。正确使用的理论是Abelian群的理论（逆，恒等式，可交换运算）。例如，度量单位m * s * s?¹应等于m。当涉及主体类型和let-generalization时，会进一步复杂化。例如，以下代码不会在F＃中进行类型检查：

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

因为y推断具有type float<'_a> -> float<'b * '_a?¹>，而不是更一般的typefloat<'a> -> float<'b * 'a?¹>

无论如何，有关更多信息，我建议阅读以下博士学位论文的第3章：

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