第10章 子定型 子定型是类型上的一种关系，该关系隐含一个类型的值可以代替另一个类型的值 第10章 子定型 子定型是类型上的一种关系，该关系隐含一个类型的值可以代替另一个类型的值 和子定型有关的语言概念是记录、对象及依赖于子类型关系的各种多态性 本章考虑子定型和体现子定型在程序设计中作用的一些语言概念

第10章 子定型 本章的主要内容 带记录和子定型的简单类型化演算 等式理论和语义模型 递归类型的子定型和递归记录作为对象的模型

10.1 引 言 子定型出现在许多程序设计语言中 Fortran语言 Pascal语言 类型化面向对象语言 整型和实型（浮点）表达式混合写出 10.1 引 言 子定型出现在许多程序设计语言中 Fortran语言 整型和实型（浮点）表达式混合写出 整数到实数的转换有一些典型的子定型性质 Pascal语言 子界[1..10]是整数的子区间 类型化面向对象语言 子类型的对象可以用来代替任何超类型的对象

10.1 引 言 包容 在大多数类型化程序设计语言中，一个原则是：当两个类型相等时，若表达式属其中一个类型，则它同时也属另一个类型 10.1 引 言 包容 在大多数类型化程序设计语言中，一个原则是：当两个类型相等时，若表达式属其中一个类型，则它同时也属另一个类型 有了子定型后，则用叫做“包容” 的子定型性质来代替这个原则： 如果A是B的子类型，那么类型A的表达式也有类型B 如果A是B的子类型，那么可以用A的元素代替B的元素

10.1 引 言 记录类型 记录类型R：有整型成员a和布尔型成员b， 表达式r.a和r.b都是允许的 10.1 引 言 记录类型 记录类型R：有整型成员a和布尔型成员b， 表达式r.a和r.b都是允许的 记录类型S：仅有整型成员a，s.a是合法的 在类型S的元素上有意义的操作，在类型R的元素上也都有意义 包含类型S的记录的任何表达式中，可以安全地使用类型R的记录去代替而不会发生类型错误 R是S的子类型

10.1 引 言 记号A<:B将用来表示A是B的子类型 断言A<:B的含义有两种一般的观点 本章观点 10.1 引 言 记号A<:B将用来表示A是B的子类型 断言A<:B的含义有两种一般的观点 1、类型A的值的每种表示都是类型B的值的一种表示 2、类型A的值的每种表示都可以按某种“标准”的方式转换成类型B的值的一种表示 本章观点 一种语言和它的子定型性质可以由一组规则来定义 子定型是类型之间的关系，而继承性是实现之间的关系

10.2 有子定型的简单类型化演算 本节用子定型来拓展，得到演算<: 用它来讨论子定型的一些本质特征 笛卡儿积、和、unit及null可以加入而不会使它变得复杂 一个<:基调是一个三元组 = B, Sub, C B是类型常量集合 C是项常量的集合 Sub是类型常量b, bB之间的子定型断言b <:b的集合  

10.2 有子定型的简单类型化演算 1、类型 <:的类型表达式和的类型表达式一样  ::= b |   <:独有的特征  <: (ref <:) (trans <:) 它们是所考虑的每个子定型系统的一部分，它使 得子类型关系是一个前序关系    <:,  <:  <:

10.2 有子定型的简单类型化演算 在每个系统中，对每种类型形式，至少有一条公理或推理规则，用来标识这种类型形式的子定型性质 对于函数类型有 ( <:) 对第二个变元是单调的，但是对第一个变元是 反单调的  <:, <:   <:  

10.2 有子定型的简单类型化演算 一个简单示例：int <: real引起的下列安排 int  real int  int real  real real  int 把int  int解释成一个函数集合，这些函数的定义域至少是所有整数的集合

10.2 有子定型的简单类型化演算   <: 对<:的子定型的语义解释 从Sub中的断言，用公理和推理规则可以证明子定型断言 <: 引理 对任何基调，如果  <:，那么 匹配 对<:的子定型的语义解释 子定型可以解释为转换或者包含 转换解释有助于澄清子定型为什么是前序而不是偏序 前序解释：可能同时有 <:和 <:，但  可相互转换的值集并不一定有同样表示 

10.2 有子定型的简单类型化演算 2、项 <:项的定型规则 包括项的所有定型规则：(cst)、(var)、(Intro)、( Elim)、(add var) 新增包容规则 (subsumption)    M : ,   <:   M : 

10.2 有子定型的简单类型化演算 例10.1 假定基调中有int <: real、2: int、2.0: real和 div: realrealreal 令M是项x: real.(div x 2.0): real  real 确定M 2的类型 方式1: 利用real  real <: int  real的事实 方式2: 利用int <: real，使得2: real

10.2 有子定型的简单类型化演算 3、等式规则 <:等式证明系统和的正好包含同样的公理和推理规则 等价关系: (ref)、(sym)和(trans) 加变量到类型指派: (add var) 抽象和应用: ()、()和() 同余关系: ()和() 通常，只有在  M 和  N 都可推导时，才 把等式  M  N 看成是良形的 

10.2 有子定型的简单类型化演算 有了子定型后会引起一些定型上的混淆 外延公理()   x:. (Mx)  M x在M中不是自由的 会导致相等的项有不同的类型 适当地定义M（ y:.N且 <: ）会出现:   x:. (Mx) :     M :  其中 <: 由于 <:  是可推导的，因此   x:. (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上却相等是可能的

10.2 有子定型的简单类型化演算 子定型和等式的一般原则由下面推理规则给出 该规则是一条导出规则   M = N :,   <:    M = N :  (subsumption eq)

10.2 有子定型的简单类型化演算 例10.3 对任何<:项  x:. M:  ，并且 <:,可以证明等式   x:. M = x:. M :    证明的最后两步：   x:. (x:.M) x = x:.M:    //使用 ()   x:. (x:.M) x = x:.M:   //使用 ( ) 此例说明，在<:项上， 和归约没有合流性 可以由加一条归约规则来补救   x:.M  x:. M:   若   <: (type label) 

10.3 记 录 10.3.1 记录子定型的一般性质 类型分别为1, …, n的成员l1, …, ln构成的记录的类型 10.3 记 录 10.3.1 记录子定型的一般性质 类型分别为1, …, n的成员l1, …, ln构成的记录的类型 l1:1, …, ln:n 记录和笛卡儿积相比，有更加丰富的子定型性质，因此记录到积的翻译不能保子定型

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

10.3 记 录 例 记录子定型涉及加成员和将成员的类型限制到其子类型 10.3 记 录 例 employee  name : string, manager : string, salary : int manager  name : string, manager : string, salary : large_int , dept: department manager <: employee 记录子定型涉及加成员和将成员的类型限制到其子类型

10.3 记 录 10.3.2 带记录和子定型的类型化演算 1、类型 <:, record的基调和 <:的基调一样，类型表达式文法是  ::= b |   | l1:, …, ln: 记录类型中label : type的序没有什么意义  

 l1:1, …, ln:n, ln+1:1, …, ln+m:m <:  l1 :1, …, ln:n 10.3 记 录 子定型的公理和推理规则 包括<:的(ref <:), (trans <:)和( <:)在内 增加下面的推理规则 (record <:)  1 <: 1, . . . , n <: n  l1:1, …, ln:n, ln+1:1, …, ln+m:m <:  l1 :1, …, ln:n

10.3 记 录 记录子定型的包含解释 记录子定型的转换解释 把记录看成一个部分函数 把记录类型看成满足某种限制的部分函数集合 10.3 记 录 记录子定型的包含解释 把记录看成一个部分函数 把记录类型看成满足某种限制的部分函数集合 例：记录表达式a = 3, b = true 看成{a, 3, b, true} 记录类型a: int, b: bool的每个记录是至少在{ a, b}上有定义的函数 a: int, b: bool, c: char <: a: int, b: bool 记录子定型的转换解释

   l1=M1 , …, ln=Mn :  l1 :1, …, ln:n 10.3 记 录 2、项 <:, record预备项由下面的文法给出 M ::= c | x | M M | x:.M | l1 = M, …, ln= M | M.l <:, record增加两条定型规则 (Record Intro) (Record Elim)     M1:1 . . .   Mn:n    l1=M1 , …, ln=Mn :  l1 :1, …, ln:n   M :  l1:1, …, ln:n   M.li : i

10.3 记 录 3、等式规则 记录的等式公理类似于序对的等式公理 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 (重新定序公理) 其中是{1, …, n}的任意置换

10.3 记 录 例 b=true, a=3, c=“Hello”=a=3, b=true, c=“Hello”: 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 概述 <:最一般的转换语义 每个类型解释为一个集合 10.4 子定型的语义模型 10.4.1 概述 <:最一般的转换语义 每个类型解释为一个集合 每当A<:B，则有从A到B的“转换”函数 若A是B的子集，可用恒等函数完成从A到B的转换 

10.4 子定型的语义模型 10.4.2 子定型的转换解释 如果b1 <: b2直接由基调给出，相应的转换函数必须作为解释的一部分给出 10.4 子定型的语义模型 10.4.2 子定型的转换解释 如果b1 <: b2直接由基调给出，相应的转换函数必须作为解释的一部分给出 如果 <:是使用某个证明规则从基调可证明的，那么从该基调给出的“基本”转换函数可以定义相应的转换函数 有了转换函数，那就可以给类型化的项以含义 定义类型化项的含义的自然方式是在项的定型推导上归纳

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

10.4 子定型的语义模型 任何的语义模型可以作为<:的语义模型 只要对基本转换函数能找到适当的解释 其它转换函数都是可定义的 10.4 子定型的语义模型 任何的语义模型可以作为<:的语义模型 只要对基本转换函数能找到适当的解释 其它转换函数都是可定义的 从的等式可靠性和完备性定理中可导出<:的对应定理  

10.4 子定型的语义模型 从<:基调 = B, Sub, C开始，将上的每个<:项翻译成基调B, CSub上的项 让CSub是C和一组写成c 形式的不同常量符号的并集 对每个子定型b1<:b2,有符号c :b1b2 转换函数上的协调限制 c  …  ca = c  …  ca : a  b 所有这样的等式集合称为   b2 b1 b2 b1 a1 b a1 b al ak

10.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2<:12 12 12 2 1 2 1

10.4 子定型的语义模型 2、项的翻译 对基调 = B, Sub, C上的任何<:项M:,定义 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:) = Trans(M: ) Trans (N:)  

10.4 子定型的语义模型 引理10.6 (add var) Trans (, x:  M:) = Trans (  M:) 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.10 令 = B, Sub, C是一个<:基调，并且令M: 10.4 子定型的语义模型 命题10.10 令 = B, Sub, C是一个<:基调，并且令M: 是上的一个<:项 若对于M:有两个定型推导，并且令 M1,M2=Trans(M:) 是按这两个定型推导得到的M的两个翻译 则使用的证明规则可得  M1 = M2:   

10.5 递归类型和对象的记录模型 本节研究带函数成员的记录 用“方法结果”的记录来表示对象: 选择一个记录的成员同发送相应的消息到一个对象返回同样的值 对于带参数的方法，记录选择将返回一个函数 这个模型简单、易理解、提供了面向对象的概念可以用类型化演算来研究的某种感觉

10.5 递归类型和对象的记录模型 在面向对象的程序设计中，对象类型经常可以递归地定义 点类型 point type point = x:int, y:int, move:int  int  point 如果有带x和y坐标和一个方向的“有向”点，那么每个有向点可以有保自己方向的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: int, 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: intintt,那么使用类型等式(unfold)：t. = [t. /t] 则有 pt : x: int, y: int, move: int  int  point 于是 pt.move: int  int  point

10.5 递归类型和对象的记录模型 例 定义点“类”如下 class point instance variables 例 定义点“类”如下 class point instance variables xval: int, yval: int constructor point (xv : int) (yv : int) xval=xv, yval=yv method x: int return xval method y: int return yval method move (dx : int) (dy : int) : point return point (self.x + dx) (self.y + dy) end

10.5 递归类型和对象的记录模型 例 略去无关部分 一个类定义一个类型并定义一个创建对象的函数 例 略去无关部分 class point instance variables xval: int, yval: int constructor point (xv : int) (yv : int) xval=xv, yval=yv method move (dx : int) (dy : int) : point return point (self.x + dx) (self.y + dy) end 一个类定义一个类型并定义一个创建对象的函数 把对象的类型写成记录类型，把创建对象的函数写成返回记录的函数

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)

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_point重新写成 mk_pointfix(f:intintpoint.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: int. 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) = 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和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, intersect: 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: simple_set且r: sized_set 计算两个简单集合的交集的表达式 s.intersect t 表达式r.intersect 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, 来解决 size: int

 l1:1 , …, ln:n, ln+1:1 , …, ln+m:m <:  l1 :1, …, ln:n 10.5 递归类型和对象的记录模型 <:, record, 的等式规则和子定型规则 (trans <:)（10.2节） ( <:)（10.2节） record <:)（10.3节） 需要一条推理规则从相等断言得到子定型断言，还需要一条规则用于递归类型   <:,  <:  <:  <:,  <:   <:  1 <:  1, . . . , n <:  n  l1:1 , …, ln:n, ln+1:1 , …, ln+m:m <:  l1 :1, …, ln:n

10.5 递归类型和对象的记录模型 <:, record, 的等式规则和子定型规则 从相等断言得到子定型断言的规则 (= <:) 用于递归类型的规则 t在中不是自由的，s在中不是自由的 ( <:)   =   <:  , s <: t  <:    s. <: t.

10.5 递归类型和对象的记录模型 证明col_point <: point 最后一步的形式必定是 应先证 int <: int和 col_point <: point  int  (int  col_point) <: int  (int  point) 后者从自反性和假设col_point <: point，两次应用( <:)规则可得 col_point <: point  x: int, y: int, move: intintcol_point, c: color <: x: int, y: int, move: intint  point  col_point. . . . <:  point. . . .

 eq_col_point. . . . <:  eq_point. . . . 10.5 递归类型和对象的记录模型 加相等测试方法到点和有色点,则子定型失败 type eq_point = x: int, y: int, eq: eq_point  bool type eq_col_point=x: int, y: int, eq:eq_col_pointbool, c: color 最后一步的形式总是 需要先证int <: int和 eq_col_point <: eq_point  (eq_col_point  bool) <: (eq_point  bool) 后者需要证明 eq_col_point <: eq_point  eq_point <: eq_col_point eq_col_point <:eq_point  x:int, y:int, eq:eq_col_pointbool, c:color <: x: int, y: int, eq: eq_point bool  eq_col_point. . . . <:  eq_point. . . .

习 题 第一次：10.1, 10.4 第二次：10.14