中国科学技术大学：《程序设计语言理论》课程教学资源（PPT课件讲稿）第9章 类型推断

9.1引 言 语言L和擦除函数Erse:L→L'的类型推断问 题是： 对给定的表达式UL',找出L的类型化项 IM:t, 使得Erse(M)=U 一般来说，可能有无数多的方式用来将类型信 息插入项 可以给入f入，f(fx)以形式为(x→)→x→的任何 类型

9.1 引 言 • 语言L和擦除函数Erase: L → L的类型推断问 题是： 对给定的表达式UL ，找出L的类型化项  M:，使得Erase(M) = U • 一般来说，可能有无数多的方式用来将类型信 息插入项 –可以给f.x.f (f x)以形式为( →) →  →的任何 类型

9.1引 言 ·例若擦除的结果是 (入t.入x:tx)(At.2x:tx) 这两个函数表达式必须作用到某个类型变元 原来的项必定有下面的形式 (入.入x:tx)x)(入t.入x:tx)) -石和石只要满足≡石，→就可以了 原来的项应该是 (2t.入x:tx)t→t)(2t.入x:tx)t)

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 引 言 • 类型推断的另一种观点是 –定型是由一组推理规则给出 合式公式的语法和证明规则给出一个逻辑系统 –类型推断算法正好是一个公理理论的判定过程 决定一个合式公式是否可证明 –判定过程是回答是或不是，而类型推断算法必须 构造类型化的项

9.1引 言 类型推断和类型检查 类型检查看成是用语法制导的方式，根据上下文有 关的定型条件判定项是否为良类型的项的过程 TD入x:x.M:G 把对带无类型入的定型判定问题叫做类型推断 TD入x.M:o

9.1 引 言 • 类型推断和类型检查 – 类型检查看成是用语法制导的方式，根据上下文有 关的定型条件判定项是否为良类型的项的过程  x:.M :  –把对带无类型的定型判定问题叫做类型推断  x.M : 

9.2带类型变量的入类型推断 9.2.1语言入 考虑语言入→的类型推断 语言入 类型由下面文法定义 t::=b t t->t 项由下面文法定义 M:=c|x|入x:x.M|MM ·入→的定型公理和推理规则同入→的相同 限制：项常量的类型一定不含类型变量

9.2 带类型变量的→类型推断 9.2.1 语言t → 考虑语言t →的类型推断 • 语言t → – 类型由下面文法定义  ::= b | t |  →  – 项由下面文法定义 M ::= c | x | x: .M | M M • t →的定型公理和推理规则同→的相同 –限制：项常量的类型一定不含类型变量