OCaml，`type `!+'at` 中 `!+` 的含义

Question

我目前正在学习 OCaml，尤其是函子。map.mli我从标准库中查看，在第 70 行左右，有：

type key
(** The type of the map keys. *)

type !+'a t
(** The type of maps from type [key] to type ['a]. *)

val empty: 'a t
(** The empty map. *)

我知道这key是映射中使用的密钥的类型（或者更确切地说是它的签名，因为我们在文件中.mli），并且'a t是映射本身的（多态/抽象）类型。不过我想知道!+有什么用。我尝试寻找一些有关它的文档，但不幸的是没有找到任何文档。

如果可能的话，我希望得到有关此问题的解释和/或相关文档/教程的链接。

提前致谢。

Answer 1

变体和单射性注释返回有关抽象类型构造函数type 'a t及其参数之间关系的一些信息。例如，类型构造函数可以

• 产生或包含'a：

type 'a t = 'a * 'a

• 消耗一个'a

type 'a t = 'a -> unit

• 忽略它的论点：

type 'a t = int

• 包含对 'a 的可见且可变的引用

type 'a t = { get: unit -> 'a; store: 'a -> unit }

所有这些类型构造函数都可以通过签名进行抽象：

module Any: sig
  type 'a t
end = struct
   type 'a t = 'a * 'a
end 

在这种抽象程度下，我们最终对'a t外部世界一无所知。然而，有时了解一点比什么都不知道还是有用的。例如，如果我有一个生产者类型构造函数'a t，例如

type 'a t = 'a * 'a

，以及通过子类型关系相关的两种类型，比如说type x = < x:int >和type xy = <x:int; y:int >t。我可以从中推断出xy <: x，xy t <: y t因为可以假装存储的对象比实际生成的对象具有更少的方法。由于从to<:开始保留 关系的顺序，因此我们说类型构造函数在其类型参数中是协变的。我可以通过添加方差注释来揭示类型构造函数在接口中是协变的事实：xy :> xxy t :> x tt

type xy = <x:int; y:int>
type x = < x:int >

module Covariant: sig
  type +'a t
  val xy: xy t
end = struct
  type +'a t = 'a * 'a
  let xy = let c = object method x = 0 method y = 1 end in c, c
end

let xy = (Covariant.xy: xy Covariant.t :> x Covariant.t)

x以双重方式，例如，如果我有一个使用方法消耗对象的类型

type 'a t = 'a -> int
let x: x t = fun arg -> arg#x

假装它实际上需要更多方法是可以的。换句话说，我可以强制 ax t反转从到 的xy t 关系。我可以通过逆变注释公开这些信息xy:>xx t :> xy t

module Contravariant: sig
  type -'a t
  val x: x t
end = struct
  type -'a t = 'a -> int
  let x c = c#x
end

let xy = (Contravariant.x: x Contravariant.t :> xy Contravariant.t)

使用+和-表示逆变反映了以下规则：乘以正数保留普通顺序x < y意味着，2 x <2 y而乘以负数则反转顺序： x < y意味着 -2 y < -2x。

因此，方差注释允许我们公开类型构造函数t在子类型方面的行为方式。对于具体类型定义，类型检查器将自行推断方差，无需执行任何操作。然而，对于抽象类型构造函数，作者的角色是公开（或不公开）方差信息。

在处理对象、多态变体或私有类型时，此差异信息非常有用。但人们可能想知道这在 OCaml 中是否很重要，因为对象的使用并不多。事实上，协方差注释的主要用途是依赖于多态性和值限制。

值限制是多态性和可变性之间破坏性干扰的结果。最简单的例子是一个函数，它生成一对函数来存储或从引用中获取一些值

type 'a t = { get: unit -> 'a; store: 'a -> unit }
let init () =
  let st = ref None in
  let store x = st := Some x in
  let get () = match !st with None -> raise Not_found | Some x -> x
  in
  {store; get}

通常，我可以这样使用：

let st = init ()
let () = st.store 0
let y = st.get ()

st但是，上一个示例的第一行的类型是什么。的类型 init是unit -> 'a t因为我可以在生成的引用中存储任何类型的值。但是，具体值的类型st不能是多态的，因为我不应该能够存储整数并检索函数，例如：

let wrong = st.get () 0

因此， 的类型st是弱多态类型：'_weak1 t'其中'_weak1是只能替换一次的具体类型的占位符。st因此，在第 2 行，我们得知 的类型，'weak1=int并且 的类型t更新为int t。这就是起作用的值限制，它告诉我们我们不能一般地推断计算结果是多态的。然而，这个问题之所以出现，是因为使用存储，我们可以读取和写入类型的值'a。如果我们只能读取（或生成）类型的值'a，则可以概括由计算生成的多态值。例如，在这个例子中，

let gen_none () = None
let none = gen_None () 

令人惊讶的是， 的推断类型none是完全多态类型'a option'。事实上，选项类型'a option是不可变的容器类型，只能产生类型的值'a。因此，可以将计算类型概括 none为 from '_weak1 optionto 'a option。在这里，我们再次遇到方差注释：作为只能生成 an 的容器类型'a是描述协变类型参数的一种方法。并且可以更普遍地证明，如果类型变量仅出现在协变位置，则概括该计算的类型总是可以的。这是放宽的值限制。

然而，发生这种情况是因为对于协变类型构造函数'a t'，产生多态值的唯一可能方法是拥有某种空容器。使用 OCaml 类型系统检查这一点非常有趣：

type 'a maybe = Nothing | Just of 'a
type empty = |
type poly_maybe = { x: 'a. 'a maybe}
let a_polymorphic_maybe_is_nothing {x} = match (x:empty maybe) with
| Nothing -> ()
| _ -> .

总而言之，它们对于容器库非常有用，让用户能够

• 将整个容器强制转换为子类型，无需运行时成本
• 计算多态“空”值

单射性的用例要微妙得多。简而言之，它们仅在检查存在 GADT 的某些模式匹配的详尽性时才重要（这解释了为什么它们仅在 OCaml 4.12 中引入）。

事实上，如果方差注释涉及子类型关系的保留，那么单射性注释则涉及不等式的保留。想象一下我有两种可区分的类型，例如int和float。我总能区分int tor 吗float t？如果我看一下总和类型

type !'a sum = A

或记录

type !'a product = { x: 'a}

答案总是肯定的。换句话说，如果我 有 'a != 'b和。这种不平等的保留称为单射性。我可以添加单射性注释来检查类型检查器是否与我一致（如方差注释，单射性注释是针对具体类型定义推断的）。'a sum != 'b sum'a product !='b product

但是，如果类型参数实际上是幻像类型参数，

type 'a t = float

那么我不能保证 int t != float t（因为_ t总是 a float）。对于带有幻像参数的类型构造函数的示例，我可以定义一种带有单位的浮点数类型

type m = M
type s = S

module SI: sig
  type 'a t
  val m: m t
  val s: s t
end = struct
  type 'a t = float
  let m = 1.
  let s = 1.
end

这里，类型'a SI.t表示具有在类型中编码的单位的实数。因此，在这个例子中，我有单射类型和非单射类型。单射性什么时候很重要？答案是，为了使单射性变得重要，我需要处理显式类型方程。显式类型方程是 GADT 的领域。GADT 的精髓确实是平等见证的证明

type ('a,'b) eq = Refl: ('a,'a) eq
let conv (type a b) (Refl: (a,b) eq) (x:a) = (x:b) 

eq具有type 的值('a,'b) t证明两种类型相等。m SI.t例如，我可以使用这种类型来导出和s SI.t秘密地是同一类型的事实

module SI: sig
  type 'a t
  val m: m t
  val s: s t
  val magic: (s t, m t) eq
end = struct
  type 'a t = float
  let m = 1.
  let s = 1.
  let magic = Refl
end

然后我可以使用这个秘密相等将秒转换为米（这很糟糕）

let wrong_conversion (x:s SI.t) : m SI.t = 
  conv SI.magic x

因此，我可以使用 GADT 来揭示类型构造函数不是单射的这一事实。同样，我可以使用单射性注释来证明单射性的另一个等效定义：如果'a t = 'b t和t在其第一个参数中是单射的，那么'a = 'b：

module Inj(T: sig type !'a t end) = struct
  open T
  let conv (type a b) (Refl: (a t, b t) eq): (a,b) eq = Refl
end

所有这些都相当理论化，但单射性问题出现在更实际的问题上。想象一下我有一个容器类型vec

module Vec: sig
  type 'a t
  val v2: 'a -> 'a -> 'a t
end = struct
  type 'a t = 'a * 'a
  let v2 x y = x, y
end
type 'a vec = 'a Vec.t

（请注意现在缺少的单射性注释）使用 GADT，我可以定义与 或 一起使用的函数，int vec或者float vec通过定义正确的 GADT

type 'a monoid =
  | Int_vec: int vec monoid
  | Float_vec: float vec monoid 

例如，我可以zero通过 monoid 定义一个函数 monoid：

let zero (type a) (kind:a monoid): a = match kind with
| Int_vec -> Vec.v2 0 0
| Float_vec -> Vec.v2 0. 0.

这按预期工作。一旦我想定义一个仅适用于可能的幺半群之一的函数，麻烦就开始了。例如，只有整数向量具有有限数量的半径为 1 的元素

let unit_circle (monoid:int vec monoid) = match monoid with
| Int_vec -> Vec.[v2 1 0; v2 (-1) 0; v2 0 1; v2 0 (-1)]

但随后，我们收到了意想不到的警告：

警告 8 [部分匹配]：此模式匹配并不详尽。以下是不匹配的情况示例：Float_vec

乍一看，此警告可能看起来很奇怪Float_vechas type float vec monoid，它与 type 不匹配int vec monoid，并试图unit_circle应用于Float_vec 产量

let error = unit_circle Float_vec

错误：此表达式的类型为 float vec monoid，但表达式应为 int vec monoid 类型 float 类型与 int 类型不兼容

因此类型检查器知道 afloat vec与 an 不兼容int vec。为什么它会警告我们模式匹配案例中缺少案例？这个问题是一个上下文问题：在分析模式匹配的详尽性时，类型检查器发现该类型'a vec不是单射的，因此它不能假设周围没有一些隐藏的方程来证明事实上 afloat vec与一个int vec。相反，在应用程序案例中，类型检查器知道当前上下文中不存在这样的方程，因此它应该拒绝该应用程序（即使在某处存在这样的方程）。

因此，在我们的例子中，简单的解决方案是添加缺失的单射性注释（我们也可以添加缺失的方差）

module Vec: sig
  type +!'a t
  val v2: 'a -> 'a -> 'a t
end = struct
  type 'a t = 'a * 'a
  let v2 x y = x, y
end
type 'a vec = 'a Vec.t
type 'a monoid =
  | Int_vec: int vec monoid
  | Float_vec: float vec monoid 

由于缺少这条信息，类型检查器可以得出结论： anint vec始终与 a 不同float vec，因此我们不再收到警告

let unit_circle (monoid:int vec monoid) = match monoid with
| Int_vec -> Vec.[v2 1 0; v2 (-1) 0; v2 0 1; v2 0 (-1)]
| _ -> .

事实上，由于'a vec是单射，我们知道我们可以int vec != float vec从不等式中 推出int != float

总而言之，单射性注释是库让用户知道即使类型构造函数是抽象的它也保留不等式的一种方式。这是一条很小的信息，不会泄露太多信息。同时，它仅对通过使用 GADT 显式操作类型方程的客户端有用。