第五部分类型检查教学课件

《第五部分类型检查教学课件》由会员分享，可在线阅读，更多相关《第五部分类型检查教学课件（167页珍藏版）》请在装配图网上搜索。

1、第五章第五章 类类 型型 检检 查查 本章内容本章内容 静态检查中最典型的部分静态检查中最典型的部分 类型检查：类型检查：类型系统、类型检查、多态函数、重载。类型系统、类型检查、多态函数、重载。忽略其它的静态检查：忽略其它的静态检查：控制流检查、唯一性控制流检查、唯一性检查检查 、关联名字检查。、关联名字检查。分析分析器器类型类型检查检查器器中间中间代码代码生成生成 器器语 法语 法树树语 法语 法树树中间中间表示表示记号记号流流5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.1 引言引言 变量的类型变量的类型变量在程序执行期间的取值范围变量在程序执行期间的取值范围5.1

2、类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.1 引言引言 变量的类型变量的类型变量在程序执行期间的取值范围变量在程序执行期间的取值范围 类型化语言类型化语言变量都被给定类型的语言变量都被给定类型的语言例如，类型例如，类型Boolean的变量的变量x在程序每次运行时的值在程序每次运行时的值只能是布尔值只能是布尔值，not(x)总总有意义。有意义。5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.1 引言引言 变量的类型变量的类型变量在程序执行期间的取值范围变量在程序执行期间的取值范围 类型化语言类型化语言变量都被给定类型的语言变量都被给定类型的语言 未类型化的语

3、言未类型化的语言不限制变量值范围的语言不限制变量值范围的语言5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.1 引言引言 变量的类型变量的类型变量在程序执行期间的取值范围变量在程序执行期间的取值范围 类型化语言类型化语言变量都被给定类型的语言变量都被给定类型的语言 未类型化的语言未类型化的语言不限制变量值范围的语言不限制变量值范围的语言一个运算可以作用到任意的运算对象，其结果可能一个运算可以作用到任意的运算对象，其结果可能是一个有意义的值、一个错误、一个异常或一个未是一个有意义的值、一个错误、一个异常或一个未做说明的结果。做说明的结果。5.1 类型在程序设计语言中的作用类型

4、在程序设计语言中的作用5.1.1 引言引言 变量的类型变量的类型变量在程序执行期间的取值范围变量在程序执行期间的取值范围 类型化语言类型化语言变量都被给定类型的语言变量都被给定类型的语言 未类型化的语言未类型化的语言不限制变量值范围的语言不限制变量值范围的语言 类型系统类型系统 由一组由一组定型规则定型规则（typing rule）构成，这组规则用构成，这组规则用来给各种语言构造指派类型来给各种语言构造指派类型5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型系统类型系统的根本目的是防止程序运行时出现执行错的根本目的是防止程序运行时出现执行错误误5.1 类型在程序设计语言中的作

5、用类型在程序设计语言中的作用 类型系统类型系统的根本目的是防止程序运行时出现执行错的根本目的是防止程序运行时出现执行错误误 类型可靠的类型可靠的语言语言粗略地说，所有程序运行时都没有执行错误出现粗略地说，所有程序运行时都没有执行错误出现5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型系统类型系统的根本目的是防止程序运行时出现执行错的根本目的是防止程序运行时出现执行错误误 类型可靠的类型可靠的语言语言粗略地说，所有程序运行时都没有执行错误出现粗略地说，所有程序运行时都没有执行错误出现 类型系统的形式化类型系统的形式化类型表达式、定型断言、定型规则、类型检查算法类型表达式、定型断

6、言、定型规则、类型检查算法5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型系统类型系统的根本目的是防止程序运行时出现执行错的根本目的是防止程序运行时出现执行错误误 类型可靠的类型可靠的语言语言粗略地说，所有程序运行时都没有执行错误出现粗略地说，所有程序运行时都没有执行错误出现 类型系统的形式化类型系统的形式化类型表达式、定型断言、定型规则、类型检查算法类型表达式、定型断言、定型规则、类型检查算法 显式类型化的显式类型化的语言语言类型是语法的一部分类型是语法的一部分5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型系统类型系统的根本目的是防止程序运行时出现执行错

7、的根本目的是防止程序运行时出现执行错误误 类型可靠的类型可靠的语言语言粗略地说，所有程序运行时都没有执行错误出现粗略地说，所有程序运行时都没有执行错误出现 类型系统的形式化类型系统的形式化类型表达式、定型断言、定型规则、类型检查算法类型表达式、定型断言、定型规则、类型检查算法 显式类型化的显式类型化的语言语言类型是语法的一部分类型是语法的一部分 隐式类型化的隐式类型化的语言语言5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.2 执行错误和安全语言执行错误和安全语言执行错误执行错误 会被捕获的错误会被捕获的错误（trapped error）5.1 类型在程序设计语言中的作用类

8、型在程序设计语言中的作用5.1.2 执行错误和安全语言执行错误和安全语言执行错误执行错误 会被捕获的错误会被捕获的错误（trapped error）例：例：非法指令错误非法指令错误5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.2 执行错误和安全语言执行错误和安全语言执行错误执行错误 会被捕获的错误会被捕获的错误（trapped error）例：例：非法指令错误、非法内存访问非法指令错误、非法内存访问5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.2 执行错误和安全语言执行错误和安全语言执行错误执行错误 会被捕获的错误会被捕获的错误（trapped er

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

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

11、设计语言中的作用类型在程序设计语言中的作用5.1.2 执行错误和安全语言执行错误和安全语言执行错误执行错误 会被捕获的错误会被捕获的错误（trapped error）例：例：非法指令错误、非法内存访问非法指令错误、非法内存访问、除数为零除数为零 引起计算立即停止引起计算立即停止 不会被捕获的错误不会被捕获的错误（untrapped error）例：下标变量的例：下标变量的访问越过数组末端的数据访问越过数组末端的数据 例：例：跳到一个错误的地址，该地址开始的内存正跳到一个错误的地址，该地址开始的内存正好代表一个指令序列好代表一个指令序列 5.1 类型在程序设计语言中的作用类型在程序设计语言中的作

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

13、型在程序设计语言中的作用 安全语言安全语言任何程序不任何程序不出现不会被捕获错误出现不会被捕获错误5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 安全语言安全语言任何程序不任何程序不出现不会被捕获错误出现不会被捕获错误 禁止错误禁止错误（forbidden error）不会被捕获错误不会被捕获错误集合集合+会被捕获错误的一个会被捕获错误的一个子集。子集。5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 安全语言安全语言任何程序不任何程序不出现不会被捕获错误出现不会被捕获错误 禁止错误禁止错误（forbidden error）不会被捕获错误不会被捕获错误集合集合+会被捕

14、获错误的一个会被捕获错误的一个子集。子集。类型化语言的目标是在排除类型化语言的目标是在排除禁止错误禁止错误5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 安全语言安全语言任何程序不任何程序不出现不会被捕获错误出现不会被捕获错误 禁止错误禁止错误（forbidden error）不会被捕获错误不会被捕获错误集合集合+会被捕获错误的一个会被捕获错误的一个子集。子集。类型化语言的目标是在排除类型化语言的目标是在排除禁止错误禁止错误 良行为的良行为的程序：不出现任何禁止错误程序：不出现任何禁止错误 有不良行为的程序：出现禁止错误有不良行为的程序：出现禁止错误5.1 类型在程序设计语言中的

15、作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言 所有合法的程序都是良行为的所有合法的程序都是良行为的5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言 所有合法的程序都是良行为的所有合法的程序都是良行为的 又称为又称为强检查的语言强检查的语言 5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言 所有合法的程序都是良行为的所有合法的程序都是良行为的 又称为又称为强检查的语言强检查的语言 未类型化语言未类型化语言通过彻底的运行时详细检查来排除通过彻底的运行时详细检查来排除所有的禁止错误，如所有的禁止错误，

16、如LISP语言语言5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言 所有合法的程序都是良行为的所有合法的程序都是良行为的 又称为又称为强检查的语言强检查的语言 未类型化语言未类型化语言通过彻底的运行时详细检查来排除通过彻底的运行时详细检查来排除所有的禁止错误，如所有的禁止错误，如LISPLISP语言语言 也也可以通过静态检查来拒绝不良行为的程序可以通过静态检查来拒绝不良行为的程序 5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言 所有合法的程序都是良行为的所有合法的程序都是良行为的 又称为又称为强检查的语言强检

17、查的语言 未类型化语言未类型化语言通过彻底的运行时详细检查来排除通过彻底的运行时详细检查来排除所有的禁止错误，如所有的禁止错误，如LISPLISP语言语言 也也可以通过静态检查来拒绝不良行为的程序可以通过静态检查来拒绝不良行为的程序 类型系统就是用来支持这种静态检查的类型系统就是用来支持这种静态检查的5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言 所有合法的程序都是良行为的所有合法的程序都是良行为的 又称为又称为强检查的语言强检查的语言 未类型化语言未类型化语言通过彻底的运行时详细检查来排除通过彻底的运行时详细检查来排除所有的禁止错误，如所有的禁止错

18、误，如LISPLISP语言语言 也也可以通过静态检查来拒绝不良行为的程序可以通过静态检查来拒绝不良行为的程序 类型系统就是用来支持这种静态检查的类型系统就是用来支持这种静态检查的 这种检查叫做类型检查这种检查叫做类型检查5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言 所有合法的程序都是良行为的所有合法的程序都是良行为的 又称为又称为强检查的语言强检查的语言 未类型化语言未类型化语言通过彻底的运行时详细检查来排除通过彻底的运行时详细检查来排除所有的禁止错误，如所有的禁止错误，如LISPLISP语言语言 也也可以通过静态检查来拒绝不良行为的程序可以通过静

19、态检查来拒绝不良行为的程序 类型系统就是用来支持这种静态检查的类型系统就是用来支持这种静态检查的 这种检查叫做类型检查这种检查叫做类型检查 这样的这样的类型化语言，又称类型化语言，又称强类型化的强类型化的语言语言5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言良类型的程序良类型的程序：能够通过类型检查的程序能够通过类型检查的程序 不会出现不会被捕获错误（即是安全的）不会出现不会被捕获错误（即是安全的）5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言良类型的程序良类型的程序：能够通过类型检查的程序能够通过类型检查

20、的程序 不会出现不会被捕获错误（即是安全的）不会出现不会被捕获错误（即是安全的）不会出现已列入禁止错误的会被捕获错误不会出现已列入禁止错误的会被捕获错误5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言良类型的程序良类型的程序：能够通过类型检查的程序能够通过类型检查的程序 不会出现不会被捕获错误（即是安全的）不会出现不会被捕获错误（即是安全的）不会出现已列入禁止错误的会被捕获错误不会出现已列入禁止错误的会被捕获错误 有可能出现其它的会被捕获错误，避免它们是程有可能出现其它的会被捕获错误，避免它们是程序员的责任序员的责任5.1 类型在程序设计语言中的作用类

21、型在程序设计语言中的作用 类型可靠的类型可靠的语言语言良类型的程序良类型的程序：能够通过类型检查的程序能够通过类型检查的程序 不会出现不会被捕获错误（即是安全的）不会出现不会被捕获错误（即是安全的）不会出现已列入禁止错误的会被捕获错误不会出现已列入禁止错误的会被捕获错误 有可能出现其它的会被捕获错误，避免它们是程有可能出现其它的会被捕获错误，避免它们是程序员的责任序员的责任 静态检查的语言有静态检查的语言有ML和和Pascal等等5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 类型可靠的类型可靠的语言语言良类型的程序良类型的程序：能够通过类型检查的程序能够通过类型检查的程序 不会

22、出现不会被捕获错误（即是安全的）不会出现不会被捕获错误（即是安全的）不会出现已列入禁止错误的会被捕获错误不会出现已列入禁止错误的会被捕获错误 有可能出现其它的会被捕获错误，避免它们是程有可能出现其它的会被捕获错误，避免它们是程序员的责任序员的责任 静态检查的语言有静态检查的语言有ML和和Pascal等等 静态检查语言通常也需要一些运行时的测试静态检查语言通常也需要一些运行时的测试5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用一些实际使用的语言是弱类型化语言一些实际使用的语言是弱类型化语言 Pascal语言语言 无标志的变体记录类型无标志的变体记录类型 函数型参数函数型参数5.1

23、类型在程序设计语言中的作用类型在程序设计语言中的作用联合体（联合体（union）的类型检查一般不可能的类型检查一般不可能在运行前完成，虽然下面这个例子是可静态在运行前完成，虽然下面这个例子是可静态判断类型错误的。判断类型错误的。union U int u1;int u2;u;int p;u.u1=10;p=u.u2;p=0;5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用一些实际使用的语言是弱类型化语言一些实际使用的语言是弱类型化语言 Pascal语言语言 无标志的变体记录类型无标志的变体记录类型 函数型参数函数型参数5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用一些

24、实际使用的语言是弱类型化语言一些实际使用的语言是弱类型化语言 Pascal语言语言 无标志的变体记录类型无标志的变体记录类型 函数型参数函数型参数 C语言语言有很多不安全的并且被广泛使用的特征，如：有很多不安全的并且被广泛使用的特征，如：指针算术运算指针算术运算 类型强制类型强制 参数个数可变参数个数可变5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 在语言设计的历史上，安全性考虑不足是出在语言设计的历史上，安全性考虑不足是出于效率上的原因于效率上的原因5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用 在语言设计的历史上，安全性考虑不足是出在语言设计的历史上，安全性考

25、虑不足是出于效率上的原因于效率上的原因 在语言设计中的，安全性的位置越来越重要在语言设计中的，安全性的位置越来越重要 C的一些问题已经在的一些问题已经在C+中得以缓和中得以缓和 更多一些问题在更多一些问题在Java中已得到解决中已得到解决 ML是一个类型化的安全语言是一个类型化的安全语言5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.3 类型化语言的优点类型化语言的优点从工程的观点看，类型化语言有下面一些优点从工程的观点看，类型化语言有下面一些优点 开发的实惠开发的实惠较早发现错误较早发现错误类型信息还具有文档作用类型信息还具有文档作用5.1 类型在程序设计语言中的作用类型

26、在程序设计语言中的作用5.1.3 类型化语言的优点类型化语言的优点从工程的观点看，类型化语言有下面一些优点从工程的观点看，类型化语言有下面一些优点 开发的实惠开发的实惠较早发现错误较早发现错误类型信息还具有文档作用类型信息还具有文档作用 编译的实惠编译的实惠程序模块可以相互独立地编译程序模块可以相互独立地编译5.1 类型在程序设计语言中的作用类型在程序设计语言中的作用5.1.3 类型化语言的优点类型化语言的优点从工程的观点看，类型化语言有下面一些优点从工程的观点看，类型化语言有下面一些优点 开发的实惠开发的实惠较早发现错误较早发现错误类型信息还具有文档作用类型信息还具有文档作用 编译的实惠编译

27、的实惠程序模块可以相互独立地编译程序模块可以相互独立地编译 运行的实惠运行的实惠可得到更有效的空间安排和访问方式可得到更有效的空间安排和访问方式5.2 描述类型系统的语言描述类型系统的语言 类型系统主要用来说明程序设计语言的定型类型系统主要用来说明程序设计语言的定型规则，它独立于类型检查算法。规则，它独立于类型检查算法。5.2 描述类型系统的语言描述类型系统的语言 类型系统主要用来说明程序设计语言的定型类型系统主要用来说明程序设计语言的定型规则，它独立于类型检查算法。规则，它独立于类型检查算法。定义一个类型系统，通常的设计目标是允许定义一个类型系统，通常的设计目标是允许有效的类型检查算法。有效

28、的类型检查算法。5.2 描述类型系统的语言描述类型系统的语言 类型系统主要用来说明程序设计语言的定型类型系统主要用来说明程序设计语言的定型规则，它独立于类型检查算法。规则，它独立于类型检查算法。定义一个类型系统，通常的设计目标是允许定义一个类型系统，通常的设计目标是允许有效的类型检查算法。有效的类型检查算法。类型系统的基本概念可用于各类语言类型系统的基本概念可用于各类语言，包括包括函数式语言、命令式语言和并行语言等。函数式语言、命令式语言和并行语言等。5.2 描述类型系统的语言描述类型系统的语言 类型系统主要用来说明程序设计语言的定型类型系统主要用来说明程序设计语言的定型规则，它独立于类型检查

29、算法。规则，它独立于类型检查算法。定义一个类型系统，通常的设计目标是允许定义一个类型系统，通常的设计目标是允许有效的类型检查算法。有效的类型检查算法。类型系统的基本概念可用于各类语言类型系统的基本概念可用于各类语言，包括包括函数式语言、命令式语言和并行语言等。函数式语言、命令式语言和并行语言等。本节讨论用形式化的方法来描述类型系统本节讨论用形式化的方法来描述类型系统 5.2 描述类型系统的语言描述类型系统的语言5.2.1 定型断言定型断言断言的形式断言的形式|SS的所有自由变量都声明在的所有自由变量都声明在 中中其中其中 是一个是一个静态定型环境静态定型环境，如，如x1:T1,xn:Tn S的

30、形式随断言形式的不同而不同的形式随断言形式的不同而不同 断言有三种具体形式断言有三种具体形式5.2 描述类型系统的语言描述类型系统的语言 环境断言：用于定义环境环境断言：用于定义环境|是合式的环境是合式的环境5.2 描述类型系统的语言描述类型系统的语言 环境断言：用于定义环境环境断言：用于定义环境|是合式的环境是合式的环境 语法断言：用于规定类型表达式的语法语法断言：用于规定类型表达式的语法|Nat在环境在环境 下，下，Nat是一个类型表达式是一个类型表达式5.2 描述类型系统的语言描述类型系统的语言 环境断言：用于定义环境环境断言：用于定义环境|是合式的环境是合式的环境 语法断言：用于规定类

31、型表达式的语法语法断言：用于规定类型表达式的语法|Nat在环境在环境 下，下，Nat是一个类型表达式是一个类型表达式 定型断言定型断言|M:TM在在 中具有类型中具有类型T 例：例：|true:Boolx:Nat|x+1:Nat5.2 描述类型系统的语言描述类型系统的语言 有效断言有效断言|true:Bool 无效断言无效断言|true:Nat5.2 描述类型系统的语言描述类型系统的语言5.2.2 定型规则定型规则 1|S1,.,n|Sn|S 前提前提、结论结论、公理公理5.2 描述类型系统的语言描述类型系统的语言5.2.2 定型规则定型规则 1|S1,.,n|Sn|S 前提前提、结论结论、公

32、理公理（规则名）（注释）（规则名）（注释）定型规则定型规则（注释）注释）5.2 描述类型系统的语言描述类型系统的语言5.2.2 定型规则定型规则 1|S1,.,n|Sn|S 前提前提、结论结论、公理公理（规则名）（注释）（规则名）（注释）定型规则定型规则（注释）注释）环境规则：环境规则：(Env )|5.2 描述类型系统的语言描述类型系统的语言5.2.2 定型规则定型规则 1|S1,.,n|Sn|S 前提前提、结论结论、公理公理（规则名）（注释）（规则名）（注释）定型规则定型规则（注释）注释）环境规则：环境规则：(Env )|语法规则：语法规则：(Type Bool)|Bool5.2 描述类型

33、系统的语言描述类型系统的语言5.2.2 定型规则定型规则 1|S1,.,n|Sn|S 前提前提、结论结论、公理公理（规则名）（注释）（规则名）（注释）定型规则定型规则（注释）注释）环境规则：环境规则：(Env )|语法规则：语法规则：(Type Bool)|Bool 定型规则定型规则(Val+)|M:Nat,|N:Nat|M+N:Nat5.2 描述类型系统的语言描述类型系统的语言5.2.3 类型检查和类型推断类型检查和类型推断 类型检查类型检查用语法制导的方式，根据上下文有关的定型用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构规则来判定程序构造是否为良类型的程序构

34、造的过程造的过程。5.2 描述类型系统的语言描述类型系统的语言5.2.3 类型检查和类型推断类型检查和类型推断 类型检查类型检查用语法制导的方式，根据上下文有关的定型用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构规则来判定程序构造是否为良类型的程序构造的过程造的过程。类型推断类型推断类型信息不完全的情况下的定型判定问题类型信息不完全的情况下的定型判定问题例如：例如：f(x:t)=E 和和 f(x)=E5.3 简单类型检查器的说明简单类型检查器的说明5.3.1 一个简单的语言一个简单的语言P D;SD D;D|id:TT boolean|integer|array

35、num of T|T|T TS id:=E|if E then S|while E do S|S;SE truth|num|id|E mod E|E E|E|E(E)5.3 简单类型检查器的说明简单类型检查器的说明例：例：i:integer;j:integer;j:=i mod 20005.3 简单类型检查器的说明简单类型检查器的说明5.3.2 类型系统类型系统环境规则环境规则(Env )|(Decl Var)|T,id dom(),id:T|5.3 简单类型检查器的说明简单类型检查器的说明语法规则语法规则(Type Bool)|boolean(Type Int)|integer(Type V

36、oid)|void5.3 简单类型检查器的说明简单类型检查器的说明语法规则语法规则(Type Bool)|boolean(Type Int)|integer(Type Void)|void(Type Ref)|T|T5.3 简单类型检查器的说明简单类型检查器的说明语法规则语法规则(Type Bool)|boolean(Type Int)|integer(Type Void)|void(Type Ref)|T|T(Type Array)|T,|N:integer|array N of T5.3 简单类型检查器的说明简单类型检查器的说明语法规则语法规则(Type Bool)|boolean(Typ

37、e Int)|integer(Type Void)|void(Type Ref)|T|T(Type Array)|T,|N:integer|array N of T(Type Function)|T1,|T2|T1 T25.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则表达式表达式(Exp Truth)|truth:boolean(Exp Num)|num:integer5.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则表达式表达式(Exp Truth)|truth:boolean(Exp Num)|num:integer(Exp Id)1,id:T,2|1,id:

38、T,2|id:T5.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则表达式表达式(Exp Truth)|truth:boolean(Exp Num)|num:integer(Exp Id)1,id:T,2|1,id:T,2|id:T(Exp Mod)|E1:integer,|E2:integer|E1 mod E2:integer5.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则表达式表达式(Exp Index)|E1:arrayN of T,|E2:integer|E1E2 :T5.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则表达式表达式(Exp I

39、ndex)|E1:arrayN of T,|E2:integer|E1E2 :T(Exp Deref)|E:T|E :T5.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则表达式表达式(Exp Index)|E1:arrayN of T,|E2:integer|E1E2 :T(Exp Deref)|E:T|E :T(Exp FunCall)|E1:T1 T2,|E2:T1|E1(E2):T25.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则语句语句(State Assign)|id:T,|E:T|id:=E:void5.3 简单类型检查器的说明简单类型检查器的说明定型

40、规则定型规则语句语句(State Assign)|id:T,|E:T|id:=E:void(State If)|E:boolean,|S:void|if E then S:void5.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则语句语句(State Assign)|id:T,|E:T|id:=E:void(State If)|E:boolean,|S:void|if E then S:void(State While)|E:boolean,|S:void|while E do S:void5.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则语句语句(State As

41、sign)|id:T,|E:T|id:=E:void(State If)|E:boolean,|S:void|if E then S:void(State While)|E:boolean,|S:void|while E do S:void(State Seq)|S1:void,|S2:void|S1;S2:void5.3 简单类型检查器的说明简单类型检查器的说明定型规则定型规则程序程序(Prog)|S:void|D;S:void 5.3 简单类型检查器的说明简单类型检查器的说明5.3.3 类型检查类型检查声明语句声明语句D D;DD id:T addtype(id.entry,T.type)

42、T boolean T.type:=booleanT integer T.type:=integerT 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 简单类型检查器的

43、说明简单类型检查器的说明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)T T1 T2 T.type:=T1.type T2.type 5.3 简单类型检查器的说明简单类型检查器的说明类型检查类型检查表达式表达式E truthE.type:=boolean E numE.typ

44、e:=integerE idE.type:=lookup(id.entry)5.3 简单类型检查器的说明简单类型检查器的说明类型检查类型检查表达式表达式E truthE.type:=boolean 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=i

45、nteger 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 else type_error 5.3 简单类型检查器的说明简单类型检查器的说明类型检查类型检查表达式表达式E E1 E2 E.type:=if E2.type=integer

46、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 E1(E2)E.type:=if E2.type=s and E1.type=s t then t else type_error 5.3 简单类型检查器的说明简单类型检查器的说明类型检查类型检查语句语句S id:=E S.type:=if id.type=E.typethen void else type_error 5.3 简单类型检查器的说明简单类型检查器的说明类型检查类型检查语句语

47、句S id:=E S.type:=if id.type=E.typethen void else 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.t

48、ype=boolean then S1.type else type_error S S1;S2S.type:=if 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=integerthe

49、n integerelse if E1.type=integer and E2.type=realthen realelse if E1.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

50、end;5.4 多多 态态 函函 数数function length(lptr:link):integer;var len:integer;beginlen:=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语言很容易

51、写出求表长度的程序而不必语言很容易写出求表长度的程序而不必管表元的类型管表元的类型。fun length(lptr)=if null(lptr)then 0else length(tl(lptr)+1;length(“sun”,“mon”,“tue”)length(10,9,8 )都等于都等于35.4 多多 态态 函函 数数 多态函数多态函数 允许变元有不同的类型允许变元有不同的类型5.4 多多 态态 函函 数数 多态函数多态函数 允许变元有不同的类型允许变元有不同的类型 体中的语句可以在变元类型不同的情况下执行（体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）区别于重载的特征）5

52、.4 多多 态态 函函 数数 多态函数多态函数 允许变元有不同的类型允许变元有不同的类型 体中的语句可以在变元类型不同的情况下执行（体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）区别于重载的特征）多态算符多态算符 以不同类型的变元执行的代码段以不同类型的变元执行的代码段5.4 多多 态态 函函 数数 多态函数多态函数 允许变元有不同的类型允许变元有不同的类型 体中的语句可以在变元类型不同的情况下执行（体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）区别于重载的特征）多态算符多态算符 以不同类型的变元执行的代码段以不同类型的变元执行的代码段 例如：例如：数组索引数组索引

53、5.4 多多 态态 函函 数数 多态函数多态函数 允许变元有不同的类型允许变元有不同的类型 体中的语句可以在变元类型不同的情况下执行（体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）区别于重载的特征）多态算符多态算符 以不同类型的变元执行的代码段以不同类型的变元执行的代码段 例如：例如：数组索引数组索引、函数作用函数作用5.4 多多 态态 函函 数数 多态函数多态函数 允许变元有不同的类型允许变元有不同的类型 体中的语句可以在变元类型不同的情况下执行（体中的语句可以在变元类型不同的情况下执行（区别于重载的特征）区别于重载的特征）多态算符多态算符 以不同类型的变元执行的代码段以不同类

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

55、么结果类型是指向向的指针的指针”。5.4 多多 态态 函函 数数5.4.2 类型变量类型变量length的类型可以写成的类型可以写成 .list()integer 允许类型变量出现在类型表达式中，还便于我允许类型变量出现在类型表达式中，还便于我们讨论未知类型们讨论未知类型在不要求标识符的声明先于使用的语言中在不要求标识符的声明先于使用的语言中，通，通过类型变量的使用去确定程序变量的类型。过类型变量的使用去确定程序变量的类型。5.4 多多 态态 函函 数数例：例：type link=cell;procedure mlist(lptr:link;procedure p);begin while l

56、ptr nil do beginp(lptr);lptr:=lptr.nextendend;5.4 多多 态态 函函 数数例：例：type link=cell;procedure mlist(lptr:link;procedure p);begin while lptr nil do beginp(lptr);lptr:=lptr.nextendend;p的类型是的类型是link void 5.4 多多 态态 函函 数数例：例：function deref(p);beginreturn p end;5.4 多多 态态 函函 数数例：例：function deref(p);-对对p的类型一无所知

57、：的类型一无所知：beginreturn p end;5.4 多多 态态 函函 数数例：例：function deref(p);-对对p的类型一无所知：的类型一无所知：beginreturn p-=pointer()end;5.4 多多 态态 函函 数数例：例：function deref(p);-对对p的类型一无所知：的类型一无所知：beginreturn p-=pointer()end;deref的类型是的类型是 .pointer()5.4 多多 态态 函函 数数5.4.3 一个含多态函数的语言一个含多态函数的语言P D;E -引入类型变量、引入类型变量、D D;D|id:Q -笛卡儿积类

58、型、笛卡儿积类型、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)|basic-type deref:.pointer();|type-variable q:pointer(pointer(integer);|(T)deref(der

59、ef(q)E E(E)|E,E|id5.4 多多 态态 函函 数数增加的推理规则增加的推理规则 环境规则环境规则(Env Var)|,dom(),|语法规则语法规则(Type Var)1,2|1,2|(Type Product)|T1,|T2|T1 T2(Type Parenthesis)|T|(T)(Type Forall),|T|.T(Type Fresh)|.T,i|,i|i/T5.4 多多 态态 函函 数数增加的推理规则增加的推理规则 定型规则定型规则 (Exp Pair)|E1:T1，|E2:T2|E1,E2:T1 T2(Exp FunCall)|E1:T1 T2,|E2:T3|E1

60、(E2):S(T2)(S是是T1和和T3的最一般的合一代换的最一般的合一代换)5.4 多多 态态 函函 数数5.4.4 代换、实例和合一代换、实例和合一代换代换:类型表达式中的类型变量用其所代表的类型表达式中的类型变量用其所代表的类型表达式去替换类型表达式去替换5.4 多多 态态 函函 数数5.4.4 代换、实例和合一代换、实例和合一代换代换:类型表达式中的类型变量用其所代表的类型表达式中的类型变量用其所代表的类型表达式去替换类型表达式去替换function subst(t:type_expression):type_expression;beginif t是基本类型是基本类型 then re

61、turn 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()integer integer pointer()5.4 多多 态态 函函 数数下面左边的类型表达式不是右边的

62、实例下面左边的类型表达式不是右边的实例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 多态函数的类型检

63、查多态函数的类型检查多态函数和普通函数在类型检查上的区别多态函数和普通函数在类型检查上的区别(1)(1)同一多态函数的不同出现无须变元有相同类型同一多态函数的不同出现无须变元有相同类型apply:oderefo:pointer(o)oapply:iderefi:pointer(i)iq:pointer(pointer(integer)deref(deref(q)的带标记的语法树的带标记的语法树5.4 多多 态态 函函 数数(2)(2)必须把类型相同的概念推广到类型合一必须把类型相同的概念推广到类型合一apply:oderefo:pointer(o)oapply:iderefi:pointer(

64、i)iq:pointer(pointer(integer)deref(deref(q)的带标记的语法树的带标记的语法树5.4 多多 态态 函函 数数(2)(2)必须把类型相同的概念推广到类型合一必须把类型相同的概念推广到类型合一(3)(3)要记录表达式合一的结果要记录表达式合一的结果apply:oderefo:pointer(o)oapply:iderefi:pointer(i)iq:pointer(pointer(integer)deref(deref(q)的带标记的语法树的带标记的语法树5.4 多多 态态 函函 数数检查多态函数的翻译方案检查多态函数的翻译方案EE1(E2)p:=mklea

65、f(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 多多 态态 函函 数数apply:oderefo:pointer(o)oapply:iderefi:pointer(i)iq:pointer(pointer(integer)表表 达达 式式 ：类类 型型 代代 换换 q:pointer(pointer(integer)derefi:pointer(i)i derefi(q):poi

66、nter(integer)i=pointer(integer)derefo:pointer(o)o derefo(derefi(q):integer o=integer 5.4 多多 态态 函函 数数确定表长度的确定表长度的ML函数函数fun length(lptr)=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(t1(lptr)+1)5.4 多多 态态 函函 数数行行 定定 型型 断断 言言 代代 换换 规规 则则(1)lptr:(Exp Id)(2)length:(Exp Id)(3)length(lptr):=(Exp FunCall)(4)lptr:从从(1)可得可得(5)null:list(n)