第7章多态性ppt课件.ppt

《第7章多态性ppt课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第7章多态性类型论是集合论的一个构造逻辑分支类型论的最大成就就是揭示了证明和编程的惊人相似点：在构造性证明中的结构化问题类似于程序构造问题类型论成为编程语言类型系统的理论基石本章提出一些类型论的概念，它们是程序设计语言的多态性和数据抽象的基础第7章多态性构造性证明和非构造性证明命题：存在大于2100的素数解释为：能找到大于2100的素数构造性证明传达了更多的信息命题：存在无理数a和b，使得ab是有理数证明：1.若是有理数，取a=b=2.若是无理数，取a=，b=该证明用了排中律2222227.1引

2、言本章的主要内容多态类型系统的语法，包括谓词式的，非谓词式的和type:type版本谓词式多态演算，包括和其它两个系统的联系、等式证明系统和归约、多态声明非谓词式多态演算的纵览数据抽象和存在类型一般积与一般和本章强调各种语言的直观性质和表达能力，不再讨论语义模型7.1引言7.1.2类型作为函数变元简单类型化演算的类型约束有某种明显的缺点：很多有计算意义且有用的表达式不是良类型的排序函数：希望能作用于许多不同类型的数据Sort:(ttbool)Array[prtt]Array[prt

3、t]多态函数变元的类型可以有很多种通过拓展抽象到允许对类型进行抽象，可以把拓展到包括多态函数7.1引言以函数合成运算为例composenat,nat,nat=deff:natnat.g:natnat.x:nat.f(gx)composenat,natnat,nat=deff:(natnat)nat.g:nat(natnat).x:nat.f(gx)composer,s,t=deff:st.g:rs.x:r.f(gx)compose=defr:T.s

4、:T.t:T.composer,s,t7.1引言compose=defr:T.s:T.t:T.composer,s,t对T有几种可能的解释类型作用composenatnatnat=(r:T.s:T.t:T.f:st.g:rs.x:r.f(gx))natnatnat=f:natnat.g:natnat.x:nat.f(gx)compose的类型是什么？7.1引言多态恒等函数Id=deft:T.x:t.xId的定义域是T，但值域难以描述一种表示：Id:(t:T

5、tt)无限积tTtt(natnat)(boolbool)...(idnatnat,idboolbool,id(natnat)(natnat),...)Idnat=x:nat.x=idnatnatIdbool=x:bool.x=idboolbool代换仅在Id的类型上完成，而不是在函数本身上完成7.1引言多态恒等函数Id=deft:T.x:t.xId的定义域是T，但值域难以描述一种表示：Id:(t:Ttt)另一种表示：Id:t:T.tt是所有下述函

6、数构成的类型：每个函数对所有的t:T，给出从t到t的一个映射7.1引言为多态函数引入类型后，必须决定这些类型怎样来适合现在的类型系统对T有三种自然的选择1.谓词式多态性T仅含用、和或及一组类型常量定义的类型在已经定义了T的所有成员后才引入T2.非谓词式多态性T还包含所有的多态类型（例如t:T.tt），但不把T本身作为一个类型7.1引言为多态函数引入类型后，必须决定这些类型怎样来适合现在的类型系统对T有三种自然的选择1.谓词式多态性2.非谓词式多态性T还包含所有的多态类型（例如t:T

7、.tt），但不把T本身作为一个类型3.type:type令T包含所有的类型，包括它本身从计算的观点看，并非立即能看清楚，引入“所有类型的类型”后会引起什么错误7.1引言这三种多态性之间的简单区别1.谓词式多态性Id仅能够作用于非多态类型，例如nat或(natnat)2.非谓词式多态性Id可以作用到任何类型Id(t:T.tt)=x:(t:T.tt).x不可能把每个多态项都解释成集合论的函数Id={,x:.x

8、T}，其中有序对(t:T.tt),x:(t:T.t

9、t).x的第一元包含Id7.1引言这三种多态性之间的简单区别1.谓词式多态性2.非谓词式多态性3.type:typeId不仅表现为从类型到类型元素的函数Id还表现为从类型到类型的函数IdT=x:T.x(IdT):TT7.1引言参数化多态性和特定多态性1.参数化多态性一个多态函数对任何类型都使用“本质上一样的算法”2.特定多态性可以测试类型变元的值，然后根据这个类型的形式选择某个分支ad_hoc_compose=defr:T.s:T.t:T.f:st.g:rs.x:r.if