像“Type.eq”/“Typing_equal.equal”这样的平等见证是做什么用的？

相等类型

type ('a,'b) eq = Eq: ('a,'a) eq

可能是GADT（广义抽象数据类型）的典型例子。这证明某些类型在某些情况下是平等的。重要的是，该证人可以比这些类型相等的背景更持久。因此，当需要在函数或模块之间传输某些类型等式时，它很有用。

在 OCaml 中引入此类局部方程的最简单方法是使用模块系统隐藏方程：

module M: sig
  type t
  val x: t
  val eq: (t,int) eq
end = struct
  type t = int
  let x = 0
  let eq = Eq
end

在这里，在模块内部，= 的事实是微不足道的，我们可以用Mtint

let eq = Eq

然而，在模块之外，相等性已经丢失，它只能通过相等见证才能生存。 这意味着，我们仍然可以通过匹配 ：M.eqM.xintM.eq

let one =
  let Eq = M.eq in
  1 + M.x

在模块系统之外，局部方程主要出现在存在 GADT 的情况下，因此 GADT 是该类型有用的主要上下文。eq

事实上，任何 GADT 都可以替换为 。例如，如果我们使用 GADT 来定义一个紧凑数组系列，并在元素类型的函数中优化数组表示：Eq

type ('elt,'array) compact_array =
  | Int: (int, int array) compact_array
  | Float: (float, Float.Array.t) compact_array
  | Char: (char, Bytes.t) compact_array

我们可以使用这个定义 GADT 来定义适用于任何紧凑数组的通用函数：

let make (type elt array) (kind:(elt,array) compact_array) n (x:elt): array =
match kind with
| Int -> Array.make n x
| Float -> Float.Array.make n x
| Char -> Bytes.make n x

但是，在这里我们主要使用 GADT 构造函数中记录的类型相等性，我们可以对普通变体执行完全相同的事情 存储正确的构造函数：Eq

type ('a,'b) compact_array =
 | Int of ('a * 'b, int * int array) eq
 | Float of ('a * 'b, float * Float.Array.t) eq 
 | Char of ('a * 'b, char * Bytes.t) eq 


let make (type elt array) (kind:(elt,array) compact_array) n (x:elt): array =
match kind with
| Int Eq -> Array.make n x
| Float Eq -> Float.Array.make n x
| Char Eq -> Bytes.make n x

这内存效率较低，阅读起来有点困难，但这是可行的。 这种通用性意味着类型是在函数或类型之间传输相等性的好方法。 例如，对于上面的见证，我可以使用这个见证在数据结构中存储一个数组，其中包含其类型的见证：eqcompact_array

type packed = Pack: ('a,'b) compact_array * 'b -> packed
let packed_list = [
  Pack (Int, make Int 1 5);
  Pack (Float, make Float 2 3.);
  Pack (Char, make Char 10 'a')
]

然后，我可以匹配打包的见证来恢复类型。

let add_if_int x (Pack (w,a) as o ) = match w with
| Int -> Pack (w, Array.map ((+) x) a)
| _ -> o 

但是，我可能需要为每个证人使用一个功能。避免代码重复的解决方案是编写一个相等函数......返回相等类型：

let (===) (type e1 a1 e2 a2)
  (x: (e1,a1) compact_array)
  (y: (e2,a2) compact_array)
  : (e1 * a1, e2 * a2) eq option =
match x, y with
  | Int, Int -> Some Eq
  | Char, Char -> Some Eq
  | Float, Float -> Some Eq
  | _ -> None

与该模块之前一样，我们将上下文中的等式存储到可以比该上下文更持久的见证中。M

然后，每当我们想比较两个实现时，我们可以使用 .例如，我们可以首先编写一个通用函数，该函数适用于所有紧凑数组compact_array===map

let map (type elt a) (k:(elt,a) compact_array) (f: elt -> elt) (a:a) : a=
match k with
| Int -> Array.map f a
| Float -> Float.Array.map f a
| Char -> Bytes.map f a

然后，我们可以使用此函数并将函数映射到打包的紧凑数组，如果我们在运行时使用类型见证来猜测其类型：===

let map_if_compatible (type elt a) (k: (elt,a) compact_array) f (Pack(w,a) as p) =
match w === k with
| Some Eq -> Pack(w, map k f a)
| None -> p

Here, we are using the type has way to communicate potential type equalities discovered in the body of to the body of . We could have recoved the same equality by matching on and explicitly, but that would have been equivalent to inlining the definition of in . In brief, the give us a way to transport type equations between context in a composable way.eq===map_if_compatiblewk===map_if_compatibleeq

As a side-note, it is important to note that the types and GADTs types are all about local type equations. They are not more powerful than the type system, neither do they allow to generate types from runtime data. At most, they can bridge the types of runtime data with global type information by recovering local type equations between those types.eq