在写完这段代码之后
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
?
发布于 2016-11-09 23:47:27
我认为最简单的解释是可变值有两个内部操作: 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
是不变的。
发布于 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
复制相似问题