文档介绍：第9章类型推断
类型推断是把无类型的或“部分类型化的”项变换成良类型项的一般问题
它通过推导未给出的类型信息来完成这个变换
类型推断兼有两方面的优点
编译时完成类型检查
不需要程序中过分的类型信息
第9章类型推断
本章的主要内容
类型推断的一般框架
基于从类型化语言到无类型语言的“擦除”函数
加了类型变量后的类型推断
包括主定型和合一问题
带多态声明的, , let的类型推断算法
引言
例
给出完整类型信息的PCF表达式
D=def let dbl: (nat nat) nat nat =
f : nat nat.x: nat. f (f x)
in dbl (x: nat. x + 2 ) 4
忽略类型信息的PCF表达式
D =def let dbl = f.x. f (f x) in dbl (x: x + 2 ) 4
在多态语言中,类型推断尤其有用,因为多态项涉及约束变量的类型、类型抽象和类型作用
引言
通过选择从一种类型语言L到某种其它语言L的擦除函数Erase来确定类型推断问题
L是一种相对应的“无类型”语言,或者是部分类型信息或类型运算未给出
例从到无类型项的擦除函数删掉约束的类型指示
Erase(c) = c Erase(x:. M) = x. Erase(M)
Erase(x) = x Erase(M N) = Erase(M) Erase(N)
无类型项具有形式
U ::= c | x | | UU
引言
例, 的擦除函数
保持类型抽象和约束项变量的类型说明,但是擦除了类型作用
Erase(c) = c Erase(x:. M) = x. Erase(M)
Erase(x) = x Erase(M N) = Erase(M) Erase(N)
Erase(t. M) = (M) Erase(M ) = Erase(M)
作为擦除结果的, 程序的语法由文法
M ::= c | x | x:.M | MN |
允许多态函数作用到非多态变元而没有中间的类型作用
引言
语言L和擦除函数Erase: L L的类型推断问题是:
对给定的表达式UL,找出L的类型化项
M:,使得Erase(M) = U
一般来说,可能有无数多的方式用来将类型信息插入项
可以给f. (f x)以形式为() 的任何类型
引言
例若擦除的结果是
(t.x:) (t.x:)
这两个函数表达式必须作用到某个类型变元
原来的项必定有下面的形式
((t.x:)1) ((t.x:)2)
1 和2只要满足1 22就可以了
原来的项应该是
((t.x:) t t) ((t.x:) t)
引言
类型推断的另一种观点是
定型是由一组推理规则给出
合式公式的语法和证明规则给出一个逻辑系统
类型推断算法正好是一个公理理论的判定过程
决定一个合式公式是否可证明
判定过程是回答是或不是,而类型推断算法必须构造类型化的项
引言
类型推断和类型检查
类型检查看成是用语法制导的方式,根据上下文有关的定型条件判定项是否为良类型的项的过程
x:.M :
把对带无类型的定型判定问题叫做类型推断
:
带类型变量的类型推断
语言t
考虑语言t的类型推断
语言t
类型由下面文法定义
::= b | t |
项由下面文法定义
M ::= c | x | x: .M | M M
t的定型公理和推理规则同的相同
限制:项常量的类型一定不含类型变量