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

如何解决有没有办法在 OCaml 类型系统中嵌入单元处理逻辑？

这可能是不可能的，但我觉得我可能会学到一些东西，或者可能有一种截然不同的方法来处理它。

我正在编写一些包含一些物理模拟元素的代码，我可能要处理一堆不同的单元。我觉得让类型系统在这方面为我做一些工作是值得的，这样我就不能，例如，为距离增加质量或类似的东西。

那很容易：

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 中的结果。

我正在努力学习的是：

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

解决方法

可以使用正确的编码进行一些有限的类型级算术。然而，任何编码都会受到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 (for 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 到 {{ 的翻译1}}，这两个翻译的总和就是从 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

错误：这个表达式有类型 Unit.t 但预期类型为表达式 Unit.t 类型变量 'b 出现在 'b succ

然而，类型错误并不是真正可以理解的......这是使用编码的常见问题。

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

let error = year + au

而这个没有类型检查

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

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

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

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

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

如何解决有没有办法在 OCaml 类型系统中嵌入单元处理逻辑？

解决方法

相关推荐