像 `Type.eq` / `Typing_equal.equal` 这样的相等见证有什么用？

Question

type (_, _) eq = Equal: ('a, 'a) eq（来源）有什么用？我已经refl在 Coq 中使用过，但还不需要像 OCaml 中那样的东西。

该类型已在即将发布的 OCaml Stdlib 版本中定义Base，并且.

我如何知道何时使用此类型，以及使用此类型的代码是什么样的？

基地文档说：

Type_equal 的目的是表示类型检查器不知道的类型相等性，否则可能是因为类型相等性取决于动态数据，或者可能是因为类型系统不够强大。

所以听起来我正在寻找类型相等性依赖于动态数据或类型系统不够强大的示例，而类型equal是有帮助的。

我发现使用了equal具有相同定义的类型，Stdlib.camlinternalFormat但不理解它

更新上面的基本文档中的引用可能不是具体eq的，并且可能与Base.Type_equal.Idiuc 更相关。

Answer 1

平等类型

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

可能是 GADT（通用抽象数据类型）的典型例子。它证明某些类型在某些情况下是平等的。重要的是，该见证人可以比这些类型平等的环境更长久。因此，当需要在函数或模块之间传输某种类型相等性时，它非常有用。

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

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

在这里，在模块内部M，t=int是微不足道的，我们可以用

let eq = Eq

然而，在模块之外，平等性已经消失，只有通过M.eq平等见证才能生存。这意味着，我们仍然可以通过匹配 来了解M.x实际上是a ：intM.eq

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

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

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

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

我们可以使用这个定义 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：

let eq = Eq

这会降低内存效率，并且难以阅读，但这是可行的。这种通用性意味着eq类型是在函数或类型之间传输相等性的好方法。例如，通过compact_array上面的见证，我可以使用此见证在数据结构中存储一个具有其类型见证的数组：

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

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

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

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

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

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

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

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

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

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

在这里，我们使用eq类型 has 方法将在 的主体中发现的潜在类型相等性传达给 的===主体map_if_compatible。我们可以通过显式匹配 onw和来恢复相同的相等性k，但这相当于内联===in的定义map_if_compatible。简而言之，它eq为我们提供了一种以可组合的方式在上下文之间传输类型方程的方法。

附带说明一下，需要注意的是，eq类型和 GADT 类型都是关于局部类型方程的。它们并不比类型系统更强大，也不允许从运行时数据生成类型。最多，它们可以通过恢复这些类型之间的局部类型方程来将运行时数据的类型与全局类型信息联系起来。