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 | 'B) array作为一个'A array.是的,这会很奇怪,因为我的数组可以包含'B但奇怪的是我认为它与函数相同.也许,最后,我并不理解一切,但我想在这里提出我的想法,因为我花了很长时间才理解它.

TL; DR:

持久性: +'a

功能 : -'a

mutable:invariant('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是不变的.