《第9类型推断.ppt》由会员分享，可在线阅读，更多相关《第9类型推断.ppt（31页珍藏版）》请在三一办公上搜索。
1、第9章 类型推断,类型推断是把无类型的或“部分类型化的”项变换成良类型项的一般问题它通过推导未给出的类型信息来完成这个变换类型推断兼有两方面的优点编译时完成类型检查不需要程序中过分的类型信息,第9章 类型推断,本章的主要内容类型推断的一般框架基于从类型化语言到无类型语言的“擦除”函数加了类型变量后的类型推断包括主定型和合一问题带多态声明的,let的类型推断算法,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
2、dbl=f.x.f(f x)in dbl(x:x+2)4在多态语言中，类型推断尤其有用，因为多态项涉及约束变量的类型、类型抽象和类型作用,9.1 引 言,通过选择从一种类型语言L到某种其它语言L的擦除函数Erase来确定类型推断问题L是一种相对应的“无类型”语言，或者是部分类型信息或类型运算未给出例 从到无类型项的擦除函数删掉约束的类型指示Erase(c)=cErase(x:.M)=x.Erase(M)Erase(x)=xErase(M N)=Erase(M)Erase(N)无类型项具有形式U:=c|x|x.U|UU,9.1 引 言,例,的擦除函数保持类型抽象和约束项变量的类型说明，但是擦除了
3、类型作用Erase(c)=cErase(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的类型推断问题是：对给定的表达式UL，找出L的类型化项 M:，使得Erase(M)=U一般来说，可能有无数多的方式用来将类型信息插入项可以给f.x.f(f x)以形式为()的任何类型,9.1 引 言,例 若擦
4、除的结果是(t.x:t.x)(t.x:t.x)这两个函数表达式必须作用到某个类型变元原来的项必定有下面的形式(t.x:t.x)1)(t.x:t.x)2)1 和2只要满足1 22就可以了原来的项应该是(t.x:t.x)t t)(t.x:t.x)t),9.1 引 言,类型推断的另一种观点是定型是由一组推理规则给出 合式公式的语法和证明规则给出一个逻辑系统类型推断算法正好是一个公理理论的判定过程 决定一个合式公式是否可证明判定过程是回答是或不是，而类型推断算法必须构造类型化的项,9.1 引 言,类型推断和类型检查类型检查看成是用语法制导的方式，根据上下文有关的定型条件判定项是否为良类型的项的过程 x
5、:.M:把对带无类型的定型判定问题叫做类型推断 x.M:,9.2 带类型变量的类型推断,9.2.1 语言t考虑语言t的类型推断语言t类型由下面文法定义:=b|t|项由下面文法定义M:=c|x|x:.M|M Mt的定型公理和推理规则同的相同限制：项常量的类型一定不含类型变量,9.2 带类型变量的类型推断,命题 令 M是任意的良类型t项。如果由类型化项上的和归约有M N，那么由无类型项上的同样归约有Erase(M)Erase(N)。反过来，如果由无类型的归约有Erase(M)V，那么存在一个类型化项 N，使得M N且Erase(N)V。M M1.MkErase(M)Erase(M1).Erase(
6、Mk),9.2 带类型变量的类型推断,事实 一个无类型项U，只有不存在从它开始的无类型归约的无穷序列时，它才可能被类型化例(x.xx)(x.xx)推论1 如果U不是强范式的，那么就不存在可推导的定型 M:，使得Erase(M)=U 推论2 如果U是不可类型化的，那么由t的主语归约性质，知道没有一个能归约到U的项是可类型化的M M1.MkErase(M)Erase(M1).Erase(Mk),9.2 带类型变量的类型推断,9.2.2 代换、实例与合一事实 在t的类型推断中，可推导的定型断言封闭于代换类型代换类型代换S作用到类型表达式 S是把中的每个变量t用S(t)代替类型代换S作用到类型指派S=
7、x:S|x:类型代换S作用到t项结果S M同M的区别仅在约束变元的类型,9.2 带类型变量的类型推断,实例定型断言 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 wS=t,v w,s,(v w)v代换结果(v w)v=(v w)v,v w=v wS合一E,9.2 带类型变量的类型推断,最一般的合一代换如果存在某个代换T使得R=TS，那么S比R更
8、一般如果不存在比S更一般的代换，则称S是最一般的合一代换 最一般代换是使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)计算得出一个最一般
9、的合一代换.如果E不可合一，那么Unify(E)失败如果和都是类型指派，那么合一可以用来找出最一般的代换S，使得S S 是合式的直接合一所有等式=的集合就可以了，其中x:并且x:,9.2 带类型变量的类型推断,递归算法Unify1.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(/tE)/t 4.Unify(E 1 2=1 2)=Unify(E 1=1 2=2),9.2 带类型变量的类
10、型推断,9.2.3 主定型算法显式定型如果U是一个无类型项，能够使得Erase(M)=U的合式的类型化项 M:是U的一个显式定型主显式定型（简称主定型）如果U的每个显式定型都是 M:的一个实例，那么 M:是U的主定型,9.2 带类型变量的类型推断,t主定型算法PT1.PT(c)=c:,其中是c的类型,它不含类型变量2.PT(x)=x:t x:t3.PT(x.U)=let M:=PT(U)in if x:（对某个）then-x:x:.M:else x:s.M:s 其中s是新的类型变量,9.2 带类型变量的类型推断,t主定型算法PTPT(UV)=let M:=PT(U)N:=PT(V)其中类型变量
11、重新命名以区别于PT(U)中的变量 S=Unify(=|x:并且 x:=t)，其中t是新类型变量in S S S(MN):St,9.2 带类型变量的类型推断,例 计算x.y.xy的主定型PT(xy)=letx:r x:r=PT(x)y:s y:s=PT(y)S=Unify(r=s t)inx:Sr y:Ss xy:StPT(xy)=x:s t,y:s xy:tPT(x.y.xy)=x:s t.y:s.xy:(s t)s t,9.2 带类型变量的类型推断,例 算法PT为什么对x.xx会失败PT(xx)=letx:r x:r=PT(x)x:s x:s=PT(x)S=Unify(r=s r=s t)
12、inx: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是类型的常量，中无类
13、型变量(cst)x:x:(var)(abs)(app)(add var),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,
