第子定型教案資料

第10章子定型子定型是類型上的一種關(guān)系，該關(guān)系隱含一個(gè)類型的值可以代替另一個(gè)類型的值和子定型有關(guān)的語言概念是記錄、對(duì)象及依賴于子類型關(guān)系的各種多態(tài)性本章考慮子定型和體現(xiàn)子定型在程序設(shè)計(jì)中作用的一些語言概念第10章子定型本章的主要內(nèi)容帶記錄和子定型的簡(jiǎn)單類型化

演算等式理論和語義模型遞歸類型的子定型和遞歸記錄作為對(duì)象的模型10.1引言

子定型出現(xiàn)在許多程序設(shè)計(jì)語言中Fortran語言整型和實(shí)型（浮點(diǎn)）表達(dá)式混合寫出整數(shù)到實(shí)數(shù)的轉(zhuǎn)換有一些典型的子定型性質(zhì)Pascal語言子界[1..10]是整數(shù)的子區(qū)間類型化面向?qū)ο笳Z言子類型的對(duì)象可以用來代替任何超類型的對(duì)象10.1引言包容在大多數(shù)類型化程序設(shè)計(jì)語言中，一個(gè)原則是：當(dāng)兩個(gè)類型相等時(shí)，若表達(dá)式屬其中一個(gè)類型，則它同時(shí)也屬另一個(gè)類型有了子定型后，則用叫做“包容”的子定型性質(zhì)來代替這個(gè)原則：

如果A是B的子類型，那么類型A的表達(dá)式也有類型B如果A是B的子類型，那么可以用A的元素代替B的元素10.1引言記號(hào)A<:B將用來表示A是B的子類型斷言A<:B的含義有兩種一般的觀點(diǎn)1、類型A的值的每種表示都是類型B的值的一種表示2、類型A的值的每種表示都可以按某種“標(biāo)準(zhǔn)”的方式轉(zhuǎn)換成類型B的值的一種表示本章觀點(diǎn)一種語言和它的子定型性質(zhì)可以由一組規(guī)則來定義子定型是類型之間的關(guān)系，而繼承性是實(shí)現(xiàn)之間的關(guān)系10.2有子定型的簡(jiǎn)單類型化

演算本節(jié)用子定型來拓展

，得到演算

<:用它來討論子定型的一些本質(zhì)特征笛卡兒積、和、unit及null可以加入而不會(huì)使它變得復(fù)雜一個(gè)

<:基調(diào)是一個(gè)三元組=B,Sub,C

B是類型常量集合C是項(xiàng)常量的集合Sub是類型常量b,b

B之間的子定型斷言b<:b

的集合

10.2有子定型的簡(jiǎn)單類型化

演算1、類型

<:的類型表達(dá)式和

的類型表達(dá)式一樣

::=b|

<:獨(dú)有的特征

<:

(ref<:) (trans<:) 它們是所考慮的每個(gè)子定型系統(tǒng)的一部分，它使得子類型關(guān)系是一個(gè)前序關(guān)系

<:

,

<:

<:

10.2有子定型的簡(jiǎn)單類型化

演算在每個(gè)系統(tǒng)中，對(duì)每種類型形式，至少有一條公理或推理規(guī)則，用來標(biāo)識(shí)這種類型形式的子定型性質(zhì)對(duì)于函數(shù)類型有 (

<:)

對(duì)第二個(gè)變?cè)菃握{(diào)的，但是對(duì)第一個(gè)變?cè)欠磫握{(diào)的

<:

,

<:

<:

10.2有子定型的簡(jiǎn)單類型化

演算一個(gè)簡(jiǎn)單示例：int<:real引起的下列安排

int

real

int

int

real

real

real

int

把int

int解釋成一個(gè)函數(shù)集合，這些函數(shù)的定義域至少是所有整數(shù)的集合10.2有子定型的簡(jiǎn)單類型化

演算

<:

從Sub中的斷言，用公理和推理規(guī)則可以證明子定型斷言

<:

引理對(duì)任何基調(diào)

，如果

<:

，那么

匹配

對(duì)

<:的子定型的語義解釋子定型可以解釋為轉(zhuǎn)換或者包含轉(zhuǎn)換解釋有助于澄清子定型為什么是前序而不是偏序前序解釋：可能同時(shí)有

<:

和

<:

，但

可相互轉(zhuǎn)換的值集并不一定有同樣表示

10.2有子定型的簡(jiǎn)單類型化

演算2、項(xiàng)

<:項(xiàng)的定型規(guī)則包括

項(xiàng)的所有定型規(guī)則：(cst)、(var)、(Intro)、(Elim)、(addvar)新增包容規(guī)則

(subsumption)

M:

,

<:

M:

10.2有子定型的簡(jiǎn)單類型化

演算例10.1假定基調(diào)中有int<:real、2:int、2.0:real和 div:real

real

real令M是項(xiàng)x:real.(divx2.0):real

real確定M

2的類型方式1:利用real

real<:int

real的事實(shí)方式2:利用int<:real，使得2:real10.2有子定型的簡(jiǎn)單類型化

演算3、等式規(guī)則

<:等式證明系統(tǒng)和

的正好包含同樣的公理和推理規(guī)則等價(jià)關(guān)系:

(ref)、(sym)和(trans)加變量到類型指派:(addvar)抽象和應(yīng)用:

(

)、(

)和(

)同余關(guān)系:

(

)和(

)通常，只有在

M

和

N

都可推導(dǎo)時(shí)，才把等式

M

N

看成是良形的

10.2有子定型的簡(jiǎn)單類型化

演算有了子定型后會(huì)引起一些定型上的混淆外延公理(

)

x:

.(Mx)

M

x在M中不是自由的會(huì)導(dǎo)致相等的項(xiàng)有不同的類型

適當(dāng)?shù)囟xM（

y:

.N且

<:

）會(huì)出現(xiàn):

x:

.(Mx):

M:

其中

<:

由于

<:

是可推導(dǎo)的，因此

x:

.(Mx)

M:

可以使用10.2有子定型的簡(jiǎn)單類型化

演算兩個(gè)項(xiàng)在一種類型下相等而在另一種類型下不相等在

中，等式的形式寫成

M

N:

，以直接表示這兩個(gè)項(xiàng)的公共定型

x:real.x

x:real.x:real

real

x:real.x

x:real.x:int

real通常，如果A<:B，在類型A上有不同值的表達(dá)式在類型B上卻相等是可能的

M=N:

,

<:

M=N:

10.2有子定型的簡(jiǎn)單類型化

演算子定型和等式的一般原則由下面推理規(guī)則給出 該規(guī)則是一條導(dǎo)出規(guī)則(subsumptioneq)10.2有子定型的簡(jiǎn)單類型化

演算例10.3

對(duì)任何

<:項(xiàng)

x:

.M:

，并且

<:

,可以證明等式

x:

.M=x:

.M:

證明的最后兩步：

x:

.(x:

.M)x=x:

.M:

//使用(

)

x:

.(x:

.M)x=x:

.M:

//使用(

)此例說明，在

<:項(xiàng)上，

和

歸約沒有合流性

可以由加一條歸約規(guī)則來補(bǔ)救

x:

.M

x:

.M:

若

<:

(typelabel)

10.3記錄10.3.1記錄子定型的一般性質(zhì)類型分別為

1,…,

n的成員l1,…,ln構(gòu)成的記錄的類型

l1:

1,…,ln:

n

記錄和笛卡兒積相比，有更加豐富的子定型性質(zhì)，因此記錄到積的翻譯不能保子定型10.3記錄例employee

name:string,manager:string,

salary:int

manager

name:string,manager:string, salary:int,dept:department

manager<:employee確定一個(gè)記錄類型是否為另一個(gè)的子類型的主要原則是所有的操作必須保持合理和良定義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的基調(diào)和

<:的基調(diào)一樣，類型表達(dá)式文法是

::=b|

|l1:

,…,ln:

記錄類型中l(wèi)abel:type的序沒有什么意義

10.3記錄子定型的公理和推理規(guī)則包括

<:的(ref<:),(trans<:)和(<:)在內(nèi)增加下面的推理規(guī)則 (record<:)

1

<:

1,...,

n

<:

n

l1:

1,…,ln:

n,ln+1:

1,…,ln+m:

m

<:

l1:

1,…,ln:

n

10.3記錄記錄子定型的包含解釋把記錄看成一個(gè)部分函數(shù)把記錄類型看成滿足某種限制的部分函數(shù)集合例：記錄表達(dá)式a=3,b=true

看成{a,3,b,true}記錄類型a:int,b:bool

的每個(gè)記錄是至少在{a,b}上有定義的函數(shù)

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

a:int,b:bool

記錄子定型的轉(zhuǎn)換解釋10.3記錄2、項(xiàng)

<:,record預(yù)備項(xiàng)由下面的文法給出M::=c|x|MM|x:

.M|l1

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

<:,record增加兩條定型規(guī)則 (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、等式規(guī)則記錄的等式公理類似于序?qū)Φ牡仁焦?/p>

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概述

<:最一般的轉(zhuǎn)換語義每個(gè)類型解釋為一個(gè)集合每當(dāng)A<:B，則有從A到B的“轉(zhuǎn)換”函數(shù)若A是B的子集，可用恒等函數(shù)完成從A到B的轉(zhuǎn)換

10.4子定型的語義模型10.4.2子定型的轉(zhuǎn)換解釋如果b1<:b2直接由基調(diào)給出，相應(yīng)的轉(zhuǎn)換函數(shù)必須作為解釋的一部分給出如果

<:

是使用某個(gè)證明規(guī)則從基調(diào)可證明的，那么從該基調(diào)給出的“基本”轉(zhuǎn)換函數(shù)可以定義相應(yīng)的轉(zhuǎn)換函數(shù)有了轉(zhuǎn)換函數(shù)，那就可以給類型化的項(xiàng)以含義定義類型化項(xiàng)的含義的自然方式是在項(xiàng)的定型推導(dǎo)上歸納10.4子定型的語義模型定義類型化項(xiàng)的含義的自然方式是在項(xiàng)的定型推導(dǎo)上歸納如果

M:

可由 推導(dǎo)，那么該項(xiàng)的含義將是把

到

的轉(zhuǎn)換函數(shù)應(yīng)用到與

M:

的定型推導(dǎo)有關(guān)的含義上對(duì)于<:，所需要的轉(zhuǎn)換函數(shù)是恒等函數(shù)、基本轉(zhuǎn)換和由函數(shù)合成定義的轉(zhuǎn)換

M:

<:

M:

10.4子定型的語義模型任何

的語義模型可以作為

<:的語義模型只要對(duì)基本轉(zhuǎn)換函數(shù)能找到適當(dāng)?shù)慕忉屍渌D(zhuǎn)換函數(shù)都是可定義的從

的等式可靠性和完備性定理中可導(dǎo)出<:的對(duì)應(yīng)定理

10.4子定型的語義模型從<:基調(diào)=B,Sub,C

開始，將上的每個(gè)<:項(xiàng)翻譯成基調(diào)B,CSub

上的

項(xiàng)讓CSub是C和一組寫成c形式的不同常量符號(hào)的并集對(duì)每個(gè)子定型b1<:b2,有符號(hào)c

:b1

b2轉(zhuǎn)換函數(shù)上的協(xié)調(diào)限制

c

…

ca=c

…

ca:a

b所有這樣的等式集合稱為

b2b2baka1al

ba1

b1b110.4子定型的語義模型1、轉(zhuǎn)換函數(shù)c

的定義是在

<:

證明上的歸納(ref<:)

<:

c

x:

.x(trans<:) c

x:

.c

(c

x)(<:) c

f:

1

2.

x:

1.c(f(c

x)) 通過一系列不改變相關(guān)轉(zhuǎn)換函數(shù)的證明變換，可以證明這些轉(zhuǎn)換函數(shù)是唯一的

<:

<:

<:

1<:

1

2<:

2

1

2<:

1

2

1

2

1

2

2

2

1

1

10.4子定型的語義模型2、項(xiàng)的翻譯 對(duì)基調(diào)=B,Sub,C

上的任何

<:項(xiàng)

M:

,定義它到基調(diào)

B,CSub

上的

項(xiàng)的翻譯Trans(

M:

),由

<:項(xiàng)的定型規(guī)則上的歸納，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:

推導(dǎo)的，則

Trans(

M:

)＝c

Trans(

M:

)引理10.6 如果

M:

是基調(diào)

B,Sub,C

上一個(gè)可推導(dǎo)的

<:定型斷言，則

Trans(

M:

):

是基調(diào)

B,CSub

上可推導(dǎo)的

定型斷言

10.4子定型的語義模型命題10.10

令=B,Sub,C

是一個(gè)

<:基調(diào)，并且令

M:

是

上的一個(gè)

<:項(xiàng) 若對(duì)于

M:

有兩個(gè)定型推導(dǎo)，并且令

M1,M2=Trans(

M:

)是按這兩個(gè)定型推導(dǎo)得到的M的兩個(gè)翻譯 則使用

的證明規(guī)則可得

M1

=M2:

10.5遞歸類型和對(duì)象的記錄模型本節(jié)研究帶函數(shù)成員的記錄用“方法結(jié)果”的記錄來表示對(duì)象:

選擇一個(gè)記錄的成員同發(fā)送相應(yīng)的消息到一個(gè)對(duì)象返回同樣的值對(duì)于帶參數(shù)的方法，記錄選擇將返回一個(gè)函數(shù)這個(gè)模型簡(jiǎn)單、易理解、提供了面向?qū)ο蟮母拍羁梢杂妙愋突?/p>

演算來研究的某種感覺10.5遞歸類型和對(duì)象的記錄模型在面向?qū)ο蟮某绦蛟O(shè)計(jì)中，對(duì)象類型經(jīng)?？梢赃f歸地定義點(diǎn)類型pointtype

point=x:int,y:int,move:int

int

point

如果有帶x和y坐標(biāo)和一個(gè)方向的“有向”點(diǎn)，那么每個(gè)有向點(diǎn)可以有保自己方向的move方法

<:,record,

的類型表達(dá)式

::=t|b|

|l1:

1,…,lk:

k|t.

其中

t.

看成是fix(t.

)的語法美化。為了可讀性，仍用形式為t=

的聲明來定義遞歸類型

10.5遞歸類型和對(duì)象的記錄模型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=

的聲明來定義遞歸類型類型表達(dá)式等式公理

t.

=s.[s/t]

s在

中不是自由的(

)

t.

=[t.

/t]

(unfold) 相當(dāng)于fixM=M(fixM)10.5遞歸類型和對(duì)象的記錄模型若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遞歸類型和對(duì)象的記錄模型例定義點(diǎn)“類”如下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遞歸類型和對(duì)象的記錄模型例略去無關(guān)部分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一個(gè)類定義一個(gè)類型并定義一個(gè)創(chuàng)建對(duì)象的函數(shù)把對(duì)象的類型寫成記錄類型，把創(chuàng)建對(duì)象的函數(shù)寫成返回記錄的函數(shù)10.5遞歸類型和對(duì)象的記錄模型例（續(xù)）對(duì)象的記錄模型點(diǎn)對(duì)象的類型是遞歸記錄類型type

point=x:int,y:int,move:int

int

point

創(chuàng)建該類型的點(diǎn)的函數(shù)可以遞歸定義如下letrec

mk_point(xv:int)(yv:int)=

x=xv,y=yv,move=dx:int.dy:int.mk_point(xv+dx)(yv+dy)10.5遞歸類型和對(duì)象的記錄模型例（續(xù)）對(duì)象的記錄模型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遞歸類型和對(duì)象的記錄模型(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遞歸類型和對(duì)象的記錄模型下面討論遞歸類型的子定型先考慮一些直觀的例子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的子類型關(guān)鍵看pt.move和c_pt.move是否“相容”可以通過考慮操作序列來理解它們的相容性10.5遞歸類型和對(duì)象的記錄模型第二個(gè)例子：子定型失敗在表面上類似的遞歸記錄類型上

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

兩個(gè)intersect的變?cè)愋褪遣煌?0.5遞歸類型和對(duì)象的記錄模型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計(jì)算兩個(gè)簡(jiǎn)單集合的交集的表達(dá)式s.intersectt表達(dá)式r.intersectt可能會(huì)引起錯(cuò)誤10.5遞歸類型和對(duì)象的記錄模型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遞歸類型和對(duì)象的記錄模型

<:,record,

的等式規(guī)則和子定型規(guī)則 (trans<:)（10.2節(jié)） (<:)（10.2節(jié)）

record<:)（10.3節(jié)）需要一條推理規(guī)則從相等斷言得到子定型斷言，還需要一條規(guī)則用于遞歸類型

<:

,

<:

<:

<:

,

<:

<:

1

<:

1,...,

n

<:

n

l1:

1

,…,ln:

n,l