f# - 是否可以在OCaml中实现F#度量单位？

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定义了一些函数，这些函数可以使Measurements进行乘，除和乘幂运算):

// 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的问题，进行了有趣的讨论，但除了“可能不是”以外，没有明确的答案)。

最佳答案

快速解答:不，这超出了当前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)的变量)，两个事物才相等。

度量单位的问题在于，生成的方程式无法使用句法等式以独特的方式求解。正确使用的理论是Abelian群的理论(逆，恒等式，可交换运算)。例如，度量单位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

关于f# - 是否可以在OCaml中实现F#度量单位？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/21538563/