第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的类型是什么？