更新时间:2022-10-24 23:06
协变是在计算机科学中,描述具有父/子型别关系的多个型别通过型别构造器、构造出的多个复杂型别之间是否有父/子型别关系的用语。
许多程序设计语言的类型系统支持子类型。例如,如果Cat是Animal的子类型,那么Cat类型的表达式可用于任何出现Animal类型表达式的地方。所谓的变型(variance)是指如何根据组成类型之间的子类型关系,来确定更复杂的类型之间(例如Cat列表之于Animal列表,回传Cat的函数之于回传Animal的函数...等等)的子类型关系。当我们用类型构造出更复杂的类型,原本类型的子类型性质可能被保持、反转、或忽略───取决于类型构造器的变型性质。例如在C#中:
编程语言的设计者在制定数组、继承、泛型数据类别等的类型规则时,必须将“变型”列入考量。将类型构造器设计成是协变、逆变而非不变的,可以让更多的程序俱备良好的类型。另一方面,程序员经常觉得逆变是不直观的;如果为了避免运行时期错误而精确追踪变型,可能导致复杂的类型规则。为了保持类型系统简单同时允许有用的编程,一个编程语言可能把类型构造器视为不变的,即使它被视为可变也是安全的;或是把类型构造器视为协变的,即使这样可能会违反类型安全。
在一门程序设计语言的类型系统中,一个类型规则或者类型构造器是:
下文中将叙述这些概念如何适用于常见的类型构造器。
首先考虑数组类型构造器: 从Animal类型,可以得到Animal[](“animal数组”)。 是否可以把它当作
如果要避免类型错误,且数组支持对其元素的读、写操作,那么只有第3个选择是安全的。Animal[]并不是总能当作Cat[],因为当一个客户读取数组并期望得到一个Cat,但Animal[]中包含的可能是个Dog。所以逆变规则是不安全的。
反之,一个Cat[]也不能被当作一个Animal[]。因为总是可以把一个Dog放到Animal[]中。在协变数组,这就不能保证是安全的,因为背后的存储可以实际是Cat[]。因此协变规则也不是安全的—数组构造器应该是不变。注意,这仅是可写(mutable)数组的问题;对于不可写(只读)数组,协变规则是安全的。
这示例了一般现像。只读数据类型(源)是协变的;只写数据类型(汇/sink)是逆变的。可读可写类型应是“不变”的。
Java与C#中的协变数组
早期版本的Java与C#不包含泛型(generics,即参数化多态)。在这样的设置下,使数组为“不变”将导致许多有用的多态程序被排除。然而,如果数组类型被处理为“不变”,那么它仅能用于确切为Object[]类型的数组。对于字符串数组等就不能做重排操作了。所以,Java与C#把数组类型处理为协变。在C#中,string[]是object[]的子类型,在Java中,String[]是Object[]的子类型。这个方法的缺点是留下了运行时错误的可能,而一个更严格的类型系统本可以在编译时识别出该错误。这个方法还有损性能,因为在运行时要运行额外的类型检查。Java与C#有了泛型后,有了类型安全的编写这种多态函数。数组比较与重排可以给定参数类型,也可以强制C#方法只读方式访问一个集合,可以用界面IEnumerable
支持一等函数的语言具有函数类型,比如“一个函数期望输入一只 Cat 并返回一只 Animal(写为OCaml的Cat -> Animal或C#的Func
这些语言需要指明什么时候一个函数类型是另一个函数类型的子类型—也就是说,在一个期望某个函数类型的上下文中,什么时候可以安全地使用另一个函数类型。可以说,函数f可以安全替换函数g,如果与函数g相比,函数f接受更一般的参数类型,返回更特化的结果类型。
例如,函数类型Cat->Cat可安全用于期望Cat->Animal的地方;类似地,函数类型Animal->Animal可用于期望Cat->Animal的地方——典型地,在 Animal a=Fn(Cat(...)) 这种语境下进行调用,由于 Cat 是 Animal 的子类所以即使 Fn 接受一只 Animal 也同样是安全的。一般规则是:
S1→ S2≦ T1→ T2当T1≦ S1且S2≦ T2.
换句话说,类型构造符→对输入类型是逆变的而对输出类型是协变的。这一规则首先被Luca Cardelli正式提出。在处理高端函数时,这一规则可以应用多次。例如,可以应用这一规则两次,得到(A'→B)→B ≦ (A→B)→B 当 A'≦A。即,类型(A→B)→B在A位置是协变的。在跟踪判断为何某一类型特化不是类型安全的可能令人困扰,但是比较容易计算哪个位置是协变或逆变:一个位置是协变当且仅当在偶数个箭头的左边。
下表总结了语言有关覆写方法的规则。
这些术语来源于范畴论中函子的记法。考虑范畴 C,其中的对象是类型、其态射代表了子类关系≦(这是一个任何偏序集合可被看成范畴的例子);那么诸如函数的类型构造器接受两个类型 p 和 r 并创建一个新类型 p→r,即它把 C2中的对象映射到 C 中。通过函数类型的子类规则,这个运算逆转了第一参数上的≦顺序而在第二参数上保持该顺序,即它是一个在第一参数上逆变、而在第二参数上协变的函子。