第7章多態(tài)性PPT課件

1、第第7章章 多態(tài)性多態(tài)性 本章和下一章介紹類型論的一些概念，它們本章和下一章介紹類型論的一些概念，它們是程序設(shè)計語言的多態(tài)性和數(shù)據(jù)抽象的基礎(chǔ)是程序設(shè)計語言的多態(tài)性和數(shù)據(jù)抽象的基礎(chǔ) 這些概念與下面的語言概念有關(guān)這些概念與下面的語言概念有關(guān) Ada的程序包和類屬的程序包和類屬 C的模板的模板 ML以及相近語言以及相近語言Miranda和和Haskell的多態(tài)性、的多態(tài)性、抽象類型和模塊等抽象類型和模塊等 現(xiàn)實語言出于效率上的考慮，所采用的副本沒有現(xiàn)實語言出于效率上的考慮，所采用的副本沒有相應(yīng)的類型化相應(yīng)的類型化 演算那么靈活演算那么靈活7.1 引引 言言 本章的主要內(nèi)容本章的主要內(nèi)容 多態(tài)類型系統(tǒng)

2、的語法，包括直謂式的，非直謂式多態(tài)類型系統(tǒng)的語法，包括直謂式的，非直謂式的和的和type: type版本版本 直謂式多態(tài)直謂式多態(tài) 演算，包括和其它兩個系統(tǒng)之間的演算，包括和其它兩個系統(tǒng)之間的聯(lián)系，它的等式證明系統(tǒng)和歸約、多態(tài)聲明聯(lián)系，它的等式證明系統(tǒng)和歸約、多態(tài)聲明 非直謂式多態(tài)非直謂式多態(tài) 演算的縱覽演算的縱覽 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 類型表達式的分類類型表達式的分類7.1 引引 言言7.1.2 類型作為函數(shù)變元類型作為函數(shù)變元 簡單類型化簡單類型化 演算有某種明顯的缺點演算有某種明顯的缺點很多有計算意義且有用的表達式不是良類型的很多有計算意義且有用的表達式不是良類型的排序函

3、數(shù)：希望能應(yīng)用于許多不同類型的數(shù)據(jù)排序函數(shù)：希望能應(yīng)用于許多不同類型的數(shù)據(jù) Sort : (t t bool ) Arrayprt t Array prt t 多態(tài)函數(shù)多態(tài)函數(shù)變元的類型可以有多種不同的情況變元的類型可以有多種不同的情況通過拓展通過拓展 抽象到允許對類型進行抽象到允許對類型進行 抽象，可以把抽象，可以把 拓展到包括多態(tài)函數(shù)拓展到包括多態(tài)函數(shù)7.1 引引 言言 再以更簡潔一些的函數(shù)合成運算為例再以更簡潔一些的函數(shù)合成運算為例composenat, nat, nat f : nat nat. g: nat nat. x: nat.f (g x) composenat, nat na

4、t, nat f : (nat nat) nat. g: nat (nat nat). x: nat.f (g x)composer, s, t f : s t. g: r s. x: r.f (g x)compose r : T. s: T. t: T. composer, s, t7.1 引引 言言 考察考察compose r:T. s:T. t:T. composer, s, t對對T（類型的集合）（類型的集合）有幾種可能的解釋有幾種可能的解釋 類型應(yīng)用類型應(yīng)用compose nat nat nat = ( r:T. s:T. t:T. f :s t. g:r s. x:r. f (g

5、x) nat nat nat= f :nat nat. g:nat nat. x:nat. f (g x) compose的類型是什么？的類型是什么？7.1 引引 言言 以多態(tài)恒等函數(shù)為例以多態(tài)恒等函數(shù)為例Id t : T. x : t. x Id的定義域是的定義域是T，但但值域難以描述值域難以描述 一種表示：一種表示：Id : ( t :T t t) t :T t t是是無限積無限積 t T t t ： (nat nat) (bool bool) . . . (idnat nat, idbool bool, . . .)是該類型的一個值是該類型的一個值Id nat = x : nat. x

6、= idnat natId bool = x : bool. x = idbool bool代換僅在代換僅在Id的類型上完成，而不是在函數(shù)本身上的類型上完成，而不是在函數(shù)本身上完成完成7.1 引引 言言 以多態(tài)恒等函數(shù)為例以多態(tài)恒等函數(shù)為例Id t : T. x : t. x Id的定義域是的定義域是T，但但值域難以描述值域難以描述 一種表示：一種表示：Id : ( t :T t t) 另一種表示：另一種表示： Id : t: T. t t t: T. t t是所有下述函數(shù)構(gòu)成的類型：是所有下述函數(shù)構(gòu)成的類型：每個函數(shù)對所有的每個函數(shù)對所有的t:T，給出從給出從t 到到t 的一個映射的一個映射

7、下面先只考慮第一種表示法下面先只考慮第一種表示法7.1 引引 言言 對對T有三種自然的選擇有三種自然的選擇為多態(tài)函數(shù)引入類型后，必須決定這些類型怎樣為多態(tài)函數(shù)引入類型后，必須決定這些類型怎樣來適合現(xiàn)在的類型系統(tǒng)來適合現(xiàn)在的類型系統(tǒng)1、直謂式多態(tài)性、直謂式多態(tài)性 T僅含用僅含用、 和和 或或 及一組類型常量定義的類型及一組類型常量定義的類型 這是在已經(jīng)定義了這是在已經(jīng)定義了T的所有成員后才引入的所有成員后才引入T2、非直謂式多態(tài)性、非直謂式多態(tài)性 T還包含所有的多態(tài)類型（例如還包含所有的多態(tài)類型（例如 t: T. t t），），但不把但不把T本身作為一個類型本身作為一個類型7.1 引引 言言 對

8、對T有三種自然的選擇有三種自然的選擇為多態(tài)函數(shù)引入類型后，必須決定這些類型怎樣為多態(tài)函數(shù)引入類型后，必須決定這些類型怎樣來適合現(xiàn)在的類型系統(tǒng)來適合現(xiàn)在的類型系統(tǒng)1、直謂式多態(tài)性、直謂式多態(tài)性2、非直謂式多態(tài)性、非直謂式多態(tài)性3、type : type令令T包含所有的類型，包括它本身包含所有的類型，包括它本身從計算的觀點看，并非立即能看清楚：從計算的觀點看，并非立即能看清楚：引入引入“所有類型的類型所有類型的類型”后會引起什么錯誤后會引起什么錯誤7.1 引引 言言 三種多態(tài)性之間的簡單區(qū)別三種多態(tài)性之間的簡單區(qū)別1、直謂式多態(tài)性、直謂式多態(tài)性 Id僅能夠應(yīng)用于非多態(tài)類型僅能夠應(yīng)用于非多態(tài)類型，例

9、如例如nat 或或 (nat nat) Id (nat nat) = x : nat nat. x2. 非直謂式多態(tài)性非直謂式多態(tài)性 Id可以應(yīng)用到任何類型可以應(yīng)用到任何類型 Id ( t: T. t t) = x : ( t: T. t t). x不可能把每個多態(tài)不可能把每個多態(tài) 項都解釋成集合論的函數(shù)項都解釋成集合論的函數(shù)Id = , x: . x | T，其中序?qū)ζ渲行驅(qū)?( t: T. t t), x: ( t: T. t t). x 的第一元包含的第一元包含Id7.1 引引 言言 三種多態(tài)性之間的簡單區(qū)別三種多態(tài)性之間的簡單區(qū)別1、直謂式多態(tài)性、直謂式多態(tài)性 Id (nat nat)

10、 = x : nat nat. x2. 非直謂式多態(tài)性非直謂式多態(tài)性 Id ( t: T. t t) = x : ( t: T. t t). x3、type : typeId T = x:T. x(Id T): T T7.1 引引 言言 參數(shù)多態(tài)性和特定多態(tài)性參數(shù)多態(tài)性和特定多態(tài)性1、參數(shù)化多態(tài)性、參數(shù)化多態(tài)性 一個多態(tài)函數(shù)對任何類型都使用一個多態(tài)函數(shù)對任何類型都使用“本質(zhì)上一樣的本質(zhì)上一樣的算法算法”2、特定多態(tài)性、特定多態(tài)性 可以可以測試類型變元的值，根據(jù)它的類型類型選擇測試類型變元的值，根據(jù)它的類型類型選擇某個分支某個分支ad_hoc_compose r: T. s: T. t: T.

11、f : s t. g: r s. x: r. if Eq? s t then f (f (g x) else f (g x) 7.2 直謂式多態(tài)演算直謂式多態(tài)演算7.2.1 類型和項的語法類型和項的語法 的類型分成兩類的類型分成兩類 類型類型全域全域 U1“小小”全域全域 用用 構(gòu)造的多態(tài)類型構(gòu)造的多態(tài)類型 全域全域 U2 “大大”全域全域 各類表達式（上下文、類型表達式、項）的各類表達式（上下文、類型表達式、項）的語法各由一個斷言證明系統(tǒng)給出語法各由一個斷言證明系統(tǒng)給出 在在 中中將使用形式為將使用形式為 A: B的斷言的斷言 是上下文，指出每個變量的類型或全域是上下文，指出每個變量的類型或

12、全域 A是類型表達式，則是類型表達式，則B是是U1，U2 A是項，則是項，則B是是類型表達式類型表達式7.2 直謂式多態(tài)演算直謂式多態(tài)演算 良形上下文的公理和推理規(guī)則良形上下文的公理和推理規(guī)則 上下文是一個有序序列，它給變量以類型或全域上下文是一個有序序列，它給變量以類型或全域 = v1 : A1, , vk : Ak 每個每個Ai必須僅在假設(shè)必須僅在假設(shè)v1 : A1, , vi -1 : Ai1下就可證下就可證明為良形的明為良形的 可以使用公理和推理規(guī)則來將它形式化可以使用公理和推理規(guī)則來將它形式化 例：例： t : U1. x : t t. y: t. xy 確定確定xy類型時的上下文：

13、類型時的上下文：t : U1, x : t t, y: t 7.2 直謂式多態(tài)演算直謂式多態(tài)演算 良形上下文的公理和推理規(guī)則良形上下文的公理和推理規(guī)則 context (empty context) t不在不在 中中(U1 context) x不在不在 中中 (Ui type context) context , t : U1 context : Ui , x : context7.2 直謂式多態(tài)演算直謂式多態(tài)演算 良形上下文的公理和推理規(guī)則良形上下文的公理和推理規(guī)則 (var) (add var) 這兩條規(guī)則可用于多個類型系統(tǒng)這兩條規(guī)則可用于多個類型系統(tǒng) 第二條規(guī)則可用于推導(dǎo)第二條規(guī)則可用于

14、推導(dǎo)x:A, y:B x:A這樣的斷這樣的斷言言 , x : A context , x : A x : A A : B , x : C context , x : C A : B 7.2 直謂式多態(tài)演算直謂式多態(tài)演算 U1和和U2類型表達式的語法規(guī)則類型表達式的語法規(guī)則 U1的類型表達式由三個公理和推理規(guī)則給出的類型表達式由三個公理和推理規(guī)則給出 b: U1 (cst U1) （限制到（限制到U1的變量）的變量） (var) ( U1) : U1, : U1 : U1 , x : A context , x : A x : A 7.2 直謂式多態(tài)演算直謂式多態(tài)演算 第二第二個全域個全域U2包

15、含類型包含類型U1和多態(tài)函數(shù)類型和多態(tài)函數(shù)類型 (U1 U2) ( U2) 雖然有雖然有屬于屬于U2的類型表達式，但是沒有的類型表達式，但是沒有U2的變量的變量 如果如果加了變量和加了變量和 抽象到抽象到U2上，它就會導(dǎo)致形式上，它就會導(dǎo)致形式是是 t:U2. 的類型，它將屬于第三個全域的類型，它將屬于第三個全域U3 , t : U1 : U2 ( t : U1. ) : U2 : U1 : U27.2 直謂式多態(tài)演算直謂式多態(tài)演算 例例證明證明 t: U1.t t是屬于是屬于U2的良形的類型表達式的良形的類型表達式 context由由(empty context)t: U1 context由

16、由(U1 context)t: U1 t: U1(var)t: U1 t t: U1(U1)t: U1 t t: U2(U1 U2) ( t: U1.t t) : U2( U2)7.2 直謂式多態(tài)演算直謂式多態(tài)演算 項的語法項的語法（先給（先給 , 預(yù)備預(yù)備項的文法項的文法 ）M := b | x | x: . M | MM | t: U1.M | M 定型規(guī)則用來判斷項是否為良類型的定型規(guī)則用來判斷項是否為良類型的 (var) (add var) , x : A context , x : A x : A A : B , x : C context , x : C A : B 7.2 直謂式

17、多態(tài)演算直謂式多態(tài)演算 c: (cst) (Intro) (Elim)任何任何 項（可能包括了用類型變量取代類型常項（可能包括了用類型變量取代類型常量）都是量）都是 , 的項的項 , x : M : : U1 : U1 ( x : . M) : M : N : MN : 7.2 直謂式多態(tài)演算直謂式多態(tài)演算 ( Intro) ( Elim) (type eq)在類型在類型 t: U1. 中將省略中將省略t所屬的全域所屬的全域U1，寫成寫成 t. , t : U1 M : ( t : U1. M) : ( t: U1. ) M : ( t: U1. ) : U1 M : /t M : 1 1 =

18、 2 : Ui M : 27.2 直謂式多態(tài)演算直謂式多態(tài)演算 ( Intro) ( Elim) (type eq)若若 M 是從公理和是從公理和 , 定型規(guī)則可推導(dǎo)，則定型規(guī)則可推導(dǎo)，則說，說，M在上下文在上下文 中是類型為中是類型為 的的 , 項項 , t : U1 M : ( t : U1. M) : ( t: U1. ) M : ( t: U1. ) : U1 M : /t M : 1 1 = 2 : Ui M : 27.2 直謂式多態(tài)演算直謂式多態(tài)演算 規(guī)則規(guī)則U1 U2 和規(guī)則和規(guī)則U1 :U21、規(guī)則、規(guī)則U1 U2 可以只用一個可以只用一個 形成規(guī)則形成規(guī)則 U1 U2沒有在該

19、語言上設(shè)置任何額外的語義限制沒有在該語言上設(shè)置任何額外的語義限制2、規(guī)則、規(guī)則U1 :U2 因為因為 在任意在任意U2類型上無任何有意義的運算，類型上無任何有意義的運算，因此看起來沒有任何理由取因此看起來沒有任何理由取U1 :U2 在在 的非直謂式拓展中，加入的非直謂式拓展中，加入U1 :U2規(guī)則將是規(guī)則將是一個合理的語言設(shè)計一個合理的語言設(shè)計7.2 直謂式多態(tài)演算直謂式多態(tài)演算7.2.2 和其它形式多態(tài)性的比較和其它形式多態(tài)性的比較 其它兩種演算都可看成直謂式多態(tài)演算的特其它兩種演算都可看成直謂式多態(tài)演算的特殊情況殊情況 非直謂非直謂式類型化式類型化 演算演算強加強加“全域等式全域等式”U1

20、 = U2 “type: type”演算演算強加了等式強加了等式U1 = U2和條件和條件U1:U27.2 直謂式多態(tài)演算直謂式多態(tài)演算 非直謂式演算非直謂式演算 在在 , 中已經(jīng)有中已經(jīng)有U1 U2, 加入逆向包含加入逆向包含U2 U1來獲得來獲得U1 = U2(U2 U1) : U2 : U17.2 直謂式多態(tài)演算直謂式多態(tài)演算 例例 證明語法證明語法斷言斷言 (I ( t.tt)I: t.tt， 其中其中I t:U1. x:t.x 由（由（ , 的定型規(guī)則的定型規(guī)則） I: ( t.tt)，其中其中( t.tt):U2 ( t.tt):U1 由由(U2 U1) I ( t.tt) : (

21、 t.tt) ( t.tt) 由由( Elim) ) I ( t.tt) I : ( t.tt) 由由( Elim) )7.2 直謂式多態(tài)演算直謂式多態(tài)演算 type : type加上加上U2 = U1和和U1:U2 對前者加語法規(guī)則（對前者加語法規(guī)則（U2 U1） 對后者加公理對后者加公理 U1:U2 (U1:U2) 可以寫出非常復(fù)雜的類型函數(shù)可以寫出非常復(fù)雜的類型函數(shù) 一個有效的一個有效的編譯時的類型檢查算法是不可能的編譯時的類型檢查算法是不可能的 7.2 直謂式多態(tài)演算直謂式多態(tài)演算 的簡化語法的簡化語法 第一個約定是使用兩類變量第一個約定是使用兩類變量項變量項變量x, y, z, 類型

22、變量類型變量r, t, s, 代表代表U1的類型的類型 第二個第二個約定約定對對U1的類型表達式使用的類型表達式使用 , , 1, 對對U2的類型表達式使用的類型表達式使用 , , 1, U1和和U2的類型表達式的語法的類型表達式的語法 := t | b | := | t. 7.2 直謂式多態(tài)演算直謂式多態(tài)演算 上下文上下文 = x1: 1, , xk: k不再需要類型變量不再需要類型變量 語法簡化后的規(guī)則語法簡化后的規(guī)則 x: x: (var) c: (cst) (add var) (Intro) M : , x : M : , x : M : ( x : . M) : 7.2 直謂式多態(tài)演

23、算直謂式多態(tài)演算 (Elim) （t在在 中不是自由的）中不是自由的） ( Intro) ( Elim) M : N : MN : M : t . M : t. M : t. M : /t 7.2 直謂式多態(tài)演算直謂式多態(tài)演算7.2.3 等式證明系統(tǒng)和歸約等式證明系統(tǒng)和歸約 , 等式的形式是等式的形式是 M = N: ，其中其中M和和N都是類型都是類型 的項的項 , , 的等式推理系統(tǒng)是的等式推理系統(tǒng)是 證明系統(tǒng)的一個拓證明系統(tǒng)的一個拓展，增加了一些公理和推理規(guī)則展，增加了一些公理和推理規(guī)則 該證明系統(tǒng)包含該證明系統(tǒng)包含 自反公理，對稱和傳遞規(guī)則自反公理，對稱和傳遞規(guī)則 同項形成規(guī)則對應(yīng)的推理

24、規(guī)則同項形成規(guī)則對應(yīng)的推理規(guī)則 同普通的同普通的 抽象和應(yīng)用對應(yīng)的推理規(guī)則抽象和應(yīng)用對應(yīng)的推理規(guī)則7.2 直謂式多態(tài)演算直謂式多態(tài)演算 增加了類型抽象和類型應(yīng)用公理增加了類型抽象和類型應(yīng)用公理 t. M = s. s tM : t. ( ) ( t. M) = tM : t ( ) t. Mt = M : t. t在在M中沒有自由出現(xiàn)中沒有自由出現(xiàn) ( ) 7.2 直謂式多態(tài)演算直謂式多態(tài)演算 對類型抽象和應(yīng)用，還有下面的同余規(guī)則對類型抽象和應(yīng)用，還有下面的同余規(guī)則 ( ( ) ) ( ) M = N : t. M = t. N : t. M = N : t. M = N : /t 7.2 直

25、謂式多態(tài)演算直謂式多態(tài)演算 這些等式公理可以從左向右定向這些等式公理可以從左向右定向, ,得到一個歸得到一個歸約系統(tǒng)約系統(tǒng) 例例 ( t. x: t.x) y ( x: .x) y y 可以證明歸約多態(tài)可以證明歸約多態(tài) , , 項的合流性和強范式項的合流性和強范式化化 命題命題7.1 歸約保項的類型歸約保項的類型7.2 直謂式多態(tài)演算直謂式多態(tài)演算7.2.4 ML風(fēng)格的多態(tài)聲明風(fēng)格的多態(tài)聲明 ML的類型系統(tǒng)可看成的類型系統(tǒng)可看成 的一個拓展的一個拓展 主要區(qū)別是，主要區(qū)別是，ML包含多態(tài)的包含多態(tài)的let聲明聲明 通過調(diào)查多態(tài)函數(shù)在通過調(diào)查多態(tài)函數(shù)在 中的使用來啟發(fā)這種中的使用來啟發(fā)這種let

26、聲聲明的形式明的形式 可以寫出可以寫出Id ( t. x : t.x) : t. t t Id nat 3和和 Id bool true都是良類型的項都是良類型的項 寫不出寫不出( f :( t.t t). f nat 3f bool true) t. x:t.x因為因為 t. t t是是U2的一個類型的一個類型7.2 直謂式多態(tài)演算直謂式多態(tài)演算 對于對于U2類型，使用一種非常有限的變量約束類型，使用一種非常有限的變量約束形式，對需要多態(tài)函數(shù)的許多實際程序設(shè)計形式，對需要多態(tài)函數(shù)的許多實際程序設(shè)計來說已經(jīng)足夠了來說已經(jīng)足夠了 這種方式利用這種方式利用let x: = N in M和和( x:

27、 .M)N在在語義上都等價于語義上都等價于N/xM，而定型卻不一樣而定型卻不一樣7.2 直謂式多態(tài)演算直謂式多態(tài)演算 對于對于U2類型，使用一種非常有限的變量約束類型，使用一種非常有限的變量約束形式，對需要多態(tài)函數(shù)的許多實際程序設(shè)計形式，對需要多態(tài)函數(shù)的許多實際程序設(shè)計來說已經(jīng)足夠了來說已經(jīng)足夠了 ML的方式的方式 , let使用使用 let x : = N in M 表達式，增加規(guī)則和公理：表達式，增加規(guī)則和公理： (let) (let x: = N in M) = N/xM: (let)eq , x : M : N : (let x : = N in M) : 7.2 直謂式多態(tài)演算直謂式

28、多態(tài)演算 例例 考慮考慮compose: r. s. t. 其中其中 = (st) (rs) (rt) compose在一個表達式中使用多次在一個表達式中使用多次，讓其函數(shù)體讓其函數(shù)體僅寫一次僅寫一次 let x: ( r. s. t. ) = compose in M，則，則 ( let x: ( r. s. t. ) = compose in M) = compose/xM: 避免寫下面的表達式，并能達到同樣的效果避免寫下面的表達式，并能達到同樣的效果( f :( t.t t). f nat 3f bool true) t. x:t.x7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算7.3.1 引

29、言引言 非直謂式多非直謂式多態(tài)態(tài) 演算忽略直謂式演算忽略直謂式 的全域的全域U1和和U2的區(qū)別的區(qū)別 由所有類型的一個聚集由所有類型的一個聚集T來代替來代替U1和和U2 用用 表示，以區(qū)別直謂式系統(tǒng)表示，以區(qū)別直謂式系統(tǒng) 類型由文法類型由文法 := b | t | | t. 定義，無須用公理和推理規(guī)則給出定義，無須用公理和推理規(guī)則給出 7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算 類型表達式的文法類型表達式的文法 := b | t | | t. 項的形成依據(jù)項的形成依據(jù)7.2.2節(jié)的變量公理節(jié)的變量公理(var)、常量公理常量公理(cst)、增加自增加自由變量類型假設(shè)的規(guī)則由變量類型假設(shè)的規(guī)則(a

30、dd var)、規(guī)則規(guī)則( Intro)、規(guī)則規(guī)則( Elim)、規(guī)則規(guī)則( Intro)和規(guī)則和規(guī)則( Elim)這些規(guī)則中的這些規(guī)則中的 由由 代替并且對有關(guān)的類型全域代替并且對有關(guān)的類型全域沒有限制沒有限制7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算 非直謂演算可能是最廣泛研究的一種多態(tài)性非直謂演算可能是最廣泛研究的一種多態(tài)性1、其語法的簡單性、其語法的簡單性 該語言語法上比該語言語法上比 簡單，因為沒有全域的限制簡單，因為沒有全域的限制 但是但是證明它的強范式性非常困難證明它的強范式性非常困難2、語義的復(fù)雜性、語義的復(fù)雜性 想提供直觀和數(shù)學(xué)嚴(yán)格的語義，本質(zhì)上很困難想提供直觀和數(shù)學(xué)嚴(yán)格的語義

31、，本質(zhì)上很困難 多態(tài)恒等函數(shù)多態(tài)恒等函數(shù)可應(yīng)用到它自己的類型可應(yīng)用到它自己的類型，造成了不造成了不可能把這樣的類型解釋成普通集合論函數(shù)的集合可能把這樣的類型解釋成普通集合論函數(shù)的集合Id = , x: . x | T，其中序?qū)ζ渲行驅(qū)?( t: T. t t), x: ( t: T. t t). x 的第一元包含的第一元包含Id7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算 非直謂演算可能是最廣泛研究的一種多態(tài)性非直謂演算可能是最廣泛研究的一種多態(tài)性3、編程的靈活性、編程的靈活性 提供了一提供了一個非常靈活的多態(tài)類型系統(tǒng)，象個非常靈活的多態(tài)類型系統(tǒng)，象Ada、CLU和和ML等語言的多態(tài)性特征都可以看

32、成是作等語言的多態(tài)性特征都可以看成是作了某種限制的了某種限制的 多態(tài)性多態(tài)性 可以可以用用 中的中的 抽象來模仿抽象來模仿ML的的let let x: t. = M in N: （ ML方式）方式）它是項它是項 ( x: t. .N)M: 的一種語法美化的一種語法美化 7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算7.3.2 非直謂式多態(tài)非直謂式多態(tài) 演算的表達能力演算的表達能力給出一個例子來展示非直謂式多態(tài)給出一個例子來展示非直謂式多態(tài) 演算的表演算的表達能力達能力在二階在二階Peano算術(shù)中算術(shù)中 可證明為全函數(shù)的遞歸函數(shù)恰好是在非直謂式可證明為全函數(shù)的遞歸函數(shù)恰好是在非直謂式多態(tài)多態(tài) 演算中可

33、以定義的數(shù)值函數(shù)演算中可以定義的數(shù)值函數(shù) 這是多態(tài)這是多態(tài) 演算和二階邏輯的證明論之間的聯(lián)演算和二階邏輯的證明論之間的聯(lián)系的一部分系的一部分在此僅概述數(shù)值函數(shù)的某些表示方面的內(nèi)容在此僅概述數(shù)值函數(shù)的某些表示方面的內(nèi)容7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算 在在無無類型常量的純類型常量的純 中，自然數(shù)類型中，自然數(shù)類型的的一一種自然選擇種自然選擇 若有常量若有常量zero:nat和和succ:natnat，則可以用表達則可以用表達式式succ(succ(succ zero) )表示自然數(shù)表示自然數(shù)n 在純在純 中，沒有常量中，沒有常量zero和和succ，但是可以把這但是可以把這些符號當(dāng)作變量

34、看待，并且對它們進行些符號當(dāng)作變量看待，并且對它們進行 抽象抽象 zero:nat. succ:natnat.succ(succ(succ zero)7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算 類型類型名名nat是任意選擇的，把這個符號也當(dāng)作變量是任意選擇的，把這個符號也當(dāng)作變量看待，并且對它進行看待，并且對它進行 抽象抽象 nat. zero:nat. succ:natnat.succ(succ(succ zero) 通常用通常用更簡單的變量名寫出，作為自然數(shù)的一種更簡單的變量名寫出，作為自然數(shù)的一種有用表示有用表示( (Church數(shù)碼數(shù)碼) )n t. f : t t. x : t. f

35、nx 所有所有的的Church數(shù)碼都具有類型數(shù)碼都具有類型nat t.(t t) t t7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算 多態(tài)多態(tài)Church數(shù)碼上的加法和乘法運算是合成數(shù)碼上的加法和乘法運算是合成函數(shù)的形式函數(shù)的形式 mult x:nat. y:nat. t. f: tt.x t (y t f) add x:nat. y:nat. t. f: tt. z:t.x t f (y t f z) 7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算mult 2 3 ( x:nat. y:nat. t. f: tt.x t (y t f)( t. f : t t. x : t. f 2x) ( t. f

36、 : t t. x : t. f 3x)= t. f: tt. ( t. f : t t. x : t. f 2x) t ( t. f : t t. x : t. f 3x) t f)= t. f: tt. ( t. f : t t. x : t. f 2x) t ( x : t. f 3x)= t. f: tt. ( x : t. ( x : t. f 3x) ( x : t. f 3x) x)= t. f: tt. ( x : t. ( x : t. f 3x) (f 3x)= t. f: t t. x : t. f 6x 67.3 非直謂式多態(tài)演算非直謂式多態(tài)演算 還可以用一個正好帶兩個

37、范式的類型來表示還可以用一個正好帶兩個范式的類型來表示布爾值布爾值 true t. x:t. y:t.x false t. x:t. y:t.y bool t.ttt zero? x:nat.x bool ( x:bool.false) true7.3 非直謂式多態(tài)演算非直謂式多態(tài)演算7.3.3 歸約的終止性歸約的終止性略去不介紹略去不介紹7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 數(shù)據(jù)抽象以及相應(yīng)的程序規(guī)范和模塊性的概數(shù)據(jù)抽象以及相應(yīng)的程序規(guī)范和模塊性的概念可能是二十世紀(jì)七十年代有關(guān)程序設(shè)計語念可能是二十世紀(jì)七十年代有關(guān)程序設(shè)計語言最有影響的研究言最有影響的研究 抽象數(shù)據(jù)類型的聲明，作為一

38、種支持?jǐn)?shù)據(jù)抽抽象數(shù)據(jù)類型的聲明，作為一種支持?jǐn)?shù)據(jù)抽象的語言機制，已出現(xiàn)在一些程序設(shè)計語言象的語言機制，已出現(xiàn)在一些程序設(shè)計語言中，包括中，包括Ada、Clu和和ML 本節(jié)本節(jié)調(diào)查抽象數(shù)據(jù)類型聲明的一種一般形式調(diào)查抽象數(shù)據(jù)類型聲明的一種一般形式7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 形式為形式為abstype t with x1: 1, , xk: k is , M1, , Mk in N的聲明描述抽象類型的聲明描述抽象類型t例例abstype stream withs: stream,first: stream nat,rest: streamstreamis , M1, M2, M3

39、inN7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 使用笛卡兒積，可以把任何抽象數(shù)據(jù)類型聲使用笛卡兒積，可以把任何抽象數(shù)據(jù)類型聲明寫成明寫成abstype t with x: is , M in N的形式的形式 抽象數(shù)據(jù)類型聲明可以加到直謂式或非直謂抽象數(shù)據(jù)類型聲明可以加到直謂式或非直謂式語言中式語言中 分別考慮抽象數(shù)據(jù)類型聲明和數(shù)據(jù)類型實現(xiàn)分別考慮抽象數(shù)據(jù)類型聲明和數(shù)據(jù)類型實現(xiàn) 拓展類型表達式的語法，以包含存在類型拓展類型表達式的語法，以包含存在類型 := | t. 存在類型用于抽象數(shù)據(jù)類型的實現(xiàn)存在類型用于抽象數(shù)據(jù)類型的實現(xiàn) 存在類型存在類型 t. 的每個元素由一個類型的每個元素由一個類型

40、 和類型和類型 /t 的一個元素組成的一個元素組成 7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 例：例：stream的實現(xiàn)總有類型的實現(xiàn)總有類型 t. (t (t nat) (t t) 抽象數(shù)據(jù)類型的實現(xiàn)將以抽象數(shù)據(jù)類型的實現(xiàn)將以 t = , M: 的形式寫的形式寫出，其中出，其中 t = 表示在該表達式的剩余部分將表示在該表達式的剩余部分將t約束到約束到 稱為稱為t的表示類型的表示類型7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 存在類型的公理和推理規(guī)則存在類型的公理和推理規(guī)則 ( Intro) t = , M : = s = , M : s/t : t. s在在 中不是自由的中不是自由的

41、下面規(guī)則允許把名字約束到數(shù)據(jù)類型實現(xiàn)的類型下面規(guī)則允許把名字約束到數(shù)據(jù)類型實現(xiàn)的類型成分和值成分成分和值成分 ( Elim) M : /t t = , M : : t. M : t. , , x : N : (abstype t with x: is M in N) : 7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 作為記號上的方便，把多于一個運算的聲明作為記號上的方便，把多于一個運算的聲明作為一種語法美化：作為一種語法美化：abstype t with x1: 1, , xn: n is M in N abstype t with y: 1 n is M in Proj1 y, , Proj

42、n y/x1, , xnN nn7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型例例: abstype cmplx withcreate: real real cmplx,plus: cmplx cmplx cmplx,re: cmplx realim: cmplx realis t = real real, C, P, R, I : (real real t) (t t t) (t real) (t real) inN7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 C, P, R, I : 可以寫成：可以寫成：C = p: real real. pP = z: real real, w: real

43、 real . Proj1 z + Proj1 w, Proj2 z + Proj2 w R = z: real real. Proj1 zI = z: real real. Proj2 z7.4 數(shù)據(jù)抽象和存在類型數(shù)據(jù)抽象和存在類型 abstype的主要等式公理的主要等式公理 (abstype t with x: is t = , M: in N) = M/x /tN: ( ) ( x .M)N =N/xM : ( ) abstype t with x: is M in N =abstype s with y: s/t is M in y/xs/tN: ( ) x .M = y .y/xM

44、: ,其中其中y FV(M) ( ) abstype t with x: is y in t = t, x: = y: t. ( ) x .(Mx) =M : , 其中其中x FV(M) ( )7.5 類型表達式的分類類型表達式的分類7.5.1 類型表達式的種類類型表達式的種類 （1）7.2節(jié)把類型表達式分成兩個層次節(jié)把類型表達式分成兩個層次 普通類型和多態(tài)類型普通類型和多態(tài)類型 在給出一些簡化約定的情況下在給出一些簡化約定的情況下，類型表達式類型表達式可用可用文法文法分成同樣的兩個層次分成同樣的兩個層次 由于除了類型常量和類型變量外，只涉及函數(shù)類由于除了類型常量和類型變量外，只涉及函數(shù)類型型

45、，使得用，使得用文法推出的類型表達式都是良形的文法推出的類型表達式都是良形的 7.5 類型表達式的分類類型表達式的分類（2）類型表達式分成小全域和大全域，不足類型表達式分成小全域和大全域，不足以解決類型表達式是否以解決類型表達式是否為為良形的問題良形的問題 在在 演算上再增加積類型或和類型時演算上再增加積類型或和類型時 若類型變量若類型變量t代表二元積類型，則代表二元積類型，則fst(t)（?。ㄈ的第的第一元）是良形的類型表達式，否則一元）是良形的類型表達式，否則fst(t)不是良形不是良形的類型表達式的類型表達式 這時這時良形的類型表達式很難用良形的類型表達式很難用7.2節(jié)的文法形式表節(jié)的

46、文法形式表示示 7.5 類型表達式的分類類型表達式的分類（3）需要考慮類型表達式新的分類方式）需要考慮類型表達式新的分類方式 例如例如，所有的函數(shù)類型、所有的表類型、所有的所有的函數(shù)類型、所有的表類型、所有的二叉樹類型等二叉樹類型等，并且對類型表達式的量化是以這并且對類型表達式的量化是以這樣的類型族為論域樣的類型族為論域 可以通過豐富語言結(jié)構(gòu)來解決這些問題可以通過豐富語言結(jié)構(gòu)來解決這些問題用用類型對項進行分類類型對項進行分類用較高層次的種類用較高層次的種類（kind）來對類型進行分類來對類型進行分類當(dāng)前很多研究工作中的類型系統(tǒng)都是按這種思當(dāng)前很多研究工作中的類型系統(tǒng)都是按這種思路來設(shè)計路來設(shè)計

47、7.5 類型表達式的分類類型表達式的分類 , 演算有項、類型和種類三種語法范疇演算有項、類型和種類三種語法范疇語法范疇語法范疇項目項目具體形式具體形式種類種類 := Type | | 類型類型 := b | t | | | fst( ) | snd( ) | t: . | 項項M := c | x | x: .M | MM | M, N | Proj1M | Proj2M | t: .M | M 種類文法產(chǎn)生的任何種類表達式都是良形的種類文法產(chǎn)生的任何種類表達式都是良形的 符號符號和和 在這里是重載的在這里是重載的 基本類型和普通函數(shù)類型歸到基本類型和普通函數(shù)類型歸到Type種類種類7.5 類

48、型表達式的分類類型表達式的分類 , 演算有項、類型和種類三種語法范疇演算有項、類型和種類三種語法范疇語法范疇語法范疇項目項目具體形式具體形式種類種類 := Type | | 類型類型 := b | t | | | fst( ) | snd( ) | t: . | 項項M := c | x | x: .M | MM | M, N | Proj1M | Proj2M | t: .M | M 任意兩個類型，它們的積屬于某個積種類任意兩個類型，它們的積屬于某個積種類 1 2 由由 t: . 表示的類型上的函數(shù)屬于某個函數(shù)種類表示的類型上的函數(shù)屬于某個函數(shù)種類 7.5 類型表達式的分類類型表達式的分類7.5.2 類型表達式的定類與相等類型表達式的定類與相等 類型表達式的定類（類型表達式的定類（kinding）斷言斷言 斷言的形式為斷言的形式為 : ，其中，其中定類上下文定類上下文 是形是形式為式為 = t1 : 1, , tn : n 其中其中dom( ) = t1, , tn類似于項的定型斷言類似于項的定型斷言 M : 7.5 類型表達式的