第9章 类型推断 类型推断是把无类型的或“部分类型化的”项 变换成良类型项的一般问题 它通过推导未给出的类型信息来完成这个变换 类型推断兼有两方面的优点 编译时完成类型检查 不需要程序中过分的类型信息
第9章 类型推断 • 类型推断是把无类型的或“部分类型化的”项 变换成良类型项的一般问题 • 它通过推导未给出的类型信息来完成这个变换 • 类型推断兼有两方面的优点 –编译时完成类型检查 –不需要程序中过分的类型信息
第9章 类型推断 本章的主要内容 ·类型推断的一般框架 -基于从类型化语言到无类型语言的“擦除”函数 加了类型变量后的类型推断 -包括主定型和合一问题 ·带多态声明的的类型推断算法
第9章 类型推断 本章的主要内容 • 类型推断的一般框架 –基于从类型化语言到无类型语言的“擦除”函数 • 加了类型变量后的→类型推断 –包括主定型和合一问题 • 带多态声明的→, , let的类型推断算法
9.1引 言 例 给出完整类型信息的PCF表达式 D'=der let dbl&(nat-→nat）→nat→nat= 入f:nat→nat.入x:nat.f(fx in dbl(入x:nat.x+2)4 忽略类型信息的PCF表达式 D=der let dbl-=入fx.ffx)in dbl(入x:x+2)4 在多态语言中，类型推断尤其有用，因为多态 项涉及入约束变量的类型、类型抽象和类型作 用
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来确定类型推断问题 L'是一种相对应的“无类型”语言，或者是分类 型信息或类型运算未给出 例从入到无类型入项的擦除函数删掉)约束的 类型指示 Erase(c) =C Erase(Ax:t.M)=Ax.Erase(M) Erase(x)=x Erase(M N)Erase(M)Erase(N) 无类型)项具有形式 U:=c|x|入x.UUU
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引 言 例入，Ⅱ的擦除函数 保持类型抽象和，约束项变量的类型说明，但是擦 除了类型作用 Erase(c)c Erase(入x:x.M)=入x.Erase(M Erase(x)=x Erase(M N Erase(M)Erase(N) Erase(入t.M)=入t.Erase(M) Erase(M t)=Erase(M) 作为擦除结果的入，亚程序的语法由文法 M:=clxl入x:x.M|MN|入t.M 允许多态函数作用到非多态变元而没有中间的类型 作用
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和擦除函数Erse:L→L'的类型推断问 题是： 对给定的表达式UL',找出L的类型化项 IM:t, 使得Erse(M)=U 一般来说，可能有无数多的方式用来将类型信 息插入项 可以给入f入，f(fx)以形式为(x→)→x→的任何 类型
9.1 引 言 • 语言L和擦除函数Erase: L → L的类型推断问 题是： 对给定的表达式UL ，找出L的类型化项 M:，使得Erase(M) = U • 一般来说，可能有无数多的方式用来将类型信 息插入项 –可以给f.x.f (f x)以形式为( →) → →的任何 类型
9.1引 言 ·例若擦除的结果是 (入t.入x:tx)(At.2x:tx) 这两个函数表达式必须作用到某个类型变元 原来的项必定有下面的形式 (入.入x:tx)x)(入t.入x:tx)) -石和石只要满足≡石，→就可以了 原来的项应该是 (2t.入x:tx)t→t)(2t.入x:tx)t)
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引 言 类型推断和类型检查 类型检查看成是用语法制导的方式，根据上下文有 关的定型条件判定项是否为良类型的项的过程 TD入x:x.M:G 把对带无类型入的定型判定问题叫做类型推断 TD入x.M:o
9.1 引 言 • 类型推断和类型检查 – 类型检查看成是用语法制导的方式，根据上下文有 关的定型条件判定项是否为良类型的项的过程 x:.M : –把对带无类型的定型判定问题叫做类型推断 x.M :
9.2带类型变量的入类型推断 9.2.1语言入 考虑语言入→的类型推断 语言入 类型由下面文法定义 t::=b t t->t 项由下面文法定义 M:=c|x|入x:x.M|MM ·入→的定型公理和推理规则同入→的相同 限制：项常量的类型一定不含类型变量
9.2 带类型变量的→类型推断 9.2.1 语言t → 考虑语言t →的类型推断 • 语言t → – 类型由下面文法定义 ::= b | t | → – 项由下面文法定义 M ::= c | x | x: .M | M M • t →的定型公理和推理规则同→的相同 –限制：项常量的类型一定不含类型变量