有没有办法在 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。

我想学习的是：

1. 到底有没有办法让这个想法发挥作用？
2. 如果没有，是否有形式/理论上的原因这很难？ （仅用于我自己的教育）
3. 是否有完全不同的方法来干净地处理类型系统中的不同单元？

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

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

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

错误：这个表达式有类型 Unit.t 但表达式应为类型 Unit.t 类型变量 'b 出现在 '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

幸运的是，由于我们的幻像类型参数是协变的，因此放宽的值限制将确保大多数时候类型变量按时泛化；并且只有将不同维度的函数参数混合在一起时才会出现问题。

这种编码的另一个重要限制是我们仅限于单位的加法、减法、乘法和除法。例如，用这种表示法计算平方根是不可能的。

解除此限制的一种方法是，仍为单位使用幻像类型参数，使用类型构造函数表示加法、乘法等，并在这些类型构造函数之间添加一些公理平等。但随后用户必须手动证明同一整数的不同表示之间的等价性。