第7章 多态性 本章和下一章介绍类型论的一些概念，它们是程序设计语言的多态性和数据抽象的基础 这些概念与下面的语言概念有关

Presentation on theme: "第7章 多态性 本章和下一章介绍类型论的一些概念，它们是程序设计语言的多态性和数据抽象的基础 这些概念与下面的语言概念有关"— Presentation transcript:

1 第7章 多态性 本章和下一章介绍类型论的一些概念，它们是程序设计语言的多态性和数据抽象的基础 这些概念与下面的语言概念有关
第7章 多态性 本章和下一章介绍类型论的一些概念，它们是程序设计语言的多态性和数据抽象的基础 这些概念与下面的语言概念有关 Ada的程序包和类属 C的模板 ML以及相近语言Miranda和Haskell的多态性、抽象类型和模块等 现实语言出于效率上的考虑，所采用的副本没有相应的类型化演算那么灵活

2 7.1 引 言 本章的主要内容 多态类型系统的语法，包括直谓式的，非直谓式的和type: type版本
7.1 引 言 本章的主要内容 多态类型系统的语法，包括直谓式的，非直谓式的和type: type版本 直谓式多态演算，包括和其它两个系统之间的联系，它的等式证明系统和归约、多态声明 非直谓式多态演算的纵览 数据抽象和存在类型 类型表达式的分类

3 7.1 引 言 7.1.2 类型作为函数变元 简单类型化演算有某种明显的缺点 多态函数 很多有计算意义且有用的表达式不是良类型的
7.1 引 言 7.1.2 类型作为函数变元 简单类型化演算有某种明显的缺点 很多有计算意义且有用的表达式不是良类型的 排序函数：希望能应用于许多不同类型的数据 Sort : (t  t  bool )  Array[prt t]  Array [prt t] 多态函数 变元的类型可以有多种不同的情况 通过拓展抽象到允许对类型进行抽象，可以把拓展到包括多态函数

4 7.1 引 言 再以更简洁一些的函数合成运算为例 composenat, nat, nat 
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

5 7.1 引 言 考察compose  r:T. s:T. t:T. composer, s, t 对T（类型的集合）有几种可能的解释
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的类型是什么？

6 7.1 引 言 以多态恒等函数为例 Id  t : T. x : t. x Id的定义域是T，但值域难以描述
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 7.1 引 言 以多态恒等函数为例 Id  t : T. x : t. x Id的定义域是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 的一个映射 下面先只考虑第一种表示法

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

9 7.1 引 言 对T有三种自然的选择 为多态函数引入类型后，必须决定这些类型怎样 来适合现在的类型系统 1、直谓式多态性 2、非直谓式多态性
7.1 引 言 对T有三种自然的选择 为多态函数引入类型后，必须决定这些类型怎样 来适合现在的类型系统 1、直谓式多态性 2、非直谓式多态性 3、type : type 令T包含所有的类型，包括它本身 从计算的观点看，并非立即能看清楚： 引入“所有类型的类型”后会引起什么错误

10 7.1 引 言 三种多态性之间的简单区别 1、直谓式多态性 Id仅能够应用于非多态类型，例如nat 或 (nat  nat)
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

11 7.1 引 言 三种多态性之间的简单区别 1、直谓式多态性 Id (nat  nat) = x : nat  nat. x
7.1 引 言 三种多态性之间的简单区别 1、直谓式多态性 Id (nat  nat) = x : nat  nat. x 2. 非直谓式多态性 Id (t: T. t  t) = x : (t: T. t  t). x 3、type : type Id T = x:T. x (Id T): T  T

12 7.1 引 言 参数多态性和特定多态性 1、参数化多态性 一个多态函数对任何类型都使用“本质上一样的算法” 2、特定多态性
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)

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

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

15 7.2 直谓式多态演算 良形上下文的公理和推理规则  context (empty context) t不在中 (U1 context)
7.2 直谓式多态演算 良形上下文的公理和推理规则  context (empty context) t不在中 (U1 context) x不在中 (Ui type context)  context , t : U1 context    : Ui , x :  context

16 7.2 直谓式多态演算 良形上下文的公理和推理规则 (var) (add var) 这两条规则可用于多个类型系统
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

17 7.2 直谓式多态演算 U1和U2类型表达式的语法规则   b: U1 (cst U1) U1的类型表达式由三个公理和推理规则给出
7.2 直谓式多态演算 U1和U2类型表达式的语法规则 U1的类型表达式由三个公理和推理规则给出   b: U (cst U1) （限制到U1的变量） (var) ( U1) , x : A context , x : A  x : A    : U1,    : U1      : U1

18 7.2 直谓式多态演算 (U1U2) (U2) 第二个全域U2包含类型U1和多态函数类型    : U1    : U2
7.2 直谓式多态演算 第二个全域U2包含类型U1和多态函数类型 (U1U2) (U2) 虽然有属于U2的类型表达式，但是没有U2的变量 如果加了变量和抽象到U2上，它就会导致形式是t:U2.的类型，它将属于第三个全域U3    : U1    : U2 , t : U1   : U2   ( t : U1. ) : U2

19 7.2 直谓式多态演算 例 证明t: U1.t  t是属于U2的良形的类型表达式  context 由(empty context)
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)

20 7.2 直谓式多态演算 (add var) 项的语法（先给,  预备项的文法 ）
7.2 直谓式多态演算 项的语法（先给,  预备项的文法 ） 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

21 , x :  M :     : U1    : U1
7.2 直谓式多态演算   c:  (cst) (Intro) (Elim) 任何项（可能包括了用类型变量取代类型常量）都是,的项 , x :  M :     : U    : U1   (x : . M) :      M :      N :    MN : 

22 7.2 直谓式多态演算 ( Intro) , t : U1  M :    (t : U1. M) : (t: U1. )
7.2 直谓式多态演算 ( Intro) ( 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

23 7.2 直谓式多态演算 ( Intro) ( Elim) (type eq) 若  M是从公理和, 定型规则可推导，则
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

24 7.2 直谓式多态演算 规则U1 U2 和规则U1 :U2 1、规则U1 U2 可以只用一个形成规则
7.2 直谓式多态演算 规则U1 U2 和规则U1 :U2 1、规则U1 U2 可以只用一个形成规则 U1 U2没有在该语言上设置任何额外的语义限制 2、规则U1 :U2 因为在任意U2类型上无任何有意义的运算，因此看起来没有任何理由取U1 :U2 在的非直谓式拓展中，加入U1 :U2规则将是一个合理的语言设计

25 7.2 直谓式多态演算 7.2.2 和其它形式多态性的比较 其它两种演算都可看成直谓式多态演算的特殊情况 非直谓式类型化演算
7.2 直谓式多态演算 7.2.2 和其它形式多态性的比较 其它两种演算都可看成直谓式多态演算的特殊情况 非直谓式类型化演算 强加“全域等式”U1 = U2 “type: type”演算 强加了等式U1 = U2和条件U1:U2

26 7.2 直谓式多态演算 非直谓式演算 在, 中已经有U1 U2, 加入逆向包含U2 U1来获得U1 = U2 (U2U1)
7.2 直谓式多态演算 非直谓式演算 在, 中已经有U1 U2, 加入逆向包含U2 U1来获得U1 = U2 (U2U1)    : U2    : U1

27 7.2 直谓式多态演算 例 证明语法断言  (I (t.tt))I:  t.tt， 其中I  t:U1.x:t.x
7.2 直谓式多态演算 例 证明语法断言  (I (t.tt))I:  t.tt， 其中I  t:U1.x:t.x  由（, 的定型规则）   I: (t.tt)，其中(t.tt):U2  (t.tt):U1 由(U2 U1)  I (t.tt) : (t.tt)  (t.tt) 由( Elim)  I (t.tt) I : (t.tt) 由( Elim)

28 7.2 直谓式多态演算 type : type 加上U2 = U1和U1:U2 对前者加语法规则（U2 U1）
7.2 直谓式多态演算 type : type 加上U2 = U1和U1:U2 对前者加语法规则（U2 U1） 对后者加公理   U1:U (U1:U2) 可以写出非常复杂的类型函数 一个有效的编译时的类型检查算法是不可能的

29 7.2 直谓式多态演算  的简化语法 第一个约定是使用两类变量 项变量x, y, z, …
7.2 直谓式多态演算  的简化语法 第一个约定是使用两类变量 项变量x, y, z, … 类型变量r, t, s, … 代表U1的类型 第二个约定 对U1的类型表达式使用, , 1, … 对U2的类型表达式使用, , 1, … U1和U2的类型表达式的语法  ::= t | b |     ::=  | t.

30 7.2 直谓式多态演算 上下文  = {x1: 1, … , xk: k} －－不再需要类型变量 语法简化后的规则
7.2 直谓式多态演算 上下文  = {x1: 1, … , xk: k} －－不再需要类型变量 语法简化后的规则 {x: }  x:  (var)   c: (cst) (add var) (Intro)   M :  , x :   M :  , x :  M :    (x : . M) :   

31 7.2 直谓式多态演算 (Elim)   M :      N :    MN : 
7.2 直谓式多态演算 (Elim) （t在中不是自由的） ( Intro) ( Elim)   M :      N :    MN :    M :    t . M : t.   M : t.   M  : [/t]

32 7.2 直谓式多态演算 7.2.3 等式证明系统和归约 , 等式的形式是  M = N:，其中M和N都是类型的项
7.2 直谓式多态演算 7.2.3 等式证明系统和归约 , 等式的形式是  M = N:，其中M和N都是类型的项 ,的等式推理系统是证明系统的一个拓展，增加了一些公理和推理规则 该证明系统包含 自反公理，对称和传递规则 同项形成规则对应的推理规则 同普通的抽象和应用对应的推理规则

33 7.2 直谓式多态演算 增加了类型抽象和类型应用公理   t. M = s. [st]M : t. ()
7.2 直谓式多态演算 增加了类型抽象和类型应用公理   t. M = s. [st]M : t. ()   (t. M) = [t]M : [t] ()   t. Mt = M : t. t在M中没有自由出现 ()

34 7.2 直谓式多态演算 对类型抽象和应用，还有下面的同余规则 ()   M = N :  ()
7.2 直谓式多态演算 对类型抽象和应用，还有下面的同余规则 () ()   M = N :    t. M = t. N : t.   M = N : t.   M = N : [/t]

35 7.2 直谓式多态演算 这些等式公理可以从左向右定向,得到一个归约系统
7.2 直谓式多态演算 这些等式公理可以从左向右定向,得到一个归约系统 例 (t.x: t.x)  y  (x: .x) y  y 可以证明归约多态,项的合流性和强范式化 命题7.1 归约保项的类型

36 7.2 直谓式多态演算 7.2.4 ML风格的多态声明 ML的类型系统可看成 的一个拓展  
7.2 直谓式多态演算 ML风格的多态声明 ML的类型系统可看成 的一个拓展 主要区别是，ML包含多态的let声明 通过调查多态函数在 中的使用来启发这种let声明的形式   可以写出Id  (t. x : t.x) : t. t  t Id nat 3和 Id bool true都是良类型的项 写不出(f :(t.t t). … f nat 3…f bool true)t.x:t.x 因为t. t  t是U2的一个类型

37 7.2 直谓式多态演算 对于U2类型，使用一种非常有限的变量约束形式，对需要多态函数的许多实际程序设计来说已经足够了
7.2 直谓式多态演算 对于U2类型，使用一种非常有限的变量约束形式，对需要多态函数的许多实际程序设计来说已经足够了 这种方式利用let x:  = N in M和(x:.M)N在语义上都等价于[N/x]M，而定型却不一样

38 7.2 直谓式多态演算 对于U2类型，使用一种非常有限的变量约束形式，对需要多态函数的许多实际程序设计来说已经足够了
7.2 直谓式多态演算 对于U2类型，使用一种非常有限的变量约束形式，对需要多态函数的许多实际程序设计来说已经足够了 ML的方式 , let 使用 let x :  = N in M 表达式，增加规则和公理： (let)   (let x: = N in M) = [N/x]M: (let)eq , x :   M :    N :    (let x :  = N in M) : 

39 7.2 直谓式多态演算 例 考虑compose: r.s.t. 其中 = (st)  (rs)  (rt)
7.2 直谓式多态演算 例 考虑compose: r.s.t. 其中 = (st)  (rs)  (rt) compose在一个表达式中使用多次，让其函数体仅写一次 let x: (r.s.t.) = compose in M，则   ( let x: (r.s.t.) = compose in M) = [compose/x]M:  避免写下面的表达式，并能达到同样的效果 (f :(t.t t). … f nat 3…f bool true)t.x:t.x

40 7.3 非直谓式多态演算 7.3.1 引言 非直谓式多态演算忽略直谓式 的全域U1和U2的区别 
由所有类型的一个聚集T来代替U1和U2 用表示，以区别直谓式系统  类型由文法  ::= b | t |    | t. 定义，无须用公理和推理规则给出

41 7.3 非直谓式多态演算  类型表达式的文法  ::= b | t |    | t. 项的形成依据
7.2.2节的变量公理(var)、常量公理(cst)、增加自 由变量类型假设的规则(add var)、规则( Intro)、 规则( Elim)、规则( Intro)和规则( Elim) 这些规则中的由代替并且对有关的类型全域 没有限制

42 7.3 非直谓式多态演算 非直谓演算可能是最广泛研究的一种多态性 1、其语法的简单性 该语言语法上比 简单，因为没有全域的限制
但是证明它的强范式性非常困难 2、语义的复杂性 想提供直观和数学严格的语义，本质上很困难 多态恒等函数可应用到它自己的类型，造成了不可能把这样的类型解释成普通集合论函数的集合 Id = {, x: . x |  T}，其中序对 (t: T. t  t), x: (t: T. t  t). x  的第一元包含Id

43 7.3 非直谓式多态演算 非直谓演算可能是最广泛研究的一种多态性 3、编程的灵活性
提供了一个非常灵活的多态类型系统，象Ada、CLU和ML等语言的多态性特征都可以看成是作了某种限制的多态性 可以用中的抽象来模仿ML的let   let x:t. = M in N: （ ML方式） 它是项  ( x:t..N)M:的一种语法美化

44 7.3 非直谓式多态演算 7.3.2 非直谓式多态演算的表达能力 给出一个例子来展示非直谓式多态演算的表 达能力 在二阶Peano算术中
可证明为全函数的递归函数恰好是在非直谓式多态演算中可以定义的数值函数 这是多态演算和二阶逻辑的证明论之间的联系的一部分 在此仅概述数值函数的某些表示方面的内容

45 7.3 非直谓式多态演算 在无类型常量的纯中，自然数类型的一种自然选择
若有常量zero:nat和succ:natnat，则可以用表达式 succ(succ…(succ zero)… ) 表示自然数n 在纯中，没有常量zero和succ，但是可以把这些符号当作变量看待，并且对它们进行抽象 zero:nat.succ:natnat.succ(succ…(succ zero)…)

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

47 7.3 非直谓式多态演算 多态Church数码上的加法和乘法运算是合成函数的形式
mult  x:nat.y:nat.t.f: tt.x t (y t f) add  x:nat.y:nat.t.f: tt.z:t.x t f (y t f z)

48 7.3 非直谓式多态演算 mult 2 3  (x:nat.y:nat.t.f: tt.x t (y t f))
(t.f : t  t.x : t. f 2x) (t.f : t  t.x : t. f 3x) = t.f: tt. (t.f : t  t.x : t. f 2x) t ((t.f : t  t.x : t. f 3x) t f) = t.f: tt. (t.f : t  t.x : t. f 2x) t (x : t. f 3x) = t.f: tt. (x : t. (x : t. f 3x) ((x : t. f 3x) x)) = t.f: tt. (x : t. (x : t. f 3x) (f 3x)) = t.f: t  t. x : t. f 6x  6

49 7.3 非直谓式多态演算 还可以用一个正好带两个范式的类型来表示布尔值 true  t.x:t.y:t.x
false  t.x:t.y:t.y bool  t.ttt zero?  x:nat.x bool (x:bool.false) true

50 7.3 非直谓式多态演算 7.3.3 归约的终止性 略去不介绍

51 7.4 数据抽象和存在类型 数据抽象以及相应的程序规范和模块性的概念可能是二十世纪七十年代有关程序设计语言最有影响的研究
7.4 数据抽象和存在类型 数据抽象以及相应的程序规范和模块性的概念可能是二十世纪七十年代有关程序设计语言最有影响的研究 抽象数据类型的声明，作为一种支持数据抽象的语言机制，已出现在一些程序设计语言中，包括Ada、Clu和ML 本节调查抽象数据类型声明的一种一般形式

52 7.4 数据抽象和存在类型 形式为 abstype t with x1: 1, …, xk: k is
7.4 数据抽象和存在类型 形式为 abstype t with x1: 1, …, xk: k is , M1, …, Mk in N 的声明描述抽象类型t 例 abstype stream with s: stream, first: stream  nat, rest: streamstream is , M1, M2, M3 in N

53 7.4 数据抽象和存在类型 使用笛卡儿积，可以把任何抽象数据类型声明写成abstype t with x: is , M in N的形式 抽象数据类型声明可以加到直谓式或非直谓式语言中 分别考虑抽象数据类型声明和数据类型实现 拓展类型表达式的语法，以包含存在类型  ::= … | t. 存在类型用于抽象数据类型的实现 存在类型t.的每个元素由一个类型和类型[/t] 的一个元素组成

54 7.4 数据抽象和存在类型 例：stream的实现总有类型 抽象数据类型的实现将以t =, M:的形式写出，其中
7.4 数据抽象和存在类型 例：stream的实现总有类型 t. (t  (t  nat)  (t  t)) 抽象数据类型的实现将以t =, M:的形式写出，其中 t =表示在该表达式的剩余部分将t约束到  称为t的表示类型

55   (abstype t with x: is M in N) : 
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) : 

56 7.4 数据抽象和存在类型 作为记号上的方便，把多于一个运算的声明作为一种语法美化：
7.4 数据抽象和存在类型 作为记号上的方便，把多于一个运算的声明作为一种语法美化： 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, …, xn]N n n

57 7.4 数据抽象和存在类型 例: abstype cmplx with create: real  real  cmplx,
7.4 数据抽象和存在类型 例: abstype cmplx with create: real  real  cmplx, plus: cmplx  cmplx  cmplx, re: cmplx  real im: cmplx  real is t = real  real, C, P, R, I: (real  real t)  (t  t  t)  (t  real)  (t real) in N

58 7.4 数据抽象和存在类型 C, P, R, I :…可以写成： C = p: real  real. p
7.4 数据抽象和存在类型 C, P, R, I :…可以写成： C = p: real  real. p P = z: real  real, w: real  real. Proj1 z + Proj1 w, Proj2 z + Proj2 w R = z: real  real. Proj1 z I = z: real  real. Proj2 z

59 7.4 数据抽象和存在类型 abstype的主要等式公理
7.4 数据抽象和存在类型 abstype的主要等式公理   (abstype t with x: is t = , M: in N) = [M/x][/t]N: ()   (x.M)N =[N/x]M : ()   abstype t with x: is M in N = abstype s with y: [s/t] is M in [y/x][s/t]N: ()   x.M =y.[y/x]M : ,其中yFV(M) ()   abstype t with x: is y in t = t, x: = y: t. ()   x.(Mx) =M : , 其中x FV(M) ()

60 7.5 类型表达式的分类 7.5.1 类型表达式的种类 （1）7.2节把类型表达式分成两个层次 普通类型和多态类型
7.5 类型表达式的分类 类型表达式的种类 （1）7.2节把类型表达式分成两个层次 普通类型和多态类型 在给出一些简化约定的情况下，类型表达式可用文法分成同样的两个层次 由于除了类型常量和类型变量外，只涉及函数类型，使得用文法推出的类型表达式都是良形的

61 7.5 类型表达式的分类 （2）类型表达式分成小全域和大全域，不足以解决类型表达式是否为良形的问题 在 演算上再增加积类型或和类型时
7.5 类型表达式的分类 （2）类型表达式分成小全域和大全域，不足以解决类型表达式是否为良形的问题 在 演算上再增加积类型或和类型时 若类型变量t代表二元积类型，则fst(t)（取t的第一元）是良形的类型表达式，否则fst(t)不是良形的类型表达式 这时良形的类型表达式很难用7.2节的文法形式表示

62 7.5 类型表达式的分类 （3）需要考虑类型表达式新的分类方式
7.5 类型表达式的分类 （3）需要考虑类型表达式新的分类方式 例如，所有的函数类型、所有的表类型、所有的二叉树类型等，并且对类型表达式的量化是以这样的类型族为论域 可以通过丰富语言结构来解决这些问题 用类型对项进行分类 用较高层次的种类（kind）来对类型进行分类 当前很多研究工作中的类型系统都是按这种思路来设计

63 7.5 类型表达式的分类  , 演算有项、类型和种类三种语法范畴 语法范畴 项目 具体形式
7.5 类型表达式的分类  , 演算有项、类型和种类三种语法范畴 语法范畴 项目 具体形式 种类  ::= Type |   |   类型  ::= b | t |   |   | fst() | snd() | t:. |  项 M ::= c | x | x:.M | MM | M, N | Proj1M | Proj2M | t:.M | M 种类文法产生的任何种类表达式都是良形的 符号和在这里是重载的 基本类型和普通函数类型归到Type种类

64 7.5 类型表达式的分类  , 演算有项、类型和种类三种语法范畴 语法范畴 项目 具体形式
7.5 类型表达式的分类  , 演算有项、类型和种类三种语法范畴 语法范畴 项目 具体形式 种类  ::= Type |   |   类型  ::= b | t |   |   | fst() | snd() | t:. |  项 M ::= c | x | x:.M | MM | M, N | Proj1M | Proj2M | t:.M | M 任意两个类型，它们的积属于某个积种类12 由t:.表示的类型上的函数属于某个函数种类

65 7.5 类型表达式的分类 7.5.2 类型表达式的定类与相等 类型表达式的定类（kinding）断言
7.5 类型表达式的分类 类型表达式的定类与相等 类型表达式的定类（kinding）断言 断言的形式为   : ，其中定类上下文 是形式为  = {t1 : 1, …, tn : n} 其中dom() = {t1, …, tn} 类似于项的定型断言  M : 

66 7.5 类型表达式的分类 7.5.2 类型表达式的定类与相等 类型表达式的定类（kinding）断言
7.5 类型表达式的分类 类型表达式的定类与相等 类型表达式的定类（kinding）断言 断言的形式为   : ，其中定类上下文 是形式为  = {t1 : 1, …, tn : n} 其中dom() = {t1, …, tn} 它给类型变量进行种类指派，类似于项的定型断言  M : 

67 7.5 类型表达式的分类 定类规则   b : Type （每个类型常量b : Type） (cstt)
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

68 7.5 类型表达式的分类 定类规则 (k Elim)1    :12   fst() :1 (k Elim)2
7.5 类型表达式的分类 定类规则 (k Elim)1 (k Elim)2 (k Intro) (k Elim)    :12   fst() :1    :12   snd() :2 , t :1  2 :2   (t :1. ): 1 2   1 :   2 :   12 : 

69   fst()snd() = :12
7.5 类型表达式的分类 类型表达式的相等规则 (Projt)1 (Projt)2 (spt)   (t:.) = (t:.[t/t]) :    其中tFV() (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

70   (t: .1)2 = [2/t]1:
7.5 类型表达式的分类 类型表达式的相等规则 (t) (t) 上述类型表达式的定类规则和相等规则给出 了类型表达式上一个简单的演算系统 类型表达式被称为语言的静态数据，而项被 称为语言的动态数据 , t:  1:   2:   (t: .1)2 = [2/t]1:    :1 2 tdom()   (t:1. t) =  :1 2

71 7.5 类型表达式的分类 7.5.3 项的定型 定型断言   M :  种类指派  = {t1 : 1, …, tn : n}
7.5 类型表达式的分类 7.5.3 项的定型 定型断言   M :  种类指派  = {t1 : 1, …, tn : n} 类型指派  = {x1 : 1, …, xn : n} 和都是无序集合，两者的次序不能颠倒 下面默认：出现定型公理和推理规则的在定类上下文下都是良种类的类型表达式    c :  （对基调中的每个项常量c : ）(cst)  , x :  x : (var)

72 7.5 类型表达式的分类 (add var)   M:  , x : M: ( Intro)
7.5 类型表达式的分类 (add var) ( Intro) ( Elim) ( Intro)   M:  , x : M:  , x :1M:2    (x :1.M): 12   M:   N :    MN:   M:1   N : 2    MN:12

73 7.5 类型表达式的分类 ( Elim)1    :12   M:  Proj1(M) : fst()
7.5 类型表达式的分类 ( Elim)1 ( Elim)2 ( Intro) ( Elim)    :1   M:  Proj1(M) : fst()    :1   M:  Proj2(M) : snd() , t:  M:    (t:.M):  (t:.)   M:(t:.)    :    M :(t:.)

74 7.5 类型表达式的分类 (type eq)   M:1   1 = 2 :    M:2

75 习 题 第一次：7.1, 7.2, 7.3(a), 7.5 第二次： 7.11 (a), 7.15 (a)