子类型概述

Introduction and Rules.

我们定义某个 static type system 的expressiveness (表达性) 为：not rejecting too many programs that do nothing wrong and programmers are likely to write。

• ML type system 的表达性来自 parametric polymorphism (参数多态)，即 generics (泛型)。
• 许多 OOP style (Java, C#) 的 type system 的表达性更多的来自于 subtype polymorphism (子类型多态)，也即我们所说的 subtyping。

我们将使用一种类 ML 的 MUPL 来介绍 subtyping；但请注意，ML 本身是不支持 subtyping 的。

我们来看一个例子：

1
2
3
4
5

fun distToOrigin(p:{x:real, y:real}) =
    Math.sqrt(p.x*p.x + p.y*p.y)

val c : {x:real, y:real, color:string} = {x=3.0, y=4.0, color="green"}
val five : real = distToOrigin(c)

该程序是一个典型的 false positive (假阳性) 程序。在不支持 subtyping 的语言中，将 c 传入 distToOrigin 方法将会产生 type error。这引出了 subtyping 的必要性：它在一定程度上令 type system 更加 complete，从而提高了其 expressiveness。(关于 type system 的分析见 Part B)

c 的类型 {x:real, y:real, color:string} 是形参 p 类型 {x:real, y:real} 的子类型，而 subtype can have any of its supertypes，所以 c 能够顺利传入 distToOrigin 方法中。

Width Subtyping

对于类型 t1 与 t2，若 t1 是 t2 的 subtype，我们标记为 t1 <: t2。那么 subtyping 可以表示为这么一条最基本的 typing tule：If e has type t1 and t1 <: t2, then e (also) has type t2.

为了进一步提升 type system 的 expressiveness，还有四条 rules；其中最重要的是对 <: 关系本身的定义。最常见的一种定义是 width subtyping，即 supertype 与 subtype 呈宽度展开关系：在 width subtyping 中，supertype 中含有的 fields 一定是 subtype 的子集。

• Width subtyping. A supertype can have a subset of fields with the same type, i.e., a subtype can have extra fields: {f1:t1,...,fm:tm,...,fn:tn} <: {f1:t1,...,fm:tm}.
• Permutation subtyping. A supertype can have the same set of fields with the same types in a different order: {y:real, x:real} <: {x:real, y:real}.
• Transitivity. If t1 <: t2 and t2 <: t3, then t1 <: t3.
• Reflexitivity. Every type is a subtype of itself: t <: t.

结合 width subtyping, permutation subtyping 与 transitivity，我们能够做到类似 {x:real, foo:string, y:real} :< {y:real, x:real} 的子类型关系，这大大提高了 type system 的 expressiveness。