第子定型教案資料

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

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

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

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

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

，得到演算

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

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

B是類型常量集合C是項常量的集合Sub是類型常量b,b

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

的集合

10.2有子定型的簡單類型化

演算1、類型

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

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

::=b|

<:獨有的特征

<:

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

<:

,

<:

<:

10.2有子定型的簡單類型化

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

<:)

對第二個變元是單調(diào)的，但是對第一個變元是反單調(diào)的

<:

,

<:

<:

10.2有子定型的簡單類型化

演算一個簡單示例：int<:real引起的下列安排

int

real

int

int

real

real

real

int

把int

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

演算

<:

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

<:

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

，如果

<:

，那么

匹配

對

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

<:

和

<:

，但

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

10.2有子定型的簡單類型化

演算2、項

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

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

(subsumption)

M:

,

<:

M:

10.2有子定型的簡單類型化

演算例10.1假定基調(diào)中有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、等式規(guī)則

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

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

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

(

)、(

)和(

)同余關(guān)系:

(

)和(

)通常，只有在

M

和

N

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

M

N

看成是良形的

10.2有子定型的簡單類型化

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

)

x:

.(Mx)

M

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

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

y:

.N且

<:

）會出現(xiàn):

x:

.(Mx):

M:

其中

<:

由于

<:

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

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上有不同值的表達(dá)式在類型B上卻相等是可能的

M=N:

,

<:

M=N:

10.2有子定型的簡單類型化

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

演算例10.3

對任何

<:項

x:

.M:

，并且

<:

,可以證明等式

x:

.M=x:

.M:

證明的最后兩步：

x:

.(x:

.M)x=x:

.M:

//使用(

)

x:

.(x:

.M)x=x:

.M:

//使用(

)此例說明，在

<:項上，

和

歸約沒有合流性

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

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確定一個記錄類型是否為另一個的子類型的主要原則是所有的操作必須保持合理和良定義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記錄記錄子定型的包含解釋把記錄看成一個部分函數(shù)把記錄類型看成滿足某種限制的部分函數(shù)集合例：記錄表達(dá)式a=3,b=true

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

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

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

a:int,b:bool

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

<:,record預(yù)備項由下面的文法給出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)換語義每個類型解釋為一個集合每當(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ù)必須作為解釋的一部分給出如果

<:

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

M:

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

到

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

M:

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

M:

<:

M:

10.4子定型的語義模型任何

的語義模型可以作為

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

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

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

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

上的

項讓CSub是C和一組寫成c形式的不同常量符號的并集對每個子定型b1<:b2,有符號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、項的翻譯 對基調(diào)=B,Sub,C

上的任何

<:項

M:

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

B,CSub

上的

項的翻譯Trans(

M:

),由

<:項的定型規(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

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

<:定型斷言，則

Trans(

M:

):

是基調(diào)

B,CSub

上可推導(dǎo)的

定型斷言

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

令=B,Sub,C

是一個

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

M:

是

上的一個

<:項 若對于

M:

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

M1,M2=Trans(

M:

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

的證明規(guī)則可得

M1

=M2:

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

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

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

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

int

point

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

<:,record,

的類型表達(dá)式

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

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

t.

=s.[s/t]

s在

中不是自由的(

)

t.

=[t.

/t]

(unfold) 相當(dāng)于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遞歸類型和對象的記錄模型例略去無關(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一個類定義一個類型并定義一個創(chuàng)建對象的函數(shù)把對象的類型寫成記錄類型，把創(chuàng)建對象的函數(shù)寫成返回記錄的函數(shù)10.5遞歸類型和對象的記錄模型例（續(xù)）對象的記錄模型點對象的類型是遞歸記錄類型type

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

int

point

創(chuàng)建該類型的點的函數(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遞歸類型和對象的記錄模型例（續(xù)）對象的記錄模型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的子類型關(guān)鍵看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計算兩個簡單集合的交集的表達(dá)式s.intersectt表達(dá)式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,

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

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

<:

,

<:

<:

<:

,

<:

<:

1

<:

1,...,

n

<:

n

l1:

1

,…,ln:

n,l