Fam的度量单位可以在OCaml中实现吗?

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!" 

它也处理转换(我猜测这意味着测量有一些定义的函数,让度量值相乘,分割和指数):

 // 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中实现吗? 有人build议我看幻像types,但是它们看起来不像单位一样组成。

(披露:几个月前,我问了关于Haskell的这个问题,得到了一个有趣的讨论,但没有超出“可能不是”的明确答案)。

快速回答:不,这超出了当前OCamltypes推断的function。

再解释一下:大多数函数式语言中的types推理是基于一个叫做统一的概念,这个概念实际上只是求解方程式的一个具体方式。 例如,推断一个expression式的types

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

首先创build一组方程(其中, lij的types分别是'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) listf : (int * int) list -> int -> int -> bool 。 如你所见,这些方程不是很难解决, 实际上,统一的唯一理论是语法上的平等 ,也就是说,如果两个事物相同, 当且仅当它们以相同的方式写入(特别考虑未绑定的variables)。

措施单位的问题在于,所产生的方程不能用语法上的相等方式以独特的方式解决; 正确的理论是阿贝尔群理论 (逆,身份要素,交换作用)。 例如,度量单位m * s * s⁻¹应该等于m 。 当涉及主要types和推广时,还有一个更复杂的问题。 例如,以下不在F#中进行types检查:

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

因为y被推断为具有typesfloat<'_a> -> float<'b * '_a⁻¹> ,而不是更通用的typesfloat<'a> -> float<'b * 'a⁻¹>

无论如何,更多的信息,我build议阅读以下博士论文的第3章:

pub/thesis/thesis-2013-12-03.pdf

它不能在types系统的语法中直接expression,但是一些编码是可能的。 例如在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 xy = x *. y let add xy = 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 

但是,对于某些事情,它会推断出过于严格的types:

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