Programming Languages, UW, Part C - Subtyping

Posted on 繁/简： set

我们定义某个 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 的。


  This article is a self-administered course note.

  It will NOT cover any exam or assignment related content.


Introduction and Rules

Letting an expression that has one type also have another type that has less information is the idea of 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。


Depth Subtyping: A Bad Idea With Mutation

在使用 subtyping 时，最常见的错误如下：

1
2
3
4
5
fun circleY (c:{center:{x:real, y:real}, r:real}) = 
    c.center.y

val sphere:{center:{x:real, y:real, z:real}, r:real} = {center={x=3.0, y=4.0, z=5.0}, r=1.0}
val _ = circleY(sphere)

circleY 方法返回传入圆的圆心的 y 坐标。自然的，对于一个球 sphere，我们可能会认为其可以作为圆 circle 的子类型传入 circleY 方法，并成功得到球心的 y 坐标。

实际上，circle 类型与 sphere 类型之间的关系并不遵循 width subtyping 规则：circle 类型的 fields 并不是 sphere 类型的子集，因此该程序将无法 type check。但抛开圆与球类型继承上的逻辑问题，该程序本质上是 false positive 的：它在运行时并不会出现 field missing 的错误。

为了进一步提升 type system 的 expressiveness，不妨再添加一条 subtyping rule，称为 depth subtyping:

  • Depth subtyping: If ta <: tb, then {f1:t1,...,f:ta,...,fn:tn} <: {f1:t1,...,f:tb,...,fn:tn}.

在该规则下，以上的程序就能 type-check 了。

遗憾的是，depth subtyping 这一规则会破坏我们的 type system；一些 false negative 的程序将通过 type check。这也是程序员常犯的错误之一：认为 depth subtyping 是被允许的。见下例：

1
2
3
4
5
6
fun setToOrigin (c:{center:{x:real, y:real}, r:real}) =
    c.center = {x=0.0, y=0.0}

val sphere:{center:{x:real, y:real, z:real}, r:real} = {center={x=3.0, y=4.0, z=0.0}, r=1.0}
val _ = setToOrigin(sphere)
val _ = sphere.center.z

在允许 depth subtyping 的语言中，该程序能通过 type check。但在运行时，最后一行 sphere.center.z 将出现 field missing 错误；这是由于 setToOrigin 方法 mutate 其参数，使得 center 失去了 z 域。

In a language with records (or objects) with getters and setters for fields, depth subtyping is unsound, i.e., you cannot have a different type for a field in the subtype and the supertype.

对于一个支持 subtyping 的语言，以下三个 features 最多只能同时做到其中两个：

  • Fields of objects are settable (i.e., immutable).
  • Supporting depth subtyping.
  • Having a type system actually prevent field-missing errors.


Array Subtyping

我们来看一段 Java 代码，其在 Java 中是 type check 的。

1
2
3
4
5
6
7
8
9
10
11
12
13
class Point { ... }    // has fields double x, y
class ColorPoint extends Point { ... } // adds field String color

void m1(Point[] pt_arr) {
    pt_arr[0] = new Point(3, 4);
}

String m2(int x) {
    ColorPoint[] cpt_arr = new ColorPoint[x];
    for (int i = 0; i < x; ++i)
        cpt_arr[i] = new ColorPoint(0, 0, "green");
    m1(cpt_arr);
}

这样的操作称为 array subtyping：即 If ta <: tb, then ta[] <: tb[]。它本质上就是 depth subtyping。根据上文中我们总结的规律，Java 支持三个 features 中的两个：

  • Array subtyping.
  • Array indices are mutable.

那么 Java 的 type system 就无法阻止某些程序的 field-missing 错误。事实确实如此，上述程序能够通过 Java 的 type check。为了解决这个问题，Java 引入了 run-time checks。

Java use run-time checks to maintain the invariant that an object of type t[] always holds objects that have type t or a subtype, but not a supertype.

于是当程序运行到 pt_arr[0] = new Point(3, 4) 这一语句时，Java 的 run-time check 会发现 ColorPoint[] 类的数组存储了其 supertype Point 类的对象，于是 ArrayStoreException 错误将被抛出。

Java 与 C# 以加入 run-time checks 的代价换取了 depth subtyping，这是因为 depth subtyping 自有其意义：它的确提升了语言的灵活性 (flexibility) 与 type system 的 expressiveness。

除了利用 run-time checks 之外，还有其他的方法可以达到相同的目的：

  • Bounded polymorphism. Use generics (parametric polymorphism) combined with subtyping.
  • Having support for indicating that a method will not update array elemtents, in which case depth subtyping is sound.


Function Subtyping

函数 (方法) 也拥有它的类型，因此研究函数类型间的 subtyping 关系也是很有必要的。It is just as important for understanding how to safely override methods in object-oriented languages.

When we talk about function subtyping, we are talking about using a function of one type in place of a function of another type.

我们以 higher-order function 为例研究函数类型间的 subtyping 关系：distMoved function computes the distance between the two-dimensional point p and the result of calling f with p.

1
2
3
4
5
6
7
8
9
fun distMoved (f : {x:real,y:real}->{x:real,y:real},
               p : {x:real,y:real}) = 
    let val p2 : {x:real,y:real} = f p
        val dx : real = p2.x - p.x
        val dy : real = p2.y - p.y
    in Math.sqrt(dx*dx + dy*dy) end
    
fun flip p = {x=~p.x, y=~p.y}
val d = distMoved(flip, {x=3.0, y=4.0})

那么函数 distMoved 的类型为 (({x:real,y:real}->{x:real,y:real}) * {x:real,y:real}) -> real.

函数 flip 的类型为 {x:real, y:real} -> {x:real, y:real}，与函数 distMoved 期待的参数类型是相符的；以函数 flip 为参数调用函数 distMoved 没有用到 subtyping。

Convariant Return Type

The subtyping for the return types works covariant as for the types overall.

函数类型与其返回值类型的 subtyping 关系是 covariant (协变) 的: If ta <: tb, then t -> ta <: t -> tb.

1
2
fun flipGreen p = {x=~p.x, y=~p.y, color="green"}
val d = distMoved(flipGreen, {x=3.0, y=4.0})

如上例，flipGreen 函数作为参数传入 distMoved 函数不会产生任何问题。

  • flipGreen 函数的返回值类型为 {x:real,y:real,color:string}，是 distMoved 形参函数返回值类型 {x:real,y:real} 的 subtype。
  • 而 flipGreen 函数类型 {x:real,y:real}->{x:real,y:real,color:string} 是 distMoved 形参函数类型 {x:real,y:real}->{x:real,y:real} 的 subtype。

可以看出函数类型与其返回值类型 subtyping 的协变关系。

Contravariant Argument Type

The subtyping for argument types is the reverse of the subtyping for the types overall.

函数类型与其参数类型的 subtyping 关系是 contravariant (逆变) 的: If ta <: tb, then tb -> t <: ta -> t.

1
2
fun flipX_Y0 p = {x=~p.x, y=0}
val d = distMoved(flipX_Y0, {x=3.0, y=4.0})

如上例，flipX_Y0 函数作为参数传入 distMoved 函数不会产生任何问题。

  • flipX_Y0 函数的参数类型为 {x:real}，是 distMoved 形参函数参数类型 {x:real,y:real} 的 supertype。
  • 而 flipX_Y0 函数类型 {x:real}->{x:real,y:real} 是 distMoved 形参函数类型 {x:real,y:real}->{x:real,y:real} 的 subtype。

可以看出函数类型与其参数类型 subtype 的逆变关系。

The general rule for function subtyping is: If t3 <: t1 (argument type) and t2 <: t4 (return type), then t1->t2 <: t3->t4. This rule, combined with reflexivity lets us use contravariant arguments, covariant results, or both.

注意在 OOP 语言中，self (或 this) 是被特殊处理的，它的类型与对象的类型始终是 convariant (共变) 的。


Subtyping for OOP

在 Java 与 C# 这些 statically typed OOP 语言中存在许多容易混淆的概念，如 inheritance v.s. subtyping, class v.s. type 等，这一节将对其进行澄清。(很重要的一节！)

在之前，我们使用 ML-like MUPL 中的 record feature 来解释了 subtyping。其实对于 OOP 中的 object，我们也可以视为一个 record：An object is basically a record holding fields (which we assume here are mutable) and methods (we assume the "slots" for methods are immutable).

结合之前我们基于 record 与 higher-order function 研究的 width typing 与 function typing，我们定义 OOP 中的 subtyping 规则如下：

  • (Width typing for fields) A subtype can have extra fields.
  • (NO depth typing for fields) Because fields are mutable, a subtype cannot have a different type for a field.
  • (Width typing for methods) A subtype can have extra methods.
  • (Depth typing for methods) Because methods are immutable, a subtype can have a subtype for method, which means the method in the subtype can have contravariant argument types and a covariant result type.

虽然我们可以将 object 视为 PL 中的 record，Java 与 C# 中的 object types 与 ML-like 的 record types，function types 却有着很大的不同。

In Java and C#, we reuse class (interfaces) names as types. If there is a class Foo, then the type Foo includes in it all fields and methods inplied by the class definition (including superclasses).

Subtyping in Java and C# includes only the subtyping explicitly stated via:

  • the subclass relationship.
  • the interfaces that classes explicitly indicate they implement (including interfaces implemented by superclasses).

接下来我们介绍 OOP 中的 subclassing 规则：它比 subtyping 规则更为严格，因此可以 soundly 地阻止 field missing 与 method missing 错误。

  • A subclass can add fields but not remove them.
  • A subclass can add methods but not removed them.
  • A subclass can override a method with a covariant return type. (在 C++ 中，这条规则更为严格，重写方法地参数表与返回值地类型均不能改变)
  • A class can implement more methods than an interface requires or implement a required method with a covariant return type.

注意，classes 与 types 是两个完全不同的概念！！！

在 C# 与 Java 这种语言中，每个 class declaration 在定义 class 的同时引入同名的 type。为了方便， classes 与 types 的界限被刻意模糊了。类似的，inheritance (subclassing) 与 subtyping 的界限也变得很暧昧。

但实际上这些概念是有本质上的区别的。(高能预警，接下来的内容很精华，就不翻译了)

A class defines an object's behavior. Subclassing inherits behavior, modifying behavior via extension and override.

A type describes what fields an object has and what messages it can respond to. Subtyping is a question of substitutability and what we want to flag as a type error.


Generics v.s. Subtyping

关于 generics (parametric polymorphism) 与 subtyping polymorphism 的比较也是一个很重要的话题。

What are generics good for?

先来看看 generics (parametric polymorphism) 的两种最常见的应用。

  1. higher-order function 的复合。

    1
    val compose : ('b -> 'c) * ('a -> 'b) -> ('a -> 'c)

  2. functions that operate over collections/containers where different collections/containers can hold values of different types.

    1
    2
    3
    val length : 'a list -> int
    val map : ('a -> 'b) * 'a list -> 'b list
    val swap : ('a * 'b) -> ('b * 'a)

generic types 放松了对函数参数类型的限制，从而提高了代码的复用性。举例来说，如果没有 generics，那么对于每一对不同类型的 pair 都需要编写一个 swap 函数。

Subtyping is bad substitute for generics

在不支持 generics 的语言中，程序员有时会用 subtyping 实现 generics，但是：

  • Somewhat lame generics.
  • Doing so is like painting with a hammer instead of a paintbrush.
1
2
3
4
5
6
7
8
9
class LamePair {
    Object x;
    Object y;
    LamePair(Object _x, Object _y) { x=_x; y=_y; }
    LamePair swap() { return new LamePair(y,x); }
    ...
}

String s = (String)(new LamePair("hi", 4).y); // error caught only at run-time

这是用 subtyping 实现 generics 的一个例子：由于 Object 类型是所有类型的 supertype，任何类型的数据都能传入 LamePair 的域中。问题出在从 LamePair 中提取数据：我们只能获得一个 Object 类型的数据，因此必须使用强制类型转换 downcast 来将其转换为“原本”的类型。

downcast 将对被转换的数据类型执行 run-time checks，因此上述程序中的类型错误只有在运行时才能被侦测到；这一方面增加了动态检查的时空成本，一方面潜在降低了程序的安全性。

When you use Object and downcasts, you are essentially taking a dynamic typing approach: any object could be stored in an Object field, so it is up to programmers, without help from the type system, to keep straight what kind of data is where.

What is subtyping good for?

subtyping 的优势区间在于 allowing code to be reused with data that has extra information.

1
2
3
fun distToOrigin {x=x, y=y} = 
    Math.sqrt(x*x + y*y)
val five = distToOrigin {x=3.0, y=4.0, color="red"}

该代码在不支持 subtyping 的语言如 ML 中将不会 type check。而在支持 subtyping 的语言中，distToOrigin 函数既能作用于 Point 类的对象，又能作用于 ColorPoint 类的对象：其中 ColorPoint is data that has extra information for Point.


Bounded Polymorphism

既然 generics 与 subtyping 都有着各自的优势区间，许多 statically typed 语言 (例如 Java 与 C#) 选择同时实现这 generics 与 subtyping。同时拥有这两种 polymorphism 机制带来了：

  • Some complications. (e.g. static overloading & subtyping are more difficult to define)
  • Merits brought by generics and subtyping separately.
  • More code reuse and expressiveness with the combination of the two ideas.

generics 与 subtyping 的结合带来了 bounded polymorphism, 具体体现为 bounded generic types。

Bounded generic types allow us to say, for all types 'a that are subtype of T.

  • (generics) We use 'a multiple times to indicate where two things must have the same type.
  • (subtyping) We can treat 'a as a subtype of T, accessing whatever fields and methods we know a T has.

见下例，Point 类中定义了 distance 方法。

1
2
3
4
5
class Pt {
    double x, y;
    double distance(Pt pt) { return Math.sqrt((x-pt.x)*(x-pt.x)+(y-pt.y)*(y-pt.y)); }
    Pt(double _x, double _y) { x = _x; y = _y; }
}

接下来是一个静态函数，输入一个 point 类 list 与一个圆，返回 list 中所有在该圆内的 point。

1
2
3
4
5
6
7
static List<Pt> inCircle(List<Pt> pts, Pt center, double radius) {
    List<Pt> result = new ArrayList<Pt>();
    for (Pt pt : pts)
        if (pt.distance(center) <= radious)
            result.add(pt)
    return result;
}

对于一个 ColorPt 类型的 list，我们能否将其传入 inCircle 方法实现代码的复用？该问题我们已经讨论过。

  • 一方面，list 中的各个 entry 是 mutable 的，这意味着 depth subtyping 不成立，List<ColorPt> 并非 List<Pt> 的 subtype。
  • 另一方面，即使 List<ColorPt> 传入了 inCircle 方法，其返回的 list 类型是 List<Pt> 而不是 List<ColorPt>，我们必须用到丑陋的 downcast。

好消息是，Java 的 bounded polymorphism 使得我们能够结合 generics 与 subtyping，实现该功能：

1
2
3
4
5
6
7
static <T extends Pt> List<T> inCircle(List<T> pts, Pt center, double radius) {
    List<T> result = new ArrayList<T>();
    for (T pt : pts)
        if (pt.distance(center) <= radius)
            result.add(pt);
    return result;
}

利用 generics，我们将 T 声明为一个 generic type；利用 subtyping，我们规定该 generic type T 必须是 Pt 的 subtype。当传入 List<ColorPt> 时，T 将被指定为 ColorPt，且 ColorPt 的确是 Pt 的 subtype。

这样，我们不仅能够传入 List<ColorPt> 类型的 list，该方法也将返回相同类型的 list 而无需用到 downcast。


Reference

  This article is a self-administered course note.

  References in the article are from corresponding course materials if not specified.

Supplementry notes:

My notes in CnBlogs.

Inheritance 与 subtyping 到底有什么区别 -知乎.

Course info:

Programming Languages, Part C, University of Washington, Lecturer: Professor Dan Grossman.

-----------------------------------そして、次の曲が始まるのです。-----------------------------------