OCaml方差(+'a，-'a)和不变性
在写完这段代码之后
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，但奇怪的是，我认为它和函数是一样的。也许，最后，我并不是什么都懂，但我想把我的想法放在这里，因为我花了很长时间才理解它。
TL;DR：
持久化：
+'a
函数：-'a
可变:不变('a)？为什么我不能强制它为-'a ?
回答 2
Stack Overflow用户
发布于 2016-11-09 23:47:27
我认为最简单的解释是可变值有两个内部操作: getter和setter，这两个操作是使用字段访问和字段集语法表示的：
type 'a t = {mutable data : 'a}
let x = {data = 42}
(* getter *)
x.data
(* setter *)
x.data <- 56Getter具有类型'a t -> 'a，其中'a类型变量出现在右侧(因此它施加了协方差约束)，而setter具有类型变量出现在箭头左侧的'a t -> 'a -> unit类型，这施加了逆变量约束。所以，我们有一个类型，既是协变的，也是逆变的，这意味着类型变量'a是不变的。
Stack Overflow用户
发布于 2016-11-10 00:10:31
您的类型t基本上允许两个操作:获取和设置。非正式地，and的类型为'a t -> 'a list，setting的类型为'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是不变的。
https://stackoverflow.com/questions/40510195
复制相似问题