第9类型推断ppt课件

第第9章章 类型推断类型推断 类型推断是把无类型的或类型推断是把无类型的或“部分类型化的项部分类型化的项变换成良类型项的普通问题变换成良类型项的普通问题 它经过推导未给出的类型信息来完成这个变换它经过推导未给出的类型信息来完成这个变换 类型推断兼有两方面的优点类型推断兼有两方面的优点 编译时完成类型检查编译时完成类型检查 不需求程序中过分的类型信息不需求程序中过分的类型信息 第第9章章 类型推断类型推断本章的主要内容本章的主要内容类型推断的普通框架类型推断的普通框架基于从类型化言语到无类型言语的基于从类型化言语到无类型言语的“擦除函数擦除函数加了类型变量后的加了类型变量后的类型推断类型推断包括主定型和合一问题包括主定型和合一问题带多态声明的带多态声明的,let,let的类型推断算法的类型推断算法9.1 引引 言言 例例 给出完好类型信息的给出完好类型信息的PCFPCF表达式表达式D D=def let dbl:(nat =def let dbl:(nat nat)nat)nat nat nat=nat=f:nat f:nat nat.nat.x:nat.f x:nat.f(f x)(f x)in dbl(in dbl(x:nat.x+2)4x:nat.x+2)4 忽略类型信息的忽略类型信息的PCFPCF表达式表达式D=def let dbl=D=def let dbl=f.f.x.f(f x)in x.f(f x)in dbl(dbl(x:x+2)4x:x+2)4 在多态言语中，类型推断尤其有用，由于多态在多态言语中，类型推断尤其有用，由于多态项涉及项涉及约束变量的类型、类型笼统和类型作约束变量的类型、类型笼统和类型作用用9.1 引引 言言 经过选择从一种类型言语经过选择从一种类型言语L L到某种其它言语到某种其它言语L L的擦除函数的擦除函数EraseErase来确定类型推断问题来确定类型推断问题 L L是一种相对应的是一种相对应的“无类型言语，或者是无类型言语，或者是部分类型信息或类型运算未给出部分类型信息或类型运算未给出 例例 从从到无类型到无类型项的擦除函数删掉项的擦除函数删掉约约束的类型指示束的类型指示 Erase(c)Erase(c)=c=cErase(Erase(x:x:.M)=.M)=x.Erase(M)x.Erase(M)Erase(x)Erase(x)=x=xErase(M N)Erase(M N)=Erase(M)Erase(N)Erase(M)Erase(N)无类型无类型项具有方式项具有方式U:=c|x|U:=c|x|x.U|UU 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的类型推断的类型推断问题是：问题是：对给定的表达式对给定的表达式UL，找出，找出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 22就可以了就可以了 原来的项应该是原来的项应该是(t.x:t.x)t t)(t.x:t.x)t)9.1 引引 言言 类型推断的另一种观念是类型推断的另一种观念是 定型是由一组推理规那么给出定型是由一组推理规那么给出 合式公式的语法和证明规那么合式公式的语法和证明规那么给出一个逻辑系统给出一个逻辑系统 类型推断算法正好是一个公理实际的断定过程类型推断算法正好是一个公理实际的断定过程 决议一个合式公式能否可证明决议一个合式公式能否可证明 断定过程是回答是或不是，而类型推断算法必断定过程是回答是或不是，而类型推断算法必需构造类型化的项需构造类型化的项9.1 引引 言言 类型推断和类型检查类型推断和类型检查 类型检查看成是用语法制导的方式，根据上下类型检查看成是用语法制导的方式，根据上下文有关的定型条件断定项能否为良类型的项的文有关的定型条件断定项能否为良类型的项的过程过程 x:x:.M:.M:把对带无类型把对带无类型的定型断定问题叫做类型推断的定型断定问题叫做类型推断 x.M:x.M:9.2 带类型变量的带类型变量的类型推断类型推断9.2.1 言语言语 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 M1 .Mk Erase(M)Erase(M1).Erase(Mk)9.2 带类型变量的带类型变量的类型推断类型推断 现实现实 一个无类型项一个无类型项U U，只需不存在从它开场，只需不存在从它开场的无类型归约的无穷序列时，它才能够被类型的无类型归约的无穷序列时，它才能够被类型化化例例(x.xx)(x.xx)(x.xx)x.xx)推论推论1 1 假设假设U U不是强范式的，那么就不存在可不是强范式的，那么就不存在可推导的定型推导的定型 M:M:，使得，使得Erase(M)=U Erase(M)=U 推论推论2 2 假设假设U U是不可类型化的，那么由是不可类型化的，那么由 t t的主语归约性质，知道没有一个能归约到的主语归约性质，知道没有一个能归约到U U的的项是可类型化的项是可类型化的 M M M1 M1 .Mk Mk Erase(M)Erase(M)Erase(M1)Erase(M1).Erase(Mk)Erase(Mk)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:是是 M:M:的实例，假设存的实例，假设存在类型代在类型代 换换S S使得使得 S S ,M,M =S M=S M并且并且 =S=S 引理引理 假设定型断言假设定型断言 M:M:是可推导的，那是可推导的，那么它的每个实例么它的每个实例S S SM: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合一合一E9.2 带类型变量的带类型变量的类型推断类型推断 最普通的合一代换最普通的合一代换 假设存在某个代换假设存在某个代换T T使得使得R=TR=T S S，那么，那么S S比比R R更更普通普通 假设不存在比假设不存在比S S更普通的代换，那么称更普通的代换，那么称S S是最普是最普通的合一代换通的合一代换 最普通代换是使最普通代换是使E 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)w9.2 带类型变量的带类型变量的类型推断类型推断 引理引理 令令E是类型表达式之间的恣意等式集合。是类型表达式之间的恣意等式集合。存在一个算法存在一个算法Unify，使得假设，使得假设E是可合一的，是可合一的，那么那么Unify(E)计算得出一个最普通的合一代换计算得出一个最普通的合一代换.假设假设E不可合一，那么不可合一，那么Unify(E)失败失败 假设假设 和和都是类型指派，那么合一可以用来都是类型指派，那么合一可以用来找出最普通的代换找出最普通的代换S，使得，使得S S 是合式的是合式的 直接合一一切等式直接合一一切等式 =的集合就可以了，其中的集合就可以了，其中x:并且并且x:9.2 带类型变量的带类型变量的类型推断类型推断 递归算法递归算法Unify 1.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 带类型变量的带类型变量的类型推断类型推断9.2.3 主定型算法主定型算法显式定型显式定型假设假设U是一个无类型是一个无类型 项，可以使得项，可以使得Erase(M)=U的合式的类型化项的合式的类型化项 M:是是U的一个显式定型的一个显式定型主显式定型简称主定型主显式定型简称主定型假设假设U的每个显式定型都是的每个显式定型都是 M:的一个实例，的一个实例，那么那么 M:是是U的主定型的主定型 9.2 带类型变量的带类型变量的类型推断类型推断 t t主定型算法主定型算法PTPT 1.PT(c)=1.PT(c)=c:c:,其中其中 是是c c的类型的类型,它它不含类型变量不含类型变量 2.PT(x)=x:t x:t2.PT(x)=x:t x:t 3.PT(3.PT(x.U)=x.U)=let let M:M:=PT(U)=PT(U)in in if x:if x:对某个对某个 t h e n t h e n -x:-x:x:x:.M:.M:else else x:s.M:s x:s.M:s 其中其中s s是新的类型是新的类型变量变量 9.2 带类型变量的带类型变量的类型推断类型推断 t t主定型算法主定型算法PTPT PT(UV)=PT(UV)=let let M:M:=PT(U)=PT(U)N:N:=PT(V)=PT(V)其中类型变其中类型变量重新命名以量重新命名以区别于区别于PT(U)PT(U)中的中的变量变量 S=Unify(S=Unify(=|x:|x:并并且且 x:x:=t)t)，其中，其中t t是新类型变量是新类型变量inin S S S S S(MN):St S(MN):St9.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: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)=letx:r x:r=PT(x)x:s x:s=PT(x)S=Unify(r=s r=s t)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是类型是类型 的常量，的常量，中无类型变量中无类型变量 (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 定型和合一的等价定型和合一的等价类型推断和合一是算法地等价的类型推断和合一是算法地等价的每个类型推断问题产生一个合一问题每个类型推断问题产生一个合一问题每个合一问题出如今某个项的类型推断中每个合一问题出如今某个项的类型推断中 9.2 带类型变量的带类型变量的类型推断类型推断另一个类型推断算法另一个类型推断算法本质上是从定型到合一的归约本质上是从定型到合一的归约TE(c,t)=t=TE(c,t)=t=,其中其中 是是c c的类型，的类型，中无自在变量中无自在变量TE(x,t)=t=txTE(x,t)=t=tx，其中其中tx tx 是是x x的类型的类型TE(U V,t)=TE(U,r)TE(U V,t)=TE(U,r)TE(V,s)TE(V,s)r=s r=s tt其中其中r r，s s都是新的类型变量都是新的类型变量TE(TE(x.U,t)=TE(U,s)x.U,t)=TE(U,s)t=tx t=tx ss其中其中s s是新的类型变量是新的类型变量假设假设U U是无类型项，是无类型项，t t是类型变量，并且是类型变量，并且E=E=TE(U,t)TE(U,t)，那么，那么U U的每个定型是的每个定型是S S U U:U U:StSt的一个实例对某个使的一个实例对某个使E E可以合一的最普通可以合一的最普通合一代换合一代换 S S习习 题题 第一次：第一次：9.2