【教学课件】第9章类型推断

Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,*,*,第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,dbl,=,f,.,x,.,f,(,f x,),in,dbl,(,x,:,x,+2)4,在多态语言中，类型推断尤其有用，因为多态项涉及,约束变量的类型、类型抽象和类型作用,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,)=,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,的类型推断问题是：,对给定的表达式,U,L,，,找出,L,的类型化项,M,:,，,使得,Erase,(,M,)=,U,一般来说，可能有无数多的方式用来将类型信息插入项,可以给,f,.,x,.,f,(,f x,),以形式为,(,),的任何类型,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,引 言,类型推断和类型检查,类型检查,看成是用语法制导的方式，根据上下文有关的定型条件判定项是否为良类型的项的过程,x,:,.,M,:,把对带无类型,的定型判定问题叫做,类型推断,x,.,M,:,9.2 带类型变量的,类型推断,语言,t,考虑语言,t,的类型推断,语言,t,类型由下面文法,定义,:=,b,|,t,|,项由下面文法,定义,M,:=,c,|,x,|,x,:,.,M,|,M M,t,的定型公理和推理规则同,的相同,限制：项常量的类型一定不含类型变量,9.2 带类型变量的,类型推断,命题,令,M,是任意的良类型,t,项。如果由类型化项上的,和,归约有,M,N,，,那么由无类型项上的同样归约有,Erase,(,M,),Erase,(,N,)。,反过来，如果由无类型的归约有,Erase,(,M,),V,，,那么存在一个类型化,项,N,，,使得,M,N,且,Erase,(,N,),V,。,M,M,1,.,M,k,Erase,(,M,),Erase,(,M,1,).,Erase,(,M,k,),9.2 带类型变量的,类型推断,事实 一个无类型项,U,，,只有不存在从它开始的无类型归约的无穷序列时，它才可能被类型化,推论,1,如果,U,不是强范式的，那么就不存在可推导的定型,M,:,，,使得,Erase,(,M,)=,U,推论,2,如果,U,是不可类型化的，那么由的主语归约性质，知道没有一个能归约到,U,的项是可类型化的,M,M,1,.,M,k,Erase,(,M,),Erase,(,M,1,).,Erase,(,M,k,),9.2 带类型变量的,类型推断,9.2.2 代换、实例与合一,事实 在,t,的类型推断中，可推导的定型断言封闭于代换,类型代换,类型代换,S,作用到类型表达式,S,是把,中的每个变量,t,用,S,(,t,),代替,类型代换,S,作用到类型指派,S,=,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,w,S,=,t,v,w,s,(,v,w,),v,代换结果(,v,w,),v,=(,v,w,),v,v,w,=,v,w,S,合一,E,9.2 带类型变量的,类型推断,最一般的合一代换,如果存在某个代换,T,使得,R,=,T,S,，,那么,S,比,R,更一般,如果不存在比,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,),计算得出一个最一般的合一代换.如果,E,不可合一，那么,Unify,(,E,),失败,如果和都是类型指派，那么合一可以用来找出最一般的代换,S,，,使得,S,S,都是合式的。,直接合一所有等式,=,的集合就可以了，其中,x,:,并且,x,:,9.2 带类型变量的,类型推断,递归算法,Unify,1.,Unify,()=,2.,Unify,(,E,b,1,=,b,2,)=,if,b,1,b,2,then,fail,else,Unify,(,E,),3.,Unify,(,E,t,=,)=,if(,t,)then,Unify,(,E,),else if,t,occurs in,then,fail,else,Unify,(,/,t,E,),/,t,4.,Unify,(,E,1,2,=,1,2,)=,Unify,(,E,1,=,1,2,=,2,),9.2 带类型变量的,类型推断,9.2.3 主定型算法,显式定型,如果,U,是一个无类型,项，使得,Erase,(,M,)=,U,的,合式,的类型化项,M,:,是,U,的一个显式定型,主显式定型（简称主定型）,如果,U,的每个显式定型都是,M,:,的一个实例，那么,M,:,是,U,的主定型,9.2 带类型变量的,类型推断,t,主定型算法,PT,1.,PT,(,c,)=,c,:,其中,是,c,的类型,它不含类型变量,2.,PT,(,x,)=,x,:,t,x,:,t,3.,PT,(,x,.,U,)=,let,M,:,=,PT,(,U,),in,if,x,:,（,对某个,）,then-,x,:,x,:,.,M,:,else ,x,:,s,.,M,:,s,其中,s,是新的类型变量,9.2 带类型变量的,类型推断,t,主定型算法,PT,PT,(,UV,)=,let,M,:,=,PT,(,U,),N,:,=,PT,(,V,),其中类型变量重新命名以,区别于,PT,(,U,),中的变量,S,=,Unify,(,=,|,x,:,并且,x,:,=,t,)，,其中,t,是新类型变量,in,S,S,S,(,MN,):,St,9.2 带类型变量的,类型推断,例,计算,x,.,y,.,xy,的主定型,PT,(,xy,)=let,x,:,r x,:,r,=,PT,(,x,),y,:,s y,:,s,=,PT,(,y,),S,=,Unify,(,r,=,s,t,),in,x,:,Sr,y,:,Ss,xy,:,St,PT,(,xy,)=,x,:s,t,y,:,s,xy,:,t,PT,(,x,.,y,.,xy,)=,x,:,s,t,.,y:s,.,xy,:(,s,t,),s,t,9.2 带类型变量的,类型推断,例,算法,PT,为什么对,x,.,xx,会失败,PT,(,xx,)=let,x,:,r x,:,r,=,PT,(,x,),x,:,s x,:,s,=,PT,(,x,),S,=,Unify,(,r,=,s,r,=,s,t,),in,x,:,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,是类型,的常量，,中无类型变量 (,cst,),x,:,x,:,(,var,),(,abs,),(,app,),(,add var,),x,:,U,:,(,x,.,U,):,U,:,V,:,UV,:,U,:,x,:,U,:,x,不在,中,9.2 带类型变量的,类型推断,引理 如果,M,:,是良类型的项，那么,|-,C,Erase,(,M,),.,反过来,如果,|-,C,U,，,那么存在类型化的项,M,:,，,使得,Erase,(,M,)=,U,9.2 带类型变量的,类型推断,9.2.5 定型和合一的等价,类型推断和合一是算法地等价的,每个类型推断问题产生一