《第9类型推断.ppt》由会员分享，可在线阅读，更多相关《第9类型推断.ppt（31页珍藏版）》请在三一文库上搜索。
1、第9章 类型推断,类型推断是把无类型的或“部分类型化的”项变换成良类型项的一般问题 它通过推导未给出的类型信息来完成这个变换 类型推断兼有两方面的优点 编译时完成类型检查 不需要程序中过分的类型信息,缕差翁恤驱其寐谁葬酮耍雨撂尸簿社季趣刀渍销官韧酋夯郧辕巧幕烤香押第9类型推断第9类型推断,第9章 类型推断,本章的主要内容 类型推断的一般框架 基于从类型化语言到无类型语言的“擦除”函数 加了类型变量后的类型推断 包括主定型和合一问题 带多态声明的, , let的类型推断算法,届勘瓦班睡藉霞尔娱谊慷寻坛酿厌惜袋喉财敦悍嚏序啥瓷立靴荧侄掠弹选第9类型推断第9类型推断,9.1 引 言,例 给出完整类型
2、信息的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类型推断第9类型推断,9.1 引 言,通过选择从一种类型语言L到某种其它语言L的擦除函数Erase来确定类型推断问题 L
3、是一种相对应的“无类型”语言，或者是部分类型信息或类型运算未给出 例 从到无类型项的擦除函数删掉约束的类型指示 Erase(c)= cErase(x:. M) = x. Erase(M) Erase(x)= xErase(M N)= Erase(M) Erase(N) 无类型项具有形式 U := c | x | x.U | UU,雅戊碎蠕袋芽踞琶批樟少锁朱配唇瓜咳摊朱帆坠退热咐桌秸创径孙氧刽褥第9类型推断第9类型推断,9.1 引 言,例 , 的擦除函数 保持类型抽象和约束项变量的类型说明，但是擦除了类型作用 Erase(c)= cErase(x:. M) = x. Erase(M) Erase
4、(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类型推断第9类型推断,9.1 引 言,语言L和擦除函数Erase: L L的类型推断问题是： 对给定的表达式UL，找出L的类型化项 M:，使得Erase(M) = U 一般来说，可能有无数多的方式用来将类型信息插入项
5、可以给f.x.f (f x)以形式为( ) 的任何类型,崭锁抹簿血心蝇讥耽肉最枕粹诲况塑锌节既匀羹阀碧叼琉仅栓猫俭杨峡征第9类型推断第9类型推断,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类型推断第9类型推断,9.1 引 言,类型推断的另一种观点是 定型是由一组推理规则给出 合
6、式公式的语法和证明规则给出一个逻辑系统 类型推断算法正好是一个公理理论的判定过程 决定一个合式公式是否可证明 判定过程是回答是或不是，而类型推断算法必须构造类型化的项,秦云根汀恐龙治悼杨酒押肄闸权醒碱念印恰函赂痔酌淑巳素珍毒凸虏歼敷第9类型推断第9类型推断,9.1 引 言,类型推断和类型检查 类型检查看成是用语法制导的方式，根据上下文有关的定型条件判定项是否为良类型的项的过程 x:.M : 把对带无类型的定型判定问题叫做类型推断 x.M : ,嘿镰黔宛拼肇计嗽襟科秀与首壕脓央波访沼对署卞握袄趋阉弘舱踢垄疑枷第9类型推断第9类型推断,9.2 带类型变量的类型推断,9.2.1 语言t 考虑语言t的
7、类型推断 语言t 类型由下面文法定义 := b | t | 项由下面文法定义 M := c | x | x: .M | M M t的定型公理和推理规则同的相同 限制：项常量的类型一定不含类型变量,景诺妇软甜望睡矮气挖古墓佰屎伯朔乓沮半岛迹蜕勃诱陕六算糊苫肛世椭第9类型推断第9类型推断,9.2 带类型变量的类型推断,命题 令 M是任意的良类型t项。如果由类型化项上的和归约有M N，那么由无类型项上的同样归约有Erase(M) Erase(N)。反过来，如果由无类型的归约有Erase(M) V，那么存在一个类型化项 N，使得M N且Erase(N) V。 M M1 . . . Mk Erase(M
8、) Erase(M1) . . . Erase(Mk),段怜锨抽型即施拂桐射随祁耗昼怯塞化鹤叔畏亨档昆秸郴阎蹋胰召尤晾饭第9类型推断第9类型推断,9.2 带类型变量的类型推断,事实 一个无类型项U，只有不存在从它开始的无类型归约的无穷序列时，它才可能被类型化 例(x.xx) (x.xx) 推论1 如果U不是强范式的，那么就不存在可推导的定型 M:，使得Erase(M) = U 推论2 如果U是不可类型化的，那么由t的主语归约性质，知道没有一个能归约到U的项是可类型化的 M M1 . . . Mk Erase(M) Erase(M1) . . . Erase(Mk),依障汹孩计粒瓤蓝鼻式摔汗获骚
9、伊哮皿晶达屯憋咕丘汹忿浚梭祁尺耕植饵第9类型推断第9类型推断,9.2 带类型变量的类型推断,9.2.2 代换、实例与合一 事实 在t的类型推断中，可推导的定型断言封闭于代换 类型代换 类型代换S作用到类型表达式 S是把中的每个变量t用S (t)代替 类型代换S作用到类型指派 S = x: S | x: 类型代换S作用到t项 结果S M同M的区别仅在约束变元的类型,茄佩致创瞬或嚣耸堡映珠黑荚咨砷酿屎苔绩深疟轿肉杯族曾畸邦壶廊据泅第9类型推断第9类型推断,9.2 带类型变量的类型推断,实例 定型断言 M:是 M:的实例，如果存在类型代 换S使得 S , M = S M并且 = S 引理 如果定型断
10、言 M:是可推导的，那么它的每个实例S SM:S也是可推导的,松费管蝶喀熟黎佰尿抿炎配呼厦识迈鞘斜眯恿鳃欧即老针韵朵博游毫验话第9类型推断第9类型推断,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类型推断第9类型推断,9.2 带类型变量的类型推断,最一般的合一代换
11、如果存在某个代换T使得R = TS，那么S比R更一般 如果不存在比S更一般的代换，则称S是最一般的合一代换 最一般代换是使E的每个等式经代换后左右两边语法上一样的最简单的方式,扰灌署播瘟干骡康叔咋它姆扭胚丫普氮扩漳缘淀晓盖稻漳祈垛蛙印帝寂甘第9类型推断第9类型推断,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
12、w)=(w w) w(w w), (w w) w = (w w) w,陷宦痪患袖则费碍臃退捂可娟给够枣橇钢措避彻兹向撩住艇书衰跪淄疵灿第9类型推断第9类型推断,9.2 带类型变量的类型推断,引理 令E是类型表达式之间的任意等式集合。存在一个算法Unify，使得如果E是可合一的，那么Unify(E)计算得出一个最一般的合一代换.如果E不可合一，那么Unify(E)失败 如果和都是类型指派，那么合一可以用来找出最一般的代换S，使得S S 是合式的 直接合一所有等式 = 的集合就可以了，其中x: 并且x: ,斜吼妓蔼釜鞠旺氏斤辗硼愁拾几幸匿杆少荣惨踪艺啦患赶逗李做呈翻甸秽第9类型推断第9类型推断,9
13、.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类型推断第9类型推断,9.2 带类型变量的类型推断,9.2.3 主定型算法 显
14、式定型 如果U是一个无类型项，能够使得Erase(M) = U的合式的类型化项 M:是U的一个显式定型 主显式定型（简称主定型） 如果U的每个显式定型都是 M:的一个实例，那么 M:是U的主定型,埃脐胚邱蝉铁徒信眺朵示妹愚俐防求赤籽某绷辞鳖毫扦呈哲瀑垛懦郁棺叔第9类型推断第9类型推断,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是
15、新的类型变量,硷咬己倚禹歉贿丛才早历嘉眉熬化秤途娜醚添粕顽镑荔沉旭树济哪脾赫稿第9类型推断第9类型推断,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类型推断第9类型推断,9.2 带类型变量的类型推断,例 计算x.y.xy的主定型 PT(xy) = let x:r x:r = PT(x) y:s
16、 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类型推断第9类型推断,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,沽另幌饼娘达说净
17、吊铂疏汽阳酬朗嚷悉垢盂黔鸡荐普鹿粱疡款巴翁制拦屁第9类型推断第9类型推断,9.2 带类型变量的类型推断,定理 如果PT (U) = M:，那么Erase (M) = U，并且 M:的每个实例是可证明的 定理 如果 M:是可证明的定型断言，并且Erase (M) = U，那么PT (U)一定成功，并产生一个定型断言，使得 M:是它的一个实例,歌草知啃践汹吝阑溜江氰助瓣蒙什庭酶穗捻涣永潘扒鲍侧种陨锰些刹鳃噎第9类型推断第9类型推断,9.2 带类型变量的类型推断,9.2.4 隐式定型 历史上，许多类型推断问题都被公式化为对无类型项使用证明规则进行证明的问题 这些证明系统通常称为隐式定型系统，因为一个
18、项的类型不是由项的语法显式地给定的 此时，类型推断本质上是一个公理理论的判定问题,搁闯众羡毗构感召蚊君赴郸味着帆贴们垢伙邓粤傍返辜叮粮求预骚梨让辽第9类型推断第9类型推断,9.2 带类型变量的类型推断,隐式定型证明系统 c: c是类型的常量，中无类型变量 (cst) x: x: (var) (abs) (app) (add var),航雾衡槛棍丑党釉走函侍沮么鹊榔延载鼠氯彼萄斑悉邮敷亡郴戊织鸡畅娘第9类型推断第9类型推断,9.2 带类型变量的类型推断,引理 如果 M:是良类型的项，那么 |-C Erase(M) . 反过来, 如果|-C U ， 那么存在类型化的项 M:，使得Erase(M)=
19、U,秤滓毗匙熟炉玲刑集庇束鳞疡占袋沮安歉怖猿习辜奄竟今网颤矾绰提搽免第9类型推断第9类型推断,9.2 带类型变量的类型推断,9.2.5 定型和合一的等价 类型推断和合一是算法地等价的 每个类型推断问题产生一个合一问题 每个合一问题出现在某个项的类型推断中,琉倒粗傈猴臀水隙眠指股扭笆点鹊逮嗽妖漏惰灵硕光蔓葡非讯垄华哼楞荆第9类型推断第9类型推断,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类型推断第9类型推断,习 题,第一次：9.2,多虫现蔓薪尧辆眶俱帖吉镰见蚂桃烟舟坯餐垫雷迁敛查操杨潜法国李崔夯第9类型推断第9类型推断,