第9章类型推断.ppt

第第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) = cErase( x: . M) =  x. Erase(M)Erase(x) = xErase(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 带类型变量的带类型变量的 类型推断类型推断9.2.1 语言语言 t t考虑语言考虑语言 t t的类型推断的类型推断•语言语言 t t–类型由下面文法类型由下面文法定义定义  ::= b | t |     –项由下面文法项由下面文法定义定义M ::= c | x |  x:  .M | M M• t t的定型公理和推理规则同的定型公理和推理规则同 的相同的相同–限制：项常量的类型一定不含类型变量限制：项常量的类型一定不含类型变量 9.2 带类型变量的带类型变量的 类型推断类型推断•命题命题 令令  M  是任意的良类型是任意的良类型 t t项。

如果项如果由类型化项上的由类型化项上的 和和 归约有归约有M N，，那么由那么由无类型项上的同样归约有无类型项上的同样归约有Erase(M)  Erase(N)反过来，如果由无类型的归约有反过来，如果由无类型的归约有Erase(M)  V，，那么存在一个类型化那么存在一个类型化 项项  N  ，，使得使得M N且且Erase(N)   VM  M1  . . .  MkErase(M)  Erase(M1)  . . .  Erase(Mk) 9.2 带类型变量的带类型变量的 类型推断类型推断•事实事实 一个无类型项一个无类型项U，，只有不存在从它开始只有不存在从它开始的无类型归约的无穷序列时，它才可能被类型的无类型归约的无穷序列时，它才可能被类型化化例例( x.xx) ( x.xx)–推论推论1 如果如果U不是强范式的，那么就不存在可推不是强范式的，那么就不存在可推导的定型导的定型  M: ，，使得使得Erase(M) = U –推论推论2 如果如果U是不可类型化的，那么由是不可类型化的，那么由 t t的主语的主语归约性质，知道没有一个能归约到归约性质，知道没有一个能归约到U的项是可类型的项是可类型化的化的M  M1  . . .  MkErase(M)  Erase(M1)  . . .  Erase(Mk)9.2 带类型变量的带类型变量的 类型推断类型推断9.2.2 代换、实例与合一代换、实例与合一•事实事实 在在 t t的类型推断中，可推导的定型断的类型推断中，可推导的定型断言封闭于代换言封闭于代换•类型代换类型代换–类型代换类型代换S作用到类型表达式作用到类型表达式  S 是把是把 中的每个变量中的每个变量t用用S (t)代替代替–类型代换类型代换S作用到类型指派作用到类型指派 S   = {x: S  | x:      }–类型代换类型代换S作用到作用到 t 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 带类型变量的带类型变量的 类型推断类型推断•递归算法递归算法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([ /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 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 t主定型算法主定型算法PTPT(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) = letx: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) = letx: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 定型和合一的等价定型和合一的等价•类型推断和合一是算法地等价的类型推断和合一是算法地等价的–每个类型推断问题产生一个合一问题每个类型推断问题产生一个合一问题–每个合一问题出现在某个项的类型推断中每个合一问题出现在某个项的类型推断中 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。