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.UUU9.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