OCaml 方差 (+'a， -'a) 和不变性

Question

写完这段代码之后

module type TS = sig
  type +'a t
end
  
module T : TS = struct
  type 'a t = {info : 'a list}
end

我意识到我需要info可变的。

我写道，然后：

module type TS = sig
  type +'a t
end
  
module T : TS = struct
  type 'a t = {mutable info : 'a list}
end

但是，令人惊讶的是，

Type declarations do not match:
  type 'a t = { mutable info : 'a list; }
is not included in
  type +'a t
Their variances do not agree.

哦，我记得听说过差异。这是关于协方差和逆变的东西。我是一个勇敢的人，我会独自找到我的问题！

我

找到了这两篇有趣的文章(这里和这里(，我明白了！

我会写

module type TS = sig
  type (-'a, +'b) t
end
  
module T : TS = struct
  type ('a, 'b) t = 'a -> 'b
end

但后来我想知道。为什么可变数据类型是不变的，而不仅仅是协变的？

我的意思是，我知道'A list可以被视为('A | 'B) list的子类型，因为我的列表无法更改。对于函数也是如此，如果我有一个类型 'A | 'B -> 'C 的函数，它可以被视为类型 'A -> 'C | 'D 函数的子类型，因为如果我的函数可以处理'A并且'B它只能处理'A，如果我只返回 'C 的，我肯定可以期待'C或'D的(但我只会得到'C的(。

但是对于数组？如果我有一个'A array我不能将其视为('A | 'B) array因为如果我修改数组中的元素放置'B那么我的数组类型是错误的，因为它确实是一个('A | 'B) array而不是一个'A array了。但是作为'A array的('A | 'B) array呢.是的，这会很奇怪，因为我的数组可以包含'B但奇怪的是我认为它与函数相同。也许，最后，我并没有理解所有内容，但我想把我的想法放在这里，因为我花了很长时间才理解它。

博士 ：

持久 ： +'a

功能 ： -'a

可变：不变('a( ？为什么我不能强迫它-'a？

Answer 1

我认为最简单的解释是可变值有两个内在操作：getter 和 setter，它们使用字段访问和字段集语法表示：

type 'a t = {mutable data : 'a}
let x = {data = 42}
(* getter *)
x.data
(* setter *)
x.data <- 56

Getter 有一个类型'a t -> 'a，其中'a类型变量出现在

右侧(因此它施加了协方差约束(，而 setter 具有类型 'a t -> 'a -> unit，其中类型变量出现在箭头的左侧，这施加了逆变约束。因此，我们有一个既是协变又是逆变的类型，这意味着类型变量'a是不变量的。

Answer 2

你的类型t基本上允许两个操作：获取和设置。非正式地，获取具有类型 'a t -> 'a list，设置具有类型 'a t -> 'a list -> unit 。综合起来，'a既发生在正位置，也发生在消极位置。

[编辑：以下是我最初所写内容的(希望(更清晰的版本。我认为它更优越，所以我删除了以前的版本。

我将尝试使其更明确。假设 sub 是 super 的正确子类型，witness 是 super 类型的某个值，它不是 sub 类型的值。现在f : sub -> unit让我们成为某个在值witness上失败的函数。类型安全是为了确保witness永远不会传递给f。我将通过示例来说明，如果允许将sub t视为super t的子类型，或者相反，则类型安全将失败。

let v_super = ({ info = [witness]; } : super t) in
let v_sub = ( v_super : sub t ) in   (* Suppose this was allowed. *)
List.map f v_sub.info   (* Equivalent to f witness. Woops. *)

因此，不允许将super t视为sub t的亚型。这显示了您已经知道的协方差。现在是逆变。

let v_sub = ({ info = []; } : sub t) in
let v_super = ( v_sub : super t ) in  (* Suppose this was allowed. *)
v_super.info <- [witness];
   (* As v_sub and v_super are the same thing,
      we have v_sub.info=[witness] once more. *)
List.map f v_sub.info   (* Woops again. *)

因此，也不能允许将sub t视为super t的亚型，显示出逆变。总之，'a t是不变的。