第9章类型推断

第9章类型推断内容摘要：

用到类型表达式  S是把 中的每个变量 t用 S (t)代替 – 类型代换 S作用到类型指派  S  = {x: S | x:   } – 类型代换 S作用到 t项 结果 S M同 M的区别仅在 约束变元的类型 带类型变量的 类型推断 • 实例 定型断言  M:是  M:的 实例 ， 如果存在类型代 换 S使得   S , M = S M并且  = S • 引理 如果定型断言  M:是可推导的 ， 那么它的每个实例 S   SM:S也是可推导的 带类型变量的 类型推断 合一算法 • 合一 如果 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 带类型变量的 类型推断 • 最一般的合一代换 – 如果存在某个代换 T使得 R = TS， 那么 S比 R更一般 – 如果不存在比 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 = {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} 带类型变量的 类型推断 • 引理 令 E是类型表达式之间的任意等式集合。 存在一个算法 Unify， 使得如果 E是可合一的 ，那么 Unify(E)计算得出一个最一般的合一代换 .如果 E不可合一 ， 那么 Unify(E)失败 • 如果 和 都是类型指派 ， 那么合一可以用来找出最一般的代换 S， 使得 S  S 都是合式的。 – 直接合一所有等式  = 的集合就可以了 ， 其中 x:  并且 x:   带类型变量的 类型推断 • 递归算法 Unify 1. Unify() =  2. Unify(E  {b1 = b2}) = if b1  b2 then f。