第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 允许多态函数作用到非多态变元而没有中间的类型 作用