第7章多态性精选PPT.ppt

《第7章多态性精选PPT.ppt》由会员分享，可在线阅读，更多相关《第7章多态性精选PPT.ppt（75页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、第7章多态性第1页，本讲稿共75页7.1 引引 言言本章的主要内容本章的主要内容多态类型系统的语法，包括直谓式的，非直谓式多态类型系统的语法，包括直谓式的，非直谓式的和的和type:type版本版本直谓式多态直谓式多态 演算，包括和其它两个系统之间的演算，包括和其它两个系统之间的联系，它的等式证明系统和归约、多态声明联系，它的等式证明系统和归约、多态声明非直谓式多态非直谓式多态 演算的纵览演算的纵览数据抽象和存在类型数据抽象和存在类型类型表达式的分类类型表达式的分类第2页，本讲稿共75页7.1 引引 言言7.1.2 类型作为函数变元类型作为函数变元简单类型化简单类型化 演算有某种明显的缺点演算

2、有某种明显的缺点很多有计算意义且有用的表达式不是良类型的很多有计算意义且有用的表达式不是良类型的排序函数：希望能应用于许多不同类型的数据排序函数：希望能应用于许多不同类型的数据 Sort:(t t bool)Arrayprt t Array prt t多态函数多态函数变元的类型可以有多种不同的情况变元的类型可以有多种不同的情况通过拓展通过拓展 抽象到允许对类型进行抽象到允许对类型进行 抽象，可以把抽象，可以把 拓展到包括多态函数拓展到包括多态函数第3页，本讲稿共75页7.1 引引 言言再以更简洁一些的函数合成运算为例再以更简洁一些的函数合成运算为例composenat,nat,nat f:na

3、t nat.g:nat nat.x:nat.f(g x)composenat,nat nat,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,t第4页，本讲稿共75页7.1 引引 言言考察考察compose r:T.s:T.t:T.composer,s,t对对T（类型的集合）（类型的集合）有几种可能的解释有几种可能的解释类型应用类型应用compose nat nat nat=(r:T.s:T.t:T.f:s t.g:r

4、 s.x:r.f(g x)nat nat nat=f:nat nat.g:nat nat.x:nat.f(g x)compose的类型是什么？的类型是什么？第5页，本讲稿共75页7.1 引引 言言以多态恒等函数为例以多态恒等函数为例Id t:T.x:t.xId的定义域是的定义域是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=idnat natId bool=x:b

5、ool.x=idbool bool代换仅在代换仅在Id的类型上完成，而不是在函数本身上的类型上完成，而不是在函数本身上完成完成第6页，本讲稿共75页7.1 引引 言言以多态恒等函数为例以多态恒等函数为例Id t:T.x:t.xId的定义域是的定义域是T，但，但值域难以描述值域难以描述一种表示：一种表示：Id:(t:T t t)另一种表示：另一种表示：Id:t:T.t t t:T.t t是所有下述函数构成的类型：是所有下述函数构成的类型：每个函数对所有的每个函数对所有的t:T，给出从，给出从t 到到t 的一个映射的一个映射下面先只考虑第一种表示法下面先只考虑第一种表示法第7页，本讲稿共75页7.

6、1 引引 言言对对T有三种自然的选择有三种自然的选择为多态函数引入类型后，必须决定这些类型怎样为多态函数引入类型后，必须决定这些类型怎样来适合现在的类型系统来适合现在的类型系统1、直谓式多态性、直谓式多态性T仅含用仅含用、和和 或或 及一组类型常量定义的类型及一组类型常量定义的类型这是在已经定义了这是在已经定义了T的所有成员后才引入的所有成员后才引入T2、非直谓式多态性、非直谓式多态性T还包含所有的多态类型（例如还包含所有的多态类型（例如 t:T.t t），但），但不把不把T本身作为一个类型本身作为一个类型第8页，本讲稿共75页7.1 引引 言言对对T有三种自然的选择有三种自然的选择为多态函数

7、引入类型后，必须决定这些类型怎样为多态函数引入类型后，必须决定这些类型怎样来适合现在的类型系统来适合现在的类型系统1、直谓式多态性、直谓式多态性2、非直谓式多态性、非直谓式多态性3、type:type令令T包含所有的类型，包括它本身包含所有的类型，包括它本身从计算的观点看，并非立即能看清楚：从计算的观点看，并非立即能看清楚：引入引入“所有类型的类型所有类型的类型”后会引起什么错误后会引起什么错误第9页，本讲稿共75页7.1 引引 言言三种多态性之间的简单区别三种多态性之间的简单区别1、直谓式多态性、直谓式多态性Id仅能够应用于非多态类型仅能够应用于非多态类型，例如例如nat 或或 (nat n

8、at)Id(nat nat)=x:nat nat.x2.非直谓式多态性非直谓式多态性Id可以应用到任何类型可以应用到任何类型Id(t:T.t t)=x:(t:T.t t).x不可能把每个多态不可能把每个多态 项都解释成集合论的函数项都解释成集合论的函数Id=,x:.x|T，其中序对其中序对(t:T.t t),x:(t:T.t t).x 的第一元包含的第一元包含Id第10页，本讲稿共75页7.1 引引 言言三种多态性之间的简单区别三种多态性之间的简单区别1、直谓式多态性、直谓式多态性Id(nat nat)=x:nat nat.x2.非直谓式多态性非直谓式多态性Id(t:T.t t)=x:(t:T

9、.t t).x3、type:typeId T=x:T.x(Id T):T T第11页，本讲稿共75页7.1 引引 言言参数多态性和特定多态性参数多态性和特定多态性1、参数化多态性、参数化多态性一个多态函数对任何类型都使用一个多态函数对任何类型都使用“本质上一样的本质上一样的算法算法”2、特定多态性、特定多态性可以可以测试类型变元的值，根据它的类型类型选择测试类型变元的值，根据它的类型类型选择某个分支某个分支ad_hoc_compose r:T.s:T.t:T.f:s t.g:r s.x:r.if Eq?s t then f(f(g x)else f(g x)第12页，本讲稿共75页7.2 直谓

10、式多态演算直谓式多态演算7.2.1 类型和项的语法类型和项的语法 的类型分成两类的类型分成两类 类型类型全域全域 U1“小小”全域全域用用 构造的多态类型构造的多态类型 全域全域 U2 “大大”全域全域各类表达式（上下文、类型表达式、项）的各类表达式（上下文、类型表达式、项）的语法各由一个断言证明系统给出语法各由一个断言证明系统给出在在 中中将使用形式为将使用形式为 A:B的断言的断言 是上下文，指出每个变量的类型或全域是上下文，指出每个变量的类型或全域A是类型表达式，则是类型表达式，则B是是U1，U2A是项，则是项，则B是是类型表达式类型表达式第13页，本讲稿共75页7.2 直谓式多态演算直

11、谓式多态演算良形上下文的公理和推理规则良形上下文的公理和推理规则上下文是一个有序序列，它给变量以类型或全域上下文是一个有序序列，它给变量以类型或全域 =v1:A1,vk:Ak每个每个Ai必须仅在假设必须仅在假设v1:A1,vi-1:Ai1下就可下就可证明为良形的证明为良形的可以使用公理和推理规则来将它形式化可以使用公理和推理规则来将它形式化例：例：t:U1.x:t t.y:t.xy 确定确定xy类型时的上下文：类型时的上下文：t:U1,x:t t,y:t 第14页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算良形上下文的公理和推理规则良形上下文的公理和推理规则 context (empt

12、y context)t不在不在 中中(U1 context)x不在不在 中中 (Ui type context)context ,t:U1 context :Ui ,x:context第15页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算良形上下文的公理和推理规则良形上下文的公理和推理规则 (var)(add var)这两条规则可用于多个类型系统这两条规则可用于多个类型系统 第二条规则可用于推导第二条规则可用于推导x:A,y:B x:A这样的断言这样的断言,x:A context ,x:A x:A A:B ,x:C context ,x:C A:B 第16页，本讲稿共75页7.2 直谓式

13、多态演算直谓式多态演算U1和和U2类型表达式的语法规则类型表达式的语法规则U1的类型表达式由三个公理和推理规则给出的类型表达式由三个公理和推理规则给出 b:U1 (cst U1)（限制到（限制到U1的变量）的变量）(var)(U1):U1,:U1 :U1 ,x:A context ,x:A x:A 第17页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算第二第二个全域个全域U2包含类型包含类型U1和多态函数类型和多态函数类型 (U1 U2)(U2)虽然有虽然有属于属于U2的类型表达式，但是没有的类型表达式，但是没有U2的变量的变量如果如果加了变量和加了变量和 抽象到抽象到U2上，它就会导致

14、形式上，它就会导致形式是是 t:U2.的类型，它将属于第三个全域的类型，它将属于第三个全域U3,t:U1 :U2 (t:U1.):U2 :U1 :U2第18页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算例例证明证明 t:U1.t t是属于是属于U2的良形的类型表达式的良形的类型表达式 context由由(empty context)t:U1 context由由(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)第19页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算项的语法项的语法（

15、先给（先给,预备预备项的文法项的文法）M:=b|x|x:.M|MM|t:U1.M|M 定型规则用来判断项是否为良类型的定型规则用来判断项是否为良类型的(var)(add var),x:A context ,x:A x:A A:B ,x:C context ,x:C A:B 第20页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算 c:(cst)(Intro)(Elim)任何任何 项（可能包括了用类型变量取代类型常量）都项（可能包括了用类型变量取代类型常量）都是是,的项的项,x:M:U1 :U1 (x:.M):M:N:MN:第21页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算 (In

16、tro)(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=2:Ui M:2第22页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算 (Intro)(Elim)(type eq)若若 M 是从公理和是从公理和,定型规则可推导，则定型规则可推导，则说，说，M在上下文在上下文 中是类型为中是类型为 的的,项项,t:U1 M:(t:U1.M):(t:U1.)M:(t:U1.):U1 M :/t M:1 1=2:Ui M:2第23页，本讲稿

17、共75页7.2 直谓式多态演算直谓式多态演算规则规则U1 U2 和规则和规则U1:U21、规则、规则U1 U2可以只用一个可以只用一个 形成规则形成规则U1 U2没有在该语言上设置任何额外的语义限制没有在该语言上设置任何额外的语义限制2、规则、规则U1:U2因为因为 在任意在任意U2类型上无任何有意义的运算，类型上无任何有意义的运算，因此看起来没有任何理由取因此看起来没有任何理由取U1:U2在在 的非直谓式拓展中，加入的非直谓式拓展中，加入U1:U2规则将是一规则将是一个合理的语言设计个合理的语言设计第24页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算7.2.2 和其它形式多态性的比较

18、和其它形式多态性的比较其它两种演算都可看成直谓式多态演算的特其它两种演算都可看成直谓式多态演算的特殊情况殊情况非直谓非直谓式类型化式类型化 演算演算强加强加“全域等式全域等式”U1=U2“type:type”演算演算强加了等式强加了等式U1=U2和条件和条件U1:U2第25页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算非直谓式演算非直谓式演算在在,中已经有中已经有U1 U2,加入逆向包含加入逆向包含U2 U1来获得来获得U1=U2(U2 U1):U2 :U1第26页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算例例证明语法证明语法断言断言 (I(t.tt)I:t.tt，其中其中I

19、 t:U1.x:t.x 由（由（,的定型规则的定型规则）I:(t.tt)，其中其中(t.tt):U2 (t.tt):U1 由由(U2 U1)I(t.tt):(t.tt)(t.tt)由由(Elim)I(t.tt)I:(t.tt)由由(Elim)第27页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算type:type加上加上U2=U1和和U1:U2 对前者加语法规则（对前者加语法规则（U2 U1）对后者加公理对后者加公理 U1:U2 (U1:U2)可以写出非常复杂的类型函数可以写出非常复杂的类型函数一个有效的一个有效的编译时的类型检查算法是不可能的编译时的类型检查算法是不可能的 第28页，本

20、讲稿共75页7.2 直谓式多态演算直谓式多态演算 的简化语法的简化语法第一个约定是使用两类变量第一个约定是使用两类变量项变量项变量x,y,z,类型变量类型变量r,t,s,代表代表U1的类型的类型第二个第二个约定约定对对U1的类型表达式使用的类型表达式使用,1,对对U2的类型表达式使用的类型表达式使用,1,U1和和U2的类型表达式的语法的类型表达式的语法 :=t|b|:=|t.第29页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算上下文上下文 =x1:1,xk:k不再需要类型变量不再需要类型变量语法简化后的规则语法简化后的规则 x:x:(var)c:(cst)(add var)(Intro

21、)M:,x:M:,x:M:(x:.M):第30页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算 (Elim)（t在在 中不是自由的）中不是自由的）(Intro)(Elim)M:N:MN:M:t.M:t.M:t.M :/t 第31页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算7.2.3 等式证明系统和归约等式证明系统和归约,等式的形式是等式的形式是 M=N:，其中其中M和和N都是类型都是类型 的项的项,的等式推理系统是的等式推理系统是 证明系统的一个拓证明系统的一个拓展，增加了一些公理和推理规则展，增加了一些公理和推理规则该证明系统包含该证明系统包含自反公理，对称和传递规则自反公理

22、，对称和传递规则同项形成规则对应的推理规则同项形成规则对应的推理规则同普通的同普通的 抽象和应用对应的推理规则抽象和应用对应的推理规则第32页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算增加了类型抽象和类型应用公理增加了类型抽象和类型应用公理 t.M=s.s tM:t.()(t.M)=tM:t ()t.Mt=M:t.t在在M中没有自由出现中没有自由出现 ()第33页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算对类型抽象和应用，还有下面的同余规则对类型抽象和应用，还有下面的同余规则 ()()M =N:t.M =t.N:t.M =N:t.M =N :/t 第34页，本讲稿共75页7

23、.2 直谓式多态演算直谓式多态演算这些等式公理可以从左向右定向这些等式公理可以从左向右定向,得到一个归得到一个归约系统约系统例例 (t.x:t.x)y (x:.x)y y 可以证明归约多态可以证明归约多态,项的合流性和强范式项的合流性和强范式化化命题命题7.1 归约保项的类型归约保项的类型第35页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算7.2.4 ML风格的多态声明风格的多态声明ML的类型系统可看成的类型系统可看成 的一个拓展的一个拓展主要区别是，主要区别是，ML包含多态的包含多态的let声明声明通过调查多态函数在通过调查多态函数在 中的使用来启发这种中的使用来启发这种let声声明

24、的形式明的形式 可以写出可以写出Id (t.x:t.x):t.t tId nat 3和和 Id bool true都是良类型的项都是良类型的项写不出写不出(f:(t.t t).f nat 3f bool true)t.x:t.x因为因为 t.t t是是U2的一个类型的一个类型第36页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算对于对于U2类型，使用一种非常有限的变量约束类型，使用一种非常有限的变量约束形式，对需要多态函数的许多实际程序设计形式，对需要多态函数的许多实际程序设计来说已经足够了来说已经足够了这种方式利用这种方式利用let x:=N in M和和(x:.M)N在在语义上都等价

25、于语义上都等价于N/xM，而定型却不一样，而定型却不一样第37页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算对于对于U2类型，使用一种非常有限的变量约束类型，使用一种非常有限的变量约束形式，对需要多态函数的许多实际程序设计形式，对需要多态函数的许多实际程序设计来说已经足够了来说已经足够了ML的方式的方式 ,let使用使用 let x:=N in M 表达式，增加规则和公理：表达式，增加规则和公理：(let)(let x:=N in M)=N/xM:(let)eq ,x:M:N:(let x:=N in M):第38页，本讲稿共75页7.2 直谓式多态演算直谓式多态演算例例考虑考虑com

26、pose:r.s.t.其中其中 =(st)(rs)(rt)compose在一个表达式中使用多次在一个表达式中使用多次，让其函数体让其函数体仅写一次仅写一次 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.x第39页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算7.3.1 引言引言非直谓式多非直谓式多态态 演算忽略直谓式演算忽略直谓式 的全域的

27、全域U1和和U2的区别的区别由所有类型的一个聚集由所有类型的一个聚集T来代替来代替U1和和U2用用 表示，以区别直谓式系统表示，以区别直谓式系统 类型由文法类型由文法 :=b|t|t.定义，无须用公理和推理规则给出定义，无须用公理和推理规则给出 第40页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算 类型表达式的文法类型表达式的文法 :=b|t|t.项的形成依据项的形成依据7.2.2节的变量公理节的变量公理(var)、常量公理、常量公理(cst)、增加、增加自自由变量类型假设的规则由变量类型假设的规则(add var)、规则、规则(Intro)、规则规则(Elim)、规则、规则(In

28、tro)和规则和规则(Elim)这些规则中的这些规则中的 由由 代替并且对有关的类型全域代替并且对有关的类型全域没有限制没有限制第41页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算非直谓演算可能是最广泛研究的一种多态性非直谓演算可能是最广泛研究的一种多态性1、其语法的简单性、其语法的简单性该语言语法上比该语言语法上比 简单，因为没有全域的限制简单，因为没有全域的限制但是但是证明它的强范式性非常困难证明它的强范式性非常困难2、语义的复杂性、语义的复杂性想提供直观和数学严格的语义，本质上很困难想提供直观和数学严格的语义，本质上很困难多多态态恒恒等等函函数数可可应应用用到到它它自自己己的

29、的类类型型，造造成成了了不不可能把这样的类型解释成普通集合论函数的集合可能把这样的类型解释成普通集合论函数的集合Id=,x:.x|T，其中序对其中序对(t:T.t t),x:(t:T.t t).x 的第一元包含的第一元包含Id第42页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算非直谓演算可能是最广泛研究的一种多态性非直谓演算可能是最广泛研究的一种多态性3、编程的灵活性、编程的灵活性提提供供了了一一个个非非常常灵灵活活的的多多态态类类型型系系统统，象象Ada、CLU和和ML等等语语言言的的多多态态性性特特征征都都可可以以看看成成是是作作了某种限制的了某种限制的 多态性多态性可以可以用

30、用 中的中的 抽象来模仿抽象来模仿ML的的let let x:t.=M in N:（ML方式）方式）它是项它是项 (x:t.N)M:的一种语法美化的一种语法美化 第43页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算7.3.2 非直谓式多态非直谓式多态 演算的表达能力演算的表达能力给出一个例子来展示非直谓式多态给出一个例子来展示非直谓式多态 演算的表演算的表达能力达能力在二阶在二阶Peano算术中算术中 可可证证明明为为全全函函数数的的递递归归函函数数恰恰好好是是在在非非直直谓谓式式多态多态 演算中可以定义的数值函数演算中可以定义的数值函数 这这是是多多态态 演演算算和和二二阶阶逻逻

31、辑辑的的证证明明论论之之间间的的联联系的一部分系的一部分在此仅概述数值函数的某些表示方面的内容在此仅概述数值函数的某些表示方面的内容第44页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算在在无无类类型型常常量量的的纯纯 中中，自自然然数数类类型型的的一一种自然选择种自然选择若若有有常常量量zero:nat和和succ:natnat，则则可可以以用用表表达达式式succ(succ(succ zero)表示自然数表示自然数n在在纯纯 中中，没没有有常常量量zero和和succ，但但是是可可以以把把这这些符号当作变量看待，并且对它们进行些符号当作变量看待，并且对它们进行 抽象抽象 zero

32、:nat.succ:natnat.succ(succ(succ zero)第45页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算类类型型名名nat是是任任意意选选择择的的，把把这这个个符符号号也也当当作作变变量量看待，并且对它进行看待，并且对它进行 抽象抽象 nat.zero:nat.succ:natnat.succ(succ(succ zero)通通常常用用更更简简单单的的变变量量名名写写出出，作作为为自自然然数数的的一一种种有用表示有用表示(Church数码数码)n t.f:t t.x:t.f nx所有所有的的Church数码都具有类型数码都具有类型nat t.(t t)t t第

33、46页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算多多态态Church数数码码上上的的加加法法和和乘乘法法运运算算是是合合成成函数的形式函数的形式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)第47页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算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:t t.x:t.f 3x)=t.f:tt.(t.f:t t.x:t.f 2x)t(t.f:t t.x:t

34、.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 6第48页，本讲稿共75页7.3 非直谓式多态演算非直谓式多态演算还还可可以以用用一一个个正正好好带带两两个个范范式式的的类类型型来来表表示示布尔值布尔值true t.x:t.y:t.xfalse t.x:t.y:t.ybool t.tttzero?x:nat.x bool(x:bool.false)true第49页，本讲稿共75页7.3

35、非直谓式多态演算非直谓式多态演算7.3.3 归约的终止性归约的终止性略去不介绍略去不介绍第50页，本讲稿共75页7.4 数据抽象和存在类型数据抽象和存在类型数数据据抽抽象象以以及及相相应应的的程程序序规规范范和和模模块块性性的的概概念念可可能能是是二二十十世世纪纪七七十十年年代代有有关关程程序序设设计计语语言最有影响的研究言最有影响的研究抽抽象象数数据据类类型型的的声声明明，作作为为一一种种支支持持数数据据抽抽象象的的语语言言机机制制，已已出出现现在在一一些些程程序序设设计计语语言言中，包括中，包括Ada、Clu和和ML本节本节调查抽象数据类型声明的一种一般形式调查抽象数据类型声明的一种一般形

36、式第51页，本讲稿共75页7.4 数据抽象和存在类型数据抽象和存在类型形式为形式为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 inN第52页，本讲稿共75页7.4 数据抽象和存在类型数据抽象和存在类型使使用用笛笛卡卡儿儿积积，可可以以把把任任何何抽抽象象数数据据类类型型声声明明写写成成abstype t with x:is ,M in N的的形形式式抽抽象象数数据据类类型

37、型声声明明可可以以加加到到直直谓谓式式或或非非直直谓谓式语言中式语言中分别考虑抽象数据类型声明和数据类型实现分别考虑抽象数据类型声明和数据类型实现拓展类型表达式的语法，以包含存在类型拓展类型表达式的语法，以包含存在类型 :=|t.存在类型用于抽象数据类型的实现存在类型用于抽象数据类型的实现存存在在类类型型 t.的的每每个个元元素素由由一一个个类类型型 和和类类型型/t 的一个元素组成的一个元素组成 第53页，本讲稿共75页7.4 数据抽象和存在类型数据抽象和存在类型例：例：stream的实现总有类型的实现总有类型 t.(t (t nat)(t t)抽抽象象数数据据类类型型的的实实现现将将以以

38、t=,M:的的形形式式写出，其中写出，其中 t=表示在该表达式的剩余部分将表示在该表达式的剩余部分将t约束到约束到 称为称为t的表示类型的表示类型第54页，本讲稿共75页7.4 数据抽象和存在类型数据抽象和存在类型存在类型的公理和推理规则存在类型的公理和推理规则 (Intro)t=,M:=s=,M:s/t :t.s在在 中不是自由的中不是自由的下面规则允许把名字约束到数据类型实现的类型下面规则允许把名字约束到数据类型实现的类型成分和值成分成分和值成分 (Elim)M:/t t=,M:t.M:t.,x:N:(abstype t with x:is M in N):第55页，本讲稿共75页7.4

39、数据抽象和存在类型数据抽象和存在类型作作为为记记号号上上的的方方便便，把把多多于于一一个个运运算算的的声声明明作为一种语法美化：作为一种语法美化：abstype t with x1:1,xn:n is M in N abstype t with y:1 n is M in Proj1 y,Projn y/x1,xnN nn第56页，本讲稿共75页7.4 数据抽象和存在类型数据抽象和存在类型例例:abstype cmplx withcreate:real real cmplx,plus:cmplx cmplx cmplx,re:cmplx realim:cmplx realis t=real r

40、eal,C,P,R,I:(real real t)(t t t)(t real)(t real)inN第57页，本讲稿共75页7.4 数据抽象和存在类型数据抽象和存在类型 C,P,R,I :可以写成：可以写成：C=p:real real.pP=z:real real,w:real real.Proj1 z+Proj1 w,Proj2 z+Proj2 w R=z:real real.Proj1 zI=z:real real.Proj2 z第58页，本讲稿共75页7.4 数据抽象和存在类型数据抽象和存在类型abstype的主要等式公理的主要等式公理 (abstype t with x:is t=,

41、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:,其其中中y FV(M)()abstype t with x:is y in t=t,x:=y:t.()x .(Mx)=M:,其中其中x FV(M)()第59页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类7.5.1 类型表达式的种类类型表达式的种类（1）7.2节把类型表达式分成两个层次节把类型表达式分成两个层次普通类型和多态类型普通类型和多态类型在在给给出出一一些

42、些简简化化约约定定的的情情况况下下，类类型型表表达达式式可可用用文法分成同样的两个层次文法分成同样的两个层次由由于于除除了了类类型型常常量量和和类类型型变变量量外外，只只涉涉及及函函数数类类型，使得用文法推出的类型表达式都是良形的型，使得用文法推出的类型表达式都是良形的 第60页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类（2）类类型型表表达达式式分分成成小小全全域域和和大大全全域域，不不足足以解决类型表达式是否为良形的问题以解决类型表达式是否为良形的问题在在 演算上再增加积类型或和类型时演算上再增加积类型或和类型时若若类类型型变变量量t代代表表二二元元积积类类型型，则则fst(t

43、)（取取t的的第第一一元元）是是良良形形的的类类型型表表达达式式，否否则则fst(t)不不是是良良形形的类型表达式的类型表达式这这时时良良形形的的类类型型表表达达式式很很难难用用7.2节节的的文文法法形形式式表表示示 第61页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类（3）需要考虑类型表达式新的分类方式）需要考虑类型表达式新的分类方式例例如如，所所有有的的函函数数类类型型、所所有有的的表表类类型型、所所有有的的二二叉叉树树类类型型等等，并并且且对对类类型型表表达达式式的的量量化化是是以以这这样的类型族为论域样的类型族为论域可以通过丰富语言结构来解决这些问题可以通过丰富语言结构来解

44、决这些问题用类型对项进行分类用类型对项进行分类用较高层次的种类（用较高层次的种类（kind）来对类型进行分类）来对类型进行分类当当前前很很多多研研究究工工作作中中的的类类型型系系统统都都是是按按这这种种思思路路来设计来设计第62页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类 ,演算有项、类型和种类三种语法范畴演算有项、类型和种类三种语法范畴语法范畴语法范畴项目项目具体形式具体形式种类种类:=Type|类型类型:=b|t|fst()|snd()|t:.|项项M:=c|x|x:.M|MM|M,N|Proj1M|Proj2M|t:.M|M 种类文法产生的任何种类表达式都是良形的种类文法产

45、生的任何种类表达式都是良形的符号符号和和 在这里是重载的在这里是重载的基本类型和普通函数类型归到基本类型和普通函数类型归到Type种类种类第63页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类 ,演算有项、类型和种类三种语法范畴演算有项、类型和种类三种语法范畴语法范畴语法范畴项目项目具体形式具体形式种类种类:=Type|类型类型:=b|t|fst()|snd()|t:.|项项M:=c|x|x:.M|MM|M,N|Proj1M|Proj2M|t:.M|M 任意两个类型，它们的积属于某个积种类任意两个类型，它们的积属于某个积种类 1 2由由 t:.表表示示的的类类型型上上的的函函数数属属

46、于于某某个个函函数数种种类类 第64页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类7.5.2 类型表达式的定类与相等类型表达式的定类与相等类型表达式的定类（类型表达式的定类（kinding）断言）断言断言的形式为断言的形式为 :，其中定类上下文，其中定类上下文 是形是形式为式为 =t1:1,tn:n 其中其中dom()=t1,tn类似于项的定型断言类似于项的定型断言 M:第65页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类7.5.2 类型表达式的定类与相等类型表达式的定类与相等类型表达式的定类（类型表达式的定类（kinding）断言）断言断言的形式为断言的形式为 :，其

47、中定类上下文，其中定类上下文 是形是形式为式为 =t1:1,tn:n 其中其中dom()=t1,tn它给类型变量进行种类指派，类似于项的定型断它给类型变量进行种类指派，类似于项的定型断言言 M:第66页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类定类规则定类规则 b:Type（每个类型常量（每个类型常量b:Type）(cstt)t:t:(vark)(add vark)(WF-Type)(k Intro):,t:1:Type 2:Type 1 2:Type 1:1 2:2 1 2:1 2 第67页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类定类规则定类规则 (k Elim

48、)1 (k Elim)2 (k Intro)(k Elim):1 2 fst():1 ,t:1 2:2 (t:1.):1 2 1:2:1 2:1 2 snd():2第68页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类类型表达式的相等规则类型表达式的相等规则(Projt)1(Projt)2(spt)(t:.)=(t:.t/t):其其中中tFV()(t)1 2:1 2 fst(1 2)=1:1 1 2:1 2 snd(1 2)=2:2 :1 2 fst()snd()=:1 2第69页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类类型表达式的相等规则类型表达式的相等规则 (t)

49、(t)上上述述类类型型表表达达式式的的定定类类规规则则和和相相等等规规则则给给出出了类型表达式上一个简单的演算系统了类型表达式上一个简单的演算系统类类型型表表达达式式被被称称为为语语言言的的静静态态数数据据，而而项项被被称为语言的动态数据称为语言的动态数据 ,t:1:2:(t:.1)2=2/t 1:1 2 t dom()(t:1.t)=:1 2第70页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类7.5.3 项的定型项的定型定型断言定型断言 M:种类指派种类指派 =t1:1,tn:n类型指派类型指派 =x1:1,xn:n 和和 都是无序集合，两者的次序不能颠倒都是无序集合，两者的次序

50、不能颠倒下面默认：出现定型公理和推理规则的下面默认：出现定型公理和推理规则的 在定类在定类上下文上下文 下都是良种类的类型表达式下都是良种类的类型表达式 c:（对基调中的每个项常量（对基调中的每个项常量c:）(cst),x:x:(var)第71页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类 (add var)(Intro)(Elim)(Intro)M:,x:M:,x:1M:2 (x:1.M):1 2 M:N:MN:M:1 N:2 M N:1 2第72页，本讲稿共75页7.5 类型表达式的分类类型表达式的分类 (Elim)1 (Elim)2 (Intro)(Elim):1 2 M:P