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