第10章子定型

1、第第10章章 子定型子定型 子定型是类型上的一种关系，该关系隐含一子定型是类型上的一种关系，该关系隐含一个类型的值可以代替另一个类型的值个类型的值可以代替另一个类型的值 和子定型有关的语言概念是记录、对象及依和子定型有关的语言概念是记录、对象及依赖于子类型关系的各种多态性赖于子类型关系的各种多态性 本章考虑子定型和体现子定型在程序设计中本章考虑子定型和体现子定型在程序设计中作用的一些语言概念作用的一些语言概念第第10章章 子定型子定型本章的主要内容本章的主要内容 带记录和子定型的简单类型化带记录和子定型的简单类型化 演算演算 等式理论和语义模型等式理论和语义模型 递归类型的子定型和递归记录作为

2、对象的模递归类型的子定型和递归记录作为对象的模型型10.1 引引 言言 子定型出现在许多程序设计语言中子定型出现在许多程序设计语言中 Fortran语言语言 整型和实型（浮点）表达式混合写出整型和实型（浮点）表达式混合写出 整数到实数的转换有一些典型的子定型性质整数到实数的转换有一些典型的子定型性质 Pascal语言语言 子界子界1.10是整数的子区间是整数的子区间 类型化面向对象语言类型化面向对象语言 子类型的对象可以用来代替任何超类型的对象子类型的对象可以用来代替任何超类型的对象10.1 引引 言言 包容包容 在大在大多数类型化程序设计语言中，一个原则是：多数类型化程序设计语言中，一个原则

3、是：当两个类型相等时，若表达式属其中一个类型，当两个类型相等时，若表达式属其中一个类型，则它同时也属另一个类型则它同时也属另一个类型 有了子有了子定型后，则用叫做定型后，则用叫做“包容包容” 的子定型性的子定型性质来代替这个原则：质来代替这个原则： 如果如果A是是B的子类型，那么类型的子类型，那么类型A的表达式也的表达式也有类型有类型B 如果如果A是是B的子类型，那么可以用的子类型，那么可以用A的元素代替的元素代替B的元素的元素10.1 引引 言言 记录类型记录类型 记录类型记录类型R：有整型成员有整型成员a和布尔型成员和布尔型成员b，表达式表达式r. .a和和r. .b都是允许的都是允许的

4、记记录类型录类型S：仅有整型成员仅有整型成员a，s. .a是合法的是合法的 在类型在类型S的元素上有意义的操作，在类型的元素上有意义的操作，在类型R的元素的元素上也都有意义上也都有意义 包包含类型含类型S的记录的任何表达式中，可以安全地的记录的任何表达式中，可以安全地使用类型使用类型R的记录去代替而不会发生类型错误的记录去代替而不会发生类型错误 R是是S的子类型的子类型10.1 引引 言言 记号记号A:B将用来表示将用来表示A是是B的子类型的子类型 断言断言A:B的含义有两种一般的观点的含义有两种一般的观点1、类型、类型A的值的每种表示都是类型的值的每种表示都是类型B的的值的一种表值的一种表示

5、示2、类型类型A的值的每种表示都可以按某种的值的每种表示都可以按某种“标准标准”的的方式转换成类型方式转换成类型B的值的一种表示的值的一种表示 本章观点本章观点一种语言和它的子定型性质可以由一组规则来定义一种语言和它的子定型性质可以由一组规则来定义 子定型是类型之间的关系，而继承性是实现子定型是类型之间的关系，而继承性是实现之间的关系之间的关系10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 本节用子定型来拓展本节用子定型来拓展 ，得到，得到演算演算 : 用它用它来讨论子定型的一些本质特征来讨论子定型的一些本质特征 笛卡儿积笛卡儿积、和、和、unit及及null可以加入而不会使它变

6、可以加入而不会使它变得复杂得复杂 一个一个 :基调是一个三元组基调是一个三元组 = B, Sub, C B是类型常量集合是类型常量集合 C是项常量的集合是项常量的集合 Sub是类型常量是类型常量b, bB之间的子定型断言之间的子定型断言b :b 的的集合集合10.2 有子定型的简单类型化有子定型的简单类型化 演算演算1、类型、类型 :的类型表达式和的类型表达式和 的类型表达式一样的类型表达式一样 := b | :独有的特征独有的特征 : (ref :) (trans :)它们是所考虑的每个子定型系统的一部分，它使它们是所考虑的每个子定型系统的一部分，它使得子类型关系是一个前序关系得子类型关系是

7、一个前序关系 : , : : 10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 在每个系统中，对每种类型形式，至少有一在每个系统中，对每种类型形式，至少有一条公理或推理规则，用来标识这种类型形式条公理或推理规则，用来标识这种类型形式的子定型性质的子定型性质 对于函数类型有对于函数类型有( :)对第二个变元是单调的，但是对第一个变元是对第二个变元是单调的，但是对第一个变元是反单调的反单调的 : , : : 10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 一个简单示例：一个简单示例：int : real引起的下列安排引起的下列安排 int realint intreal

8、real real int把把int int解释成一个函数集合，这些函数的定解释成一个函数集合，这些函数的定义域义域至少至少是所有整数的集合是所有整数的集合10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 : 从从Sub中的断言，用公理和推理规则可以证明子中的断言，用公理和推理规则可以证明子定型断言定型断言 : 引理引理 对任何基调对任何基调 ，如果，如果 : ，那么，那么 匹配匹配 对对 :的子定型的语义解释的子定型的语义解释 子定型可以解释为转换或者包含子定型可以解释为转换或者包含 转换解释有助于澄清转换解释有助于澄清子定型为什么是前序而不是子定型为什么是前序而不是偏序偏序 前

9、序解释：可能同时有前序解释：可能同时有 : 和和 : ，但，但 可相互转换的值集并不一定有同样表示可相互转换的值集并不一定有同样表示10.2 有子定型的简单类型化有子定型的简单类型化 演算演算2、项、项 :项的定型规则项的定型规则 包括包括 项的所有定型规则：项的所有定型规则：(cst)、(var)、(Intro)、( Elim)、(add var) 新增包容规则新增包容规则 (subsumption) M : , : M : 10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 例例10.1 假定基调中有假定基调中有int : real、2: int、2.0: real和和div:

10、realrealreal 令令M是项是项 x: real.(div x 2.0): real real 确定确定M 2的类型的类型 方式方式1: 利用利用real real : int real的事实的事实 方式方式2: 利用利用int : real，使得使得2: real10.2 有子定型的简单类型化有子定型的简单类型化 演算演算3、等式规则、等式规则 :等式证明系统和等式证明系统和 的正好包含同样的公理的正好包含同样的公理和推理规则和推理规则 等价关系等价关系: (ref)、(sym)和和(trans) 加变量到类型指派加变量到类型指派: (add var) 抽象和应用抽象和应用: ( )

11、、( )和和( ) 同余关系同余关系: ( )和和( ) 通常，只有在通常，只有在 M 和和 N 都可推导时，都可推导时，才把等式才把等式 M N 看成是良形的看成是良形的10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 有了子定型后会引起一些定型上的混淆有了子定型后会引起一些定型上的混淆 外外延公理延公理( ) x: . (Mx) M x在在M中不是自由的中不是自由的会导致相等的项有不同的类型会导致相等的项有不同的类型适当地定义适当地定义M（ y: .N且且 : ）会出现）会出现: x: . (Mx) : M : 其中其中 : 由于由于 : 是可推导的，因此是可推导的，因此 x:

12、 . (Mx) M : 可以使用可以使用10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 两个项在一种类型下相等而在另一种类型下两个项在一种类型下相等而在另一种类型下不相等不相等 在在 中，等式的形式写成中，等式的形式写成 M N: ，以直接以直接表示这两个项的公共定型表示这两个项的公共定型 x: real. x x: real. x: real real x: real. x x: real. x: int real 通常，如果通常，如果A : B，在类型在类型A上有不同值的表达上有不同值的表达式在类型式在类型B上却相等是可能的上却相等是可能的 M = N : , : M = N

13、 : 10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 子定型和等式的一般原则由下面推理规则给子定型和等式的一般原则由下面推理规则给出出该规则是一条导出规则该规则是一条导出规则(subsumption eq)10.2 有子定型的简单类型化有子定型的简单类型化 演算演算 例例10.3 对任何对任何 :项项 x: . M: ，并且并且 : , ,可以证明等式可以证明等式 x: . M = x: . M : 证明的最后两步：证明的最后两步： x: . ( x: .M) x = x: .M: /使使用用 ( ) x: . ( x: .M) x = x: .M: /使使用用 ( ) 此例说明

14、，在此例说明，在 :项上，项上， 和和 归约没有合流性归约没有合流性 可以由加一条归约规则来补救可以由加一条归约规则来补救 x: .M x: . M: 若若 : (type label) 10.3 记记 录录10.3.1 记录子定型的一般性质记录子定型的一般性质 类型分别为类型分别为 1, , n的成员的成员l1, , ln构成的记构成的记录的类型录的类型 l1: 1, , ln: n 记录和笛卡儿积相比，有更加丰富的子定型记录和笛卡儿积相比，有更加丰富的子定型性质，因此记录到积的翻译不能保子定型性质，因此记录到积的翻译不能保子定型10.3 记记 录录 例例 employee name : s

15、tring, manager : string, salary : int manager name : string, manager : string, salary : int, dept: department manager : employee 确定一个记录类型是否为另一个的子类型的确定一个记录类型是否为另一个的子类型的主要原则是所有的操作必须保持合理和良定主要原则是所有的操作必须保持合理和良定义义10.3 记记 录录 例例 employee name : string, manager : string, salary : int manager name : string, m

16、anager : string, salary : large_int , dept: department manager : employee 记录子定型涉及加成员和将成员的类型限制记录子定型涉及加成员和将成员的类型限制到其子类型到其子类型10.3 记记 录录10.3.2 带记录和子定型的类型化带记录和子定型的类型化演算演算1、类型、类型 :, record的基调和的基调和 :的基调的基调一样，一样，类型表达式类型表达式文法是文法是 := b | | l1: , , ln: 记录类记录类型中型中label : type的序没有什么意义的序没有什么意义10.3 记记 录录 子定型的公理和推理

17、规则子定型的公理和推理规则 包括包括 :的的(ref :), (trans :)和和( :)在内在内 增加下增加下面的推理规则面的推理规则 (record :) 1 : 1, . . . , n : n l1: 1, , ln: n, ln+1: 1, , ln+m: m : l1 : 1, , ln: n 10.3 记记 录录 记录子定型的包含解释记录子定型的包含解释 把记录看成一个部分函数把记录看成一个部分函数 把记录类型看成满足某种限制的部分函数集合把记录类型看成满足某种限制的部分函数集合例：例：记录表达式记录表达式 a = 3, b = true 看成看成 a, 3 , b, true

18、 记录类型记录类型 a: int, b: bool 的每个记录是至少在的每个记录是至少在 a, b上有定义的函数上有定义的函数 a: int, b: bool, c: char : a: int, b: bool 记录子定型的转换解释记录子定型的转换解释10.3 记记 录录2、项、项 :, record预备项由下面的文法给出预备项由下面的文法给出M := c | x | M M | x: .M | l1 = M, , ln= M | M.l :, record增加两条定型规则增加两条定型规则 (Record Intro) (Record Elim) M : l1: 1, , ln: n M.l

19、i : i M1: 1 . . . Mn: n l1=M1 , , ln=Mn : l1 : 1, , ln: n 10.3 记记 录录3、等式规则、等式规则 记录的等式公理类似于序对的等式公理记录的等式公理类似于序对的等式公理 l1 = M1, , ln = Mn .li = Mi: i (record selection) l1 = M.l1, , ln = M.ln = M: l1: 1, , ln: n (record ext) l1 = M1, , ln = Mn = l (1) = M (1), , l (n) = M (n) : l1: 1, , ln: n (重新定序公理重新定

20、序公理)其中其中 是是1, , n的任意置换的任意置换10.3 记记 录录 例例 b=true, a=3, c=“Hello” = a=3, b=true, c=“Hello” : b : bool, a : int, c : string a =3, b = true, c = “Hello” = a =3, b = true : a : int, b : bool 10.4 子定型的语义模型子定型的语义模型10.4.1 概述概述 :最一般的转换语义最一般的转换语义 每个类型解释每个类型解释为一个集合为一个集合 每当每当A:B，则有从则有从A到到B的的“转换转换”函数函数若若A是是B的子集，

21、可用恒等函数完成从的子集，可用恒等函数完成从A到到B的转换的转换10.4 子定型的语义模型子定型的语义模型10.4.2 子定型的转换解释子定型的转换解释 如果如果b1 : b2直接由基调给出，相应的转换函数必直接由基调给出，相应的转换函数必须作为解释的一部分给出须作为解释的一部分给出 如果如果 : 是使用某个证明规则从基调可证明的，是使用某个证明规则从基调可证明的，那么从该基调给出的那么从该基调给出的“基本基本”转换函数可以定义转换函数可以定义相应的转换函数相应的转换函数 有了转换函数，那就可以给类型化的项以含义有了转换函数，那就可以给类型化的项以含义 定义类型化项的含义的自然方式是在项的定型

22、推定义类型化项的含义的自然方式是在项的定型推导上归纳导上归纳10.4 子定型的语义模型子定型的语义模型 定义类型化项的含义的自然方式是在项的定定义类型化项的含义的自然方式是在项的定型推导上归纳型推导上归纳 如果如果 M: 可由可由推导，那么该项的含义将是把推导，那么该项的含义将是把 到到 的转换函的转换函数应用到与数应用到与 M: 的定型推导有关的含义的定型推导有关的含义上上 对于对于 :，所需要的转换函数是恒等函数、基所需要的转换函数是恒等函数、基本转换和由函数合成定义的转换本转换和由函数合成定义的转换 M : : M : 10.4 子定型的语义模型子定型的语义模型 任何任何 的语义模型可以

23、作为的语义模型可以作为 :的语义模型的语义模型 只要对基本转换函数能找到适当的解释只要对基本转换函数能找到适当的解释 其它转换函数都是其它转换函数都是 可定义的可定义的 从从 的等式可靠性和完备性定理中可导出的等式可靠性和完备性定理中可导出 :的对的对应定理应定理10.4 子定型的语义模型子定型的语义模型 从从 :基调基调 = B, Sub, C 开始，将开始，将 上的每个上的每个 :项翻译成基调项翻译成基调 B, CSub 上的上的 项项 让让CSub是是C和一组写成和一组写成c 形式的不同常量符号的形式的不同常量符号的并集并集 对每个子定型对每个子定型b1:b2,有符号有符号c :b1b2

24、 转换函数上的协调限制转换函数上的协调限制 c ca = c ca : a b 所有这样所有这样的等式集合称为的等式集合称为 b2b2baka1al ba1 b1b110.4 子定型的语义模型子定型的语义模型1、转换函数、转换函数 c 的定义是在的定义是在 : 证明上的归纳证明上的归纳(ref :) : c x: .x(trans :) c x: . c (c x)( :) c f: 1 2. x: 1.c (f (c x)通过一系列不改变相关转换函数的证明变换，可通过一系列不改变相关转换函数的证明变换，可以证明这些转换函数是唯一的以证明这些转换函数是唯一的 : : : 1: 1 2: 2 1

25、 2: 1 2 1 2 1 2 2 2 1 1 10.4 子定型的语义模型子定型的语义模型2、项的翻译、项的翻译对基调对基调 = B, Sub, C 上的任何上的任何 :项项 M: , ,定义定义它到基调它到基调 B, CSub 上的上的 项的翻译项的翻译Trans( M: ), ,由由 :项的定型规则上的归纳，项的定型规则上的归纳，Trans的的定义如下定义如下(cst) Trans ( c: ) = c(var) Trans (x: x: ) = x( Intro) Trans ( x: .M: ) = x: .Trans( , x: M: )( Elim) Trans ( MN: ) =

26、 Trans( M: ) Trans ( N: ) 10.4 子定型的语义模型子定型的语义模型(add var) Trans ( , x: M: ) = Trans ( M: )(subsumption) 若若 M: 是可用是可用 : 从从 M: 推导的，则推导的，则Trans ( M: ) c Trans ( M: ) 引理引理10.6如果如果 M: 是基调是基调 B, Sub, C 上一个可推导的上一个可推导的 :定型断言，则定型断言，则 Trans( M: ): 是基调是基调 B, CSub 上可推导的上可推导的 定型断言定型断言 10.4 子定型的语义模型子定型的语义模型 命题命题10

27、.10 令令 = B, Sub, C 是一个是一个 :基调，并且令基调，并且令 M: 是是 上的一个上的一个 :项项若对于若对于 M: 有两个定型推导，并且令有两个定型推导，并且令M1, ,M2=Trans( M: )是按这两个定型推导得到的是按这两个定型推导得到的M的两个翻译的两个翻译则使用则使用 的证明规则可得的证明规则可得 M1 = M2: 10.5 递归类型和对象的记录模型递归类型和对象的记录模型本节研究带函数成员的记录本节研究带函数成员的记录 用用“方法结果方法结果”的记录来表示对象的记录来表示对象:选择一个记录的成员同发送相应的消息到一个选择一个记录的成员同发送相应的消息到一个对象

28、返回同样的值对象返回同样的值 对于带参数的方法，记录选择将返回一个函数对于带参数的方法，记录选择将返回一个函数 这个模型简单、易理解、这个模型简单、易理解、提供了面向对象的概念提供了面向对象的概念可以用类型化可以用类型化 演算来研究的某种感觉演算来研究的某种感觉10.5 递归类型和对象的记录模型递归类型和对象的记录模型 在面向对象的程序设计中，对象类型经常可在面向对象的程序设计中，对象类型经常可以递归地定义以递归地定义 点类型点类型 point type point = x:int, y:int, move:int int point 如果如果有带有带x和和y坐标和一个方向的坐标和一个方向的“

29、有向有向”点，那点，那么每个有向点可以有保自己方向的么每个有向点可以有保自己方向的move方法方法 :, record, 的类型表达式的类型表达式 := t | b | | l1: 1, , lk : k | t. 其中其中 t. 看成是看成是fix( t. . )的语法美化。为了可读的语法美化。为了可读性，仍用形式为性，仍用形式为t = 的声明来定义递归类型的声明来定义递归类型10.5 递归类型和对象的记录模型递归类型和对象的记录模型 type point = x: int, y: int, move: int int point 看成类型看成类型point t. x: int, y: in

30、t, move: int int t fix ( t. . x: int, y: int, move: int int t ) 的语法美化的语法美化即，仍用形式为即，仍用形式为t = 的声明来定义递归类型的声明来定义递归类型 类型表达式等式公理类型表达式等式公理 t. = s.s/t s在在 中不是自由的中不是自由的 ( ) t. = t. /t (unfold) 相当于相当于fix M = M(fix M)10.5 递归类型和对象的记录模型递归类型和对象的记录模型 若若pt : point t. x:int, y:int, move: intintt ,那么使用类型等式那么使用类型等式(un

31、fold)： t. = t. /t 则有则有 pt : x: int, y: int, move: int int point 于是于是 pt. .move: int int point10.5 递归类型和对象的记录模型递归类型和对象的记录模型 例例 定义点定义点“类类”如下如下class pointinstance variablesxval: int, yval: intconstructor point (xv : int) (yv : int)xval=xv, yval=yvmethod x: intreturn xvalmethod y: intreturn yvalmethod m

32、ove (dx : int) (dy : int) : pointreturn point (self.x + dx) (self.y + dy)end10.5 递归类型和对象的记录模型递归类型和对象的记录模型 例例 略去无关部分略去无关部分class pointinstance variablesxval: int, yval: intconstructor point (xv : int) (yv : int)xval=xv, yval=yvmethod move (dx : int) (dy : int) : pointreturn point (self.x + dx) (self.y

33、 + dy)end 一个类定义一个类型并定义一个创建对象的函数一个类定义一个类型并定义一个创建对象的函数 把对象的类型写成记录类型，把创建对象的函数把对象的类型写成记录类型，把创建对象的函数写成返回记录的函数写成返回记录的函数10.5 递归类型和对象的记录模型递归类型和对象的记录模型 例（续）对象的记录模型例（续）对象的记录模型 点对象的类型是递归记录类型点对象的类型是递归记录类型type point = x: int, y: int, move:int int point 创建该类型的点的函数可以递归定义如下创建该类型的点的函数可以递归定义如下letrec mk_point (xv : in

34、t) (yv : int) = x = xv, y = yv, move = dx: int. dy: int. mk_point (xv + dx) (yv + dy) 10.5 递归类型和对象的记录模型递归类型和对象的记录模型 例（续）对象的记录模型例（续）对象的记录模型type point= x: int, y: int, move:int int point letrec mk_point (xv : int) (yv : int) = x = xv, y = yv, move = dx: int. dy: int. mk_point (xv + dx) (yv + dy) mk_po

35、int重新写成重新写成mk_pointfix( f:intintpoint. xv:int. yv:int. x=xv, y=yv, move= dx:int. dy:int.f(xv + dx) (yv + dy) )其中其中fix:(int int point) (int int point) (int int point)10.5 递归类型和对象的记录模型递归类型和对象的记录模型(mk_point 3 2 ).move 4 6 (fix ( f : int int point. xv: int. yv: int. x = xv, y = yv, move = dx: int. dy: i

36、nt. f (xv + dx) (yv + dy) )3 2). move 4 6= ( xv: int. yv: int. x = xv, y = yv, move = dx: int. dy: int. (fix () (xv + dx) (yv + dy) )3 2). move 4 6= ( x =3, y =2, move = dx: int. dy: int. (fix () (3 + dx) (2 + dy) ).move 4 6= ( dx: int. dy: int. (fix () (3 + dx) (2 + dy) 4 6= (fix () (3 + 4) (2 + 6)

37、= x =7, y =8, move = dx: int. dy: int. (fix () (7 + dx) (8 + dy) 10.5 递归类型和对象的记录模型递归类型和对象的记录模型下面讨论递归类型的子定型下面讨论递归类型的子定型 先考虑一些直观的例子先考虑一些直观的例子 type point = x: int, y: int, move: int int point type col_point = x: int, y: int, c: color, move: int int col_point 总希望总希望col_point是是point的子类型的子类型 关键看关键看pt.move

38、和和c_pt.move是否是否“相容相容” 可以通过考虑操作可以通过考虑操作序列来理解序列来理解它们的相容性它们的相容性10.5 递归类型和对象的记录模型递归类型和对象的记录模型 第二个例子：第二个例子：子定型失败在表面上类似的递子定型失败在表面上类似的递归记录类型上归记录类型上 type simple_set = member? : elt bool,insert: elt simple_set,intersect: simple_set simple_set type sized_set = member? : elt bool,insert: elt sized_set,intersec

39、t: sized_set sized_set,size: int 两个两个intersect的变元类型是不同的的变元类型是不同的10.5 递归类型和对象的记录模型递归类型和对象的记录模型type simple_set = member? : elt bool,insert: elt simple_set,intersect: simple_set simple_set type sized_set = member? : elt bool,insert: elt sized_set,intersect: sized_set sized_set,size: int 假定假定s, t: simpl

40、e_set且且r: sized_set 计算两个简单集合的交集的表达式计算两个简单集合的交集的表达式 ersect t 表达式表达式ersect t可能会引起错误可能会引起错误10.5 递归类型和对象的记录模型递归类型和对象的记录模型type simple_set = member? : elt bool,insert: elt simple_set,intersect: simple_set simple_set type sized_set = member? : elt bool,insert: elt sized_set,intersect: sized_set sized_set,size: int type sized_set = member? : elt bool,改用改用insert: elt sized_set ,sized_set intersect: simple_set sized_set ,来解决来解决s