OCaml中的“协变”与“逆变”

时间:2021-10-29 20:12:34

概略地说,子类型是类型间的一种二元关系。如果t1是t2的子类型,那么使用t2的地方就可以使用t1。在OCaml中,子类型起因于多态变体polymorphic variants)。比如,[`A ]是[ `A |`B ]的子类型,因为能处理`A或`B的代码,一定能处理`A。

你可以使用表达式 (e : t1:> t2) 强制OCaml检查子类型。这个表达式有两层含义:首先核实t1是t2的子类型,其次使整个表达式的类型为t2。

就像OCaml的类型检查器有规则决定什么时候对一个let表达式/函数调用作类型检查一样,它也有规则判定是否表达式中的子类型是允许的。对多态变体的子类型规则是清楚的:如果一个多态变体t1是另一个多态变体t2的子类型,那么t1的每个构造器(constructor)也出现在t2中,且有相同的类型参数。


OCaml将子类型规则扩展到更复杂的类型。

对元组(tuple)类型的规则是:
if t1 :> t1' and t2 :> t2' then (t1, t2) :> (t1', t2')
比如:
let f x = (x :
[`A ] * [`B ]:>[`A |`C ] * [`B |`D ])


元组的子类型规则是比较直观的。想想代码是如何处理元组的,你就明白:能处理其第一与第二组件中有较多值的元组代码,也能处理有较少值的元组。


箭头式(arrow)类型(函数)的规则是:
if ta' :> ta and tr :> tr' then ta -> tr :> ta' -> tr'

比如:

let f x = (x :
[`A |`B ] -> [`C ]:>[`A ] -> [`C |`D ])

同样,想想代码是如何使用函数的,你就明白:如果代码能使用一个有较少输入和较多输出的函数,那么它也能使用一个有较多的输入和较少输出的函数。


在OCaml中,你可以使用称为变体注释(variance annotations)的“+”与“-”来声明其子类型的本质:通过组件类型的子类型方向去推导复合类型的子类型方向对于元组与函数类型,你可以写成:

type (+'a, +'b) t = 'a * 'b
type (-'a, +'b) t = 'a -> 'b


用“+”注释的类型变量是协变的(covariant),用“-”注释的类型变量是逆变的(contravariant)。比如,元组类型的所有参数是协变的;函数类型的第一个参数是逆变的,第二个参数是协变的


如果你没有写“+”与“-”,OCaml将自动推导它们。那究竟为什么还需要写“+”与“-”呢?因为模块接口设计用来表达实现者与用户之间的合同,类型变化将影响使用该类型的程序是否类型正确。比如,假设你有如下模块:

module M :sig
    type ('a, 'b) t
end = struct
    type ('a, 'b) t = 'a * 'b
end

那么如下代码能通过类型检查吗?

let f x = (x : ([ `A ], [ `B ]) M.t :> ([ `A | `C ], [ `B | `D ]) M.t)


如果你知道('a, 'b) M.t = 'a * 'b ,那么上面代码能通过类型检查(因为元组类型是协变的)。但是,用户仅仅知道接口说了什么,并不知道它的实现一定是('a, 'b) M.t = 'a * 'b,所以上面代码不能通过类型检查。


变体注释允许你揭露接口中类型的子类型内容。比如:
module M : sig
   
type (+'a,+'b) t
end = struct
    type ('a, 'b) t = 'a * 'b
end

这样,对于子类型,OCaml的类型检查器将获得足够信息去检查M.t的使用。因此如下代码将通过类型检查:
let f x = (x : ([`A ], [`B ]) M.t :> ([`A | `C ], [`B |`D ]) M.t)


当你在接口中使用变体注释时,OCaml将同平时一样检查实现是否匹配接口。比如,下面代码将不能通过类型检查(因为函数的第一个参数是逆变的,而接口要求其为协变):

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

反之,下面的代码将通过类型检查:

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


在某些地方,没有变体注释的抽象类型将导致意外的非一般化(non-generalized)的变量。比如:

module M :sig
    type
'a t                     (* 没有“+”*)
    val embed : 'a -> 'a t
end = struct
    type 'a t = 'a
    let embed x = x
end

在toplevel中试试:
# [];;
- : 'a list = []           (* 任何类型的列表 *)
# M.embed [];;
- : '_a list M.t = <abstr> (* 注意"_", 嵌入的空列表已是单态(monomorphism)的了 *)


修改模块接口试试:

module M :sig
    type +'a t                      (* 有“+”*)
    val embed : 'a -> 'a t
end = struct
    type 'a t = 'a
    let embed x = x
end


# M.embed [];;
- : 'a list M.t = <abstr>  (* 没有"_", 嵌入的空列表还是多态(polymorphism)的 *)