第子定型教案资料

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

演算等式理论和语义模型递归类型的子定型和递归记录作为对象的模型10.1引言

子定型出现在许多程序设计语言中Fortran语言整型和实型（浮点）表达式混合写出整数到实数的转换有一些典型的子定型性质Pascal语言子界[1..10]是整数的子区间类型化面向对象语言子类型的对象可以用来代替任何超类型的对象10.1引言包容在大多数类型化程序设计语言中，一个原则是：当两个类型相等时，若表达式属其中一个类型，则它同时也属另一个类型有了子定型后，则用叫做“包容”的子定型性质来代替这个原则：

如果A是B的子类型，那么类型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)、(addvar)新增包容规则

(subsumption)

M:

,

<:

M:

10.2有子定型的简单类型化

演算例10.1假定基调中有int<:real、2:int、2.0:real和 div:real

real

real令M是项x:real.(divx2.0):real

real确定M

2的类型方式1:利用real

real<:int

real的事实方式2:利用int<:real，使得2:real10.2有子定型的简单类型化

演算3、等式规则

<:等式证明系统和

的正好包含同样的公理和推理规则等价关系:

(ref)、(sym)和(trans)加变量到类型指派:(addvar)抽象和应用:

(

)、(

)和(

)同余关系:

(

)和(

)通常，只有在

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上却相等是可能的

M=N:

,

<:

M=N:

10.2有子定型的简单类型化

演算子定型和等式的一般原则由下面推理规则给出 该规则是一条导出规则(subsumptioneq)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:

若

<:

(typelabel)

10.3记录10.3.1记录子定型的一般性质类型分别为

1,…,

n的成员l1,…,ln构成的记录的类型

l1:

1,…,ln:

n

记录和笛卡儿积相比，有更加丰富的子定型性质，因此记录到积的翻译不能保子定型10.3记录例employee

name:string,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,manager:string, salary:large_int

,dept:department

manager<:employee记录子定型涉及加成员和将成员的类型限制到其子类型10.3记录10.3.2带记录和子定型的类型化演算1、类型

<:,record的基调和

<:的基调一样，类型表达式文法是

::=b|

|l1:

,…,ln:

记录类型中label:type的序没有什么意义

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记录记录子定型的包含解释把记录看成一个部分函数把记录类型看成满足某种限制的部分函数集合例：记录表达式a=3,b=true

看成{a,3,b,true}记录类型a:int,b:bool

的每个记录是至少在{a,b}上有定义的函数

a:int,b:bool,c:char<:

a:int,b:bool

记录子定型的转换解释10.3记录2、项

<:,record预备项由下面的文法给出M::=c|x|MM|x:

.M|l1

=M,…,ln=M|M.l

<:,record增加两条定型规则 (RecordIntro) (RecordElim)

M

:

l1:

1,…,ln:

n

M.li:

i

M1:

1

...

Mn:

n

l1=M1

,…,ln=Mn

:

l1:

1,…,ln:

n

10.3记录3、等式规则记录的等式公理类似于序对的等式公理

l1

=M1,…,ln=Mn.li

=Mi:

i(recordselection)

l1

=M.l1,…,ln=M.ln

=M:l1:

1,…,ln:

n

(recordext)

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”:

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的子集，可用恒等函数完成从A到B的转换

10.4子定型的语义模型10.4.2子定型的转换解释如果b1<:b2直接由基调给出，相应的转换函数必须作为解释的一部分给出如果

<:

是使用某个证明规则从基调可证明的，那么从该基调给出的“基本”转换函数可以定义相应的转换函数有了转换函数，那就可以给类型化的项以含义定义类型化项的含义的自然方式是在项的定型推导上归纳10.4子定型的语义模型定义类型化项的含义的自然方式是在项的定型推导上归纳如果

M:

可由 推导，那么该项的含义将是把

到

的转换函数应用到与

M:

的定型推导有关的含义上对于<:，所需要的转换函数是恒等函数、基本转换和由函数合成定义的转换

M:

<:

M:

10.4子定型的语义模型任何

的语义模型可以作为

<:的语义模型只要对基本转换函数能找到适当的解释其它转换函数都是可定义的从

的等式可靠性和完备性定理中可导出<:的对应定理

10.4子定型的语义模型从<:基调=B,Sub,C

开始，将上的每个<:项翻译成基调B,CSub

上的

项让CSub是C和一组写成c形式的不同常量符号的并集对每个子定型b1<:b2,有符号c

:b1

b2转换函数上的协调限制

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

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:

)=

Trans(

M:

)Trans(

N:

)

10.4子定型的语义模型(addvar) 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:

是

上的一个

<:项 若对于

M:

有两个定型推导，并且令

M1,M2=Trans(

M:

)是按这两个定型推导得到的M的两个翻译 则使用

的证明规则可得

M1

=M2:

10.5递归类型和对象的记录模型本节研究带函数成员的记录用“方法结果”的记录来表示对象:

选择一个记录的成员同发送相应的消息到一个对象返回同样的值对于带参数的方法，记录选择将返回一个函数这个模型简单、易理解、提供了面向对象的概念可以用类型化

演算来研究的某种感觉10.5递归类型和对象的记录模型在面向对象的程序设计中，对象类型经常可以递归地定义点类型pointtype

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) 相当于fixM=M(fixM)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

point10.5递归类型和对象的记录模型例定义点“类”如下classpoint instancevariables xval:int,yval:int constructorpoint(xv:int)(yv:int) xval=xv,yval=yv methodx:int returnxval methody:int returnyval methodmove(dx:int)(dy:int):point returnpoint(self.x+dx)(self.y+dy) end10.5递归类型和对象的记录模型例略去无关部分classpoint instancevariables xval:int,yval:int constructorpoint(xv:int)(yv:int) xval=xv,yval=yv methodmove(dx:int)(dy:int):point returnpoint(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_point32).move46 (fix(f:int

int

point.xv:int.yv:int.

x=xv,y=yv,move=dx:int.dy:int.f(xv+dx)(yv+dy))32).move46 =((xv:int.yv:int.x=xv,y=yv,

move=dx:int.dy:int.(fix(…))(xv+dx)(yv+dy))32).move46 =(x=3,y=2,move=dx:int.dy:int.(fix(…))(3+dx)(2+dy)).move46 =(dx:int.dy:int.(fix(…))(3+dx)(2+dy))

46 =(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.intersectt表达式r.intersectt可能会引起错误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

10.5递归类型和对象的记录模型

<:,record,

的等式规则和子定型规则 (trans<:)（10.2节） (<:)（10.2节）

record<:)（10.3节）需要一条推理规则从相等断言得到子定型断言，还需要一条规则用于递归类型

<:

,

<:

<:

<:

,

<:

<:

1

<:

1,...,

n

<:

n

l1:

1

,…,ln:

n,l