f# - 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 类型推断的能力。

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

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。正如您所看到的，这些方程并不难解；事实上，统一的唯一理论是句法相等，即两个事物相等当且仅当它们以相同的方式编写(特别考虑未绑定(bind)变量)。

测量单位的问题是生成的方程无法使用句法等式以独特的方式求解；正确使用的理论是阿贝尔群理论(逆、恒等元、交换运算)。例如，计量单位m * s * s⁻¹应等于m。当涉及到主要类型和 let 泛化时，情况会更加复杂。例如，以下代码在 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