7 类型
我们已理解如何用解释器建模程序的运行时行为。现在，我们用同样的技术不加运行 地分析或预测程序的行为。
我们已见识过一些了：我们的词法地址翻译器在分析阶段预测程序在运行时如何从环境中找 出各个变量。而且，翻译器本身看起来就像一个解释器，只是我们传递的不是环境，而是静 态环境。
我们的目标是分析程序，预测程序求值是否安全 (safe)，即，求值过程是否能避 免某些类型的错误，但安全的含义视语言而不同。如果我们能保证求值是安全的，我们就能 确保程序满足其合约。
本章，我们考虑类似表达式 LETREC的语言。这些语言求值安全，当且仅当：
-
每个待求值的变量 var 都已绑定。
-
每个待求值的差值表达式 (diff-exp exp_1 exp_2) 中，exp_1 和 exp_2 的值都是 num-val。
-
每个待求值的表达式 (zero?-exp exp_1) 中，exp_1 的值都是 num-val。
-
每个待求值的条件表达式 (if-exp exp_1 exp_2 exp_3) 中， exp_1 的值都是 bool-val。
-
每个待求值的过程调用 (call-exp rator rand) 中，rator 的 值都是 proc-val。
这些条件确保每个操作符都作用于正确类型的操作数。因此，我们说违反这些条件 是类型错误 (type error)。
安全的求值仍可能因为其他原因而失败：除以零，取空列表的 car，等等。我们不把 这些算作安全的定义，因为在预测安全性时，保证这些条件要比上面列出的难得多。同样地， 安全的求值可能永远运行。我们的安全定义不包含不终止，因为检查程序是否终止也很困难 （事实上，这一般是无法判定的）。有些语言的类型系统给出比上述更强的保证，但它们要 比我们这里考虑的复杂得多。
我们的目标是写出过程，查看程序文本，接受或者拒绝它。而且，我们希望我们的分析过程 保守一点：如果分析接受程序，那么我们确保求程序的值是安全的。如果分析不能确定求值 是否安全，它必须拒绝程序。我们称这样的分析是健壮的 (sound)。
拒绝所有程序的分析仍是健壮的，可我们还是想让我们的分析接受一大批程序。本章的分析 将接受足够多的程序，因此是有用的。
这里是一些示例程序，以及它们应被分析拒绝或接受：
if 3 then 88 else 99 拒绝：条件非布尔值
proc (x) (3 x) 拒绝：rator非过程值
proc (x) (x 3) 接受
proc (f) proc (x) (f x) 接受
let x = 4 in (x 3) 拒绝：rator非过程值
(proc (x) (x 3) 拒绝：同前例
4)
let x = zero?(0) 拒绝：diff-exp 参数非整数
in -(3, x)
(proc (x) -(3,x) 拒绝：同前例
zero?(0))
let f = 3 拒绝：rator非过程值
in proc (x) (f x)
(proc (f) proc (x) (f x) 拒绝：同前例
3)
letrec f(x) = (f -(x,-1)) 接受，不终止，但是安全
in (f 1)
虽然最后一个例子求值不终止，但根据上述定义，求值仍是安全的，所以我们的分析可以接 受它。之所以接受它，是因为我们的分析器不够好，不足以判定这个程序不会终止。
7.1 值及其类型
由于安全条件只涉及 num-val、bool-val 和 proc-val，有人可能以为记 录这三种类型就足够了。但那是不够的：如果我们只知道 f 绑定到一个 proc-val，我们根本无法确认 (f 1) 的值。从这个角度来看，我们需要更细致 地记录与过程相关的信息。这些更细致的信息叫做语言的类型结 构 (type structure)。
我们的语言将有一种非常简单的类型结构。现在，考虑 LETREC 中的表达值。这些值只包含 单参数过程，但处理 中的多参数过程也很明了：只需做些额外工作， 没有任何新思想。
\begin{cornertext}[title=类型语法] \begin{align*}\mathit{Type} &::= \mathit{int} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{int-type ()} \\[5pt] \mathit{Type} &::= \mathit{bool} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{bool-type ()} \\[5pt] \mathit{Type} &::= (\mathit{Type} -> \mathit{Type}) \\[-3pt] &\mathrel{\phantom{::=}} \fbox{proc-type (arg-type result-type)}\end{align*} \end{cornertext}
要理解这个系统如何工作，让我们来看些例子。
\begin{cornertext}[title=值及其类型的例子]3 的值类型为 int。
-(33,22) 的值类型为 int。
zero?(11) 的值类型为bool。
proc (x) -(x,11) 的值类型为 int -> int，因为给定一个整数时，它返回一个 整数。
proc (x) let y = -(x,11) in -(x,y)
的值类型为 int -> int， 因为给定一个整数时，它返回一个整数。proc (x) if x then 11 else 22
的值类型为 bool -> int，因为 给定一个布尔值时，它返回一个整数。proc (x) if x then 11 else zero?(11) 在我们的类型系统中没有类型，因为给定一 个布尔值时，它既可能返回一个整数，也可能返回一个布尔值，而我们没有描述这种行为的 类型。
proc (x) proc (y) if y then x else 11
的值类型为 (int -> (bool -> int))，因为给定一个布尔值时，它返回一个过程，该过程取一布尔值，返回一 整数。proc (f) (f 3) 的值类型为 ((int -> t) -> t)，t 是任意类型， 因为给定一个类型为 (int -> t) 的过程，它返回类型为 t 的值。
proc (f) proc (x) (f (f x)) 的值类型为 ((t -> t) -> (t -> t))，t 是任意类型，因为给定一个类型为 (t -> t) 的过程，它 返回另一过程，该过程取一类型为 t 的参数，返回一类型为 t 的值。
\end{cornertext}
我们用下面的定义解释这些例子。
有时，我们不说“v类型为t”，而说 “v 具有类型 t”。
此定义归纳自 t。但是它依赖于上面另行定义的类型错误。
在该系统中，值 v 可以有多个类型。比如，值 proc (x) x 类型为 (t \to t)，t 是任意类型。有些值可能没有类型，比如 proc (x) if x then 11 else zero?(11)。
\textnormal{[}{\star}\textnormal{]} 下面是一些含有闭包的表达式。想想每个表达式的值。每个值的类型是什么（可能不止一 个）？有些值的类型在我们的有类型语言中可能无法描述。
proc (x) -(x,3)
proc (f) proc (x) -((f x), 1)
proc (x) x
proc (x) proc (y) (x y)
proc (x) (x 3)
proc (x) (x x)
proc (x) if x then 88 else 99
proc (x) proc (y) if x then y else 99
(proc (p) if p then 88 else 99
33)
(proc (p) if p then 88 else 99
proc (z) z)
proc (f)
proc (g)
proc (p)
proc (x) if (p (f x)) then (g 1) else -((f x),1)
proc (x)
proc(p)
proc (f)
if (p x) then -(x,1) else (f p)
proc (f)
let d = proc (x)
proc (z) ((f (x x)) z)
in proc (n) ((f (d d)) n)
\textnormal{[}{\star}{\star}\textnormal{]} 根据，有没有表达值恰好有两种类型？
\textnormal{[}{\star}{\star}\textnormal{]} 在语言 LETREC 中，能否判定表达值 val 的类型为 t？
7.2 赋予表达值类型
现在，我们只解决了表达值的类型。为了分析程序，我们要写出过程，预测表达式值的类型。
更准确地说，我们的目标是写出过程 type-of。给定一个表达式（名为 exp）和 一个将变量映射到某一类型的类型环境 (type environment)（名为tenv）， 它赋给 exp 一个类型 t，且 t 具有性质：
\begin{cornertext}[title=type-of 规范]不论何时求 exp 的值，若环境中所有变量对应值的类型都由 tenv 指定，则发生 如下之一：
结果类型为 t，
求值不终止，或
求值因类型错误之外的原因失败。
\end{cornertext}
如果我们可以赋予表达式一个类型，我们说该表达式是正常类型 (well-typed) 的， 否则说它是异常类型 (ill-typed) 或无类型 的。
我们的分析基于以下原则：如果我们能预测表达式中所有子表达式的值类型，就能预测表达 式的值类型。
我们用这一想法写出 type-of 遵循的一些规则。设 tenv 为一类型环境， 将各个变量映射到类型。那么我们有：
\begin{cornertext}[title=简单判类规则]
(type-of (const-exp num) tenv) = int
(type-of (var-exp num) tenv) = tenv(var)
\infer{(type-of (zero?-exp exp_1) tenv) = bool} {(type-of exp_1 tenv) = int}
\infer{(type-of (diff-exp exp_1 exp_2) tenv) = int} {(type-of exp_1 tenv) = int & (type-of exp_2 tenv) = int}
\infer{(type-of (let-exp var exp_1 body) tenv) = t_2} {(type-of exp_1 tenv) = t_1 & (type-of body [var=t_1]tenv) = t_2}
\infer{(type-of (if-exp exp_1 exp_2 exp_3) tenv) = t} {\begin{gathered} (type-of exp_1 tenv) = bool \\ (type-of exp_2 tenv) = t \\ (type-of exp_2 tenv) = t \end{gathered}}
\infer{(type-of (call-exp rator rand) tenv) = t_2} {(type-of rator tenv) = t_1 \to t_2 & (type-of rand tenv) = t_1}
\end{cornertext}
若我们在适当的环境中求类型为 t 的表达式 exp 的 值，我们不仅知道值的类型为 t，而且知道与这个值有关的历史信息。因为求 exp 的值保证是安全的，我们知道 exp 的值一定是由符合类型 t 的操作符产 生的。在模块，我们更细致地思考数据抽象时，这种观点会很有帮助。
过程呢？如果 proc(var) body 类型为 t_1 \to t_2，那么应该用类型 为 t_1 的参数调用它。求 body 的值时，绑定到变量 var 的值类型为 t_1。
这意味着如下规则：
\infer{(type-of (proc-exp var body) tenv) = t_1 \to t_2} {(type-of body [var=t_1]tenv) = t_2}
这条规则是健壮的：如果 type-of 对 body 做出了正确预测，那么它也能对 (proc-exp var body) 做出正确预测。
只有一个问题：如果我们要计算 proc 表达式的类型，我们怎么找出绑定变量的类型 t_1？它无处可寻。
要解决这个问题，有两种标准设计：
-
类型检查 (Type Checking)：按这种方法，程序员需要指出缺失的绑定变 量类型，类型检查器推断其他表达式的类型，检查它们是否一致。
-
类型推导 (Type Inference)：按这种方法，类型检查器根据程序中变量的 使用，尝试推断 (infer) 绑定变量的类型。如果语言设计得当，类型检查器可以 推断出大多数甚至所有这样的类型。
\textnormal{[}{\star}\textnormal{]} 用本节的规则，像deriv-tree那样，写出 proc (x) x 和 proc (x) (x y) 的类型推导。运用规则，给每个表达式赋予至少两种类型。这些表达式的值类型相 同吗？
7.3 CHECKED：带有类型检查的语言
除了要求程序员写出所有绑定变量的类型之外，我们的新语言和 LETREC 相同。对由 letrec 绑定的变量，我们还要求程序员指定过程结果的类型。
这里是一些 CHECKED 程序例子。
proc (x : int) -(x,1)
letrec
int double (x : int) = if zero?(x)
then 0
else -((double -(x,1)), -2)
in double
proc (f : (bool -> int)) proc (n : int) (f zero?(n))
double 结果的类型为 int，但 double 本身的类型为 (int -> int)， 因为它是一个过程，取一整数，返回一整数。
要定义这种语言的语法，我们改变 proc 和 letrec 表达式的生成式。
\begin{cornertext}[title=修改后的生成式，适用于 CHECKED]\begin{align*}\mathit{Expression} &::= proc (\mathit{Identifier : Type}) \mathit{Expression} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{proc-exp (var ty body)} \\[5pt] \mathit{Expression} &::= letrec \\[-3pt] &\mathrel{\phantom{::=}} \phantom{x}\mathit{Type} \mathit{Identifier} (\mathit{Identifier} : \mathit{Type}) = \mathit{Expression} \\[-3pt] &\mathrel{\phantom{::=}} in \mathit{Expression} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{\begin{math}\begin{alignedat}{-1} &letrec-exp \\ &\phantom{xx}(p-result-type p-name b-var b-var-type \\ &\phantom{xxx}p-body \\ &\phantom{xxx}letrec-body) \end{alignedat}\end{math}}\end{align*}
\end{cornertext}
对指定绑定变量类型的 proc 表达式，规则变为：
\infer{(type-of (proc-exp var t_{var} body) tenv) = t_{var} \to t_{res}} {(type-of body [var=t_{var}]tenv) = t_{res}}
letrec 呢？典型的 letrec 如下：
letrec
t_{res} p (var : t_{var}) = e_{proc\mbox{-}body}
in e_{letrec\mbox{-}body}
该表达式声明一个名为 p 的过程，其形参是类型为 t_{var} 的变量 var，主 体为 e_{proc\mbox{-}body}。因此，p 的类型应为 t_{var} \to t_{res}。
检查 letrec 中的表达式 e_{proc\mbox{-}body} 和 e_{letrec\mbox{-}body} 时，类型环境中的所有变量都必须有正确的类型。我们可以 用定界规则判断当前作用域属于哪些变量，并由此判断变量对应的类型。
e_{letrec\mbox{-}body} 在过程名 p 的作用域内。如上所述，p 的类型声明 为 t_{var} \to t_{res}。因此，检查 e_{letrec\mbox{-}body} 时的类型环境应 为：
tenv_{letrec\mbox{-}body} = \text{[}p=(t_{var} \to t_{res})\text{]}tenv
e_{proc\mbox{-}body} 呢？e_{proc\mbox{-}body} 在变量 p 的作用域内， p 的类型为 t_{var} \to t_{res}；e_{proc\mbox{-}body} 也在变量 var 的作用域内，var 的类型为 t_{var}。因此，e_{proc\mbox{-}body} 的类型环境应为：
tenv_{proc\mbox{-}body} = \text{[}var=t_{var}\text{]}tenv_{letrec\mbox{-}body}
而且，在这个类型环境中，e_{proc\mbox{-}body} 的结果类型应为 t_{res}。
把这些写成一条规则，我们有：
\infer{(type-of\ (letrec-exp t_{res} p (var : t_{var}) =\ e_{proc\mbox{-}body} in e_{letrec\mbox{-}body}) tenv) =\ t} {\begin{gathered} (type-of e_{proc\mbox{-}body} [var=t_{var}][p=(t_{var} \to t_{res})]tenv) = t_{res} \\ (type-of e_{letrec\mbox{-}body} [p=(t_{var} \to t_{res})]tenv) = t \end{gathered}}
7.3.1 检查器
我们需要比较类型是否相等。我们用过程 check-equal-type! 做比较，它比较两个类 型，若二者不等则报错。check-equal-type! 的第三个参数是一表达式，指明类型不 等的位置。
check-equal-type! : \mathit{Type} \times \mathit{Type} \times \mathit{Exp} \to \mathit{Unspecified} (define check-equal-type! (lambda (ty1 ty2 exp) (if (not (equal? ty1 ty2)) (report-unequal-types ty1 ty2 exp)))) report-unequal-types : \mathit{Type} \times \mathit{Type} \times \mathit{Exp} \to \mathit{Unspecified} (define report-unequal-types (lambda (ty1 ty2 exp) (eopl:error 'check-equal-type! "Types didn't match: ~s != ~a in~%~a" (type-to-external-form ty1) (type-to-external-form ty2) exp)))
我们不使用 check-equal-type! 调用的返回值，因此如同定义显式引用操作中的 setref 那样，check-equal-type! 的执行只求效果。
过程 report-unequal-types 用 type-to-external-form，将类型转换为易读的 列表。
type-to-external-form : \mathit{Type} \to \mathit{List} (define type-to-external-form (lambda (ty) (cases type ty (int-type () 'int) (bool-type () 'bool) (proc-type (arg-type result-type) (list (type-to-external-form arg-type) '-> (type-to-external-form result-type))))))
现在，我们可以将规则转换为程序，就像处理表达式中的解释器那样。结果 如–fig-7.3 所示。
\mathit{Tenv} = \mathit{Var} \to \mathit{Type} type-of-program : \mathit{Program} \to \mathit{Type} (define type-of-program (lambda (pgm) (cases program pgm (a-program (exp1) (type-of exp1 (init-tenv)))))) type-of : \mathit{Exp} \times \mathit{Tenv} \to \mathit{Type} (define type-of (lambda (exp tenv) (cases expression exp \fbox{(type-of num tenv) = int} (const-exp (num) (int-type)) \fbox{(type-of var tenv) = tenv(var)} (var-exp (var) (apply-tenv tenv var)) \fbox{\infer{(type-of (diff-exp e_1 e_2) tenv) = int}{(type-of e_1 tenv) = int & (type-of e_2 tenv) = int}} (diff-exp (exp1 exp2) (let ((ty1 (type-of exp1 tenv)) (ty2 (type-of exp2 tenv))) (check-equal-type! ty1 (int-type) exp1) (check-equal-type! ty2 (int-type) exp2) (int-type))) \fbox{\infer{(type-of (zero?-exp e_1) tenv) = bool}{(type-of e_1 tenv) = int}} (zero?-exp (exp1) (let ((ty1 (type-of exp1 tenv))) (check-equal-type! ty1 (int-type) exp1) (bool-type))) \fbox{\infer{(type-of (if-exp e_1 e_2 e_3) tenv) = t}{\begin{gathered}(type-of e_1 tenv) = bool \\ (type-of e_2 tenv) = t \\ (type-of e_3 tenv) = t\end{gathered}}} (if-exp (exp1 exp2 exp3) (let ((ty1 (type-of exp1 tenv)) (ty2 (type-of exp2 tenv)) (ty3 (type-of exp3 tenv))) (check-equal-type! ty1 (bool-type) exp1) (check-equal-type! ty2 ty3 exp) ty2)) \begin{comment} ...))) \end{comment} \smallskip
[!ht]
\fbox{\infer{(type-of (let-exp var e_1 body) tenv) = t_2}{(type-of body [var=t_1]tenv) = t_2 & (type-of e_1 tenv) = t_1}} (let-exp (var exp1 body) (let ((exp1-type (type-of exp1 tenv))) (type-of body (extend-tenv var exp1-type tenv)))) \fbox{\infer{(type-of (proc-exp var t_{var} body) tenv) = (t_{var} \to t_{res})}{(type-of body [var=t_{var}]tenv) = t_res}} (proc-exp (var var-type body) (let ((result-type (type-of body (extend-tenv var var-type tenv)))) (proc-type var-type result-type))) \fbox{\infer{(type-of (call-exp rator rand) tenv) = t_2}{(type-of rator tenv) = (t_1 \to t_2) & (type-of rand tenv) = t_1}} (call-exp (rator rand) (let ((rator-type (type-of rator tenv)) (rand-type (type-of rand tenv))) (cases type rator-type (proc-type (arg-type result-type) (begin (check-equal-type! arg-type rand-type rand) result-type)) (else (report-rator-not-a-proc-type rator-type rator)))))
[!ht]
\smallskip \begin{comment} ((( \end{comment} \fbox{\infer{(type-of\ letrec\ t_{res}\ p\ (var : t_{var})\ =\ e_{proc\mbox{-}body}\ in\ e_{letrec\mbox{-}body}\ tenv)\ =\ t}{\begin{gathered}(type-of e_{proc\mbox{-}body} [var=t_{var}][p =(t_{var} \to t_{res})]tenv) = t_{res} \\ (type-of e_{letrec\mbox{-}body} [p = (t_{var} \to t_{res})]tenv) = t\end{gathered}}} (letrec-exp (p-result-type p-name b-var b-var-type p-body letrec-body) (let ((tenv-for-letrec-body (extend-tenv p-name (proc-type b-var-type p-result-type) tenv))) (let ((p-body-type (type-of p-body (extend-tenv b-var b-var-type tenv-for-letrec-body)))) (check-equal-type! p-body-type p-result-type p-body) (type-of letrec-body tenv-for-letrec-body)))))))
\textnormal{[}{\star}{\star}\textnormal{]} 扩展检查器，处理多声明 let、多参数过程、以及多声明 letrec。你需要添加 形如 t_1 * t_2 * \dots * t_n -> t 的类型来处理多参数过 程。
\textnormal{[}{\star}\textnormal{]} 扩展检查器，处理赋值（IMPLICIT-REFS：隐式引用语言）。
\textnormal{[}{\star}\textnormal{]} 修改检查 if-exp 的代码，若条件不是布尔值，则不检查其他表达式。给出一个表达 式，使新旧两个版本的检查器表现出不同的行为。
\textnormal{[}{\star}{\star}\textnormal{]} 给语言添加类型 pairof。比如，当且仅当一个值是序对，且所含值类型为 t_1 和 t_2 时，其类型为 pairof t_1 * t_2。给语言添加下列生成式：
\begin{align*}\mathit{Type} &::= pairof \mathit{Type} * \mathit{Type} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{pair-type (ty1 ty2)} \\[5pt] \mathit{Expression} &::= pair (\mathit{Expression} , \mathit{Expression}) \\[-3pt] &\mathrel{\phantom{::=}} \fbox{pair-exp (exp1 exp2)} \\[5pt] \mathit{Expression} &::= unpair \mathit{Identifier} \mathit{Identifier} = \mathit{Expression} \\[-3pt] &\mathrel{\phantom{::=}} in \mathit{Expression} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{unpair-exp (var1 var2 exp body)}\end{align*}
pair 表达式生成一个序对，unpair 表达式（同）将两 个变量绑定到表达式的两部分。这些变量的作用域是 body。pair 和 unpair 的判类规则为：
\infer{(type-of (pair-exp e_1 e_2) tenv) = pairof t_1 * t_2} {\begin{gathered} (type-of e_1 tenv) = t_1 \\ (type-of e_2 tenv) = t_2 \\ \end{gathered}}
\infer{(type-of (unpair-exp var_1 var_2 e_1 e_{body}) tenv) = t_{body}} {\begin{gathered} (type-of e_{pair} tenv) = (pairof t_1 t_2) \\ (type-of e_{body} [var_1=t_1][var_2=t_2]tenv) = t_{body} \\ \end{gathered}}
扩展 CHECKED，实现这些规则。在 type-to-external-form 中，用列表 (pairof t_1 t_2) 表示序对。
\textnormal{[}{\star}{\star}\textnormal{]} 给语言添加类型 listof，其操作与 类似。当且仅当值是列表， 且所有元素类型均为 t 时，值类型为 listof t。用下列生成式扩展语言：
\begin{align*}\mathit{Type} &::= listof \mathit{Type} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{list-type (ty)} \\[5pt] \mathit{Expression} &::= list (\mathit{Expression} \{,\mathit{Expression}}\^{*}) \\[-3pt] &\mathrel{\phantom{::=}} \fbox{list-exp (exp1 exps)} \\[5pt] \mathit{Expression} &::= cons (\mathit{Expression} , \mathit{Expression}) \\[-3pt] &\mathrel{\phantom{::=}} \fbox{cons-exp (exp1 exp2)} \\[5pt] \mathit{Expression} &::= null? (\mathit{Expression}) \\[-3pt] &\mathrel{\phantom{::=}} \fbox{null-exp (exp1)} \\[5pt] \mathit{Expression} &::= emptylist_\mathit{Type} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{emptylist-exp (ty)} \\[5pt]\end{align*}
以及四条与类型相关的规则：
\infer{(type-of (list-exp e_1 (e_2 ... e_n)) tenv) = listof t} {\begin{gathered} (type-of e_1 tenv) = t \\ (type-of e_2 tenv) = t \\ \vdots \\ (type-of e_n tenv) = t \end{gathered}}
\infer{(type-of cons(e_1, e_2) tenv) = listof t} {\begin{gathered} (type-of e_1 tenv) = t \\ (type-of e_2 tenv) = listof t \end{gathered}}
\infer{(type-of null?(e_1) tenv) = bool} {(type-of e_1 tenv) = listof t}
(type-of emptylist[t] tenv) = listof t
虽然 cons 和 pair 类似，它们的判类规则却完全不同。
为 car 和 cdr 写出类似的规则，扩展检查器，处理这些和上述表达式。 用 中的小技巧避免与 proc-type-exp 的冲突。这些规则应确 保 car 和 cdr 应用于列表，但它们无法保证列表非空。为什么让规则确保列表 非空不合理？为什么 emptylist 中的类型参数是必需的？
\textnormal{[}{\star}{\star}\textnormal{]} 扩展检查器，处理 EXPLICIT-REFS。你需要这样做：
\textnormal{[}{\star}{\star}\textnormal{]} 扩展检查器，处理 MUTABLE-PAIRS。
7.4 INFERRED：带有类型推导的语言
在程序中写出类型虽然有助于设计和文档，但很耗时。另一种设计是让编译器根据变量的使 用以及程序员可能给出的信息，推断出所有变量的类型。令人惊讶的是，对设计严谨的语言， 编译器总能推断出变量的类型。这种策略叫做类型推导。它适用于 LETREC 这样的语言，也适用于比较大型的语言。
我们从语言 CHECKED 入手研究类型推导的实例。然后，我们修改语言，令所有类型表达式 成为可选项。我们用标记 ? 替代缺失的类型表达式。因此，典型的程序看起来像是：
letrec
? foo (x : ?) = if zero?(x)
then 1
else -(x, (foo -(x,1)))
in foo
每个问号（当然，除了 zero? 结尾那个）指出所在之处有一个待推导的类型。
由于类型表达式是可选的，我们可以用类型替代某些 ?，例如：
letrec
? even (x : int) = if zero?(x) then 1 else (odd -(x,1))
bool odd (x : ?) = if zero?(x) then 0 else (even -(x,1))
in (odd 13)
要定义这种语法，我们新添一个非终结符，\mathit{Optional\mbox{-}type}，并修改 proc 和 letrec 的生成式，令其用可选类型替代类型。
\begin{align*}\mathit{Optinal\mbox{-}Type} &::= ? \\[-3pt] &\mathrel{\phantom{::=}} \fbox{no-type ()} \\[5pt] \mathit{Optinal\mbox{-}Type} &::= \mathit{Type} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{a-type (ty)} \\[5pt] \mathit{Expression} &::= proc (\mathit{Identifier : Optinal\mbox{-}Type}) \mathit{Expression} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{proc-exp (var otype body)} \\[5pt] \mathit{Expression} &::= letrec \\[-3pt] &\mathrel{\phantom{::=}} \phantom{x}\mathit{Optinal\mbox{-}Type} \mathit{Identifier} (\mathit{Identifier} : \mathit{Optinal\mbox{-}Type}) = \mathit{Expression} \\[-3pt] &\mathrel{\phantom{::=}} in \mathit{Expression} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{\begin{math}\begin{alignedat}{-1} &letrec-exp \\ &\phantom{xx}(p-result-otype p-name \\ &\phantom{xxx}b-var b-var-otype p-body \\ &\phantom{xxx}letrec-body) \end{alignedat}\end{math}}\end{align*}
排除的类型就是需要我们找出的类型。要找出它们，我们遍历抽象语法树，生成类型之间的 方程，方程中可能含有这些未知类型。然后，我们求解含有未知类型的方程。
要理解这一流程，我们需要给未知类型起名字。对每个表达式 e 或绑定变量 var， 设 t_e 或 t_{var} 表示表达式或绑定变量的类型。
对表达式抽象语法树中的每个节点，类型规则决定了类型之间必须成立的某些方程。对我们 的 PROC 语言，这些方程是：
\begin{align*}(diff-exp e_1 e_2) &: t_{e_1} = int \\ &\mathrel{\phantom{:}} t_{e_2} = int \\ &\mathrel{\phantom{:}} t_{(diff-exp e_1 e_2)} = int \\[1em] (zero?-exp e_1) &: t_{e_1} = int \\ &\mathrel{\phantom{:}} t_{(zero?-exp e_1)} = bool \\[1em] (if-exp e_1 e_2 e_3) &: t_{e_1} = bool \\ &\mathrel{\phantom{:}} t_{e_2} = t_{(if-exp e_1 e_2 e_3)} \\ &\mathrel{\phantom{:}} t_{e_3} = t_{(if-exp e_1 e_2 e_3)} \\[1em] (proc-exp var body) &: t_{(proc-exp var body)} = (t_{var} \to t_{body}) \\[1em] (call-exp rator rand) &: t_{rator} = (t_{rand} \to t_{(call-exp rator rand)})\end{align*}
-
第一条规则是说，diff-exp 的参数和结果类型均为 int。
-
第二条规则是说，zero?-exp 的参数为 int，结果为 bool。
-
第三条规则是说，if 表达式中的条件类型必须为 bool，两个分支的类 型必须与整个 if 表达式的类型相同。
-
第四条规则是说，proc 表达式的类型是一过程，其参数类型为绑定变量的类 型，其结果类型为主体的类型。
-
第五条规则是说，在过程调用中，操作符类型必须是一过程，其参数类型必须与操 作数相同，其结果类型与整个调用表达式的类型相同。
要推导表达式的类型，我们为所有子表达式和绑定变量分配一个类型变量，给出所有子表达 式的约束条件，然后求解得出的方程。要理解这一流程，我们来推导几个示例表达式的类型。
我们从表达式 proc(f) proc(x) -((f 3),(f x)) 开始。我们首先做一张表，涵盖这 个表达式中的所有绑定变量、proc 表达式、if 表达式和过程调用，并给它们分 别分配一个变量。
|
表达式 |
|
类型变量 |
|
f |
|
t_f |
|
x |
|
t_x |
|
proc(f)proc(x)-((f 3),(f x)) |
|
t_0 |
|
proc(x)-((f 3),(f x)) |
|
t_1 |
|
-((f 3),(f x)) |
|
t_2 |
|
(f 3) |
|
t_3 |
|
(f x) |
|
t_4 |
现在，对每个复杂表达式，都可以根据上述规则写出一个类型方程。
|
表达式 |
|
方程 |
|
proc(f)proc(x)-((f 3),(f x)) |
|
\text{1.\quad}t_0 = t_f \to t_1 |
|
proc(x)-((f 3),(f x)) |
|
\text{2.\quad}t_1 = t_x \to t_2 |
|
-((f 3),(f x)) |
|
\text{3.\quad}t_3 = int |
|
|
\text{4.\quad}t_4 = int |
|
|
|
\text{5.\quad}t_2 = int |
|
|
(f 3) |
|
\text{6.\quad}t_f = int \to t_3 |
|
(f x) |
|
\text{7.\quad}t_f = t_x \to t_4 |
-
方程 1 是说，整个表达式生成一个过程，其参数类型为 t_f，结果类型与 proc(x)-((f 3),(f x)) 相同。
-
方程 2 是说，proc(x)-((f 3),(f x)) 产生一过程，其参数类型为 t_x， 结果类型与 -((f 3),(f x)) 相同。
-
方程 3-5 是说，减法操作 -((f 3),(f x)) 的参数和结果都是整数。
-
方程 6 是说，f 期望的参数类型为 int，返回值类型与 (f 3) 相 同。
-
类似地，方程 7 是说，f 期望的参数类型与 x 相同，返回值类型与 (f x) 相同。
只要满足如下方程，t_f、t_x、t_0、t_1、t_2、t_3 和 t_4 的解可以是任意值：
t_0 = t_f \to t_1
t_1 = t_x \to t_2
t_3 = int
t_4 = int
t_2 = int
t_f = int \to t_3
t_f = t_x \to t_4
我们的目标是找出变量的值，使所有方程成立。我们可以把这样的解表示为一组方程，方程 的左边都是变量。我们称这组方程为一组代换式 (substitution)，称代换式方程 左边的变量绑定 (bound) 于代换式。
我们可以按部就班地求解这些方程。这一过程叫做合一 (unification)。
我们把计算分为两种状态，一种是待求解的方程，一种是已发现的代换式。最开始，所有方 程都待求解，没有一个代换式。
|
|
|
我们依次考虑每个方程。如果方程左边是一个变量，我们将其移到代换式组中。
|
|
|
但是，这样做可能会改变代换式组。例如，下一个方程给出了 t_1 的值。代换式 t_0 右边的值包含 t_1，我们要在其中使用这一信息。所以，我们把代换式右边出 现的每个 t_1 换掉。那么，我们有：
|
|
|
如果方程右边是一变量，我们调换两侧，然后仍照上面操作。我们可以按照这种方式，继续 处理下面的的三个方程。
|
|
|
|
|
|
|
|
|
现在，下一个要处理的方程含有 t_3，已经在代换式组中绑定到 int。所以，我 们用 int 替换方程中的 t_3。方程中的其他类型变量也这样处理。我们称之为对 方程应用 (apply) 代换式。
|
|
|
我们把得到的方程移入代换式组中，并更新需要更新的代换式。
|
|
|
下一个方程，t_f = t_x \to t_4，包含 t_f 和 t_4，均已绑定于代换式，所 以我们对该方程应用代换式，得：
|
|
|
如果方程两边都不是变量，我们可以将其化简，得到两个方程：
|
|
|
我们还是照常处理：像之前那样，对调第一个方程的两侧，加入代换式组，更新代换式组。
|
|
|
|
|
|
没有方程了，所以我们已完成。从这个计算，我们得出结论：原表达式 proc (f) proc (x) -((f 3),(f x)) 的类型应为：
((int \to int) \to (int \to int))
这是合理的：f 的第一个参数必须是一个 int，因为它接受 3 做参数。它 必须生成一个 int，因为它的值用作减法操作的参数。x 也必须是一个 int，因为它也用作 f 的参数。
我们再看另一个例子：proc (f) (f 11)。我们仍从分配类型变量开始。
|
表达式 |
|
类型变量 |
|
f |
|
t_f |
|
proc (f) (f 11) |
|
t_0 |
|
(f 11) |
|
t_1 |
接下来我们写出方程：
|
表达式 |
|
方程 |
|
proc(f)(f 11) |
|
t_0 = t_f \to t_1 |
|
(f 11) |
|
t_f = int \to t_1 |
然后求解：
|
|
|
|
|
|
|
|
|
这意味着可以给 proc (f) (f 11) 赋予类型 (int \to t_1) \to t_1，其 中 t_1 是任何类型。这也是合理的：我们可以推出 f 必须取一 int 参数， 但对 f 结果的类型一无所知。而且，对任何 t_1，这个代码都切实可行，只要 f 取一 int 参数，返回一类型为 t_1 的值。我们称t_1 对它 是多态 (polymorphic) 的。
再来看一个例子。考虑 if x then -(x,1) else 0。我们还是给每个不是常数的子表 达式分配一个类型变量。
|
表达式 |
|
类型变量 |
|
x |
|
t_x |
|
if x then -(x,1) else 0 |
|
t_0 |
|
-(x,1) |
|
t_1 |
然后给出方程：
|
表达式 |
|
方程 |
|
if x then -(x,1) else 0 |
|
t_x = bool |
|
|
t_1 = t_0 |
|
|
|
int = t_0 |
|
|
-(x,1) |
|
t_x = int |
|
|
t_1 = int |
像之前那样处理这些方程，我们有：
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
由于 t_x 已经绑定于代换式组，我们对下一方程应用代换，得：
|
|
|
怎么回事？从这些方程，我们推出 bool = int。所以在这些方程中的解中，均有 bool = int。但 bool 和 int 不可能相等。因此，这些方程无解，也就无 法赋予这个表达式类型。这是合理的，因为表达式 if x then -(x,1) else 0 中， x 同时用作布尔值和整数值，而在我们的类型系统中，这是不允许的。
再来看一个例子。考虑 proc (f) zero?((f f))。我们仍像之前那样处理。
|
表达式 |
|
类型变量 |
|
proc (f) zero?((f f)) |
|
t_0 |
|
f |
|
t_f |
|
zero?((f f)) |
|
t_1 |
|
(f f) |
|
t_2 |
|
表达式 |
|
方程 |
|
proc (f) zero?((f f)) |
|
t_0 = t_f \to t_1 |
|
zero?((f f)) |
|
t_1 = bool |
|
|
t_2 = int |
|
|
(f f) |
|
t_f = t_f \to t_2 |
然后，我们仍像之前那样求解：
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
问题来了。我们推导出 t_f = t_f \to int。但没有一种类型具有这种性质，因 为这个方程的右边总是比左边大：如果 t_f 的语法树包含 k 个节点，那么方程右 边总是包含 k+2 个节点。
所以，如果我们推导的方程形如 tv = t，且类型变量 tv 出现在类型 t 中， 我们只能得出结论：原方程无解。这个附加条件叫做验存 (occurrence check)。
这个条件也意味着我们生成的代换式应满足如下不变式：
\begin{cornertext}[title=无存不变式] 代换式中绑定的变量不应出现在任何代换式的右边。 \end{cornertext}
\textnormal{[}{\star}\textnormal{]} 用本节的方法，推导 中每个表达式的类型，或者判定表达式没有类 型。就像本节的其他练习那样，假设每个绑定变量都有对应的 ?。
\textnormal{[}{\star}\textnormal{]} 写出 let 表达式的类型推导规则。用你的规则，推导下列各表达式的类型，或者判定 表达式无类型。
let x = 4 in (x 3)
let f = proc (z) z in proc (x) -((f x), 1)
let p = zero?(1) in if p then 88 else 99
let p = proc (z) z in if p then 88 else 99
\textnormal{[}{\star}\textnormal{]} 下面的表达式有何问题？
letrec
? even(odd : ?) =
proc (x : ?)
if zero?(x) then 1 else (odd -(x,1))
in letrec
? odd(x : bool) =
if zero?(x) then 0 else ((even odd) -(x,1))
in (odd 13)
\textnormal{[}{\star}{\star}\textnormal{]} 写出 letrec 表达式的类型推导规则。你的规则应能处理多声明的 letrec。用 你的规则推导下列每个表达式的类型，或者判定表达式无类型。
letrec ? f (x : ?)
= if zero?(x) then 0 else -((f -(x,1)), -2)
in f
letrec ? even (x : ?)
= if zero?(x) then 1 else (odd -(x,1))
? odd (x : ?)
= if zero?(x) then 0 else (even -(x,1))
in (odd 13)
letrec ? even (odd : ?)
= proc (x) if zero?(x)
then 1
else (odd -(x,1))
in letrec ? odd (x : ?) =
if zero?(x)
then 0
else ((even odd) -(x,1))
in (odd 13)
\textnormal{[}{\star}{\star}{\star}\textnormal{]} 修改 INFERRED 的语法，排除缺失类型，不再用 ? 做标记。
7.4.1 代换式
我们将类型变量表示为数据类型 type 的新变体。这里用到的技术和实现词法地址中 处理词法地址的相同。我们给语法添加生成式：
\begin{align*}\mathit{Type} &::= %tvar-type \ \mathit{Number} \\[-3pt] &\mathrel{\phantom{::=}} \fbox{tvar-type (serial-number)}\end{align*}
我们把这些扩展后的类型称为类型表达式 (type expression)。 类型表达式的基本操作是用类型代换类型变量，由 apply-one-subst 定义。(apply-one-subst t_0 tv t_1) 将 t_0 中出现的每个tv 代换为 t_1，返回代换后的表达式。有时，这写作 t_0[tv=t_1]。
apply-one-subst : \mathit{Type} \times \mathit{Tvar} \times \mathit{Type} \to \mathit{Type} (define apply-one-subst (lambda (ty0 tvar ty1) (cases type ty0 (int-type () (int-type)) (bool-type () (bool-type)) (proc-type (arg-type result-type) (proc-type (apply-one-subst arg-type tvar ty1) (apply-one-subst result-type tvar ty1))) (tvar-type (sn) (if (equal? ty0 tvar) ty1 ty0)))))
这个过程用来代换单个类型变量。它不能像上节中描述的那样处理所有代换。
代换式组是一个方程列表，方程两边分别为类型变量和类型。该列表也可视为类型变量到类 型的函数。当且仅当类型变量出现于代换式组中某个方程的左侧时，我们说该变量绑 定于代换式。
我们用序对 (类型变量 . 类型) 的列表表示代换式组。代换式组的必要观测器是 apply-subst-to-type。它遍历类型 t，把每个类型变量替换为代换式组 \sigma 中的绑定。如果一个变量未绑定于代换式，那么保持不变。我们用 t\sigma 表示得到的类型。
这一实现用 Scheme 过程 assoc 在代换式组中查找类型变量。若给定类型是列表中某 个序对的首项，assoc 返回对应的（类型变量，类型）序对，否则返回 #f。我 们将它写出来：
apply-subst-to-type : \mathit{Type} \times \mathit{Subst} \to \mathit{Type} (define apply-subst-to-type (lambda (ty subst) (cases type ty (int-type () (int-type)) (bool-type () (bool-type)) (proc-type (t1 t2) (proc-type (apply-subst-to-type t1 subst) (apply-subst-to-type t2 subst))) (tvar-type (sn) (let ((tmp (assoc ty subst))) (if tmp (cdr tmp) ty))))))
代换式组的构造器有 empty-subst 和 extend-subst。(empty-subst) 生 成空代换式组的表示。(extend-subst \sigma tv t) 取一代换式组 \sigma，像上节那样给它添加方程 tv = t。这个操作分两步：首先把代换式组中 所有方程右边的 tv 替换为 t，然后把方程 tv = t 添加到列表中。用公式表 示为：
\begin{pmatrix} tv_1 = t_1 \\ \vdots \\ tv_n = t_n \end{pmatrix}[tv = t] = \begin{pmatrix} tv = t \\ tv_1 = t_1[tv = t] \\ \vdots \\ tv_n = t_n[tv = t] \end{pmatrix}
该定义具有如下性质：对任意类型 t，
(t\sigma)[tv = t{}’] = t(\sigma[tv = t{}’])
extend-subst 的实现依照上式。它把 \sigma_0 所有绑定中的 t_0 代换为 tv_0。
empty-subst : \mathit{()} \to \mathit{Subst} (define empty-subst (lambda () '())) extend-subst : \mathit{Subst} \times \mathit{Tvar} \times \mathit{Type} \to \mathit{Subst} 用法 : tvar 尚未绑定于 subst。 (define extend-subst (lambda (subst tvar ty) (cons (cons tvar ty) (map (lambda (p) (let ((oldlhs (car p)) (oldrhs (cdr p))) (cons oldlhs (apply-one-subst oldrhs tvar ty)))) subst))))
这一实现保持无存不变式，但既不依赖它，也不强制它。那是下一节中合一器的工作。
\textnormal{[}{\star}{\star}\textnormal{]} 在我们的实现中，当 \sigma 很大时，extend-subst 要做大量工作。实现另一种 表示，则 extend-subst 变成：
(define extend-subst (lambda (subst tvar ty) (cons (cons tvar ty) subst))) 其余工作移至 apply-subst-to-type，而性质 t(\sigma[tv = t{}’]) = (t\sigma)[tv = t{}’] 仍然满足。这样定义 extend-subst 还需要无存不变式吗？
\textnormal{[}{\star}{\star}\textnormal{]} 修改前一道练习中的实现，则对任意类型变量，apply-subst-to-type 最多只需计算 一次代换。
7.4.2 合一器
合一器的主要过程是 unifier。合一器执行上述推导流程中的这一的步骤：取两个类 型 t_1 和 t_2，满足无存不变式的代换式组 \sigma，以及表达式 exp，将 t_1 = t_2 添加到 \sigma，返回得到的代换式组。这是合并 t_1\sigma 和 t_2\sigma 后所得的最小 \sigma 扩展。这组代换式仍满足无 存不变式。若添加 t_1 = t_2 导致矛盾，或者违反了无存不变式，那么合一器报错， 指出错误所在的表达式 exp。这通常是得出方程 t_1 = t_2 的表达式。
这个算法用 cases 来写十分不便，所以我们改用类型的谓词和提取器。算法 如 所示，其流程如下：
-
首先，像上面那样，我们对类型 t_1 和 t_2 分别应用代换式。
-
如果结果类型相同，我们立即返回。这一步对应上面的删除简单方程。
-
如果 ty1 为未知类型，那么无存不变式告诉我们，它未绑定于代换式。由于 它未绑定，我们尝试把 t_1 = t_2 添加到代换式组。但我们要验存，以保证无存不变 式成立。当且仅当类型变量 tv 不在 t 中时，调用 (no-occurrence? tv t) 返回 #t（）。
-
如果 t_2 为未知类型，则对调 t_1 和 t_2，也照这样处理。
-
如果 t_1 和 t_2 都不是类型变量，那么我们再做进一步分析。
如果它们都是 proc 类型，那么我们化简方程，在两个参数类型之间建立方程，得到 一组代换式，然后用这组代换式在结果类型之间建立方程。
否则，t_1 和 t_2 中一个是 int，另一个是 bool，或一个是 proc，另一个是 int 或 bool。不管是哪种情况，方程都无解，引发报错。
从另一种角度来思考这些有助于理解。代换式组是一个存储器，未知类型是指向存 储器中某位置的引用。unifier 把 ty1 = ty2 添加到存储器中，得到一 个新的存储器。
\textnormal{[}{\star}\textnormal{]} 我们说：“如果ty1为未知类型，那么无存不变式告诉我们，它未绑定 于代换式。”详细解释为什么如此。
\textnormal{[}{\star}{\star}\textnormal{]} 修改合一器，不是对合一器的实参，而是只对类型变量调用 apply- subst-to-type。
\textnormal{[}{\star}{\star}\textnormal{]} 我们说代换式组就像存储器。用 中的代换式组表示实现合一器，用 全局 Scheme 变量记录代换式组，就像 和 fig-4.2 那 样。
\textnormal{[}{\star}{\star}\textnormal{]} 优化前一道练习的实现，在常数时间内获取类型变量的绑定。
[!t]
unifier : \mathit{Type} \times \mathit{Type} \times \mathit{Subst} \times \mathit{Exp} \to \mathit{Subst} (define unifier (lambda (ty1 ty2 subst exp) (let ((ty1 (apply-subst-to-type ty1 subst)) (ty2 (apply-subst-to-type ty2 subst))) (cond ((equal? ty1 ty2) subst) ((tvar-type? ty1) (if (no-occurrence? ty1 ty2) (extend-subst subst ty1 ty2) (report-no-occurrence-violation ty1 ty2 exp))) ((tvar-type? ty2) (if (no-occurrence? ty2 ty1) (extend-subst subst ty2 ty1) (report-no-occurrence-violation ty2 ty1 exp))) ((and (proc-type? ty1) (proc-type? ty2)) (let ((subst (unifier (proc-type->arg-type ty1) (proc-type->arg-type ty2) subst exp))) (let ((subst (unifier (proc-type->result-type ty1) (proc-type->result-type ty2) subst exp))) subst))) (else (report-unification-failure ty1 ty2 exp))))))
no-occurrence? : \mathit{Tvar} \times \mathit{Type} \to \mathit{Bool} (define no-occurrence? (lambda (tvar ty) (cases type ty (int-type () #t) (bool-type () #t) (proc-type (arg-type result-type) (and (no-occurrence? tvar arg-type) (no-occurrence? tvar result-type))) (tvar-type (serial-number) (not (equal? tvar ty))))))
7.4.3 找出表达式的类型
我们用 otype->type 为每个 ? 定义一个新类型变量，把可选类型转换为未知类 型。
otype->type : \mathit{OptionalType} \to \mathit{Type} (define otype->type (lambda (otype) (cases optional-type otype (no-type () (fresh-tvar-type)) (a-type (ty) ty)))) fresh-tvar-type : \mathit{()} \to \mathit{Type} (define fresh-tvar-type (let ((sn 0)) (lambda () (set! sn (+ sn 1)) (tvar-type sn))))
把类型转换为外在表示时，我们用包含序号的符号表示类型变量。
type-to-external-form : \mathit{Type} \to \mathit{List} (define type-to-external-form (lambda (ty) (cases type ty (int-type () 'int) (bool-type () 'bool) (proc-type (arg-type result-type) (list (type-to-external-form arg-type) '-> (type-to-external-form result-type))) (tvar-type (serial-number) (string->symbol (string-append "ty" (number->string serial-number)))))))
现在我们可以写 type-of 了。它取一表达式，一个将程序变量映射到类型表达式的类 型环境，和一个满足无存不变式的代换式组，返回一个类型和满足无存不变式的新代换式组。
类型环境将各类型表达式与程序变量对应起来。代换式组解释了类型表达式中每个类型变量 的含义。我们把代换式组比作存储器，把类型变量比作存储器引用。因此， type-of 返回两个值：一个类型表达式，和一个解释表达式中类型变量的代换式组。 像 那样，我们在实现时新定义一种包含两个值的数据类型，用作返 回值。
type-of 的定义如–fig-7.8 所示。对每个表达式， 我们递归处理子表达式，一路传递代换式组参数中现有的解。然后，我们根据规范，为当前 表达式建立方程，调用 unifier，在代换式组中记录这些。
\mathit{Answer} = \mathit{Type} \to \mathit{Subst} (define-datatype answer answer? (an-answer (ty type?) (subst substitution?))) type-of-program : \mathit{Program} \to \mathit{Type} (define type-of-program (lambda (pgm) (cases program pgm (a-program (exp1) (cases answer (type-of exp1 (init-tenv) (empty-subst)) (an-answer (ty subst) (apply-subst-to-type ty subst))))))) type-of : \mathit{Exp} \times \mathit{Tenv} \times \mathit{Subst} \to \mathit{Answer} (define type-of (lambda (exp tenv subst) (cases expression exp (const-exp (num) (an-answer (int-type) subst)) \fbox{\begin{math}\begin{alignedat}{-1}(zero?-exp e_1) &: t_{e_1} = int \\ &\mathrel{\phantom{:}} t_{(zero?-exp e_1)} = bool\end{alignedat}\end{math}} (zero?-exp (exp1) (cases answer (type-of exp1 tenv subst) (an-answer (ty1 subst1) (let ((subst2 (unifier ty1 (int-type) subst1 exp))) (an-answer (bool-type) subst2))))) \begin{comment} ...))) \end{comment} \smallskip
\fbox{\begin{math}\begin{alignedat}{-1}(diff-exp e_1 e_2) &: t_{e_1} = int \\ &\mathrel{\phantom{:}} t_{e_2} = int \\ &\mathrel{\phantom{:}} t_{(diff-exp e_1 e_2)} = int\end{alignedat}\end{math}} (diff-exp (exp1 exp2) (cases answer (type-of exp1 tenv subst) (an-answer (ty1 subst1) (let ((subst1 (unifier ty1 (int-type) subst1 exp1))) (cases answer (type-of exp2 tenv subst1) (an-answer (ty2 subst2) (let ((subst2 (unifier ty2 (int-type) subst2 exp2))) (an-answer (int-type) subst2)))))))) \fbox{\begin{math}\begin{alignedat}{-1}(if-exp e_1 e_2 e_3) &: t_{e_1} = bool \\ &\mathrel{\phantom{:}} t_{e_2} = t_{(if-exp e_1 e_2 e_3)} \\ &\mathrel{\phantom{:}} t_{e_3} = t_{(if-exp e_1 e_2 e_3)}\end{alignedat}\end{math}} (if-exp (exp1 exp2 exp3) (cases answer (type-of exp1 tenv subst) (an-answer (ty1 subst) (let ((subst (unifier ty1 (bool-type) subst exp1))) (cases answer (type-of exp2 tenv subst) (an-answer (ty2 subst) (cases answer (type-of exp3 tenv subst) (an-answer (ty3 subst) (let ((subst (unifier ty2 ty3 subst exp))) (an-answer ty2 subst)))))))))) (var-exp (var) (an-answer (apply-tenv tenv var) subst)) (let-exp (var exp1 body) (cases answer (type-of exp1 tenv subst) (an-answer (exp1-type subst) (type-of body (extend-tenv var exp1-type tenv) subst))))
[!ht]
\fbox{(proc-exp var body) : t_{(proc-exp var body)} = (tvar \to t_{body})} (proc-exp (var otype body) (let ((var-type (otype->type otype))) (cases answer (type-of body (extend-tenv var var-type tenv) subst) (an-answer (body-type subst) (an-answer (proc-type var-type body-type) subst))))) \fbox{(call-exp rator rand) : t_{rator} = (t_{rand} \to t_{(call-exp rator rand)})} (call-exp (rator rand) (let ((result-type (fresh-tvar-type))) (cases answer (type-of rator tenv subst) (an-answer (rator-type subst) (cases answer (type-of rand tenv subst) (an-answer (rand-type subst) (let ((subst (unifier rator-type (proc-type rand-type result-type) subst exp))) (an-answer result-type subst))))))))
[!ht]
\fbox{\begin{math}\begin{alignedat}{-1}&letrec t_{proc\mbox{-}result} p (var : t_{var}) = e_{proc\mbox{-}body} in e_{letrec\mbox{-}body} : \\ &\phantom{xx}t_{p} = t_{var} \to t_{e_{proc\mbox{-}body}} \\ &\phantom{xx}t_{e_{letrec\mbox{-}body}} = t_{letrec t_{proc\mbox{-}result} p (var : t_{var}) = e_{proc\mbox{-}body} in e_{letrec\mbox{-}body}}\end{alignedat}\end{math}} \smallskip \begin{comment} (((... \end{comment} (letrec-exp (p-result-otype p-name b-var b-var-otype p-body letrec-body) (let ((p-result-type (otype->type p-result-otype)) (p-var-type (otype->type b-var-otype))) (let ((tenv-for-letrec-body (extend-tenv p-name (proc-type p-var-type p-result-type) tenv))) (cases answer (type-of p-body (extend-tenv b-var p-var-type tenv-for-letrec-body) subst) (an-answer (p-body-type subst) (let ((subst (unifier p-body-type p-result-type subst p-body))) (type-of letrec-body tenv-for-letrec-body subst))))))))))
因为多态的缘故，测试推导器比测试之前的解释器稍微麻烦。例如，如果给推导器输入 proc (x) x，它给出的外在表示可能是 (tvar1 -> tvar1)、(tvar2 -> tvar2) 或 (tvar3 -> tvar3)，等等。每次调用推导器结果都可能不同，所以我们写 测试项时不能直接使用它们，否则就无法比较推导出的类型和正确类型。我们需要接受上述 所有可能，但拒绝 (tvar3 -> tvar4) 或是 (int -> tvar17)。
要比较两种类型的外在表示，我们统一未知类型的名字，遍历每个外在表示，给类型变量重 新编号，使之从 ty1 开始。然后，我们就能用 equal? 比较重新编号的类型 （–fig-7.11）。
要逐个命名所有未知变量，我们用 canonical-subst 生成代换式组。我们用 table做累加器，即可直接递归。table 的长度告诉我们已找出多少个不同的未 知类型，我们可以用其长度给“下一个”ty符号编号。 这和我们在 中使用的 length 类似。
[!ht]
\mathit{TvarTypeSym} = 含有数字的符号 \mathit{A\mbox{-}list} = \mathit{Listof(Pair(TvarTypeSym,TvarTypeSym))} equal-up-to-gensyms? : \mathit{S\mbox{-}exp} \times \mathit{S\mbox{-}exp} \to \mathit{Bool} (define equal-up-to-gensyms? (lambda (sexp1 sexp2) (equal? (apply-subst-to-sexp (canonical-subst sexp1) sexp1) (apply-subst-to-sexp (canonical-subst sexp2) sexp2)))) canonical-subst : \mathit{S\mbox{-}exp} \to \mathit{A\mbox{-}list} (define canonical-subst (lambda (sexp) loop : S-exp × A-list → A-list (let loop ((sexp sexp) (table '())) (cond ((null? sexp) table) ((tvar-type-sym? sexp) (cond ((assq sexp table) table) (else (cons (cons sexp (ctr->ty (length table))) table)))) ((pair? sexp) (loop (cdr sexp) (loop (car sexp) table))) (else table)))))
[!ht]
tvar-type-sym? : \mathit{Sym} \to \mathit{Bool} (define tvar-type-sym? (lambda (sym) (and (symbol? sym) (char-numeric? (car (reverse (symbol->list sym))))))) symbol->list : \mathit{Sym} \to \mathit{List} (define symbol->list (lambda (x) (string->list (symbol->string x)))) apply-subst-to-sexp : \mathit{A\mbox{-}list} \times \mathit{S\mbox{-}exp} \to \mathit{S\mbox{-}exp} (define apply-subst-to-sexp (lambda (subst sexp) (cond ((null? sexp) sexp) ((tvar-type-sym? sexp) (cdr (assq sexp subst))) ((pair? sexp) (cons (apply-subst-to-sexp subst (car sexp)) (apply-subst-to-sexp subst (cdr sexp)))) (else sexp)))) ctr->ty : \mathit{N} \to \mathit{Sym} (define ctr->ty (lambda (n) (string->symbol (string-append "tvar" (number->string n)))))
\textnormal{[}{\star}{\star}\textnormal{]} 扩展推导器，像 那样处理序对类型。
\textnormal{[}{\star}{\star}\textnormal{]} 扩展推导器，处理多声明 let、多参数过程和多声明 letrec。
\textnormal{[}{\star}{\star}\textnormal{]} 扩展推导器，像 那样处理列表类型。修改语言，用生成式 \mathit{Expression} ::= emptylist 代替 \mathit{Expression} ::= emptylist_\mathit{Type} 提示：考虑用类型变量代替缺失的 _t。
\textnormal{[}{\star}{\star}\textnormal{]} 扩展推导器，像 那样处理 EXPLICIT-REFS。
\textnormal{[}{\star}{\star}\textnormal{]} 重写推导器，将其分为两步。第一步生成一系列方程，第二步重复调用 unify 求解它 们。
\textnormal{[}{\star}{\star}\textnormal{]} 我们的推导器虽很有用，却不够强大，不允许程序员定义多态过程，像定义多态原语 pair 或 cons 那样，适用于多种类型。例如，即使执行是安全的，我们的推导 器也会拒绝程序
let f = proc (x : ?) x
in if (f zero?(0))
then (f 11)
else (f 22)
因为 f 既是 (bool -> bool) 也是 (int -> int)。由于本节的推导器至 多只能找出 f 的一种类型，它将拒绝这段程序。
更实际的例子是这样的程序
letrec
? map (f : ?) =
letrec
? foo (x : ?) = if null?(x)
then emptylist
else cons((f car(x)),
(foo cdr(x)))
in foo
in letrec
? even (y : ?) = if zero?(y)
then zero?(0)
else if zero?(-(y,1))
then zero?(1)
else (even -(y,2))
in pair(((map proc(x : int) -(x,1))
cons(3,cons(5,emptylist))),
((map even)
cons(3,cons(5,emptylist))))
这个表达式用了两次 map，一次产生 int 列表，一次产生 bool 列表。因 此，两次使用它需要两个不同的类型。由于本节的推导器至多只能找出 map 的一种类 型，它检测到 int 和 bool 冲突，拒绝程序。
避免这个问题的一种方法是只允许 let 引入多态，然后在类型检查时区分 (let-exp var e_1 e_2) 和 (call-exp (proc-exp var e_2) e_1)。
给推导器添加多态绑定，处理表达式 (let-exp var e_1 e_2) 时，把 e_2 中自由出现的每个 var 代换为 e_1。那么，在推导器看来，let 主 体中有多个不同的 e_1 副本，它们可以有不同的类型，上述程序就能通过。
\textnormal{[}{\star}{\star}{\star}\textnormal{]} 前一道练习指出的类型推导算法会多次分析e_1，每次对应 e_2 中出现的一个 e_1。实现 Milner 的 W 算法，只需分析 e_1 一次。
\textnormal{[}{\star}{\star}{\star}\textnormal{]} 多态和副作用之间的相互作用很微妙。考虑以下文开头的一段程序
let p = newref(proc (x : ?) x)
in ...