Types and Programming Languages习题的参考解答及思考（第14章）
第14章
章节14.1
练习14.1.1
题目：
Wouldn’t it be simpler just to require the programmer to annotate error with its intended type in each context where it is used?
解答：
求值规则E-APPERR1、E-APPERR2使得错误可以从底层传播到上层，而不同位置的\( \text{error} \)可能需要不同的类型，如果一开始由程序员标注预期的类型，则向上传播到某个点后，可能就需要不同的类型了，然而标注的类型是固定的，不会随错误传播过程改变，进而可能和实际需要的类型不符，违反了PRESERVATION定理。
举个例子（注：我们用\( \text{error as T} \)来标注\( \text{error} \)的类型）：
\[ \text{t} = (\lambda \text{x}: \text{Nat. } \text{x}) \text{ } ((\lambda \text{y}: \text{Bool. } 1) \text{ } (\text{error as Bool})) \]
上面\( \text{t} \)是类型良好的，但\( \text{t} \)单步求值会得到：
\[ \text{t}' = (\lambda \text{x}: \text{Nat. } \text{x}) \text{ } (\text{error as Bool}) \]
这里单步求值得到的\( \text{t}' \)非类型良好的，违反了PRESERVATION定理。
而使用类型规则T-ERROR则没有这个问题，类型检查器可以按需决定\( \text{error} \)是什么类型。
章节14.3
练习14.3.1
题目：
The explanation of extensible variant types in alternative 4 above is rather informal. Show how to make it precise.
解答：
我们将异常类型\( \text{T}_{\text{exn}} \)看成类似可拓展variant的东西，书中对此已经给出了一个很直观的解释了，这里不再说明为什么\( \text{T}_{\text{exn}} \) 类似可拓展variant等等问题，下面重点将放在形式化上。
我们在图14-3的基础上修改，引入用户自定义异常。
我们首先引入声明异常的语法，由于我们系统目前没有top-level的概念，故我们选择让新引入的异常具有树形的作用域，如下：
\[ \text{exception } \text{l} \text{ of } \text{T}: \text{t} \]
上面语法表示引入标签为\( \text{l} \)的新异常，该类异常携带类型为\( \text{T} \)的值作为异常信息，且该新异常的作用域限定在\( \text{t} \)中，只有在\( \text{t} \)中才能引用该异常。
对应的，抛出异常的\( \text{raise} \)语句的语法也得修改，不仅得给出异常信息，还得给出异常标签（或者说异常类型），如下：
\[ \text{raise } \text{l}(\text{t}) \]
同理，处理异常的\( \text{try} \)语句的语法也得修改，得声明它能处理的异常标签，不仅如此，由于异常是带信息的，故还需要一个变量绑定到对应的异常信息，如下：
\[ \text{try } \text{t} \text{ with } \text{l}(\text{x}) \Rightarrow \text{t} \]
后半部分的\( \text{l}(\text{x}) \Rightarrow \text{t} \)的意思是：我们希望处理异常标签为\( \text{l} \)的异常，如果异常标签匹配，则请把异常信息值绑定到变量\( \text{x} \)上，然后执行\( \text{t} \)，否则，请继续向上抛异常。
由于异常类型是可拓展的，在不同位置\( \text{T}_{\text{exn}} \)可能具体不同的异常标签以及对应的异常信息类型，故用户不方便用\( \text{as} \)对异常类型进行标注，但我们需要有办法知道当前位置哪些异常标签是合法的，以及该异常标签对应的异常信息类型是什么，为此，我们引入一个类似类型上下文的机制，专门用于记录当前的异常类型，我们称它为异常类型上下文， 简称异常上下文 ，用符号\( \psi \)来表示，其形式类似variant，如\( \psi = \langle \text{l}_1: \text{T}_1, \text{l}_2: \text{T}_2, \dots, \text{l}_n: \text{T}_n \rangle \)，其中\( \forall 1 \leq i \leq n, \text{l}_i \)为异常标签，\( \text{T}_i \)则是对应的异常信息类型。
初始的时候，异常上下文为空，记为\( \psi = \empty \)，然后每当遇到\( \text{exception } \text{l} \text{ of } \text{T}: \text{t} \)的时候，拓展当前异常上下文以记录新声明的异常，假设当前异常上下文\( \psi = \langle \text{l}_1: \text{T}_1, \text{l}_2: \text{T}_2, \dots, \text{l}_n: \text{T}_n \rangle \)，则拓展后\( \psi \)变成\( \psi' = \langle \text{l}_1: \text{T}_1, \text{l}_2: \text{T}_2, \dots, \text{l}_n: \text{T}_n, \text{l}: \text{T} \rangle \)，拓展异常上下文的操作很普遍，我们用\( \langle \dots \psi, \text{l}: \text{T} \rangle \)来表示新异常上下文\( \psi' \)，它满足\( dom(\psi') = dom(\psi) \cup \{ \text{l} \}, \quad \forall 1 \leq i \leq n, \psi'(\text{l}_i) = \psi(\text{l}_i), \quad \psi'(\text{l}) = \text{T} \)。
注：我们始终假设新声明异常的标签和当前异常上下文中的任何标签都不一样。
引入异常上下文后，类型关系就得从三元关系\( \Gamma \vdash \text{t}: \text{T} \)变成四元关系\( \psi \mid \Gamma \vdash \text{t}: \text{T} \)了。类似我们当时拓展类型关系以加入类型上下文，大部分类型规则都很容易改成四元关系，但是涉及异常的语句都得注意下，首先是引入异常的\( \text{exception } \text{l} \text{ of } \text{T}: \text{t} \)，它声明了新异常，需要拓展当前异常上下文，对应的类型规则如下：
\[ \dfrac{\text{l} \notin dom(\psi) \quad \langle \dots \psi, \text{l}: \text{T}_1 \rangle \mid \Gamma \vdash \text{t}_1: \text{T}}{ \psi \mid \Gamma \vdash \text{exception } \text{l} \text{ of } \text{T}_1: \text{t}_1: \text{T}} \qquad (\text{T-EXTEND-EXN}) \]
接着是\( \text{raise } \text{l}(\text{t}) \)对应的类型规则，如下：
\[ \dfrac{\text{l} \in dom(\psi) \quad \psi \mid \Gamma \vdash \text{t}_1: \psi(\text{l})}{ \psi \mid \Gamma \vdash \text{raise } \text{l}(\text{t}_1): \text{T}} \qquad (\text{T-EXN}) \]
上述类型规则限制了两点：
- \( \text{l} \)必须是当前位置合法的异常标签，即\( \text{l} \in dom(\psi) \)。
- 异常信息\( \text{t}_1 \)的类型必须是异常标签\( \text{l} \)对应异常信息类型，不能是随意的类型，即\( \psi \mid \Gamma \vdash \text{t}_1: \psi(\text{l}) \)。
\( \text{try } \text{t} \text{ with } \text{l}(\text{x}) \Rightarrow \text{t} \)的类型规则也比较简单，首先得检查\( \text{l} \)是当前位置合法的异常标签，\( \text{x} \)的类型则从异常上下文中取，加到当前类型上下文中去，处理方法类似\( \lambda \)-抽象的变量，如下：
\[ \dfrac{\psi \mid \Gamma \vdash \text{t}_1: \text{T} \quad \text{l} \in dom(\psi) \quad \psi \mid \Gamma, \text{x}: \psi(\text{l}) \vdash \text{t}_2: \text{T}}{ \psi \mid \Gamma \vdash \text{try } \text{t}_1 \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2: \text{T}} \qquad (\text{T-TRY}) \]
上述类似规则还限制了\( \text{t}_1, \text{t}_2 \)具有相同的类型，即不管发不发生异常，求值得到的值的类型都得一致。
类型规则就这样了，接下来是求值规则。
首先是\( \text{exception } \text{l} \text{ of } \text{T}: \text{t} \)的求值规则，如下：
\[ \begin{aligned} \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \text{exception } \text{l} \text{ of } \text{T}_1: \text{t}_1 \rightarrow \text{exception } \text{l} \text{ of } \text{T}_1: \text{t}'_1} &\qquad (\text{E-EXTEND-EXN}) \\ \text{exception } \text{l} \text{ of } \text{T}_1: \text{v}_1 \rightarrow \text{v}_1 &\qquad (\text{E-EXTEND-EXNV}) \end{aligned} \]
上面两个求值规则没什么好说的，但是还得额外考虑一个情况，如果\( \text{t}_1 = \text{raise } \text{l}_1(\text{v}_1) \)怎么办，读者容易想到，继续向上抛异常就完事了，确实，如果\( \text{}_1 \neq \text{l} \)，则我们就应该继续向上抛异常，但是如果\( \text{l}_1 = \text{l} \)怎么办？不能再往上抛异常标签为\( \text{l}_1 \)的异常了，因为往上已经超出异常标签\( \text{l}_1 \)的作用域范围了（注：记得我们始终假设新声明异常的标签和当前异常上下文中的任何标签都不一样吗），这种情况属于未处理的异常，我们这样处理：
- 加入类型\( \text{Unit} \)以及对应的项\( \text{unit} \)。
- 初始的时候，异常上下文不为空，而是\( \psi = \langle \text{u}: \text{Unit} \rangle \)，这里异常标签\( \text{u} \)代表未处理异常（unhandled exception），对应的异常信息类型则为\( \text{Unit} \)，可以选其他类型，比如\( \text{String} \)，用于以字符串的形式记录未处理异常的异常标签等信息，不过我们这里就简单处理，选择\( \text{Unit} \)作为异常信息类型，相当于没有额外的异常信息。
- 让\( \text{exception } \text{l} \text{ of } \text{T}_1: \text{raise } \text{l}_1(\text{v}_1) \)求值成\( \text{raise } \text{u}(\text{unit}) \)。
综上，需要额外增加两个求值规则，如下：
\[ \begin{aligned} \dfrac{\text{l}_1 = \text{l}}{\text{exception } \text{l} \text{ of } \text{T}_1: \text{raise } \text{l}_1(\text{v}_1) \rightarrow \text{raise } \text{u}(\text{unit})} &\qquad (\text{E-EXTEND-EXN-UNHANDLED-EXN}) \\ \dfrac{\text{l}_1 \neq \text{l}}{\text{exception } \text{l} \text{ of } \text{T}_1: \text{raise } \text{l}_1(\text{v}_1) \rightarrow \text{raise } \text{l}_1(\text{v}_1)} &\qquad (\text{E-EXTEND-EXN-CONTINUE-RAISE}) \end{aligned} \]
接着是\( \text{raise } \text{l}(\text{t}) \)对应的求值规则，如下：
\[ \begin{aligned} (\text{raise } \text{l}(\text{v}_1)) \text{ } \text{t}_2 \rightarrow \text{raise } \text{l}(\text{v}_1) &\qquad (\text{E-APPRAISE1}) \\ \text{v}_1 \text{ } (\text{raise } \text{l}(\text{v}_2)) \rightarrow \text{raise } \text{l}(\text{v}_2) &\qquad (\text{E-APPRAISE2}) \\ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{\text{raise } \text{l}(\text{t}_1) \rightarrow \text{raise } \text{l}(\text{t}'_1)} &\qquad (\text{E-RAISE}) \\ \text{raise } \text{l}_2(\text{raise } \text{l}_1(\text{v}_1)) \rightarrow \text{raise } \text{l}_1(\text{v}_1) &\qquad (\text{E-RAISERAISE}) \end{aligned} \]
这几个规则和原本的类似，没什么好说的。
最后是\( \text{try } \text{t} \text{ with } \text{l}(\text{x}) \Rightarrow \text{t} \)的求值规则，如下：
\[ \begin{aligned} \text{try } \text{v}_1 \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2 \rightarrow \text{v}_1 &\qquad (\text{E-TRYV}) \\ \dfrac{\text{l}_1 = \text{l}}{\text{try } \text{raise } \text{l}_1(\text{v}_1) \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2 \rightarrow [\text{x} \mapsto \text{v}_1]\text{t}_2} &\qquad (\text{E-TRYRAISE-MATCH}) \\ \dfrac{\text{l}_1 \neq \text{l}}{\text{try } \text{raise } \text{l}_1(\text{v}_1) \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2 \rightarrow \text{raise } \text{l}_1(\text{v}_1)} &\qquad (\text{E-TRYRAISE-MISMATCH}) \\ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{\text{try } \text{t}_1 \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2 \rightarrow \text{try } \text{t}'_1 \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2} &\qquad (\text{E-TRY}) \end{aligned} \]
E-TRYV和E-TRY没什么好说的，E-TRYRAISE-MATCH和E-TRYRAISE-MISMATCH则分别处理异常标签匹配和不匹配的情况，不匹配就继续向上抛出异常，匹配就执行异常处理语句\( \text{t}_2 \)，不过由于\( \text{t}_2 \)中会用变量\( \text{x} \)去引用异常信息，故我们需要对\( \text{t}_2 \)进行变量代入，将\( \text{x} \)替换成异常信息值\( \text{v}_1 \)，注意这里没有选择求值成\( (\lambda \text{x}: \text{T}_1 \dots) \text{ } \text{v}_1 \)是因为我们在运行时不知道异常标签对应的异常信息类型\( \text{T}_1 \)，语法上没有做标注，另一种处理方法就是求值成\( (\lambda \text{x}: \text{T}_{\text{exn}} \text{. } \text{t}_2) \text{ } \text{v}_1 \)，这里\( \text{T}_{\text{exn}} \)非真实类型，而只是代表异常类型的标记符号而已，在此基础上，需要再为\( \lambda \text{x}: \text{T}_{\text{exn}} \text{. } \text{t}_2 \)添加对应的语法、类型规则、求值规则等。由于类型规则中可以访问到\( \psi \)，就绕开了不知道异常标签对应的异常信息类型的限制了。
总结下所有的语法、值、类型、求值规则、类型规则：
语法：
\[ \begin{aligned} \text{t} ::= &\text{ } \\ &\text{unit} \\ &\text{x} \\ &\lambda \text{x}: \text{T. } \text{t} \\ &\text{t t} \\ &\text{exception } \text{l} \text{ of } \text{T}: \text{t} \\ &\text{raise } \text{l}(\text{t}) \\ &\text{try } \text{t} \text{ with } \text{l}(\text{x}) \Rightarrow \text{t} \end{aligned} \]
值：
\[ \begin{aligned} \text{v} ::= &\text{ } \\ &\lambda \text{x}: \text{T. } \text{t} \\ &\text{unit} \end{aligned} \]
类型：
\[ \begin{aligned} \text{T} ::= &\text{ } \\ &\text{T} \to \text{T} \\ &\text{Unit} \end{aligned} \]
求值规则：
\[ \begin{aligned} \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{\text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}'_1 \text{ } \text{t}_2} &\qquad (\text{E-APP1}) \\ \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{\text{t}_1 \text{ } \text{t}_2 \rightarrow \text{t}_1 \text{ } \text{t}'_2} &\qquad (\text{E-APP2}) \\ (\lambda \text{x}: \text{T. } \text{t}_1) \text{ } \text{v}_2 \rightarrow [\text{x} \mapsto \text{v}_2]\text{t}_1 &\qquad (\text{E-APPABS}) \\ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \text{exception } \text{l} \text{ of } \text{T}_1: \text{t}_1 \rightarrow \text{exception } \text{l} \text{ of } \text{T}_1: \text{t}'_1} &\qquad (\text{E-EXTEND-EXN}) \\ \text{exception } \text{l} \text{ of } \text{T}_1: \text{v}_1 \rightarrow \text{v}_1 &\qquad (\text{E-EXTEND-EXNV}) \\ \dfrac{\text{l}_1 = \text{l}}{\text{exception } \text{l} \text{ of } \text{T}_1: \text{raise } \text{l}_1(\text{v}_1) \rightarrow \text{raise } \text{u}(\text{unit})} &\qquad (\text{E-EXTEND-EXN-UNHANDLED-EXN}) \\ \dfrac{\text{l}_1 \neq \text{l}}{\text{exception } \text{l} \text{ of } \text{T}_1: \text{raise } \text{l}_1(\text{v}_1) \rightarrow \text{raise } \text{l}_1(\text{v}_1)} &\qquad (\text{E-EXTEND-EXN-CONTINUE-RAISE}) \\ (\text{raise } \text{l}(\text{v}_1)) \text{ } \text{t}_2 \rightarrow \text{raise } \text{l}(\text{v}_1) &\qquad (\text{E-APPRAISE1}) \\ \text{v}_1 \text{ } (\text{raise } \text{l}(\text{v}_2)) \rightarrow \text{raise } \text{l}(\text{v}_2) &\qquad (\text{E-APPRAISE2}) \\ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{\text{raise } \text{l}(\text{t}_1) \rightarrow \text{raise } \text{l}(\text{t}'_1)} &\qquad (\text{E-RAISE}) \\ \text{raise } \text{l}_2(\text{raise } \text{l}_1(\text{v}_1)) \rightarrow \text{raise } \text{l}_1(\text{v}_1) &\qquad (\text{E-RAISERAISE}) \\ \text{try } \text{v}_1 \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2 \rightarrow \text{v}_1 &\qquad (\text{E-TRYV}) \\ \dfrac{\text{l}_1 = \text{l}}{\text{try } \text{raise } \text{l}_1(\text{v}_1) \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2 \rightarrow [\text{x} \mapsto \text{v}_1]\text{t}_2} &\qquad (\text{E-TRYRAISE-MATCH}) \\ \dfrac{\text{l}_1 \neq \text{l}}{\text{try } \text{raise } \text{l}_1(\text{v}_1) \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2 \rightarrow \text{raise } \text{l}_1(\text{v}_1)} &\qquad (\text{E-TRYRAISE-MISMATCH}) \\ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{\text{try } \text{t}_1 \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2 \rightarrow \text{try } \text{t}'_1 \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2} &\qquad (\text{E-TRY}) \end{aligned} \]
类型规则：
\[ \begin{aligned} \\ \psi \mid \Gamma \vdash \text{unit}: \text{Unit} &\qquad (\text{T-UNIT}) \\ \dfrac{x: \text{T} \in \Gamma}{\psi \mid \Gamma \vdash \text{x}: \text{T}} &\qquad (\text{T-VAR}) \\ \dfrac{\psi \mid \Gamma, \text{x}: \text{T}_1 \vdash \text{t}_1: \text{T}_2}{ \psi \mid \Gamma \vdash \lambda \text{x}: \text{T}_1 \text{. } \text{t}_1: \text{T}_1 \to \text{T}_2} &\qquad (\text{T-ABS}) \\ \dfrac{\psi \mid \Gamma \vdash \text{t}_1: \text{T}_2 \to \text{T}_1 \quad \psi \mid \Gamma \vdash \text{t}_2: \text{T}_2}{ \psi \mid \Gamma \vdash \text{t}_1 \text{ } \text{t}_2: \text{T}_2} &\qquad (\text{T-APP}) \\ \dfrac{\text{l} \notin dom(\psi) \quad \langle \dots \psi, \text{l}: \text{T}_1 \rangle \mid \Gamma \vdash \text{t}_1: \text{T}}{ \psi \mid \Gamma \vdash \text{exception } \text{l} \text{ of } \text{T}_1: \text{t}_1: \text{T}} &\qquad (\text{T-EXTEND-EXN}) \\ \dfrac{\text{l} \in dom(\psi) \quad \psi \mid \Gamma \vdash \text{t}_1: \psi(\text{l})}{ \psi \mid \Gamma \vdash \text{raise } \text{l}(\text{t}_1): \text{T}} &\qquad (\text{T-EXN}) \\ \dfrac{\psi \mid \Gamma \vdash \text{t}_1: \text{T} \quad \text{l} \in dom(\psi) \quad \psi \mid \Gamma, \text{x}: \psi(\text{l}) \vdash \text{t}_2: \text{T}}{ \psi \mid \Gamma \vdash \text{try } \text{t}_1 \text{ with } \text{l}(\text{x}) \Rightarrow \text{t}_2: \text{T}} &\qquad (\text{T-TRY}) \end{aligned} \]
练习14.3.2
题目：
We noted above that Java exceptions (those that are subclasses of \( \text{Exception} \)) are a bit more strictly controlled than exceptions in ML (or the ones we have defined here): every exception that might be raised by a method must be declared in the method’s type. Extend your solution to Exercise 14.3.1 so that the type of a function indicates not only its argument and result types, but also the set of exceptions that it may raise. Prove that your system is typesafe.
解答：
练习14.3.1的解答中有总结，就不复制到这里了。
我们首先引入语法以允许函数声明它可能抛出的异常，仿照Java的语法，不过把\( \text{throws} \)改成\( \text{raises} \)：
\[ \lambda \text{x}: \text{T. } \text{raises } \text{l}_1, \text{l}_2, \dots, \text{l}_n \text{. } \text{t} \]
上述语法表示函数可能抛出标签为\( \text{l}_1, \text{l}_2, \dots, \text{l}_n \)的异常。
对应的，我们拓展函数类型，把异常信息也包含到类型信息中去，如下：
\[ \text{T}_1 \to \text{T}_2 \uparrow \text{l}_1, \text{l}_2, \dots, \text{l}_n \]
上述类型表示函数的参数类型为\( \text{T}_1 \)，返回值类型为\( \text{T}_2 \)，可能抛出标签为\( \text{l}_1, \text{l}_2, \dots, \text{l}_n \)的异常。
接下来是对应的类型规则，如何限制目标函数只能抛出它所声明的异常呢？为此，我们需要考虑一种情况，如果函数内部抛出了不在它声明范围内的异常，但是它在函数返回前处理了该异常，那这种情况明显不算违反它的异常声明，那么我们要如何处理这种情况？一种处理方法就是不止函数类型拓展加入异常信息，而是所有类型均拓展加入异常信息，然后我们再以此在类型推导中计算一个项可能抛出的异常。
我们类型系统中目前只有两种类型，对应拓展异常信息后语法如下：
\[ \begin{aligned} \text{T} ::= &\text{ } \\ &\text{T} \to \text{T} \uparrow \text{l}_1, \text{l}_2, \dots, \text{l}_n \\ &\text{Unit} \uparrow \text{l}_1, \text{l}_2, \dots, \text{l}_n \end{aligned} \]
接下来我们举个例子，展示怎么在类型推导中计算一个项可能抛出的异常，给定如下函数：
\[ \lambda \text{x}: \text{T}_1 \text{. } \text{raises } \text{l}_1, \text{l}_2 \text{. } \text{t}_1 \]
可以看出该函数声明它能抛出\( \text{l}_1, \text{l}_2 \)两种异常，我们先不验证该声明的真假，用\( \text{try} \)语句来处理异常\( \text{l}_1 \)，如下：
\[ \text{try } (\lambda \text{x}: \text{T}_1 \text{. } \text{raises } \text{l}_1, \text{l}_2 \text{. } \text{t}_1) \text{ with } \text{l}_1(\text{y}) \Rightarrow \text{t}_2 \]
则明显的，上述项可能抛出的异常为：
\[ (\text{函数可能抛出的异常集合} \setminus \{ \text{try语句处理掉的异常} \}) \cup \text{异常处理语句可能抛出的异常集合} \]
也就是：
\[ (\{ \text{l}_1, \text{l}_2 \} \setminus \{ \text{l}_1 \}) \cup E_{\text{t}_2} \]
其中，\( E_{\text{t}_2} \)为异常处理语句\( \text{t}_2 \)可能抛出的异常集合，其他语句则大部分是取其所有子项可能抛出的异常集合的并集，需要注意的情况就是声明的异常超出作用域范围，即练习14.3.1解答中求值规则\( \text{E-EXTEND-EXN-UNHANDLED-EXN} \)对应的情况了，原本我们是以转而抛出未处理异常\( \text{u} \)来处理，现在，由于我们有办法知道一个项可能抛出的异常的集合了，故我们可以用新的方案来处理这种情况，举个例子，给定如下项：
\[ \text{t} = \text{exception } \text{l} \text{ of } \text{T}_1: \text{t}_1 \]
其中，如果\( \text{t}_1 \)具有类型\( \text{T} \uparrow \text{l}_1, \text{l}_2, \dots, \text{l}_n \) 且\( \text{l} \in \{ \text{l}_1, \text{l}_2, \dots, \text{l}_n \} \)的话，即\( \text{t}_1 \)可能抛出外层\( \text{exception} \)语句声明的异常的话，则我们直接判定整个\( \text{t} \)为非类型良好的，这迫使用户在异常超出作用域范围内必须用\( \text{try} \)语句对其进行处理，用这种方法处理，我们就不需要未处理异常\( \text{u} \)了，对应的，类型\( \text{Unit} \)也可以不要了，故我们上面的类型语法直接简化成：
\[ \text{T} ::= \text{T} \to \text{T} \uparrow \text{l}_1, \text{l}_2, \dots, \text{l}_n \]
其余的似乎就比较简单了，但容易想到一个比较严重的问题，现在类型全部包含异常信息了，那我们该怎么声明函数参数的类型，举个例子，我们想要参数\( \text{x} \)为类型\( \text{Nat} \to \text{Bool} \)的函数，原本我们只需要写\( \lambda \text{x}: \text{Nat} \to \text{Bool} \dots \)，但现在我们还得写出\( \text{x} \)可能抛出的异常，而我们希望\( \text{x} \)可以代入任意类型为\( \text{Nat} \to \text{Bool} \)的函数，我们无法为任意类型为\( \text{Nat} \to \text{Bool} \)的函数指定可能抛出的异常，实际上，任何一个同时具有高阶函数、异常两种特性的语言，都会遇到这个问题，试想下，多数支持高阶函数的语言中都有一个叫\( \text{map} \)的函数，它一般接收一个映射函数+一个列表，那用户如何为作为参数的映射函数指定其可能抛出的异常，同时又不牺牲\( \text{map} \)的通用性呢？论文《Type-based analysis of uncaught exceptions》（注：也就是书后参考解答中给出的“Leroy and Pessaux (2000)”）中给出了一种解决方案就是：类似type inference，我们不要标注可能抛出的异常，而是推导可能抛出的异常，《Type-based analysis of uncaught exceptions》中包含了许多目前我不懂的内容，就先省略了，以后有机会再补上完整的解答吧。
练习14.3.3
Many other control constructs can be formalized using techniques similar to the ones we have seen in this chapter. Readers familiar with the “call with current continuation” (\( \text{call/cc} \)) operator of Scheme (see Clinger, Friedman, and Wand, 1985; Kelsey, Clinger, and Rees, 1998; Dybvig, 1996; Friedman, Wand, and Haynes, 2001) may enjoy trying to formulate typing rules based on a type \( \text{Cont T} \) of \( \text{T} \)-continuations—i.e., continuations that expect an argument of type \( \text{T} \).
解答：
暂时略了，没动力了，先看后面的内容，以后有机会再补。
参考资料
- Type-based analysis of uncaught exceptions, Leroy and Pessaux (2000)