19

写完这段代码后

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

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

我的意思是，我知道 an'A list可以被视为 an 的子类型，('A | 'B) list因为我的列表无法更改。函数也是一样，如果我有一个类型的函数，'A | 'B -> 'C它可以被认为是类型函数的子类型，'A -> 'C | 'D因为如果我的函数可以处理'A并且'B它只能处理'A's，如果我只返回'C's 我可以当然期望'C或'D's（但我只会得到'C's）。

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

TL;博士：

执着的 ：+'a

功能 ：-'a

可变：不变量（'a）？为什么我不能强迫它成为-'a？

4

2 回答 2

18

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

type 'a t = {mutable data : 'a}

let x = {data = 42}

(* getter *)
x.data

(* setter *)
x.data <- 56

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

于 2016-11-09T15:47:27.180 回答
6

您的类型t基本上允许两种操作：获取和设置。通俗地说，getting 有 type 'a t -> 'a list，setting 有 type 'a t -> 'a list -> unit。结合，'a出现在正面和负面的位置。

[编辑：以下是我最初写的（希望）更清晰的版本。我认为它更好，所以我删除了以前的版本。]

我会尽量让它更明确。假设sub是一个适当的子类型，super并且witness是某个类型的值，super它不是类型的值sub。现在让f : sub -> unit一些函数在 value 上失败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是不变的。

于 2016-11-09T16:10:30.927 回答