第五章 类 型 检 查 本章内容 语法 分析 器 类型 检查 中间 代码 生成 语法树 表示 记号流 静态检查中最典型的部分 — 类型检查： 类型系统、类型检查、多态函数、重载 忽略其它的静态检查：控制流检查、唯一性检查、关联名字检查 语法 分析 器 类型 检查 中间 代码 生成 语法树 表示 记号流

5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 介绍一些和程序运行有联系的概念

5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类 会被捕获的错误（trapped error）

5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类 会被捕获的错误（trapped error） 例：非法指令错误

5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类 会被捕获的错误（trapped error） 例：非法指令错误、非法内存访问

5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 1、程序运行时的执行错误分成两类 会被捕获的错误（trapped error） 例：非法指令错误、非法内存访问、除数为零 引起计算立即停止 不会被捕获的错误（untrapped error） 例：下标变量的访问越过了数组的末端 例：跳到一个错误的地址，该地址开始的内存正好代表一个指令序列 错误可能会有一段时间未引起注意

5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 2、良行为的程序 3、安全语言 不同场合对良行为的定义略有区别 例如，没有任何不会被捕获错误的程序 3、安全语言 任何合法程序都是良行为的 通常是设计一个类型系统，通过静态的类型检查来拒绝不会被捕获错误 但是，设计一个类型系统，它正好只拒绝不会被捕获错误是非常困难的

5.1 类型在编程语言中的作用 5.1.1 执行错误和安全语言 禁止错误（forbidden error） 不会被捕获错误集合 + 会被捕获错误的一个子集 为语言设计类型系统的目标是在排除禁止错误 良行为程序和安全语言也可基于禁止错误来定义

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 4、类型化的语言 变量的类型 变量在程序执行期间的取值范围

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 4、类型化的语言 变量的类型 类型化的语言 变量都被给定类型的语言 表达式、语句等程序构造的类型都可以静态确定 例如，类型boolean的变量x在程序每次运行时的值只能是布尔值，not (x)总有意义

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 4、类型化的语言 变量的类型 类型化的语言 未类型化的语言 不限制变量值范围的语言： 一个运算可以作用到任意的运算对象，其结果可能是一个有意义的值、一个错误、一个异常或一个语言未加定义的结果 例如：LISP语言

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 4、类型化的语言 变量的类型 类型化的语言 未类型化的语言 显式类型化语言 类型是语法的一部分

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 4、类型化的语言 变量的类型 类型化的语言 未类型化的语言 显式类型化语言 隐式类型化的语言 不存在隐式类型化的主流语言，但可能存在忽略类型信息的程序片段，例如不需要程序员声明函数的参数类型

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 5、类型系统 语言的组成部分,它由一组定型规则（typing rule）构成，这组规则用来给各种程序构造指派类型 设计类型系统的根本目的是用静态检查的方式来保证合法程序运行时的良行为 类型系统的形式化 类型表达式、定型断言、定型规则 类型检查算法 通常是静态地完成类型检查

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 6、良类型的程序 7、合法程序 8、类型可靠（type sound）的语言 没有类型错误的程序 7、合法程序 良类型程序（若语言定义中，除了类型系统外，没有用其它方式表示的对程序的约束） 8、类型可靠（type sound）的语言 所有良类型程序（合法程序）都是良行为的 类型可靠的语言一定是安全的语言

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 语法的和静态的概念 动态的概念 类型化语言 安全语言 语法的和静态的概念 动态的概念 类型化语言 安全语言 良类型程序 良行为的程序

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 9、类型检查：未类型化语言 10、类型检查：类型化语言 可以通过彻底的运行时详细检查来排除所有的禁止错误 如LISP语言 10、类型检查：类型化语言 类型检查也可以放在运行时完成，但影响效率 一般都是静态检查，类型系统被用来支持静态检查 静态检查语言通常也需要一些运行时的检查 数组访问越界检查

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 实际使用的一些语言并不安全 禁止错误集合没有囊括所有不会被捕获的错误 Pascal语言 无标志的变体记录类型 函数类型的参数

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 实际使用的一些语言并不安全 禁止错误集合没有囊括所有不会被捕获的错误 Pascal语言 用C语言的共用体（union）来举例 union U { int u1; int u2;} u; int p; u.u1 = 10; p = u.u2; p = 0;

5.1 类型在编程语言中的作用 5.1.2 类型化语言和类型系统 实际使用的一些语言并不安全 C语言 还有很多不安全的并且被广泛使用的特征，如： 指针算术运算、类型强制、参数个数可变 在语言设计的历史上，安全性考虑不足是因为当时强调代码的执行效率 在现代语言设计上，安全性的位置越来越重要 C的一些问题已经在C++中得以缓和 更多一些问题在Java中已得到解决

5.1 类型在编程语言中的作用 5.1.3 类型化语言的优点 从工程的观点看，类型化语言有下面一些优点 开发的实惠 编译的实惠 运行的实惠 较早发现错误 类型信息还具有文档作用 编译的实惠 程序模块可以相互独立地编译 运行的实惠 可得到更有效的空间安排和访问方式

5.2 描述类型系统的语言 类型系统主要用来说明编程语言的定型规则,它独立于类型检查算法 定义一个类型系统，一种重要的设计目标是存在有效的类型检查算法 类型系统的基本概念可用于各类语言，包括函数式语言、命令式语言和并行语言等 本节讨论用形式方法来描述类型系统 然后讨论实例语言时：先定义语法，再给出类型系统的形式描述，最后写出类型检查的翻译方案

5.2 描述类型系统的语言 类型系统的形式化 类型系统是一种逻辑系统 有关自然数的逻辑系统 - 自然数表达式（需要定义它的语法） - 自然数表达式（需要定义它的语法） a+b, 3 - 良形公式 （逻辑断言，需要定义它的语法） a+b=3, (d=3)(c<10) - 推理规则 a < b, b < c a < c

5.2 描述类型系统的语言 类型系统的形式化 类型系统是一种逻辑系统 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 a+b, 3 int, int  int - 良形公式 a+b=3, (d=3)(c<10) - 推理规则 a < b, b < c a < c

5.2 描述类型系统的语言 类型系统的形式化 类型系统是一种逻辑系统 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 a+b, 3 int, int  int - 良形公式 定型断言 a+b=3, (d=3)(c<10) x:int |– x+3 : int 推理规则 ( |–左边部分x:int称为 定型环境 ) a < b, b < c a < c

5.2 描述类型系统的语言 类型系统的形式化 类型系统是一种逻辑系统 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 a+b, 3 int, int  int - 良形公式 定型断言 a+b=3, (d=3)(c<10) x:int |– x+3 : int - 推理规则 定型规则 a < b, b < c a < c  |– M : int,  |– N : int  |– M + N : int

5.2 描述类型系统的语言 类型系统的形式化 类型表达式 定型断言 定型规则 具体语法：出现在编程语言中 抽象语法：出现在定型断言和类型检查的实现中 下一节开始举例 定型断言 本节讨论它的一般形式 定型规则

5.2 描述类型系统的语言 5.2.1 断言 断言的形式  |– S S的所有自由变量都声明在中 其中 是一个静态定型环境，如x1:T1, …, xn:Tn S的形式随断言形式的不同而不同 断言有三种具体形式

5.2 描述类型系统的语言 环境断言 语法断言 定型断言  |–  该断言表示是良形的环境  |–  该断言表示是良形的环境 将用推理规则来定义环境的语法(而不是用文法) 语法断言  |– nat 在环境下，nat是类型表达式 将用推理规则来定义类型表达式的语法 定型断言  |– M : T 在环境下， M具有类型T 例： |– true : boolean x : nat |– x+1 : nat 将用推理规则来确定程序构造实例的类型

5.2 描述类型系统的语言 有效断言  |– true : boolean 无效断言  |– true : nat

5.2 描述类型系统的语言 5.2.2 推理规则 习惯表示法 前提、结论 1 |– S1, …, n |– Sn 公理、推理规则

5.2 描述类型系统的语言 5.2.2 推理规则 （规则名） （注释） 推理规则 （注释） 环境规则 (Env )  |– 

5.2 描述类型系统的语言 5.2.2 推理规则 （规则名） （注释） 推理规则 （注释） 环境规则 (Env ) 语法规则 （规则名） （注释） 推理规则 （注释） 环境规则 (Env ) 语法规则 (Type Bool)  |–   |–   |– boolean

5.2 描述类型系统的语言 5.2.2 推理规则 （规则名） （注释） 推理规则 （注释） 环境规则 (Env ) 语法规则 （规则名） （注释） 推理规则 （注释） 环境规则 (Env ) 语法规则 (Type Bool) 定型规则 (Val +)  |–   |–   |– boolean  |– M : int,  |– N : int  |– M + N : int

5.2 描述类型系统的语言 5.2.3 类型检查和类型推断 类型检查 用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构造的过程

5.2 描述类型系统的语言 5.2.3 类型检查和类型推断 类型检查 用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构造的过程 类型推断 类型信息不完全的情况下的定型判定问题 例如：f (x : t) = E 和 f (x) = E的区别

5.3 简单类型检查器的说明 5.3.1 一个简单的语言 P  D ; S D  D ; D | id : T T  boolean | integer | array [num ] of T | T | T ‘’T S  id := E | if E then S | while E do S | S ; S E  truth | num | id | E mod E | E [ E ] | E | E (E )

5.3 简单类型检查器的说明 例 i : integer; j : integer; j := i mod 2000

5.3 简单类型检查器的说明 5.3.2 类型系统 环境规则 (Env ) (Decl Var)  |–  其中id : T是该简单语言的一个声明语句 略去了基于程序中所有声明语句来构成整个的规则  |–  |T, id  dom () , id : T | 

5.3 简单类型检查器的说明 语法规则 (Type Bool)  |   | boolean (Type Int) (Type Void) void用于表示语句类型 表明编程语言和定型断言的类型表达式并非完全一致  |   | boolean  |   | integer  |   | void

5.3 简单类型检查器的说明 语法规则 (Type Ref) (T  void) 具体语法： T  | T (Type Array) (T  void) (N>0) 具体语法： array [N] of T (Type Function) (T1, T2  void) 定型断言中的类型表达式用的是抽象语法  | T  | pointer(T)  | T,  | N : integer  | array(N, T)  | T1,  | T2  | T1  T2

5.3 简单类型检查器的说明 定型规则——表达式 (Exp Truth)  |   | truth : boolean (Exp Num) (Exp Id)  |   | truth : boolean  |   | num : integer 1, id : T, 2 |  1, id : T, 2 | id : T

5.3 简单类型检查器的说明 定型规则——表达式 (Exp Mod)  | E1: integer,  | E2: integer (Exp Index) (0  E2  N1) (Exp Deref)  | E1: integer,  | E2: integer  | E1 mod E2: integer  | E1: array(N,T),  | E2: integer  | E1[E2] : T  | E : pointer(T)  | E : T

5.3 简单类型检查器的说明 定型规则——表达式 (Exp FunCall)  | E1: T1  T2,  | E2: T1  | E1 (E2) : T2

 | E : boolean,  | S : void  | E : boolean,  | S : void 5.3 简单类型检查器的说明 定型规则——语句 (State Assign) (T=boolean or T= integer) (State If) (State While)  | id : T,  | E : T  | id := E : void  | E : boolean,  | S : void  | if E then S : void  | E : boolean,  | S : void  | while E do S: void

5.3 简单类型检查器的说明 定型规则——语句 (State Seq)  | S1: void,  | S2: void  | S1; S2 : void

5.3 简单类型检查器的说明 5.3.3 类型检查 设计语法制导的类型检查器 设计依据是上节的类型系统 类型环境的信息进入符号表 对类型表达式采用抽象语法 具体：array [N] of T 抽象：array (N, T) T pointer (T) 考虑到报错的需要，增加了类型type_error

5.3 简单类型检查器的说明 5.3.3 类型检查——声明语句 D  D; D D  id : T {addtype (id.entry, T.type)} addtype：把类型信息填入符号表

5.3 简单类型检查器的说明 5.3.3 类型检查——声明语句 D  D; D D  id : T {addtype (id.entry, T.type)} T  boolean {T.type = boolean} T  integer {T.type = integer} T  T1 {T.type = pointer(T1.type)}

5.3 简单类型检查器的说明 5.3.3 类型检查——声明语句 D  D; D D  id : T {addtype (id.entry, T.type)} T  boolean {T.type = boolean} T  integer {T.type = integer} T  T1 {T.type = pointer(T1.type)} T  array [num] of T1 {T.type = array(num.val, T1.type)}

5.3 简单类型检查器的说明 5.3.3 类型检查——声明语句 D  D; D D  id : T {addtype (id.entry, T.type)} T  boolean {T.type = boolean} T  integer {T.type = integer} T  T1 {T.type = pointer(T1.type)} T  array [num] of T1 {T.type = array(num.val, T1.type)} T  T1 ‘’ T2 {T.type = T1.type  T2.type }

5.3 简单类型检查器的说明 类型检查——表达式 E  truth {E.type = boolean } E  num {E.type = integer} E  id {E.type = lookup(id.entry)}

5.3 简单类型检查器的说明 类型检查——表达式 E  truth {E.type = boolean } E  num {E.type = integer} E  id {E.type = lookup(id.entry)} E  E1 mod E2 {E.type = if E1.type == integer and E2. type == integer then integer else type_error }

5.3 简单类型检查器的说明 类型检查——表达式 E  E1 [E2 ] {E.type = if E2. type == integer and E1. type == array(s, t) then t else type_error }

5.3 简单类型检查器的说明 类型检查——表达式 E  E1 [E2 ] {E.type = if E2. type == integer and E1. type == array(s, t) then t else type_error } E  E1 {E.type = if E1.type == pointer(t) then t

5.3 简单类型检查器的说明 类型检查——表达式 E  E1 [E2 ] {E.type = if E2. type == integer and E1. type == array(s, t) then t else type_error } E  E1 {E.type = if E1.type == pointer(t) then t E  E1 (E2 ) {E. type = if E2 . type == s and E1. type == s  t then t

5.3 简单类型检查器的说明 类型检查——语句 S  id := E { if (id.type == E.type && E.type  {boolean, integer}) S.type = void; else S.type = type_error;}

5.3 简单类型检查器的说明 类型检查——语句 S  id := E { if (id.type == E.type && E.type  {boolean, integer}) S.type = void; else S.type = type_error;} S  if E then S1 {S. type = if E. type == boolean then S1. type else type_error }

5.3 简单类型检查器的说明 类型检查——语句 S  while E do S1 {S.type = if E.type == boolean then S1. type else type_error }

5.3 简单类型检查器的说明 类型检查——语句 S  while E do S1 {S.type = if E.type == boolean then S1. type else type_error } S  S1; S2 {S. type = if S1. type == void and S2. type == void then void

5.3 简单类型检查器的说明 类型检查——程序 P  D; S {P. type = if S. type == void then void else type_error }

5.3 简单类型检查器的说明 5.3.4 类型转换 E  E1 op E2 {E.type = if E1.type == integer and E2.type == integer then integer else if E1.type == integer and E2.type == real then real else if E1.type == real and E2.type == integer else if E1.type == real and E2.type == real else type_error }

5.4 多 态 函 数 5.4.1 为什么要使用多态函数 例：用Pascal语言写不出求表长度的通用程序 若有下面的类型 type link = cell ; cell = record info : integer; next : link end; 针对这个类型，可以写出下页的表长函数

5.4 多 态 函 数 function length(lptr : link) : integer; var len : integer; begin len := 0; while lptr <> nil do begin len := len + 1; lptr := lptr. next end; length := len 计算过程并不涉及 表元的数据类型 但语言的类型系统 使得该函数不能通用

5.4 多 态 函 数 例：用ML语言很容易写出求表长度的程序而不必管表元的类型 fun length (lptr) = if null (lptr) then 0 else length (tl (lptr)) + 1;

5.4 多 态 函 数 例：用ML语言很容易写出求表长度的程序而不必管表元的类型 fun length (lptr) = if null (lptr) then 0 else length (tl (lptr)) + 1; length ( [“sun”, “mon”, “tue”] ) length ( [10, 9, 8 ] ) 都等于3

5.4 多 态 函 数 多态函数 多态算符 允许变元的类型有多种不同的情况 函数体中的语句的执行能适应变元类型有多种不同的情况（区别于重载的特征） 多态算符 例如：数组索引、函数应用、通过指针间接访问 相应操作的代码段接受不同类型的数组、函数等 C语言手册中关于取地址算符&的论述是： 如果运算对象的类型是‘…’，那么结果类型是指向‘…’的指针”

5.4 多 态 函 数 5.4.2 类型变量 length的类型可以写成.list()  integer 允许使用类型变量，还便于讨论未知类型 在不要求标识符的声明先于使用的语言中，通过类型变量的使用去确定程序变量的类型

5.4 多 态 函 数 例 function deref (p); begin return p end;

5.4 多 态 函 数 例 function deref (p); -- 对p的类型一无所知： begin return p end;

5.4 多 态 函 数 例 function deref (p); -- 对p的类型一无所知： begin return p --  = pointer( ) end;

5.4 多 态 函 数 例 function deref (p); -- 对p的类型一无所知： begin return p --  = pointer( ) end; deref的类型是. pointer( )  

5.4 多 态 函 数 5.4.3 一个含多态函数的语言 P  D; E 引入类型变量、笛卡 D  D; D | id : Q 儿积类型、多态函数 Q  type-variable. Q | T T  T ‘’T | T  T | unary-constructor ( T ) | basic-type | type-variable | ( T ) E  E (E ) | E, E | id

5.4 多 态 函 数 5.4.3 一个含多态函数的语言 P  D; E 引入类型变量、笛卡 D  D; D | id : Q 儿积类型、多态函数 Q  type-variable. Q | T T  T ‘’T | T  T 这是一个抽象语言, | unary-constructor ( T ) 忽略了函数定义的 | basic-type 函数体 | type-variable | ( T ) E  E (E ) | E, E | id

5.4 多 态 函 数 5.4.3 一个含多态函数的语言 P  D; E D  D; D | id : Q Q  type-variable. Q | T T  T ‘’T | T  T | unary-constructor ( T ) 一个程序： | basic-type deref : . pointer( )  ; | type-variable q : pointer (pointer (integer)); | ( T ) deref (deref (q)) E  E (E ) | E, E | id

5.4 多 态 函 数 类型系统中增加的推理规则 环境规则 语法规则 (Env Var)  | ,   dom () (Type Var) (Type Product)  | ,   dom () ,  |  1,  , 2 |  1,  , 2 |   | T1,  | T2  | T1  T2

5.4 多 态 函 数 类型系统中增加的推理规则 语法规则 (Type Parenthesis)  | T (Type Forall) (Type Fresh)  | T  | (T ) ,  | T  | .T  | .T , , i |  , i | [i /] T

5.4 多 态 函 数 类型系统中增加的推理规则 定型规则 (Exp Pair)  | E1: T1， | E2: T2 (Exp FunCall) (其中S是T1和T3的最一般的合一代换)  | E1: T1， | E2: T2  | E1, E2: T1  T2  | E1: T1  T2,  | E2: T3  | E1 (E2) : S(T2)

5.4 多 态 函 数 5.4.4 代换、实例和合一 1、代换: 类型表达式中的类型变量用其所代表的类型表达式去替换

5.4 多 态 函 数 5.4.4 代换、实例和合一 1、代换: 类型表达式中的类型变量用其所代表的类型表达式去替换 function subst (t : type_expression ) : type_expression; begin if t是基本类型 then return t else if t是类型变量then return S(t) else if t 是t1 t2 then return subst(t1)  subst(t2) end

5.4 多 态 函 数 2、实例 把subst函数用于t后所得的类型表达式是t的一个实例，用S (t)表示。 例子（s < t 表示s是t 的实例） pointer( integer ) < pointer( ) pointer( real ) < pointer( ) integer  integer <   pointer( ) <   < 

5.4 多 态 函 数 下面左边的类型表达式不是右边的实例 integer real 代换不能用于基本类型  的代换不一致 integer       的所有出现都应该代换

5.4 多 态 函 数 3、合一 如果存在某个代换S使得S(t1) = S(t2)，那么这两个表达式t1和t2能够合一 对任何其它满足S(t1) = S(t2)的代换S，代换S(t1)是S(t1)的实例

5.4 多 态 函 数 5.4.5 多态函数的类型检查 多态函数和普通函数在类型检查上的区别 (1)同一多态函数的不同出现无须变元有相同类型 apply: o derefo:pointer(o)  o apply : i derefi : pointer(i) i q: pointer(pointer(integer)) deref(deref (q ))的带标记的语法树

5.4 多 态 函 数 (2)必须把类型相同的概念推广到类型合一 apply: o derefo:pointer(o)  o apply : i derefi : pointer(i) i q: pointer(pointer(integer)) deref(deref (q ))的带标记的语法树

5.4 多 态 函 数 (2)必须把类型相同的概念推广到类型合一 (3)要记录类型表达式合一的结果 apply: o derefo:pointer(o)  o apply : i derefi : pointer(i) i q: pointer(pointer(integer)) deref(deref (q ))的带标记的语法树

5.4 多 态 函 数 EE1 (E2 ) {p = mkleaf (newtypevar); 检查多态函数的翻译方案 EE1 (E2 ) {p = mkleaf (newtypevar); unify (E1. type, mknode ( ‘’, E2.type, p) ); E. type = p} E  E1, E2 {E. type = mknode ( ‘’, E1.type , E2.type)} E  id {E. type = fresh (lookup(id.entry))}

5.4 多 态 函 数 表 达 式 ： 类 型 代 换 q : pointer(pointer(integer)) 表 达 式 ： 类 型 代 换 q : pointer(pointer(integer)) derefi : pointer(i)  i derefi(q) : pointer(integer) i = pointer(integer) derefo : pointer(o)  o derefo(derefi (q)) : integer o = integer apply: o derefo:pointer(o)  o apply : i derefi : pointer(i)  i q: pointer(pointer(integer))

5.4 多 态 函 数 确定表长度的ML函数 fun length (lptr) = if null (lptr) then 0 else length (tl (lptr)) + 1; 为完成类型检查 把它用抽象语言来改写（见下一页）

5.4 多 态 函 数 类型声明部分 length :  ; lptr :  ; if :  . boolean    ; null :  . list ()  boolean ; tl :  . list ()  list () ; 0 : integer ; 1 : integer ; + : integer  integer  integer ; match :  .     ; match ( -- 表达式，匹配length函数的 length (lptr), -- 函数首部和函数体的类型 if (null (lptr), 0, length (tl(lptr)) +1) ) 类型声明部分

5.4 多 态 函 数 行 定 型 断 言 代 换 规 则 (1) lptr :  (Exp Id) (2) length :  (3) 定 型 断 言 代 换 规 则 (1) lptr :  (Exp Id) (2) length :  (3) length(lptr) :   =    (Exp FunCall) (4) 从(1)可得 (5) null : list(n)  boolean (Exp Id)和(Type Fresh) (6) null(lptr) : boolean  = list (n) (7) 0 : integer (Exp Num) (8) lptr : list(n)

5.4 多 态 函 数 行 定 型 断 言 代 换 规 则 (9) tl : list(t)  list(t) 定 型 断 言 代 换 规 则 (9) tl : list(t)  list(t) (Exp Id)和(Type Fresh) (10) tl(lptr) : list(n) t = n (Exp FunCall) (11) length : list(n)   从(2)可得 (12) length(tl(lptr)) :  (13) 1 : integer (Exp Num) (14) + : integer  integer  integer (Exp Id)

5.4 多 态 函 数 行 定 型 断 言 代 换 规 则 (15) length (tl(lptr)) +1 : integer 定 型 断 言 代 换 规 则 (15) length (tl(lptr)) +1 : integer  = integer (Exp FunCall) (16) if : boolean i i i (Exp Id)和(Type Fresh) (17) if ( ... ) : integer i = integer (18) match : m  m m (19) match ( … ) : integer m=integer

5.4 多 态 函 数 fun length (lptr) = if null (lptr) then 0 else length (tl (lptr)) + 1; length函数的类型是 . list()  integer

5.5 类型表达式的等价 当允许对类型表达式命名后： 类型表达式是否相同就有了不同的解释 出现了结构等价和名字等价两个不同的概念 5.5 类型表达式的等价 当允许对类型表达式命名后： 类型表达式是否相同就有了不同的解释 出现了结构等价和名字等价两个不同的概念 type link = cell; var next : link; last : link; p : cell; q, r : cell;

5.5 类型表达式的等价 5.5.1 类型表达式的结构等价 两个类型表达式完全相同（当无类型名时） type link = cell; 5.5 类型表达式的等价 5.5.1 类型表达式的结构等价 两个类型表达式完全相同（当无类型名时） type link = cell; var next : link; last : link; p : cell; q, r : cell;

5.5 类型表达式的等价 5.5.1 类型表达式的结构等价 两个类型表达式完全相同（当无类型名时） 类型表达式树一样 5.5 类型表达式的等价 5.5.1 类型表达式的结构等价 两个类型表达式完全相同（当无类型名时） 类型表达式树一样 type link = cell; var next : link; last : link; p : cell; q, r : cell;

5.5 类型表达式的等价 5.5.1 类型表达式的结构等价 两个类型表达式完全相同（当无类型名时） 类型表达式树一样 5.5 类型表达式的等价 5.5.1 类型表达式的结构等价 两个类型表达式完全相同（当无类型名时） 类型表达式树一样 相同的类型构造符作用于相同的子表达式 type link = cell; var next : link; last : link; p : cell; q, r : cell;

5.5 类型表达式的等价 5.5.1 类型表达式的结构等价 两个类型表达式完全相同（当无类型名时） 有类型名时，用它们所定义的类型表达式代换 5.5 类型表达式的等价 5.5.1 类型表达式的结构等价 两个类型表达式完全相同（当无类型名时） 有类型名时，用它们所定义的类型表达式代换 它们，所得表达式完全相同(类型定义无环时) type link = cell; var next : link; last : link; p : cell; q, r : cell; cell cell next, last, p, q和r结构等价

5.5 类型表达式的等价 类型表达式的结构等价测试sequiv(s, t) (无类型名时) if s 和 t 是相同的基本类型then 5.5 类型表达式的等价 类型表达式的结构等价测试sequiv(s, t) (无类型名时) if s 和 t 是相同的基本类型then return true else if s == array(s1, s2) and t == array(t1, t2) then return sequiv(s1, t1) and sequiv(s2, t2) else if s == s1  s2 and t == t1 t2 then else if s == pointer (s1) and t == pointer(t1) then return sequiv(s1, t1) else if s == s1  s2 and t == t1  t2 then return squiv(s1, t1) and sequiv(s2, t2) else return false

5.5 类型表达式的等价 5.5.2 类型表达式的名字等价 把每个类型名看成是一个可区别的类型 type link = cell; 5.5 类型表达式的等价 5.5.2 类型表达式的名字等价 把每个类型名看成是一个可区别的类型 type link = cell; var next : link; last : link; p : cell; q, r : cell;

5.5 类型表达式的等价 5.5.2 类型表达式的名字等价 把每个类型名看成是一个可区别的类型 两个类型表达式名字等价当且仅当这两个类 5.5 类型表达式的等价 5.5.2 类型表达式的名字等价 把每个类型名看成是一个可区别的类型 两个类型表达式名字等价当且仅当这两个类 型表达式不进行名字代换就能结构等价 type link = cell; var next : link; last : link; p : cell; q, r : cell; next和last名字等价 p, q和r名字等价

5.5 类型表达式的等价 Pascal的许多实现用隐含的类型名和每个 声明的标识符联系起来 5.5 类型表达式的等价 Pascal的许多实现用隐含的类型名和每个 声明的标识符联系起来 type link = cell; type link = cell; var next : link; np = cell; last : link; nqr = cell; p : cell; var next : link; q, r : cell; last : link; p : np; q : nqr; r : nqr; 这时，p与q和r 不是名字等价

5.5 类型表达式的等价 注意: 类型名字的引入只是类型表达式的一个语法约定问题，它并不像引入类型构造符或类型变量那样能丰富所能表达的类型

5.5 类型表达式的等价 5.5.3 记录类型 (Type Record) (li是有区别的)  | T1, …,  | Tn 5.5 类型表达式的等价 5.5.3 记录类型 (Type Record) (li是有区别的) (Val Record) (li是有区别的) (Val Record Select)  | T1, …,  | Tn  | record(l1:T1, …, ln:Tn)  | M1:T1,…,  | Mn: Tn  | record (l1=M1, …, ln=Mn) : record (l1:T1, …, ln:Tn)  | M : record(l1:T1, …, ln:Tn)  | M.lj : Tj (j 1..n)

5.5 类型表达式的等价 5.5.4 类型表示中的环 type link =  cell ; cell = record 5.5 类型表达式的等价 5.5.4 类型表示中的环 type link =  cell ; cell = record info : integer ; next : link end; cell = record ， : info pointer next integer cell 引入环的话，递归定义 的类型名可以替换掉

5.5 类型表达式的等价 5.5.4 类型表示中的环 type link =  cell ; cell = record 5.5 类型表达式的等价 5.5.4 类型表示中的环 type link =  cell ; cell = record info : integer ; next : link end; cell = record ， : info pointer next integer 结构等价测试过程有可 能不终止

5.5 类型表达式的等价 C语言对除记录（结构体）以外的所有类型使 用结构等价，而记录类型用的是名字等价，以 避免类型图中的环 5.5 类型表达式的等价 C语言对除记录（结构体）以外的所有类型使 用结构等价，而记录类型用的是名字等价，以 避免类型图中的环 cell = record ， : info pointer next integer cell

5.6 函数和算符的重载 重载符号 有多个含义，但在每个引用点的含义都是唯一的 例如： 重载的消除 在重载符号的引用点，其含义能确定到唯一 5.6 函数和算符的重载 重载符号 有多个含义，但在每个引用点的含义都是唯一的 例如： 加法算符+可用于不同类型，“+”是多个函数的名字，而不是一个多态函数的名字 在Ada中，( ) 是重载的，A( I ) 有不同含义 重载的消除 在重载符号的引用点，其含义能确定到唯一

5.6 函数和算符的重载 5.6.1 子表达式的可能类型集合 例 Ada语言 声明： 5.6 函数和算符的重载 5.6.1 子表达式的可能类型集合 例 Ada语言 声明： function “” (i, j : integer ) return complex; function “” (x, y : complex ) return complex;

5.6 函数和算符的重载 5.6.1 子表达式的可能类型集合 例 Ada语言 声明： 5.6 函数和算符的重载 5.6.1 子表达式的可能类型集合 例 Ada语言 声明： function “” (i, j : integer ) return complex; function “” (x, y : complex ) return complex; 使得算符重载，可能的类型包括： integer  integer  integer --这是预定义的类型 integer  integer  complex complex  complex  complex

5.6 函数和算符的重载 5.6.1 子表达式的可能类型集合 例 Ada语言 声明： 5.6 函数和算符的重载 5.6.1 子表达式的可能类型集合 例 Ada语言 声明： function “” (i, j : integer ) return complex; function “” (x, y : complex ) return complex; 使得算符重载，可能的类型包括： integer  integer  integer 2  (3  5) integer  integer  complex complex  complex  complex

5.6 函数和算符的重载 5.6.1 子表达式的可能类型集合 例 Ada语言 声明： 5.6 函数和算符的重载 5.6.1 子表达式的可能类型集合 例 Ada语言 声明： function “” (i, j : integer ) return complex; function “” (x, y : complex ) return complex; 使得算符重载，可能的类型包括： integer  integer  integer 2  (3  5) integer  integer  complex (3  5)  z complex  complex  complex z是复型

5.6 函数和算符的重载 以函数应用为例，考虑类型检查 在每个表达式都有唯一的类型时，函数应用 的类型检查是： 5.6 函数和算符的重载 以函数应用为例，考虑类型检查 在每个表达式都有唯一的类型时，函数应用 的类型检查是： EE1 (E2 ) {E. type = if E2. type == s and E1. type == s  t then t else type_ error }

5.6 函数和算符的重载 确定表达式可能类型的集合（类型可能不唯一） 产 生 式 语 义 规 则 E  E 5.6 函数和算符的重载 确定表达式可能类型的集合（类型可能不唯一） 产 生 式 语 义 规 则 E  E E.types = E. types E  id E. types = lookup(id. entry) E  E1 (E2) E. types = {t | E2. types中存在一个s，使得s  t属于E1.types }

5.6 函数和算符的重载 例：表达式3  5可能的类型集合 E: {i, c} E: {i} 3: {i} 5: {i}  : 5.6 函数和算符的重载 例：表达式3  5可能的类型集合 E: {i, c} E: {i} 3: {i} 5: {i}  : {i  i  i, i  i  c, c  c  c }

5.6 函数和算符的重载 5.6.2 缩小可能类型的集合 产 生 式 语 义 规 则 E  E E. types = E. types 5.6 函数和算符的重载 5.6.2 缩小可能类型的集合 产 生 式 语 义 规 则 E  E E. types = E. types E. unique = if E. types == { t } then t else type_error E. code = E.code E  id E. types = lookup(id. entry) E.code = gen(id.lexeme ‘:’ E. unique)

5.6 函数和算符的重载 E  E1 (E2) E. types = {s | E2. types中存在一个s，使得s  s属于E1. types} t = E. unique S = {s | s  E2. types and s  t  E1. types } E2. unique = if S == { s } then s else type_error E1. unique = if S == { s } then s  t else type_error E.code = E1.code || E2.code || gen(‘apply’ ‘:’ E. unique)

5.6 函数和算符的重载 注意1 重载的函数和符号的引入使得程序员可以用一个名字或符号表示多个不同类型的函数或运算，它不像引入类型构造符或类型变量那样能丰富我们所能表达的类型 注意2 刚才例子的属性计算必须用第4章提到的先分析后计算的方式 因为综合属性types和code不可能同时完成

本 章 要 点 静态检查所涉及的内容：类型检查、控制流检查、唯一性检查和关联名字检查等 类型在编程语言中的作用 本 章 要 点 静态检查所涉及的内容：类型检查、控制流检查、唯一性检查和关联名字检查等 类型在编程语言中的作用 描述类型系统的语言（类型表达式、类型断言、定型规则） 设计完成类型检查的语法制导定义 多态函数的类型检查（代换、实例和合一） 重载函数和多态函数的区别 类型表达式的等价

例 题 1 编译时的控制流检查的例子 main() { printf(“\n%ld\n”,gcd(4,12)); continue; } 例 题 1 编译时的控制流检查的例子 main() { printf(“\n%ld\n”,gcd(4,12)); continue; } 编译时的报错如下: continue.c: In function ‘main’: continue.c:3: continue statement not within a loop

例 题 2 编译时的唯一性检查的例子 main() { int i; switch(i){ 例 题 2 编译时的唯一性检查的例子 main() { int i; switch(i){ case 10: printf(“%d\n”, 10); break; case 20: printf(“%d\n”, 20); break; } 编译时的报错如下： switch.c: In function ‘main’: switch.c:6: duplicate case value switch.c:4: this is the first entry for that value

例 题 3 C语言 称&为地址运算符，&a为变量a的地址 数组名代表数组第一个元素的地址 问题： 如果a是一个数组名，那么表达式a和&a的值 例 题 3 C语言 称&为地址运算符，&a为变量a的地址 数组名代表数组第一个元素的地址 问题： 如果a是一个数组名，那么表达式a和&a的值 都是数组a第一个元素的地址，它们的使用是否 有区别？ 用四个C文件的编译报错或运行结果来提示

例 题 3 typedef int A[10][20]; A a; A *fun() { return(a); } 例 题 3 typedef int A[10][20]; A a;   A *fun() { return(a); } 该函数在Linux上用gcc编译，报告的错误如下: 第5行：warning: return from incompatible pointer type

例 题 3 typedef int A[10][20]; A a; A *fun() { return(&a); } 例 题 3 typedef int A[10][20]; A a;   A *fun() { return(&a); } 该函数在Linux上用gcc编译时，没有错误

例 题 3 typedef int A[10][20]; typedef int B[20]; A a; B *fun() { 例 题 3 typedef int A[10][20]; typedef int B[20]; A a;   B *fun() { return(a); } 该函数在Linux上用gcc编译时，没有错误

例 题 3 typedef int A[10][20]; A a; 例 题 3 typedef int A[10][20]; A a; fun() { printf(“%d,%d,%d\n”, a, a+1, &a+1);} main() { fun(); } 该程序的运行结果是： 134518112, 134518192, 134518912

例 题 3 结论 对一个t 类型的数组a[ i1 ][ i2 ]…[ in ]来说， 表达式a的类型是： 例 题 3 结论 对一个t 类型的数组a[ i1 ][ i2 ]…[ in ]来说， 表达式a的类型是： pointer(array(0.. i2–1, … array(0.. in–1, t)…)) 表达式&a的类型是： pointer(array(0.. i1–1, … array(0.. in–1, t)…))

例 题 4 在X86/Linux机器上，编译器报告最后一行有 错误：incompatible types in return 例 题 4 在X86/Linux机器上，编译器报告最后一行有 错误：incompatible types in return typedef int A1[10]; | A2 *fun1( ) { typedef int A2[10]; | return(&a); A1 a; | } typedef struct {int i;}S1; | S2 fun2( ) { typedef struct {int i;}S2; | return(s); S1 s; | } 在C语言中，数组和结构体都是构造类型， 为什么上面第2个函数有类型错误，而第1个函 数却没有？

例 题 5 编译器和连接装配器未能发现下面的调用错误 long gcd (p, q) long p, q;{/*这是参数声明的传统形式*/ 例 题 5 编译器和连接装配器未能发现下面的调用错误 long gcd (p, q) long p, q;{/*这是参数声明的传统形式*/ /*参数声明的现代形式是long gcd ( long p, long q) { */ if (p%q == 0) return q; else return gcd (q, p%q); } main() { printf(“%ld,%ld\n”, gcd(5), gcd(5,10,20));

习 题 第一次：5.4, 5.6 第二次：5.16, 5.17 第三次：5.18