我目前正在学习OCaml，特别是functor。我查看了标准库中的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是映射本身的（多态/抽象）类型。但我想知道!+用于什么。我尝试查找相关文档，但不幸的是没有找到任何信息。type 'a t 和其参数之间关系的一些信息。例如，类型构造器可能会：
'a：type 'a t = 'a * 'a
'atype 'a t = 'a -> unit
type 'a t = int
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，因为假装存储的对象比实际生成的对象少一些方法是没问题的。由于关系 <: 的顺序从 xy :> x 到 xy t :> x t 是保留的，我们说类型构造器 t 在其类型参数上是协变的。我可以通过添加一个变异注释来暴露类型构造器是协变的事实：
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
假装需要更多的方法是可以的。换句话说，我可以将x t强制转换为xy t，从而将关系从xy:>x反转为x 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相对于子类型的行为方式。
对于具体的类型定义，类型检查器将自行推断方差，无需进行任何操作。
但是，对于抽象类型构造函数，作者有责任公开（或不公开）方差信息。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是一个占位符，表示只能替换一次的具体类型。因此，在第2行，我们可以了解到st的类型为'weak1=int'，并且t的类型更新为int t。这就是值约束在发挥作用，它告诉我们不能普遍地推断出计算结果是多态的。然而，这个问题只是因为有了存储器，我们可以读取和写入类型为'a'的值。如果我们只能读取（或生成）类型'a'的值，则可以从计算中产生泛型值。例如，在这个例子中：let gen_none () = None
let none = gen_None ()
令人惊讶的是，none 的推断类型是完全多态的类型 'a option'。事实上，选项类型 'a option 是一个不可变的容器类型，只能产生类型为 'a 的值。因此，将计算的类型从 '_weak1 option 泛化为 'a option 是可以的。这就是我们再次遇到的协变注释：作为一个只能产生 '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 -> ()
| _ -> .
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 总是一个 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表示具有编码为类型的单位的实数。
使用这个例子，我既有单射类型也有非单射类型。什么情况下需要注意单射性呢？
答案是，要使单射性成为问题，我需要处理显式类型方程。
而显式类型方程是GADTs的领域。典型的GADT确实是等式证明见证。
type ('a,'b) eq = Refl: ('a,'a) eq
let conv (type a b) (Refl: (a,b) eq) (x:a) = (x:b)
具有类型为 ('a,'b) t 的值 eq 是两种类型相等的证明。例如，我可以使用此类型来证明 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
'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
（现在注意缺少注入性注释）
使用GADTs，我可以通过定义正确的GADT来定义可以处理int vec或float vec的函数。
type 'a monoid =
| Int_vec: int vec monoid
| Float_vec: float vec monoid
zero函数幺半群：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 [partial-match]：此模式匹配不是全面的。 以下是一个未匹配的示例： Float_vec
这个警告可能看起来很奇怪，因为Float_vec的类型是float vec monoid，它与int vec monoid类型不匹配，并且尝试将unit_circle应用于Float_vec会导致
let error = unit_circle Float_vec
错误：此表达式具有float vec monoid类型，但需要的是int vec monoid类型的表达式 类型float与int不兼容
因此，类型检查器知道float vec与int vec不兼容。
为什么它会警告我们模式匹配中缺失的情况呢？
这个问题涉及到上下文：在分析穷尽性的模式匹配时，
类型检查器看到类型'a vec不是可注入的，因此它不能假设
没有一些隐藏的等式证明实际上float 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
有了这个缺失的信息，类型检查器可以得出结论：一个int vec总是与一个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 != float推导出int vec != float vec。
关于单射性的结论，单射性注释是库向其用户传达的一种方式，即使类型构造器是抽象的，它仍然保留不等式。这是非常小的信息片段，不会泄露太多信息。同时，它只对通过使用GADTs显式操纵类型方程的客户端有用。