types - 有没有办法在 OCaml 类型系统中嵌入单元处理逻辑？

Question

这可能是不可能的，但我觉得我可能会学到一些东西，或者可能有一种截然不同的方法来处理它。
我正在编写一些包含一些物理模拟元素的代码，我可能正在处理一堆不同的单元。我觉得值得让类型系统在这方面为我做一些工作，这样我就不能，例如，为距离增加质量或类似的东西。
这很容易:

module Mass : sig 
  type t
  val sum : t -> t -> t
  ...
end = struct
  type t = int
  let sum = +
  ...
end
module Distance : sig 
  type t
  val sum : t -> t -> t
  ...
end = struct
  type t = int
  let sum = +
  ...
end

现在编译器将阻止我尝试混合两者(对吗？)。类似的东西也应该用于表示相同类型的单位(例如，磅与公斤)，甚至可能使我免受一些精度或溢出错误的影响。到目前为止很容易。有趣/困难的部分是我想制作一个流畅的框架来处理单位的组合，比如米每秒平方等。
我可以通过玩仿函数来接近:

module MakeProduct(F : UnitT)(S: UnitT) = struct
   type t = (F.t, S.t)
   ...
end
module MakeRatio(Numerator : UnitT)(Denominator: UnitT) = struct
   type t = (Numerator.t, Denominator.t)
   ...
end

然后我就可以

module MetersPerSecondSquared = MakeRatio(MakeRatio(Meter)( Second))(Second)

会有一些非常笨拙的函数名，但这应该会给我一个类型安全的系统，我可以在其中乘以 25 m/s^2来自 5s并获得 125m/s.除了笨拙之外，我看到的问题是系统将无法识别以不同顺序表达相同事物的类型。例如，我还可以将上述内容表示为:

MakeRatio(Meter)(Product(Second)(Second))

两者最终都应该表达相同的概念，但我不知道有什么方法可以告诉类型系统它们是相同的，或者您仍然应该能够将第二个乘以 5s并在 m/s 中得到结果.
我正在努力学习的是:

有没有办法让这个想法奏效？

如果没有，是否有正式/理论上的原因这很难？ (仅用于我自己的教育)

是否有完全不同的方法来干净地处理类型系统中的不同单元？

Answer 1

可以使用正确的编码进行一些有限的类型级算术。然而，任何编码都会受到 OCaml 类型系统不知道算术这一事实的限制，并且不能被欺骗自己证明复杂的算术定理。
一种可能在复杂性和特征之间取得良好折衷的编码是使用一组固定的核心单元(例如 m 、 s 和 kg )和描述浮点单位的幻像类型。

module Units: sig
  type 'a t
  val m: <m: ?one; s: ?zero; kg: ?zero> t
end = struct
  type 'a t = float
  let m = 1.
end

这里的类型 <m:'m; s:'s; kg:'kg> Units.t本质上是一个带有一些类型参数的浮点数 <m:'m; s:'s; kg:'kg>描述每个基本单位的单位指数。
我们希望这个指数是一个类型级别的整数(所以 ?zero 应该是 0 等的类型级别编码......)。
整数的一种有用编码是将它们编码为翻译而不是在一元整数之上。
首先，我们可以定义一元 z (对于 zero )类型和类型级别的后继函数:

type z = Zero
type 'a succ = S

然后我们可以编码 zero作为映射整数 n 的函数至 n :

type 'n zero = 'n * 'n

和 one作为映射整数 n 的函数至 n + 1 :

type 'n one = 'n * 'n succ

通过这种编码，我们可以填写 ?zero和 ?one Unit 中的占位符模块:

module Unit: sig
  type +'a t

  (* Generators *)
  val m: <m:_ one; s:_ zero; kg:_ zero> t
  val s: <m:_ zero; s:_ one; kg:_ zero> t
  val kg: <m:_ zero; s:_ zero; kg:_ one> t
  ...
end

然后我们可以使用我们的翻译编码来欺骗类型检查器通过类型统一来计算加法:

  val ( * ):
    <m:'m_low * 'm_mid; s:'s_low * 's_mid; kg:'kg_low * 'kg_mid>  t ->
    <m:'m_mid * 'm_high; s:'s_mid * 's_high; kg:'kg_mid * 'kg_high>  t ->
    <m:'m_low * 'm_high; s:'s_low * 's_high; kg:'kg_low * 'kg_high>  t

在这里，如果我们查看每个组件上发生的情况，我们实际上是在说明是否有来自 'm_low 的翻译。至 'm_mid以及来自 'm_mid 的另一个翻译至 m_high ，这两个翻译的总和是来自 'm_low 的翻译至 'm_high .因此，我们在类型级别实现了加法。
把所有东西放在一起，我们最终得到

module Unit: sig
  type +'a t

  (* Generators *)
  (* Floats are dimensionless *)
  val scalar: float -> <m:_ zero; s: _ zero; kg: _ zero> t
  val float: <m:_ zero; s: _ zero; kg: _ zero> t -> float
  (* Base units *)
  val m: <m:_ one; s:_ zero; kg:_ zero> t
  val s: <m:_ zero; s:_ one; kg:_ zero> t
  val kg: <m:_ zero; s:_ zero; kg:_ one> t

  (* Arithmetic operations *)
  val ( + ): 'a t -> 'a t -> 'a t
  val ( * ):
    <m:'m_low * 'm_mid; s:'s_low * 's_mid; kg:'kg_low * 'kg_mid>  t ->
    <m:'m_mid * 'm_high; s:'s_mid * 's_high; kg:'kg_mid * 'kg_high>  t ->
    <m:'m_low * 'm_high; s:'s_low * 's_high; kg:'kg_low * 'kg_high>  t

  val ( / ) :
    <m:'m_low * 'm_high; s:'s_low * 's_high; kg:'kg_low * 'kg_high> t ->
    <m:'m_mid * 'm_high; s:'s_mid * 's_high; kg:'kg_mid * 'kg_high> t ->
    <m:'m_low * 'm_mid ; s:'s_low * 's_mid ; kg:'kg_low * 'kg_mid > t
end = struct
 type +'a t = float
 let scalar x = x let float x = x
 let ( + ) = ( +. ) let ( * ) = ( *. ) let ( / ) = ( /. )
 let m = 1. let s = 1. let kg = 1.
end

然后我们得到预期的行为:只有具有相同维度的值才能相加(或相减)，乘法值是通过添加维度分量(除法的相反)来完成的。例如，此代码正确编译

open Units
let ( *. ) x y = scalar x * y
let au = 149_597_870_700. *. m
let c  = 299_792_458. *. m / s
let year = 86400. *. (365. *. s)
let ok = float @@ (c * year) / au

而试图在一年中添加一个天文单位会产生类型错误

let error = year + au

Error: This expression has type< kg : 'a * 'a; m : 'b * 'b succ; s : 'c * 'c > Unit.tbut an expression was expected of type< kg : 'a * 'a; m : 'b * 'b; s : 'd * 'd succ > Unit.tThe type variable 'b occurs inside 'b succ

然而，类型错误并不是真正可以理解的......这是使用编码的常见问题。
这种编码的另一个重要限制是我们使用类型变量的统一来进行计算。通过这样做，只要类型变量没有被泛化，我们就会在进行计算时消耗它。这会导致奇怪的错误。例如，这个功能工作正常

let strange_but_ok x y = m * x +  ((y/m) * m) * m

而这个没有类型检查

let strange_and_fail x = m * x +  ((x/m) * m) * m

幸运的是，由于我们的幻像类型参数是协变的，放宽的值限制将确保大多数时候类型变量按时泛化；并且只有在将不同维度的函数参数混合在一起时才会出现问题。
这种编码的另一个重要限制是我们仅限于单位的加法、减法、乘法和除法。例如，不可能用这种表示计算平方根。
解除这种限制的一种方法是仍然对单位使用幻像类型参数，使用类型构造函数表示加法、乘法等，并在这些类型构造函数之间添加一些公理相等。但随后用户必须手动证明同一整数的不同表示之间的等价性。