第9类型推断.ppt
《第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.
2、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) Eras
3、e(N) 无类型项具有形式 U := c | x | x.U | UU,9.1 引 言,例 , 的擦除函数 保持类型抽象和约束项变量的类型说明,但是擦除了类型作用 Erase(c) = c Erase(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和擦除函数
4、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 引 言,类型推断的另一种观点是 定型是由一组推理规则给出 合式公式的语法和证
5、明规则给出一个逻辑系统 类型推断算法正好是一个公理理论的判定过程 决定一个合式公式是否可证明 判定过程是回答是或不是,而类型推断算法必须构造类型化的项,9.1 引 言,类型推断和类型检查 类型检查看成是用语法制导的方式,根据上下文有关的定型条件判定项是否为良类型的项的过程 x:.M : 把对带无类型的定型判定问题叫做类型推断 x.M : ,9.2 带类型变量的类型推断,9.2.1 语言t 考虑语言t的类型推断 语言t 类型由下面文法定义 := b | t | 项由下面文法定义 M := c | x | x: .M | M M t的定型公理和推理规则同的相同 限制:项常量的类型一定不含类型变量,
6、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,只有不存在从它开始的无类型归约的无穷序列时,它才可能被类型化 例 (x.xx) (x.xx) 推论1 如果U不是强范式的,那么就不存在可推导的定型 M:,使得Erase(M) =
7、 U 推论2 如果U是不可类型化的,那么由t的主语归约性质,知道没有一个能归约到U的项是可类型化的 M M1 . . . Mk Erase(M) Erase(M1) . . . 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:的实例,如果存在类型代 换S使得 S ,
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 类型 推断
链接地址:https://www.31doc.com/p-2579023.html