第9章 类型推断 类型推断是把无类型的或“部分类型化的”项变换成良类型项的一般问题 它通过推导未给出的类型信息来完成这个变换 第9章 类型推断 类型推断是把无类型的或“部分类型化的”项变换成良类型项的一般问题 它通过推导未给出的类型信息来完成这个变换 类型推断兼有两方面的优点 编译时完成类型检查 不需要程序中过分的类型信息

第9章 类型推断 本章的主要内容 类型推断的一般框架 加了类型变量后的类型推断 带多态声明的, , let的类型推断算法 第9章 类型推断 本章的主要内容 类型推断的一般框架 基于从类型化语言到无类型语言的“擦除”函数 加了类型变量后的类型推断 包括主定型和合一问题 带多态声明的, , let的类型推断算法

9.1 引 言 例 在多态语言中，类型推断尤其有用，因为多态项涉及约束变量的类型、类型抽象和类型作用 给出完整类型信息的PCF表达式 9.1 引 言 例 给出完整类型信息的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 在多态语言中，类型推断尤其有用，因为多态项涉及约束变量的类型、类型抽象和类型作用

9.1 引 言 通过选择从一种类型语言L到某种其它语言L的擦除函数Erase来确定类型推断问题 9.1 引 言 通过选择从一种类型语言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 | x.U | UU

9.1 引 言 例 , 的擦除函数 保持类型抽象和约束项变量的类型说明，但是擦除了类型作用 9.1 引 言 例 , 的擦除函数 保持类型抽象和约束项变量的类型说明，但是擦除了类型作用 Erase(c) = c Erase(x:. M) = x. Erase(M) Erase(x) = x Erase(M N) = Erase(M) Erase(N) Erase(t. M) = t.Erase(M) Erase(M ) = Erase(M) 作为擦除结果的, 程序的语法由文法 M ::= c | x | x:.M | MN | t.M 允许多态函数作用到非多态变元而没有中间的类型作用

9.1 引 言 语言L和擦除函数Erase: L  L的类型推断问题是： 对给定的表达式UL，找出L的类型化项 9.1 引 言 语言L和擦除函数Erase: L  L的类型推断问题是： 对给定的表达式UL，找出L的类型化项  M:，使得Erase(M) = U 一般来说，可能有无数多的方式用来将类型信息插入项 可以给f.x.f (f x)以形式为( )   的任何类型

9.1 引 言 例 若擦除的结果是 (t.x:t.x) (t.x:t.x) 这两个函数表达式必须作用到某个类型变元 9.1 引 言 例 若擦除的结果是 (t.x:t.x) (t.x:t.x) 这两个函数表达式必须作用到某个类型变元 原来的项必定有下面的形式 ((t.x:t.x)1) ((t.x:t.x)2) 1 和2只要满足1 22就可以了 原来的项应该是 ((t.x:t.x) t  t) ((t.x:t.x) t)

9.1 引 言 类型推断的另一种观点是 定型是由一组推理规则给出 合式公式的语法和证明规则给出一个逻辑系统 9.1 引 言 类型推断的另一种观点是 定型是由一组推理规则给出 合式公式的语法和证明规则给出一个逻辑系统 类型推断算法正好是一个公理理论的判定过程 决定一个合式公式是否可证明 判定过程是回答是或不是，而类型推断算法必须构造类型化的项

9.1 引 言 类型推断和类型检查 类型检查看成是用语法制导的方式，根据上下文有关的定型条件判定项是否为良类型的项的过程 9.1 引 言 类型推断和类型检查 类型检查看成是用语法制导的方式，根据上下文有关的定型条件判定项是否为良类型的项的过程  x:.M :  把对带无类型的定型判定问题叫做类型推断  x.M : 

9.2 带类型变量的类型推断 9.2.1 语言t 考虑语言t的类型推断 语言t t的定型公理和推理规则同的相同 类型由下面文法定义  ::= b | t |    项由下面文法定义 M ::= c | x | x: .M | M M t的定型公理和推理规则同的相同 限制：项常量的类型一定不含类型变量

9.2 带类型变量的类型推断 命题 令 M是任意的良类型t项。如果由类型化项上的和归约有M N，那么由无类型项上的同样归约有Erase(M)  Erase(N)。反过来，如果由无类型的归约有Erase(M)  V，那么存在一个类型化项  N，使得M N且Erase(N)  V。 M  M1  . . .  Mk Erase(M)  Erase(M1)  . . .  Erase(Mk)

9.2 带类型变量的类型推断 事实 一个无类型项U，只有不存在从它开始的无类型归约的无穷序列时，它才可能被类型化 例 (x.xx) (x.xx) 推论1 如果U不是强范式的，那么就不存在可推导的定型 M:，使得Erase(M) = U 推论2 如果U是不可类型化的，那么由t的主语归约性质，知道没有一个能归约到U的项是可类型化的 M  M1  . . .  Mk Erase(M)  Erase(M1)  . . .  Erase(Mk)

9.2 带类型变量的类型推断 9.2.2 代换、实例与合一 事实 在t的类型推断中，可推导的定型断言封闭于代换 类型代换 类型代换S作用到类型表达式 S是把中的每个变量t用S (t)代替 类型代换S作用到类型指派 S  = {x: S | x:   } 类型代换S作用到t项 结果S M同M的区别仅在约束变元的类型

9.2 带类型变量的类型推断 实例 引理 如果定型断言 M:是可推导的，那么它的每个实例S   SM:S也是可推导的 定型断言 M:是 M:的实例，如果存在类型代 换S使得   S , M = S M并且 = S 引理 如果定型断言 M:是可推导的，那么它的每个实例S   SM:S也是可推导的

9.2 带类型变量的类型推断 合一算法 合一 例 如果E是类型表达式之间的一个等式集合，如果对每 个等式 =  E都有S  S，那么类型代换S合一E 例 E = {s = t  v, t = v  w} S = {t, v  w, s, (v  w)  v} 代换结果{(v  w)  v = (v  w)  v, v  w = v  w} S合一E

9.2 带类型变量的类型推断 最一般的合一代换 如果存在某个代换T使得R = TS，那么S比R更一般 最一般代换是使E的每个等式经代换后左右两边语法上一样的最简单的方式

9.2 带类型变量的类型推断 例 E = {s = t  v, t = v  w} 最一般的合一代换S = {t, v  w, s, (v  w)  v} 代换结果{(v  w)  v = (v  w)  v, v  w = v  w} 另一个合一代换S = {t, (w  w)  w, s, ((w  w)  w)  (w  w), v, w  w} 代换结果 {((w  w)  w)(w  w)=(w  w)  w(w  w), (w  w)  w = (w  w)  w}

9.2 带类型变量的类型推断 引理 令E是类型表达式之间的任意等式集合。存在一个算法Unify，使得如果E是可合一的，那么Unify(E)计算得出一个最一般的合一代换.如果E不可合一，那么Unify(E)失败 如果和都是类型指派，那么合一可以用来找出最一般的代换S，使得S  S 是合式的 直接合一所有等式 = 的集合就可以了，其中x:  并且x:  

9.2 带类型变量的类型推断 递归算法Unify 1. Unify() =  2. Unify(E  {b1 = b2}) = if b1  b2 then fail else Unify(E) 3. Unify(E  {t = }) = if (t  ) then Unify(E) else if t occurs in  then fail else Unify([/t]E) [/t] 4. Unify(E {1 2 = 1 2}) = Unify(E {1 = 1 2 = 2})

9.2 带类型变量的类型推断 9.2.3 主定型算法 显式定型 主显式定型（简称主定型） 如果U是一个无类型项，能够使得Erase(M) = U的合式的类型化项 M:是U的一个显式定型 主显式定型（简称主定型） 如果U的每个显式定型都是 M:的一个实例，那么  M:是U的主定型

9.2 带类型变量的类型推断 t主定型算法PT 1. PT(c) =  c:, 其中是c的类型, 它不含类型变量 2. PT(x) = {x : t} x : t 3. PT(x.U) = let  M: = PT(U) in if x:   （对某个） then - { x:  x:. M:  else  x:s. M:s  其中s是新的类型变量

9.2 带类型变量的类型推断 t主定型算法PT PT(UV) = let  M: = PT(U)  N: = PT(V) 其中类型变量重新命名以 区别于PT(U)中的变量 S = Unify({ =  | x:  并且 x:  }  { =  t})，其中t是新类型变量 in S   S  S (MN) : St

9.2 带类型变量的类型推断 例 计算x.y.xy的主定型 PT(xy) = let x:r x:r = PT(x) y:s y:s = PT(y) S = Unify({r = s  t}) in {x : Sr}  {y : Ss} xy:St PT(xy) = {x: s  t, y:s} xy: t PT(x.y.xy) =  x: s  t.y:s.xy: (s t ) s  t

9.2 带类型变量的类型推断 例 算法PT为什么对x.xx会失败 PT(xx) = let x:r x:r = PT(x) x:s x:s = PT(x) S = Unify({r = s}  { r = s  t}) in {x : Sr}  {x : Ss} xx:St

9.2 带类型变量的类型推断 定理 如果PT (U) =  M:，那么Erase (M) = U，并且 M:的每个实例是可证明的 定理 如果 M:是可证明的定型断言，并且Erase (M) = U，那么PT (U)一定成功，并产生一个定型断言，使得 M:是它的一个实例

9.2 带类型变量的类型推断 9.2.4 隐式定型 历史上，许多类型推断问题都被公式化为对无类型项使用证明规则进行证明的问题 这些证明系统通常称为隐式定型系统，因为一个项的类型不是由项的语法显式地给定的 此时，类型推断本质上是一个公理理论的判定问题

9.2 带类型变量的类型推断 隐式定型证明系统  c: c是类型的常量，中无类型变量 (cst) x: x: (var) (abs) (app) (add var) , x :  U :   (x.U) :    U :    V:   UV :   U :  , x :  U :  x不在中

9.2 带类型变量的类型推断 引理 如果 M:是良类型的项，那么 |--C  Erase(M) . 反过来, 如果|--C  U ， 那么存在类型化的项 M:，使得Erase(M)=U

9.2 带类型变量的类型推断 9.2.5 定型和合一的等价 类型推断和合一是算法地等价的 每个类型推断问题产生一个合一问题 每个合一问题出现在某个项的类型推断中

9.2 带类型变量的类型推断 另一个类型推断算法 本质上是从定型到合一的归约 TE(c, t) = {t = }, 其中是c的类型，中无自由变量 TE(x, t) = {t = tx}， 其中tx 是x的类型 TE(U V, t) = TE(U, r) TE(V, s) {r = s t} 其中r，s都是新的类型变量 TE(x.U, t) = TE(U, s) {t = tx s} 其中s是新的类型变量 如果U是无类型项，t是类型变量，并且E = TE(U, t)，那么U的每个定型是S U U: St的一个实例（对某个使E能够合一的最一般合一代换 S）

习 题 第一次：9.2