深度子类型

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 域。

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

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