墨滴
R

Rohee

V1

2022/12/10阅读：60主题：默认主题

15-Subtyping

在之前的章节中，我们已经通过简单类型的λ演算，研究了各种语言特征的类型化行为。本章将介绍一个基本类型的扩展：子类型（有时也称为子类型多态性）。与我们迄今为止所研究的特征不同，子类型或多或少可以相互正交地表达，子类型是一种横向扩展，以非平凡的方式与大多数其他语言特征相交互。

子类型是面向对象语言的特征，通常被认为是面向对象风格的基本特征。我们将在第18章详细探讨这种联系;不过，现在我们只介绍函数和records的子类型。

一、子类型概述

如果没有子类型，简单类型的lambda表达式的规则可能会非常僵化，不具灵活性。类型系统会要求参数类型与函数的域类型需要完全匹配，对于许多对程序员来说明显表现良好的程序，类型编译器反而会报错。例如，回想一下函数应用的键入规则：

(T-APP)

根据这一规则，行为良好的项

是被认为类型不匹配的，因为参数的类型是{x：Nat，y：Nat}，而函数接受的却是{x：Nat}。但是，很明显，函数只要求它的参数是一个带有字段x的records;它并不关心参数是否包含其他字段。

此外，我们还可以从函数的类型中看到一点，我们并不需要查看它的主体来验证它是否使用了除x之外的任何字段。将类型为{x：Nat，y：Nat}的参数传递给期望类型为{x：Nat}的函数总是安全的。

子类型的目标是细化类型规则，以便它们可以接受类似于上面的项。我们假设S是T的一个子类型，记作S <：T，表示任何S类型的项都可以安全地用在上下文中期望T类型的项中。这种子类型的观点常被称为安全替换原则。

更简单的解释是将S <：T读成“由S描述的每个值也由T描述”，即“S的元素是T的元素的子集”。

通过添加新的类型规则--所谓的包含规则--可以提供类型关系和该子类型关系之间的一个桥梁：

(T-SUB)

这个规则告诉我们，如果S <：T，则S的每个元素t也是T的元素。例如，如果我们定义子类型关系,使得{x：Nat，y：Nat} <：{x：Nat}，那么我们可以使用规则T-Sub来推导出{x = 0，y = 1} ：{x：Nat}。

二、子类型关系

子类型关系被形式化为S <：T，读作“S是T的一个子类型”（或“T是S的一个超类型”）。我们考虑每种类型（例如函数类型、记录类型等），对于每一种类型，我们引入一个或多个规则来规范允许在需要使用另一种类型的情况下安全地使用这种形式的一种类型的元素的情况。

在讨论特定类型构造函数的规则之前，我们先做两个一般性规定：首先，子类型应该是自反的，

(S-REFL)

第二，子类型是具有传递性的：

(S-TRANS)

这些规则直接来自于安全替换的直觉。

现在，对于records类型，假设我们想定义S={k1:S1…km:Sm}是T={t1:T1…Tn:Tn}的子类型，那么就有如下性质：即子类型的元素个数是大于等于父类的:

(S-RCDWIDTH)

看起来可能令人惊讶的是，“较小”的类型（子类型）居然是具有更多字段的类型。理解这一点最简单的方法是将records类型{x：Nat}描述为“至少有一个Nat类型的字段x的所有记录的集合”。像{x=3}和{x=5}这样的值是这种类型的元素，像{x=3，y=100}和{x=3，a=true，B=true}这样的值也是。

类似地，records类型{x：Nat，y：Nat}描述至少具有字段x和y的records，这两个字段的类型都是Nat。像{x=3，y=100}和{x=3，y=100，z=true}这样的值是此类型的成员，但{x=3}不是，{x=3，a=true，b=true}也不是。因此，属于第二类型的值的集合是属于第一类型的集合的真子集。records越长，要求越高，就定义了信息更多的规范，因此描述了一组较小的值。

宽度子类型规则仅适用于公共字段相同的records类型。只要两个records中每个对应字段的类型处于子类型关系中，允许各个字段的类型变化也是安全的。意思就是对于任意一个i，如果Si是Ti的子类型，那么，属于Si的li也将会是属于Ti的li的子类型。深度子类型规则描述了这种关系：

(S-RCDDEPTH)

下面的子类型派生将S-RcdWidth和S-RcdDepth一起使用，来显示嵌套records类型{x：{a：Nat，b：Nat}，y：{m：Nat}}是{x：{a：Nat}，y：{}}的子类型：

如果我们想使用S-RcdDepth来细化单个records字段的类型（而不是细化每个字段，就像我们在上面的示例中所做的那样），我们可以使用S-Refl来获取其他字段的子类型派生。

我们还可以结合宽度和深度，使用动词的规则,子类型化S-Trans。例如,我们可以来获得一个超类型:

对于records的子类型，我们还有一个规则，就是顺序无关性，即假如Kj:Sj是Li:Ti的一种排列，那么Kj:Sj就是Li:Ti的子类型。

(S-RCDPERM)

例如，S-RcdPerm告诉我们{c：Top，B：Bool，a：Nat}是{a：Nat，b：Bool，c：Top}的子类型，反之亦然。(这个表示子类型关系不是反对称的。）

S-RcdPerm可以与S-RcdWidth和S-Trans结合使用，以便于可以从记录类型中的任何位置删除字段，而不仅仅是在末尾。

练习：画一个衍生图，来证明{x: Nat, y: Nat, z: Nat}是{y: Nat}的一个子类型。

S-RcdWidth、S-RcdDepth、S-RcdPerm每个都体现了在使用records时的不同灵活性。为了便于讨论，将它们作为三个单独的规则提出是有益的。特别是，有些语言允许其中的一些，但不允许另一些。例如Abadi和Cardelli的对象演算（1996）的大多数变体省略了宽度子类型。然而，为了实现的目的，将它们组合成一个同时做所有三件事的单个宏规则是更方便的。这条规则将在下一章讨论。

由于我们使用的是高阶语言，所以不仅是数字和records，函数也可以作为参数传递给其他函数，因此我们还必须定义函数的子类型规则。

(S-ARROW)

注意，对于左边前提中的参数类型，子类型关系的意义是相反的（逆变），而对于结果类型，它的方向与函数类型本身的方向相同（协变）。直观感觉，如果我们有一个类型为S1->S2的函数f，那么我们知道f接受类型为S1的输入;显然，f也将接受S1的任何子类型T1的元素。f的类型也告诉我们它返回类型S2的元素;我们还可以查看属于S2的任何超类型T2的这些结果。也就是说，任何类型为S1->S2的函数f也可以被视为具有类型T1->T2。

另一种观点是，允许一个类型S1->S2的函数在一个期望另一个类型T1->T2的上下文中使用是安全的，只要在这个上下文中传递给函数的参数没有一个会让它不匹配（T1<:S1），并且它返回的结果中没有一个会使上下文不匹配（S2<:T2）的数据。

最后，定义一个类型是每个类型的超类型是很方便的。我们引入了一个新的类型常量Top，以及一个使Top成为子类型关系的最大元素的规则。

Top (S-TOP)

形式上，子类型关系是在我们给出的规则下最小闭合的关系。为了便于参考，图15-1、图15-2和图15-3概括了带有records和子类型的简单类型lambda演算的完整定义，突出了我们在本章中添加的语法形式和规则。注意，自反性和传递性规则的存在意味着子类型关系显然是一个前序;然而，由于记录置换规则，它不是偏序：存在许多不同类型对，其中每一类型是另一类型的子类型。

为了完成子类型关系的讨论，我们现在验证一下本章开头的示例。使用以下缩写以避免超出页面边缘。

Nat Rxy Nat, Nat

在此再定义一下通常的数值常量的类型规则，我们可以构造类型语句⊢ fxy : Nat的派生如下：

下图是未引入子类型时的简单类型的λ演算：

该图则是引入子类型后的λ演算：

三、子类型和类型的属性

在确定了具有子类型的lambda演算的定义之后，我们现在要做一些工作来验证它是否是有意义的，特别简单类型的lambda演算的定理在存在子类型的情况下仍然成立。

之前我门所学习的都是很正常的条件推结论格式。而子类型关系反演这部分呢，就是告诉我们，在结论满足的条件下，条件也是成立的。

3.1

我们从records子类型关系的一个关键性质开始，对在简单类型的λ演算中类型关系的反演引理进行模拟。如果我们知道某个S是一个arrow类型的子类型,子类型化反演引理告诉我们,S本身必须是一个arrow类型;此外,它告诉我们,箭头的左边必须(逆变)相关,右边必须(协变)。

3.2 引理【子类型关系的反转】

  1. 如果S :< T1->T2，并且T1 <: S1 、 S2 <: T2，那么S是S1类型到S2类型的函数，即S1->S2。

  2. 如果 , 并且 -i.e., 、对每一个 ， ,那么 有如下形式 。

3.3 引理

  1. 如果 , 那么 并且 .

  2. 如果 , 那么 并且 : 对每一个 都满足。

接下来，我们需要一个类型关系的替换引理。这个引理的陈述与简单类型的lambda演算并没有变化，并且他们的证明几乎是相同的。

3.4 引理【替换】

  1. 如果 并且 , 那么 。

保持理论的陈述和以前一样。然而，它的证明由于在几个点上进行了子类型化而变得有些复杂。

3.5 引理【保持】

  1. 如果 并且 , 那么 。

证明：类型推导的直接归纳法。大多数情况下类似的证明与简单类型的λ演算是相同的，为了证明records类型和包容引理，我们还需要引入一些新的例子。

  1. Case T-VAR:

不可能发生（变量没有求值规则）。

  1. Case

不可能发生（t已经是值）。

  1. Case -APP:

从E-App1, E-App2, and E-AppAbs，我们可以推出t->t'。

  1. Subcase E-APP1:

这个结果是根据诱导假说和T-App得出的。

  1. Subcase E-APP2:

  2. Subcase E-AppABS:

根据引理15.3.3（1），我们可以得知 ，并且 。通过 。通过上述和包容引理，我们可以得知 。

Case T-RCD: for each

左侧为records类型的唯一求值规则是E-Rcd。从这一规则的前提出发，我们可以看到对于每一个 ， 。这一结果来自归纳假说（应用于相应的假设 ）以及T-RCD。

Case T-PROJ:

可以被E-Proj和E-ProjRcd推导出来。

Subcase E-ProJ:

这一结论是由诱导假说和T-Proj推导出来的。

Subcase E-PROJRCD:

根据引理15.3.3（2），我们得知 并且 对每个 . In 总的来说就是, 。

Case -Sub:

由归纳假说， S。通过 T-SUB, 。

为了证明类型良好的术语不会被卡住，我们从标准型引理开始，它会告诉我们属于函数和records类型的值的可能样子。

3.6 引理【标准形式】

  1. 如果 是一个 类型的固定值, 那么 用有如下形式： 。

  2. 如果 是类型 的固定值, 那么 拥有如下形式 , 。

进展定理及其证明非常接近于我们在简单类型lambda演算中看到的。处理子类型的大部分负担已经被推到了规范形式引理中，这里只需要做一些小的修改。

3.7 定理【进展】

如果 是一个固定的，类型良好的项, 那么 要么是一个值，要么有一个 ， 。

证明：通过类型推导的直接归纳法。变量case不能出现（因为t是封闭的）。λ抽象的情况是直接的，因为抽象是值。剩下的案例更有趣。

Case T-App:

根据归纳假设， 要么是一个值，要么可以进行一步评价; 也是如此。如果 可以进行进一步操作，则规则E-App1将会应用于t。如果 是一个值，并且 可以进行进一步操作，则应用规则E-App2。最后，如果 和 都是值，则规范型引理 (15.3.6) 告诉我们 拥有 的形式, 因此规则 -APPABS 适用于 。

Case T-RcD: for each

通过归纳假设，每个 要么已经是一个值，要么可以进行一步评估。如果它们都是值，那么t是值。另一方面，如果至少有一个可以继续往下操作，那么规则E-Rcd就适用于t。

Case T-ProJ:

通过归纳假设，每个 要么已经是一个值，要么可以进行一步评估。如果 可以进行一步评估，那么（由E-Proj）t也可以。如果 是一个值, 那么由标准形引理 (15.3.6), 拥有 的形式, 并且 , 对每个 ， 。 尤其, 是在 的 标签内, 根据该规则E-ProjRcd告诉我们测试本身可以采取评估步骤。

Case -Sub:

这个结果直接来自归纳假说。

四、Top和Bottom类型

Top不是具有子类型的简单类型λ演算的必要部分;可以在不损害系统性能的情况下将其除去。但是，出于许多原因，大多数语言都包含了Top。首先，它对应于大多数面向对象语言中的Object类型。第二，Top是一个方便的技术设备，在更复杂的系统中结合了子分型和参数多态性。例如，在系统 （第26章和第28章），Top的存在允许我们从有界量化中恢复普通的无界量化，简化了系统。实际上，在系统 中，records也可以被编码，这样进一步简化演示文稿（至少为了正式学习的目的），该编码关键地依赖于Top。最后，由于Top的行为是直接的，并且在示例中经常是有用的，所以没有什么理由不保留它。

我们很自然地会问，我们是否也可以用一个最小的元素来完成子类型关系呢？因此我们就定义了一个Bot，它是每个类型的子类型。

Bot

Bot <: T

首先要注意的是Bot是空的，没有Bot类型的封闭值。如果有的话，就说v，那么包含规则加上S-Bot将允许我们导出 v : Top Tор，由此，规范型引理（15.3.6，在推广下仍然成立）告诉我们，对于某些S1和t2，v必须具有形式 。另一方面，通过包含，我们同样可以得到 ,由此规范形式引理告诉我们v一定是records类型。但我们又规定了v不能同时既是函数又是records，因此假设 : Bot把我们引向了一个矛盾。

Bot的空虚并不使它无用。相反地，Bot提供了一种非常方便的方式来表示某些操作（特别是引发异常或调用延续）不打算返回的情况。为此类表达式指定Bot类型具有两个良好的效果：首先，它向程序员发出信号，表示不期望有结果（因为如果表达式确实返回了结果，它将是Bot类型的值）;其次，它向类型检查器发出信号，表明这样的表达式可以安全地用于期望任何类型值的上下文中。例如，如果第14章中的异常引发术语error被指定为Bot类型，则：

.

if check that is reasonable then

compute result>

else

error

可以被很好的定义，因为无论正规结果的类型是什么，通过包含，项error总是可以被赋予相同的类型，因此if的两个分支是兼容的。

不幸的是，Bot的存在使为系统构建类型检查器的问题变得非常复杂。对于具有子类型的语言，一个简单的类型检查算法需要依赖于这样的推论：“如果应用程序 是良好类型的，那么 必须具有arrow类型。”在存在Bot的情况下，我们必须将其改进为“如果 是良好类型化的，则 必须具有arrow类型或Bot类型”,这一点将在16.4节中进行扩展。

这些复杂性表明添加Bot比添加Top更重要。

五、子类型及其他功能

当我们用子类型将简单的演算扩展为成熟的编程语言时，必须仔细检查每个新功能，以了解它如何与子类型化交互。在本节中,我们将考虑我们看到的一些特性。后面的章节将讨论子类型化和特性之间的交互作用，比如参数多态（第26和28章）、递归类型（第20和21章）和类型运算符（第31章）。

5.1 归属和转换

在11.4节中，我们引入了归属运算符t as T，作为一种检查文档的形式，允许程序员在程序文本中记录断言，即复杂表达式的某个子项具有某种特定类型。在我们所举的例子中，属性也被用来控制类型的打印方式，迫使类型检查器使用更可读的缩写形式，而不是它实际计算的类型。

在Java和C++等具有子类型的语言中，归属变得更加有趣。在这些语言中，它通常被称为强制转换，并被写成（T）t。实际上有两种完全不同的强制转换形式：被称为向上强制转换和向下强制转换。前者直截了当，后者涉及动态类型测试。

向上转换是标准归属运算符的实例，在向上转换中，术语被赋予类型检查器自然分配给它的类型的超类型。我们给出一个项t和一个类型T，我们打算在它上面“看”t。类型检查器通过尝试使用t的“自然”类型、包含规则T-Sub和11.4中的归属规则来构建一个派生来验证T确实是t的类型之一：

as

(T-Ascribe)

向上转换可以被看作是一种抽象形式，是一种隐藏值的某些部分的存在的方式，这样它们就不能在周围的上下文中使用。例如，如果t是一个records（或者更一般地说，是一个对象），那么我们可以使用上转换来隐藏它的一些字段（方法）。

另一方面，向下转换允许我们将类型赋值给类型检查器不能静态派生的项。为了允许向下强制类型转换，我们对as输入规则做了一个有点令人惊讶的更改：

(T-Downcast)

也就是说，我们检查 是否是类型良好的（即，它是类型S），然后指定它为类型T，而S和T之间不做任何的要求。例如，我们可以写一个函数f，它接受任何参数，将其向下转换为一个records，该记录的a字段包含一个数字，然后返回这个数字：

Top as

当然,盲目信任这样的断言将产生灾难性的影响。如果程序员犯了个错,f适用于不包含任何字段的records,结果可能(取决于编译器的细节)是完全任意的!相反，我们的座右铭应该是“信任，但要核实”。在编译时，类型检查器只接受向下转换中给定的类型。

as (E-Ascribe)

(E-Downcast)

例如，如果我们将上面的函数f应用于参数{a=5，b=true}，那么这个规则将（成功地）检查出{a=5，b=true}：{a：Nat}。另一方面，如果我们将f应用于{b=true}，则E-Downcast规则将不适用，并且求值将在这一点上停滞。

当然，我们会失去进度，因为一个类型良好的程序肯定会因为试图计算一个坏的向下转换而被卡住。提供向下转换的语言通常会以下列两种方式之一来解决这个问题：通过使失败的向下强制转换引发可由程序捕获和处理的动态异常，或者用动态类型测试的形式替换向下转换操作符：

(T-TYPETEST)