编译原理类型检查学习培训模板课件

1、第五章 类 型 检 查 本章内容静态检查中最典型的部分 类型检查：类型系统、类型检查、多态函数、重载忽略其它的静态检查：控制流检查、唯一性检查、关联名字检查分析器类型检查器中间代码生成器语法树语法树中间表示记号流5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言介绍一些和程序运行有联系的概念5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言程序运行时的执行错误分成两类会被捕获的错误（trapped error）5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误5.1 类型在编程

2、语言中的作用5.1.1 执行错误和安全语言程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误、非法内存访问5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误、非法内存访问、除数为零5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误、非法内存访问、除数为零引起计算立即停止5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言程序运行时的执行错误分成两类会被捕获

3、的错误（trapped error）例：非法指令错误、非法内存访问、除数为零引起计算立即停止不会被捕获的错误（untrapped error） 5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误、非法内存访问、除数为零引起计算立即停止不会被捕获的错误（untrapped error） 例：下标变量的访问越过了数组的末端5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言程序运行时的执行错误分成两类会被捕获的错误（trapped error）例：非法指令错误、非法内存访问、除数为零引起计算立

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

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

6、任何合法程序都是良行为的通常是设计一个类型系统，通过静态的类型检查来拒绝不会被捕获错误但是，设计一个类型系统，它正好只拒绝不会被捕获错误是非常困难的5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言禁止错误（forbidden error）不会被捕获错误集合 + 会被捕获错误的一个子集5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言禁止错误（forbidden error）不会被捕获错误集合 + 会被捕获错误的一个子集为语言设计类型系统的目标是在排除禁止错误5.1 类型在编程语言中的作用5.1.1 执行错误和安全语言禁止错误（forbidden error）不会被捕获错误

7、集合 + 会被捕获错误的一个子集为语言设计类型系统的目标是在排除禁止错误良行为程序和安全语言也可基于禁止错误来定义5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统类型化的语言变量的类型变量在程序执行期间的取值范围5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统类型化的语言变量的类型类型化的语言变量都被给定类型的语言并且表达式、语句等语法构造的类型都是可以静态确定的例如，类型boolean的变量x在程序每次运行时的值只能是布尔值，not (x)总有意义5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统类型化的语言变量的类型类型化的语言未类型化的语言不限制变

8、量值范围的语言： 一个运算可以作用到任意的运算对象，其结果可能是一个有意义的值、一个错误、一个异常或一个语言未加定义的结果例如：LISP语言5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统类型化的语言变量的类型类型化的语言未类型化的语言显式类型化语言类型是语法的一部分5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统类型化的语言变量的类型类型化的语言未类型化的语言显式类型化语言隐式类型化的语言不存在隐式类型化的主流语言，但可能存在忽略类型信息的程序片段，例如不需要程序员声明函数的参数类型5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统类型系统语言的组成部

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

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

11、语言和类型系统良类型的程序没有类型错误的程序合法程序良类型程序（若语言定义中无其它方式表示的约束）类型可靠（type sound）的语言所有良类型程序（合法程序）都是良行为的类型可靠的语言一定是安全的语言5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统语法的和静态的概念动态的概念类型化语言安全语言良类型程序良行为的程序5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统未类型化语言可以通过彻底的运行时详细检查来排除所有的禁止错误如LISP语言5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统未类型化语言可以通过彻底的运行时详细检查来排除所有的禁止错误如LIS

12、P语言类型化语言类型检查也可以放在运行时完成，但影响效率一般都是静态检查，类型系统被用来支持静态检查静态检查语言通常也需要一些运行时的检查数组访问越界检查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

13、= u.u2;p = 0;5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统实际使用的一些语言并不安全C语言还有很多不安全的并且被广泛使用的特征，如：指针算术运算、类型强制、参数个数可变5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统实际使用的一些语言并不安全C语言还有很多不安全的并且被广泛使用的特征，如：指针算术运算、类型强制、参数个数可变在语言设计的历史上，安全性考虑不足是因为强调代码的执行效率5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统实际使用的一些语言并不安全C语言还有很多不安全的并且被广泛使用的特征，如：指针算术运算、类型强制、参数个数可变

14、在语言设计的历史上，安全性考虑不足是因为强调代码的执行效率在现代语言设计上，安全性的位置越来越重要5.1 类型在编程语言中的作用5.1.2 类型化语言和类型系统实际使用的一些语言并不安全C语言还有很多不安全的并且被广泛使用的特征，如：指针算术运算、类型强制、参数个数可变在语言设计的历史上，安全性考虑不足是因为强调代码的执行效率在现代语言设计上，安全性的位置越来越重要C的一些问题已经在C+中得以缓和更多一些问题在Java中已得到解决5.1 类型在编程语言中的作用5.1.3 类型化语言的优点从工程的观点看，类型化语言有下面一些优点 开发的实惠较早发现错误类型信息还具有文档作用5.1 类型在编程语言

15、中的作用5.1.3 类型化语言的优点从工程的观点看，类型化语言有下面一些优点 开发的实惠较早发现错误类型信息还具有文档作用 编译的实惠程序模块可以相互独立地编译5.1 类型在编程语言中的作用5.1.3 类型化语言的优点从工程的观点看，类型化语言有下面一些优点 开发的实惠较早发现错误类型信息还具有文档作用 编译的实惠程序模块可以相互独立地编译 运行的实惠可得到更有效的空间安排和访问方式5.2 描述类型系统的语言类型系统主要用来说明编程语言的定型规则,它独立于类型检查算法5.2 描述类型系统的语言类型系统主要用来说明编程语言的定型规则,它独立于类型检查算法定义一个类型系统，一种重要的设计目标是存在

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

17、设计目标是存在有效的类型检查算法类型系统的基本概念可用于各类语言，包括函数式语言、命令式语言和并行语言等本节讨论用形式方法来描述类型系统然后讨论实例语言时：先定义语法，再给出类型系统的形式描述，最后写出类型检查的翻译方案5.2 描述类型系统的语言类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统-自然数表达式（需要定义它的语法） a+b, 3- 良形公式（逻辑断言，需要定义它的语法） a+b=3, (d=3)(c10)- 推理规则 a b, b ca c5.2 描述类型系统的语言类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统-自然数表达式类型表达式 a+b, 3 i

18、nt int- 良形公式 a+b=3, (d=3)(c10)- 推理规则 a b, b ca c5.2 描述类型系统的语言类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统-自然数表达式类型表达式 a+b, 3 int int- 良形公式定型断言 a+b=3, (d=3)(c10)x:int | x+3 : int- 推理规则( x:int 叫做定型环境 ) a b, b ca c5.2 描述类型系统的语言类型系统的形式化类型系统是一种逻辑系统有关自然数的逻辑系统类型系统-自然数表达式类型表达式 a+b, 3 int int- 良形公式定型断言 a+b=3, (d=3)(c10

19、)x:int | x+3 : int- 推理规则定型规则 | M : int, | N : int | M + N : int a b, b ca 0)(Type Function) (T1, T2 void)定型断言中的类型表达式也可以用抽象语法 | T | pointer(T) | T, | N : integer | array(N, T) | T1, | T2 | T1 T25.3 简单类型检查器的说明定型规则表达式(Exp Truth)(Exp Num)(Exp Id) | | truth : boolean | | num : integer 1, id : T, 2 | 1, i

20、d : T, 2 | id : T5.3 简单类型检查器的说明定型规则表达式(Exp Mod)(Exp Index)(0 E2 N1)(Exp Deref) | E1: integer, | E2: integer | E1 mod E2: integer | E1: array(N,T), | E2: integer | E1E2 : T | E : pointer(T) | E : T5.3 简单类型检查器的说明定型规则表达式(Exp FunCall) | E1: T1 T2, | E2: T1 | E1 (E2) : T25.3 简单类型检查器的说明定型规则语句(State Assign

21、)( 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: void5.3 简单类型检查器的说明定型规则语句(State Seq) | S1: void, | S2: void | S1; S2 : void5.3 简单类型检查器的说明5.3.3 类型检查设计语法制导的类型检查器设计依据是上节的类型系统类型环

22、境的信息进入符号表对类型表达式采用抽象语法 具体：array N of T抽象：array (N, T) T pointer (T)考虑到报错的需要，增加了类型type_error5.3 简单类型检查器的说明5.3.3 类型检查声明语句D D; DD id : T addtype (id.entry, T.type)addtype：把类型信息填入符号表5.3 简单类型检查器的说明5.3.3 类型检查声明语句D D; DD id : T addtype (id.entry, T.type)T boolean T.type = booleanT integer T.type = integerT

23、T1 T.type = pointer(T1.type)5.3 简单类型检查器的说明5.3.3 类型检查声明语句D D; DD id : T addtype (id.entry, T.type)T boolean T.type = booleanT integer T.type = integerT 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; DD id : T addtype (id.entry, T.type)T

24、boolean T.type = booleanT integer T.type = integerT 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 truthE.type = boolean E numE.type = integerE idE.type = lookup(id.entry)5.3 简单类型检查器的说明类型检查表达式E truthE.type = boole

25、an E numE.type = integerE idE.type = lookup(id.entry)E E1 mod E2E.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.

26、 type = integer and E1. type = array(s, t) then t else type_error E E1 E.type = if E1.type = pointer(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 else type_error E

27、E1 (E2 ) E. type = if E2 . type = s and E1. type = s t then t else type_error 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.typ

28、e = type_error; S if E then S1 S. type = if E. type = booleanthen S1. type else type_error 5.3 简单类型检查器的说明类型检查语句S while E do S1S.type = if E.type = boolean then S1. type else type_error 5.3 简单类型检查器的说明类型检查语句S while E do S1S.type = if E.type = boolean then S1. type else type_error S S1; S2S. type = if

29、S1. type = void andS2. type = void then voidelse type_error 5.3 简单类型检查器的说明类型检查程序P D; S P. type = if S. type = void then voidelse type_error 5.3 简单类型检查器的说明5.3.4 类型转换E E1 op E2E.type =if E1.type = integer and E2.type = integerthen integerelse if E1.type = integer and E2.type = realthen realelse if E1.

30、type = real and E2.type = integerthen realelse if E1.type = real and E2.type = realthen realelse 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;beginlen :

31、= 0;while lptr nil do begin len := len + 1; lptr := lptr. nextend;length := lenend;5.4 多 态 函 数用ML语言很容易写出求表长度的程序而不必管表元的类型。fun length (lptr) =if null (lptr) then 0else length (tl (lptr) + 1;5.4 多 态 函 数用ML语言很容易写出求表长度的程序而不必管表元的类型。fun length (lptr) =if null (lptr) then 0else length (tl (lptr) + 1;length

32、( “sun”, “mon”, “tue” )length ( 10, 9, 8 )都等于35.4 多 态 函 数多态函数允许变元有不同的类型5.4 多 态 函 数多态函数允许变元有不同的类型体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）5.4 多 态 函 数多态函数允许变元有不同的类型体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）多态算符用于以不同类型的变元执行的代码段5.4 多 态 函 数多态函数允许变元有不同的类型体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）多态算符用于以不同类型的变元执行的代码段例如：数组索引5.4 多 态 函 数多态函数允许

33、变元有不同的类型体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）多态算符用于以不同类型的变元执行的代码段例如：数组索引、函数作用5.4 多 态 函 数多态函数允许变元有不同的类型体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）多态算符用于以不同类型的变元执行的代码段例如：数组索引、函数作用、通过指针间接访问5.4 多 态 函 数多态函数允许变元有不同的类型体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）多态算符用于以不同类型的变元执行的代码段例如：数组索引、函数作用、通过指针间接访问C语言手册中关于指针&的论述是：如果运算对象的类型是，那么结果类型是指向的指

34、针”5.4 多 态 函 数5.4.2 类型变量length的类型可以写成.list() integer 允许使用类型变量，还便于讨论未知类型在不要求标识符的声明先于使用的语言中，通过类型变量的使用去确定程序变量的类型5.4 多 态 函 数例：function deref (p); beginreturn pend;5.4 多 态 函 数例：function deref (p); - 对p的类型一无所知：beginreturn pend;5.4 多 态 函 数例：function deref (p); - 对p的类型一无所知：beginreturn p- = pointer( ) end;5.4

35、 多 态 函 数例：function deref (p); - 对p的类型一无所知：beginreturn 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 | id5.4 多 态 函 数5.4.3 一个含多态

36、函数的语言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 | id5.4 多 态 函 数5.4.3 一个含多态函数的语言P D; ED D; D | id : QQ type-variable. Q | TT T T | T T| unary-constructor ( T )一个程序：| basi

37、c-type deref : . pointer( ) ;| type-variable q : pointer (pointer (integer);| ( T ) deref (deref (q)E E (E ) | E, E | id5.4 多 态 函 数类型系统中增加的推理规则 环境规则 (Env Var)语法规则(Type Var)(Type Product) | , dom (), | 1, , 2 | 1, , 2 | | T1, | T2 | T1 T25.4 多 态 函 数类型系统中增加的推理规则 语法规则(Type Parenthesis)(Type Forall)(Typ

38、e Fresh) | T | (T ) , | T | .T | .T , , i | , i | i / T 5.4 多 态 函 数类型系统中增加的推理规则定型规则 (Exp Pair)(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 代换、实例和合一代换: 类型表达式中的类型变量用其所代表的类型表达式去替换5.4 多 态 函 数5.4.4 代换、实例和合一代换: 类型表达式中的类型变量用其所代表的

39、类型表达式去替换function subst (t : type_expression ) : type_expression;beginif t是基本类型 then return telse if t是类型变量then return S(t)else if t 是t1 t2 then return subst(t1) subst(t2)end5.4 多 态 函 数实例把subst函数用于t后所得的类型表达式是t的一个实例，用S (t)表示。例子（s t 表示s是t 的实例）pointer( integer ) pointer( )pointer( real ) pointer( )integ

40、er integer pointer( ) 5.4 多 态 函 数下面左边的类型表达式不是右边的实例integerreal 代换不能用于基本类型integer real 的代换不一致integer 的所有出现都应该代换5.4 多 态 函 数合一如果存在某个代换S使得S(t1) = S(t2)，那么这两个表达式t1和t2能够合一 最一般的合一代换S(t1) = S(t2)；对任何其它满足S(t1) = S(t2)的代换S，代换S(t1)是S(t1)的实例5.4 多 态 函 数5.4.5 多态函数的类型检查多态函数和普通函数在类型检查上的区别(1)同一多态函数的不同出现无须变元有相同类型apply

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

42、efo:pointer(o) oapply : iderefi : pointer(i) iq: pointer(pointer(integer)deref(deref (q )的带标记的语法树5.4 多 态 函 数检查多态函数的翻译方案EE1 (E2 )p = mkleaf (newtypevar);unify (E1. type, mknode ( , E2.type, p) ); E. type = pE E1, E2E. type = mknode ( , E1.type , E2.type)E idE. type = fresh (lookup(id.entry)5.4 多 态 函

43、数apply: oderefo:pointer(o) oapply : iderefi : pointer(i) iq: 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 5.4 多 态 函 数确定表长度的ML函数fun length (lptr

44、) =if null (lptr) then 0else 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 (lptr),if (null (lptr), 0, length (tl(lptr) +1)5.4 多 态 函 数行 定 型 断 言 代

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

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

47、 if : boolean i i i (Exp Id)和(Type Fresh) (17) if ( . ) : integer i = integer (Exp FunCall) (18) match : m m m (Exp Id)和(Type Fresh) (19) match ( ) : integer m=integer (Exp FunCall) 5.4 多 态 函 数fun length (lptr) =if null (lptr) then 0else length (tl (lptr) + 1; length函数的类型是. list() integer 5.5 类型表达式的

48、等价当允许对类型表达式命名后：类型表达式是否相同就有了不同的解释出现了结构等价和名字等价两个不同的概念type link = cell;var next: link;last: link;p : cell;q, r: cell;5.5 类型表达式的等价5.5.1 类型表达式的结构等价两个类型表达式完全相同（当无类型名时）type link = cell;var next: link;last: link;p : cell;q, r: cell;5.5 类型表达式的等价5.5.1 类型表达式的结构等价两个类型表达式完全相同（当无类型名时）类型表达式树一样type link = cell;var

49、next: link;last: link;p : cell;q, r: cell;5.5 类型表达式的等价5.5.1 类型表达式的结构等价两个类型表达式完全相同（当无类型名时）类型表达式树一样相同的类型构造符作用于相同的子表达式type link = cell;var next: link;last: link;p : cell;q, r: cell;5.5 类型表达式的等价5.5.1 类型表达式的结构等价两个类型表达式完全相同（当无类型名时）把类型名都用它们定义的类型表达式代换，所得两类型表达式完全相同(类型定义无环时)type link = cell;var next: link;las

50、t: link;p : cell;q, r: cell;5.5 类型表达式的等价类型表达式的结构等价测试sequiv(s, t) (无类型名时)if s 和 t 是相同的基本类型thenreturn trueelse if s = array(s1, s2) and t = array(t1, t2) thenreturn sequiv(s1, t1) and sequiv(s2, t2)else if s = s1 s2 and t = t1 t2 thenreturn sequiv(s1, t1) and sequiv(s2, t2)else if s = pointer (s1) and

51、 t = pointer(t1) thenreturn sequiv(s1, t1)else if s = s1 s2 and t = t1 t2 thenreturn squiv(s1, t1) and sequiv(s2, t2)else return false5.5 类型表达式的等价5.5.2 类型表达式的名字等价把每个类型名看成是一个可区别的类型type link = cell;var next: link;last: link;p : cell;q, r: cell;5.5 类型表达式的等价5.5.2 类型表达式的名字等价把每个类型名看成是一个可区别的类型两个类型表达式名字等价当且

52、仅当这两个类型表达式不做名字代换就结构等价 type link = cell;var next: link;last: link;p : cell;q, r: cell;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;5.5 类型表达式的等价注意:

53、类型名字的引入只是类型表达式的一个语法约定问题，它并不像引入类型构造符或类型变量那样能丰富我们所能表达的类型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

54、 类型表达式的等价5.5.4 类型表示中的环type link = cell ;cell = recordinfo : integer ; next : linkend;cell = record，:infopointernextintegercell5.5 类型表达式的等价5.5.4 类型表示中的环type link = cell ;cell = recordinfo : integer ; next : linkend;cell = record，:infopointernextinteger5.5 类型表达式的等价 C语言对除记录（结构）以外的所有类型使用结构等价，而记录类型用的是名字等

55、价，以避免类型图中的环。 cell = record，:infopointernextintegercell5.6 函数和算符的重载重载符号有多个含义，但在引用点的含义都是唯一的例如：加法算符+可用于不同类型，是不同的函数在Ada中，( ) 是重载的，A( I ) 有不同含义5.6 函数和算符的重载重载符号有多个含义，但在引用点的含义都是唯一的例如加法算符+可用于不同类型，是不同的函数在Ada中，( ) 是重载的，A( I ) 有不同含义重载的消除在重载符号的引用点，其含义能确定到唯一 5.6 函数和算符的重载5.6.1 子表达式的可能类型集合例 Ada语言声明：function “ ” (i

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

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

58、x;function “ ” (x, y : complex ) return complex;使得算符重载，可能的类型包括：integer integer integer2 (3 5) integer integer complex(3 5) z complex complex complex z是复型 5.6 函数和算符的重载以函数应用为例，考虑类型检查在每个表达式都有唯一的类型时，函数应用的类型检查是：EE1 (E2 ) E. type = if E2. type = s and E1. type = s t then t else type_ error 5.6 函数和算符的重载确定表

59、达式可能类型的集合产 生 式 语 义 规 则 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, cE: i3: iE: i5: i : i i i, i i c, c c c 5.6 函数和算符的重载5.6.2 缩小可能类型的集合产 生 式 语 义 规 则 E E E. types = E. typesE. unique = if E. types = t then t else type_errorE. 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. typest = E. uniqueS = s | s E2. type