OCaml, `type `!+'a t` 中 `!+` 的含义
OCaml, meaning of `!+` in `type `!+'a t`
我目前正在学习 OCaml，尤其是函子。我从标准库中查看了map.mli，在line 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 是(polymorphic/abstract) 地图本身的类型。但是我想知道 !+ 有什么用。我试着寻找一些关于它的文档，但不幸的是没有找到。
如果可能的话，and/or link 相关的 documentation/tutorial，我将不胜感激。
提前致谢。
变体和单射性注释返回一些关于抽象类型构造函数 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 因为假装存储对象的方法比实际生成的方法少是可以的。由于关系 <: 的顺序保留自
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 而乘以 a负数倒序：
x < y 意味着 -2 y < -2x.
因此，方差注释使我们能够揭示类型构造函数 t 在子类型方面的行为方式。
对于具体的类型定义，类型检查器将自行推断差异，无需执行任何操作。
但是，对于抽象类型构造函数，作者的职责是暴露（或不暴露）方差信息。
这种差异信息在处理对象、多态变体或私有类型时很有用。但是人们可能想知道这在 OCaml 中是否很重要，因为对象的使用不多。事实上，协方差注释的主要用途依赖于多态性和值限制。
值限制是多态性和可变性之间破坏性干扰的结果。
最简单的例子是一个函数，它生成一对函数来存储或从中获取一些值
一个参考[=125=]
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 的值。
因此可以概括计算的类型 none 是从 '_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 -> ()
| _ -> .
总而言之，它们对容器库很有用，可以让用户能够
- 将整个容器强制转换为无运行时成本的子类型
- 计算多态“空”值
内射性的用例要微妙得多。简而言之，它们仅在检查存在 GADT 的某些模式匹配的详尽性时才重要（这解释了为什么它们仅在 OCaml 4.12 中引入）。
确实，如果方差注释与子类型关系的保存有关，则注入性注释
关注不平等的维持。假设我有两个可区分的类型，例如 int 和 float。我总能区分 int t 或 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总是一个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)
具有类型 ('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
因此，我可以使用 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
例如，我可以通过 monoid 定义一个 zero 函数 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)]
但是，我们收到一个意想不到的警告：
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Float_vec
这个警告乍一看可能很奇怪 Float_vec 的类型是 float vec monoid，它不是
与 int vec monoid 类型匹配，并尝试将 unit_circle 应用于 Float_vec 会产生
let error = unit_circle Float_vec
Error: This expression has type float vec monoid
but an expression was expected of type int vec monoid
Type float is not compatible with type 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 vec != float vec
int != float
总结一下内射性，内射性注释是库让用户知道即使类型构造函数是抽象的，它也确实保留不等式的一种方式。这是一条很小的信息，不会泄露太多信息。同时，它仅对通过使用 GADT 显式操作方程式的客户有用。
我目前正在学习 OCaml，尤其是函子。我从标准库中查看了map.mli，在line 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 是(polymorphic/abstract) 地图本身的类型。但是我想知道 !+ 有什么用。我试着寻找一些关于它的文档，但不幸的是没有找到。
如果可能的话，and/or link 相关的 documentation/tutorial，我将不胜感激。
提前致谢。
变体和单射性注释返回一些关于抽象类型构造函数 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 因为假装存储对象的方法比实际生成的方法少是可以的。由于关系 <: 的顺序保留自
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 而乘以 a负数倒序：
x < y 意味着 -2 y < -2x.
因此，方差注释使我们能够揭示类型构造函数 t 在子类型方面的行为方式。
对于具体的类型定义，类型检查器将自行推断差异，无需执行任何操作。
但是，对于抽象类型构造函数，作者的职责是暴露（或不暴露）方差信息。
这种差异信息在处理对象、多态变体或私有类型时很有用。但是人们可能想知道这在 OCaml 中是否很重要，因为对象的使用不多。事实上，协方差注释的主要用途依赖于多态性和值限制。
值限制是多态性和可变性之间破坏性干扰的结果。 最简单的例子是一个函数，它生成一对函数来存储或从中获取一些值 一个参考[=125=]
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 的值。
因此可以概括计算的类型 none 是从 '_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 -> ()
| _ -> .
总而言之，它们对容器库很有用，可以让用户能够
- 将整个容器强制转换为无运行时成本的子类型
- 计算多态“空”值
内射性的用例要微妙得多。简而言之，它们仅在检查存在 GADT 的某些模式匹配的详尽性时才重要（这解释了为什么它们仅在 OCaml 4.12 中引入）。
确实，如果方差注释与子类型关系的保存有关，则注入性注释
关注不平等的维持。假设我有两个可区分的类型，例如 int 和 float。我总能区分 int t 或 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总是一个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)
具有类型 ('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
因此，我可以使用 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
例如，我可以通过 monoid 定义一个 zero 函数 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)]
但是，我们收到一个意想不到的警告：
Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Float_vec
这个警告乍一看可能很奇怪 Float_vec 的类型是 float vec monoid，它不是
与 int vec monoid 类型匹配，并尝试将 unit_circle 应用于 Float_vec 会产生
let error = unit_circle Float_vec
Error: This expression has type float vec monoid but an expression was expected of type int vec monoid Type float is not compatible with type 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 vec != float vec
int != float
总结一下内射性，内射性注释是库让用户知道即使类型构造函数是抽象的，它也确实保留不等式的一种方式。这是一条很小的信息，不会泄露太多信息。同时，它仅对通过使用 GADT 显式操作方程式的客户有用。