第7章多态性 本章和下一章介绍类型论的一些概念，它们 是程序设计语言的多态性和数据抽象的基础 这些概念与下面的语言概念有关 Ada的程序包和类属 C+的模板 ML以及相近语言Miranda和Haskell的多态性、 抽象类型和模块等 现实语言出于效率上的考虑，所采用的副本没有 相应的类型化入演算那么灵活
第7章 多态性 • 本章和下一章介绍类型论的一些概念，它们 是程序设计语言的多态性和数据抽象的基础 • 这些概念与下面的语言概念有关 – Ada的程序包和类属 – C++的模板 – ML以及相近语言Miranda和Haskell的多态性、 抽象类型和模块等 – 现实语言出于效率上的考虑，所采用的副本没有 相应的类型化演算那么灵活
7.1引 言 本章的主要内容 多态类型系统的语法，包括直谓式的，非直谓式 的和type: type版本 直谓式多态λ演算，包括和其它两个系统之间的 联系，它的等式证明系统和归约、多态声明 -非直谓式多态λ演算的纵览 -数据抽象和存在类型 -类型表达式的分类
7.1 引 言 • 本章的主要内容 – 多态类型系统的语法，包括直谓式的，非直谓式 的和type: type版本 – 直谓式多态演算，包括和其它两个系统之间的 联系，它的等式证明系统和归约、多态声明 – 非直谓式多态演算的纵览 – 数据抽象和存在类型 – 类型表达式的分类
7.1引 言 7.1.2类型作为函数变元 简单类型化)演算有某种明显的缺点 很多有计算意义且有用的表达式不是良类型的 排序函数：希望能应用于许多不同类型的数据 Sort:(t×t→bool)×Array prt t→Array (prt t] 多态函数 变元的类型可以有多种不同的情况 -通过拓展抽象到允许对类型进行入抽象，可以把 入拓展到包括多态函数
7.1 引 言 7.1.2 类型作为函数变元 • 简单类型化演算有某种明显的缺点 –很多有计算意义且有用的表达式不是良类型的 –排序函数：希望能应用于许多不同类型的数据 Sort : (t t → bool ) Array[prt t] → Array [prt t] • 多态函数 –变元的类型可以有多种不同的情况 –通过拓展抽象到允许对类型进行抽象，可以把 →拓展到包括多态函数
7.1引 言 再以更简洁一些的函数合成运算为例 COmpOSenat,nat,nat 入f:nat-→nat.入g:nat-→nat.入x:nat.f(gx) CompOsenat,nat>nat,nat 入f:(nat-→nat）→nat. 入g:nat-→(nat→nat).入x:natf(gx) composer,s,t 入f:S→t.入g:r-→S.入x:rf(gx) compose λr:T.入s:T.入t:T.c0p0sex,s,t
7.1 引 言 • 再以更简洁一些的函数合成运算为例 composenat, nat, nat f : nat → 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
7.1引言 考察compose λr:T.入s:T.t:T.c0mp0sex,s,t -对T(类型的集合)有几种可能的解释 一类型应用 compose nat natnat =():T.入s:T.入t:T.入f:S→t.入gr→s.入x:r.f(gx) natnat nat =入f:nat-→nat.入g:nat-→nat.入x:nat.f(gx) compose的类型是什么？
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 → s. x:r. f (g x)) nat nat nat = f :nat → nat. g:nat → nat. x:nat. f (g x) – compose的类型是什么？
7.1引 言 ·以多态恒等函数为例 入t:T.入x:t.飞 -Id的定义域是T,但值域难以描述 -一种表示：Id:Πt:T.t→t) Πt:Tt→是无限积卫ert之t: (nat-→nat×(bool→boo×... (idnat→na idpool-→booh.)是该类型的一个值 Id nat=入x:nat.x=idnat-→nt Id bool=Xx bool.x idbool->bool 代换仅在I的类型上完成，而不是在函数本身上 完成
7.1 引 言 • 以多态恒等函数为例 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 = idnat → nat Id bool = x : bool. x = idbool → bool –代换仅在Id的类型上完成，而不是在函数本身上 完成
7.1引 言 ·以多态恒等函数为例 Id 入t:T.入x:t.飞 -Id的定义域是T,但值域难以描述 -一种表示：Id:Πt:T.t→t) -另一种表示：Id:V:T.t→t Vt:T.t→是所有下述函数构成的类型： 每个函数对所有的：T,给出从t到t的一个映射 ·下面先只考虑第一种表示法
7.1 引 言 • 以多态恒等函数为例 Id t : T. x : t. x – Id的定义域是T，但值域难以描述 – 一种表示：Id : (t :T t → t) – 另一种表示： Id : t: T. t → t t: T. t → t是所有下述函数构成的类型： 每个函数对所有的t:T，给出从t 到t 的一个映射 –下面先只考虑第一种表示法
7.1引 言 ·对T有三种自然的选择 为多态函数引入类型后，必须决定这些类型怎样 来适合现在的类型系统 1、直谓式多态性 -T仅含用→、+和/或×及一组类型常量定义的类型 -这是在已经定义了T的所有成员后才引入T 2、非直谓式多态性 T还包含所有的多态类型（例如Π：T.t→t),但 不把T本身作为一个类型
7.1 引 言 • 对T有三种自然的选择 为多态函数引入类型后，必须决定这些类型怎样 来适合现在的类型系统 1、直谓式多态性 – T仅含用→、+和或及一组类型常量定义的类型 – 这是在已经定义了T的所有成员后才引入T 2、非直谓式多态性 – T还包含所有的多态类型（例如t: T. t → t），但 不把T本身作为一个类型
7.1引 言 ·对T有三种自然的选择 为多态函数引入类型后，必须决定这些类型怎样 来适合现在的类型系统 1、直谓式多态性 2、非直谓式多态性 3、ype:pe -令T包含所有的类型，包括它本身 -从计算的观点看，并非立即能看清楚： 引入“所有类型的类型”后会引起什么错误
7.1 引 言 • 对T有三种自然的选择 为多态函数引入类型后，必须决定这些类型怎样 来适合现在的类型系统 1、直谓式多态性 2、非直谓式多态性 3、type : type –令T包含所有的类型，包括它本身 –从计算的观点看，并非立即能看清楚： 引入“所有类型的类型”后会引起什么错误
7.1引 言 三种多态性之间的简单区别 1、直谓式多态性 -Id仅能够应用于非多态类型，例如nat或(nat→ nat -Id(nat→nat)=入x:nat-→nat.x 2.非直谓式多态性 -Id可以应用到任何类型 -IdΠt:T.t→t)=入x:Πt:T.t→t).x -不可能把每个多态入项都解释成集合论的函数 Id={K石入x:xx)∈T,其中序对 〈t:T.t→t),入x:Πt:T.t>t).x〉的第一元包含Id
7.1 引 言 • 三种多态性之间的简单区别 1、直谓式多态性 – Id仅能够应用于非多态类型，例如nat 或 (nat → nat) – Id (nat → nat) = x : nat → nat. x 2. 非直谓式多态性 – 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