Types and Programming Languages习题的参考解答及思考（第22章）

第22章

章节22.1

练习22.2.3

题目：

Find three different solutions for the term

\[ \lambda \text{x}: \text{X. } \lambda \text{y}: \text{Y. } \lambda \text{z}: \text{Z. } (\text{x z}) (\text{y z}) \]

in the empty context.

解答：

1. (\( [\text{X} \mapsto \text{Z} \to \text{Z} \to \text{Z}, \text{Y} \mapsto \text{Z} \to \text{Z}], \text{Z}) \)
2. (\( [\text{X} \mapsto \text{Z} \to \text{Nat} \to \text{Nat}, \text{Y} \mapsto \text{Z} \to \text{Nat}], \text{Nat}) \)
3. (\( [\text{X} \mapsto \text{Z} \to \text{Z} \to \text{Z} \to \text{Z}, \text{Y} \mapsto \text{Z} \to \text{Z}], \text{Z} \to \text{Z}) \)

章节22.3

练习22.3.3

题目：

Construct a constraint typing derivation whose conclusion is

\[ \vdash \lambda \text{x}: \text{X. } \lambda \text{y}: \text{Y. } \lambda \text{z}: \text{Z. } (\text{x z}) \text{ } (\text{y z}) : \text{S} \mid_{\mathcal{X}} C \]

for some \( \text{S}, \mathcal{X}, C \).

附注：

书上Figure 22-1的规则有勘误，针对CT-APP规则前提条件中的 \( \text{X} \notin \mathcal{X}_1, \mathcal{X}_2, \text{T}_1, \text{T}_2, C_1, C_2, \Gamma, \text{t}_1, \text{ or } \text{t}_2 \)，应该改为\( \text{X} \) not mentioned in \( \mathcal{X}_1, \mathcal{X}_2, \text{T}_1, \text{T}_2, C_1, \text{ or } C_2 \)。

解答：

我们一步步来。

首先先考虑比较内层的项\( \text{t}_1 = (\text{x z}) \)，该项被嵌在3个\( \lambda \)-抽象内，故它的类型环境为\( \Gamma_1 = \text{x}: \text{X}, \text{y}: \text{Y}, \text{z}: \text{Z} \)，先确定\( \text{x} \)和\( \text{z} \)的类型，根据CT-VAR规则，可得\( \Gamma_1 \vdash \text{x}: \text{X} \mid_{\empty} \{ \} \)，同理可得\( \Gamma_1 \vdash \text{z}: \text{Z} \mid_{\empty} \{ \} \)。接着考虑\( \text{t}_1 \)本身的类型，我们需要用到CT-APP规则，为此，先要保证满足CT-APP规则的前提条件：

1. 令\( \mathcal{X}_1 = \mathcal{X}_2 = C_1 = C_2 = \empty \)，我们有\( \Gamma_1 \vdash \text{x}: \text{X} \mid_{\mathcal{X}_1} C_1, \Gamma_1 \vdash \text{z}: \text{Z} \mid_{\mathcal{X}_2} C_2 \)。
2. 由于\( FV(\text{X}) = \{ \text{X} \}, FV(\text{Z}) = \{ \text{Z} \} \)，我们有\( \mathcal{X}_1 \cap \mathcal{X}_2 = \mathcal{X}_1 \cap FV(\text{Z}) = \mathcal{X}_2 \cap FV(\text{X}) = \empty \)。
3. 选择一个没用过的类型变量\( \text{W}_1 \)，保证\( \mathcal{X}_1, \mathcal{X}_2, \text{X}, \text{Z}, C_1, C_2 \) 中均没有提到过\( \text{W}_1 \)。
4. 增加新的对类型变量\( \text{X} \)的约束，要求其为函数类型且参数类型匹配，构造新的约束集，令\( C_3 = C_1 \cup C_2 \cup \{ \text{X} = \text{Z} \to \text{W}_1 \} \)。

于是，根据CT-APP规则，可得\( \Gamma_1 \vdash \text{t}_1: \text{W}_1 \mid_{\mathcal{X}_1 \cup \mathcal{X}_2 \cup \{ \text{W}_1 \}} C_3 \)。

同理可得，\( \Gamma_1 \vdash \text{t}_2: \text{W}_2 \mid_{\mathcal{X}_3 \cup \mathcal{X}_4 \cup \{ \text{W}_2 \}} C_6 \)，这里\( \text{t}_2 = (\text{y z}), \mathcal{X}_3 = \mathcal{X}_4 = C_4 = C_5 = \empty, C_6 = C_4 \cup C_5 \cup \{ \text{Y} = \text{Z} \to \text{W}_2 \} \)。

令\( \text{t}_3 = \text{t}_1 \text{ } \text{t}_2 \)，我们考虑\( \text{t}_3 \)，也是使用规则CT-APP，类似上面，易得\( \Gamma_1 \vdash \text{t}_3: \text{W}_3 \mid_{\mathcal{X}_1 \cup \mathcal{X}_2 \cup \{ \text{W}_1 \} \cup \mathcal{X}_3 \cup \mathcal{X}_4 \cup \{ \text{W}_2 \} \cup \{ \text{W}_3 \}} C_7 \)，这里\( C_7 = C_3 \cup C_6 \cup \{ \text{W}_1 = \text{W}_2 \to \text{W}_3 \} \)。

接着反复使用三次CT-ABS规则即可，易得\( \vdash \lambda \text{x}: \text{X. } \lambda \text{y}: \text{Y. } \lambda \text{z}: \text{Z. } (\text{x z}) \text{ } (\text{y z}) : \text{S} \mid_{\mathcal{X}} C \)，这里\( \text{S} = \text{X} \to \text{Y} \to \text{Z} \to \text{W}_3, \mathcal{X} = \mathcal{X}_1 \cup \mathcal{X}_2 \cup \{ \text{W}_1 \} \cup \mathcal{X}_3 \cup \mathcal{X}_4 \cup \{ \text{W}_2 \} \cup \{ \text{W}_3 \}, C = C_7 \)。

练习22.3.9

题目：

In a production compiler, the nondeterministic choice of a fresh type variable name in the rule CT-APP would typically be replaced by a call to a function that generates a new type variable—different from all others that it ever generates, and from all type variables mentioned explicitly in the context or term being checked—each time it is called. Because such global “gensym” operations work by side effects on a hidden global variable, they are difficult to reason about formally. However, we can mimic their behavior in a fairly accurate and mathematically more tractable way by “threading” a sequence of unused variable names through the constraint generation rules.

Let \( F \) denote a sequence of distinct type variable names. Then, instead of writing \( \Gamma \vdash \text{t}: \text{T} \mid_{\mathcal{X}} C \) for the constraint generation relation, we write \( \Gamma \vdash_F \text{t}: \text{T} \mid_{F'} C \), where \( \Gamma, F \), and \( \text{t} \) are inputs to the algorithm and \( \text{T}, F' \), and \( C \) are outputs. Whenever it needs a fresh type variable, the algorithm takes the front element of \( F \) and returns the rest of \( F \) as \( F' \).

Write out the rules for this algorithm. Prove that they are equivalent, in an appropriate sense, to the original constraint generation rules.

解答：

规则如下：

\[ \dfrac{\text{x}: \text{T} \in \Gamma}{\Gamma \vdash_{F} \text{x}: \text{T} \mid_F \{ \}} \qquad \text{(CT-VAR2)} \]

\[ \dfrac{\Gamma, \text{x}: \text{T}_1 \vdash_F \text{t}_2: \text{T}_2 \mid_{F'} C}{ \Gamma \vdash_F \lambda \text{x}: \text{T}_1 \text{. } \text{t}_2: \text{T}_1 \to \text{T}_2 \mid_{F'} C} \qquad \text{(C-ABS2)} \]

\[ \dfrac{\Gamma \vdash_F \text{t}_1: \text{T}_1 \mid_{F_1} C_1 \quad \Gamma \vdash_{F_1} \text{t}_2: \text{T}_2 \mid_{F_2} C_2 \quad F_2 = \text{X}, F_3}{ \Gamma \vdash_F \text{t}_1 \text{ } \text{t}_2: \text{X} \mid_{F_3} C_1 \cup C_2 \cup C_3 \cup \{ \text{T}_1 = \text{T}_2 \to \text{X} \}} \qquad \text{(C-APP2)} \]

\[ \Gamma \vdash_F 0: \text{Nat} \mid_F \{ \} \qquad \text{(C-ZERO2)} \]

\[ \dfrac{\Gamma \vdash_F \text{t}_1: \text{T} \mid_{F'} C \quad C' = C \cup \{ \text{T} = \text{Nat} \}}{ \Gamma \vdash_F \text{succ } \text{t}_1: \text{Nat} \mid_{F'} C'} \qquad \text{(CT-SUCC2)} \]

\[ \dfrac{\Gamma \vdash_F \text{t}_1: \text{T} \mid_{F'} C \quad C' = C \cup \{ \text{T} = \text{Nat} \}}{ \Gamma \vdash_F \text{pred } \text{t}_1: \text{Nat} \mid_{F'} C'} \qquad \text{(CT-PRED2)} \]

\[ \dfrac{\Gamma \vdash_F \text{t}_1: \text{T} \mid_{F'} C \quad C' = C \cup \{ \text{T} = \text{Nat} \}}{ \Gamma \vdash_F \text{iszero } \text{t}_1: \text{Bool} \mid_{F'} C'} \qquad \text{(CT-ISZERO2)} \]

\[ \Gamma \vdash_F \text{true}: \text{Bool} \mid_F \{ \} \qquad \text{(C-TRUE2)} \]

\[ \Gamma \vdash_F \text{false}: \text{Bool} \mid_F \{ \} \qquad \text{(C-FALSE2)} \]

\[ \dfrac{\begin{gather*} &\Gamma \vdash_F \text{t}_1: \text{T}_1 \mid_{F_1} C_1 \\ &\Gamma \vdash_{F_1} \text{t}_2: \text{T}_2 \mid_{F_2} C_2 \\ &\Gamma \vdash_{F_2} \text{t}_3: \text{T}_3 \mid_{F_3} C_3 \\ &C' = C_1 \cup C_2 \cup C_3 \cup \{ \text{T}_1 = \text{Bool}, \text{T}_2 = \text{T}_3 \} \end{gather*}}{ \Gamma \vdash_F \text{if } \text{t}_1 \text{ then } \text{t}_2 \text{ else } \text{t}_3: \text{T}_2 \mid_{F_3} C'} \qquad \text{(C-IF2)} \]

两套规则的等价性可以描述为：

1. 安全性（soundness）： 如果\( \Gamma \vdash_F \text{t}: \text{T} \mid_{F'} C \)且\( F \)中不包含\( \Gamma, t \)中提到的变量，则有\( \Gamma \vdash \text{t}: \text{T} \mid_{F \setminus F'} C \)（注：这里\( F \setminus F' \)即消耗掉的类型变量）。
2. 完备性（completeness）：如果\(\Gamma \vdash \text{t}: \text{T} \mid_{\mathcal{X}} C \)，则存在有限序列\( F = (\text{X}_n)_{n = 0}^{N} \)满足：
   1. \( \Gamma \vdash_F \text{t}: \text{T} \mid_{\empty} C \)（注：这里\( F \)中所有类型变量刚好被消耗完了）
   2. \( (\text{X}_n)_{n = 0}^{N} \)为\( \mathcal{X} \)中所有类型变量的一个排列，即\( N + 1 = |\mathcal{X}| \)且\( \forall \text{X} \in \mathcal{X}, \exists i \geq 0, \text{X}_i = \text{X} \)。

这里证明就先省略了，可以预想到的，又是简单且繁杂的归纳法+分类讨论，之前的章节写太多这种东西了，以后有动力的时候再补上。

练习22.3.10

题目：

Implement the algorithm from Exercise 22.3.9 in ML. Use the datatype

1
2
3
4
5

type ty =
    TyBool
  | TyArr of ty * ty
  | TyId of string
  | TyNat

for types, and

1

type constr = (ty * ty) list

for constraint sets. You will also need a representation for infinite sequences of fresh variable names. There are lots of ways of doing this; here is a fairly direct one using a recursive datatype:

1
2
3
4
5
6

type nextuvar = NextUVar of string * uvargenerator
and uvargenerator = unit -> nextuvar

let uvargen =
  let rec f n () = NextUVar("?X_" ^ string_of_int n, f(n + 1))
  in f 0

That is, \( \text{uvargen} \) is a function that, when called with argument \( \text{()} \), returns a value of the form \( \text{NextUVar(x,f)} \), where \( \text{x} \) is a fresh type variable name and \( \text{f} \) is another function of the same form.

解答：

ML相关的内容一律跳过。

练习22.3.11

题目：

Show how to extend the constraint generation algorithm to deal with general recursive function definitions (\( \S \text{11.11} \)).

解答：

在Figure 11-12的T-FIX规则上很容易改出来对应的CT-FIX规则，如下：

\[ \dfrac{\Gamma \vdash \text{t}_1: \text{T}_1 \mid_{\mathcal{X}_1} C_1 \quad \text{X} \text{没有在} \mathcal{X}_1, \Gamma, \text{t}_1 \text{中提到过}}{ \Gamma \vdash \text{fix} \text{ } \text{t}_1: \text{X} \mid_{\mathcal{X}_1 \cup \mathcal{X}} C_1 \cup \{ \text{T}_1 = \text{X} \to \text{X} \}} \qquad \text{(CT-FIX)} \]

如上，原本我们在T-FIX中是直接要求\( \text{t}_1 \)的类型为\( \text{T}_1 \to \text{T}_1 \)，这里改成引入新类型变量并通过约束来限制其类型形式和\( \text{T}_1 \to \text{T}_1 \)一样。

章节22.4

练习22.4.3

题目：

Write down principal unifiers (when they exist) for the following sets of constraints:

\[ \begin{aligned} \{ \text{X} = \text{Nat}, \text{Y} = \text{X} \to \text{X} \} &\qquad \{ \text{Nat} \to \text{Nat} = \text{X} \to \text{Y} \} \\ \{ \text{X} \to \text{Y} = \text{Y} \to \text{Z}, \text{Z} = \text{U} \to \text{W} \} &\qquad \{ \text{Nat} = \text{Nat} \to \text{Y} \} \\ \{ \text{Y} = \text{Nat} \to \text{Y} \} &\qquad \{ \} \quad \text{(the empty set of constraints)} \end{aligned} \]

解答：

考虑\( C_1 = \{ \text{X} = \text{Nat}, \text{Y} = \text{X} \to \text{X} \} \)，针对任意能统一\( C_1 \)的替换\( \sigma \)，首先能确定的事\( \text{X} \)只能替换成\( \text{Nat} \)，没得选，因此有\( \sigma(\text{X}) = \text{Nat} \)，接着考虑\( \text{Y} = \text{X} \to \text{X} \)，由于\( \sigma(\text{X} \to \text{X}) = \sigma(\text{X}) \to \sigma(\text{X}) = \text{Nat} \to \text{Nat} \)，因此\( \text{Y} \)也只能替换成\( \text{Nat} \to \text{Nat} \)了，故\( C_1 \)有且仅有一个替换\( \sigma_1 = [\text{X} \mapsto \text{Nat}, \text{Y} \mapsto \text{Nat} \to \text{Nat}] \)能够统一\( C_1 \)，进而\( \sigma_1 \)就是\( C_1 \)的主统一者（principal unifier）。

考虑\( \{ C_2 = \text{Nat} \to \text{Nat} = \text{X} \to \text{Y} \} \)，针对任意能统一\( C_2 \)的替换\( \sigma \)，马上有\( \sigma(\text{Nat} \to \text{Nat}) = \sigma(\text{Nat}) \to \sigma(\text{Nat}) = \text{Nat} \to \text{Nat} \)，进而有\( \sigma(\text{X} \to \text{Y}) = \sigma(\text{X}) \to \sigma(\text{Y}) = \sigma(\text{Nat} \to \text{Nat}) = \text{Nat} \to \text{Nat} \)，简化就是替换后需要有\( \sigma(\text{X}) \to \sigma(\text{Y}) = \text{Nat} \to \text{Nat} \)，可得\( \sigma(\text{X}) = \sigma(\text{Nat}), \sigma(\text{Y}) = \sigma(\text{Nat}) \)，故\( C_2 \)有且仅有一个替换\( \sigma_2 = [\text{X} \mapsto \text{Nat}, \text{Y} \mapsto \text{Nat}] \)能够统一\( C_1 \)，进而\( \sigma_2 \)就是\( C_2 \)的主统一者。

考虑\( C_3 = \{ \text{X} \to \text{Y} = \text{Y} \to \text{Z}, \text{Z} = \text{U} \to \text{W} \} \)，针对任意能统一\( C_3 \)的替换\( \sigma \)，马上有\( \sigma(\text{X} \to \text{Y}) = \sigma(\text{Y} \to \text{Z}), \sigma(\text{Z}) = \sigma(\text{U} \to \text{W}) \)，由\( \sigma(\text{X} \to \text{Y}) = \sigma(\text{Y} \to \text{Z}) \)，可得\( \sigma(\text{X}) = \sigma(\text{Y}), \sigma(\text{Y}) = \sigma(\text{Z}) \)，加上\( \sigma(\text{Z}) = \sigma(\text{U} \to \text{W}) \)，可得\( \sigma(\text{X}) = \sigma(\text{Y}) = \sigma(\text{Z}) = \sigma(\text{U} \to \text{W}) \)，故显然最通用（most general）的替换就是 \( \sigma_3 = [\text{X} \mapsto \text{U} \to \text{W}, \text{Y} \mapsto \text{U} \to \text{W}, \text{Z} \mapsto \text{U} \to \text{W}] \)，进而\( \sigma_3 \)就是\( C_3 \)的主统一者。

考虑\( C_4 = \{ \text{Nat} = \text{Nat} \to \text{Y} \} \)，针对任意能统一\( C_4 \)的替换\( \sigma \)，可得\( \sigma(\text{Nat}) = \text{Nat} = \sigma(\text{Nat} \to \text{Y}) = \sigma(\text{Nat}) \to \sigma(\text{Y}) \)，但是显然有\( \text{Nat} \neq \sigma(\text{Nat}) \to \sigma(\text{Y}) \)，故约束\( C_4 \)不可统一。

考虑\( C_5 = \{ \text{Y} = \text{Nat} \to \text{Y} \} \)，针对任意能统一\( C_5 \)的替换\( \sigma \)，可得\( \sigma(\text{Y}) = \sigma(\text{Nat} \to \text{Y}) = \sigma(\text{Nat}) \to \sigma(\text{Y}) = \text{Nat} \to \sigma(\text{Y}) \)，简化就是要求\( \sigma(\text{Y}) = \text{Nat} \to \sigma(\text{Y}) \)，但是这显然不能满足（如果读者不确定，则可以自行将\( \sigma(\text{Y}) \)替换成任意复杂类型表达式\( \text{Z} \)，就明显能看出左右类型不一样，不用考虑左右类型是否等价，因为统一（unify）的定义要求替换后的类型是在字面上一致的，而不考虑等价性），故约束\( C_5 \)不可统一。

考虑\( C_6 = \{ \} \)，则任意替换都能统一\( C_6 \)，我们取空替换\( \sigma = [] \)，则\( \forall \)替换\( \sigma' \)，我们有\( \sigma' = \sigma' \circ \sigma \)，于是根据定义22.4.1，可得\( \sigma \sqsubseteq \sigma' \)，进而根据定义22.4.2，可得\( \sigma \)为\( C_6 \)的主统一者。

练习22.4.6

题目：

Implement the unification algorithm.

解答：

ML相关的内容一律跳过。

章节22.5

练习22.5.2

题目：

Find a principal type for \( \lambda \text{x}: \text{X. } \lambda \text{y}: \text{Y. } \lambda \text{z}: \text{Z. } (\text{x z}) \text{ } (\text{y z}) \).

解答：

首先我们要先得到约束类型，由\( \text{x z} \)会得到约束\( C_1 = \{ \text{X} = \text{Z} \to \text{Y}_1 \} \)，由\( \text{y z} \)会得到约束\( C_2 = \{ \text{Y} = \text{Z} \to \text{Y}_2 \} \)，最后由\( (\text{x z}) \text{ } (\text{y z}) \)会得到约束\( C = C_1 \cup C_2 \cup (C_3 = \{ \text{Y}_1 = \text{Y}_2 \to \text{Y}_3 \}) \)，令\( \Gamma = \empty \)，令\( \text{t} = \lambda \text{x}: \text{X. } \lambda \text{y}: \text{Y. } \lambda \text{z}: \text{Z. } (\text{x z}) \text{ } (\text{y z}) \)，最终可以得到\( \Gamma \vdash \text{t}: \text{Y}_3 \mid C \)。

根据Figure 22-2的算法（或者直接推下，想下怎样替换最通用，约束/限制最少，也很容易得到），可得\( C \)的主统一者为\( \sigma = [\text{Y}_1 \mapsto \text{Y}_2 \to \text{Y}_3] \circ [\text{Y} \mapsto \text{Z} \to \text{Y}_2] \circ [\text{X} \mapsto \text{Z} \to \text{Y}_1] = [\text{X} \mapsto \text{Z} \to (\text{Y}_2 \to \text{Y}_3), \text{Y} \mapsto \text{Z} \to \text{Y}_2, \text{Y}_1 \mapsto \text{Y}_2 \to \text{Y}_3] \)，加上\( \sigma(\text{Y}_3) = \text{Y}_3 \)，可得\( (\sigma, \text{Y}_3) \)为\( (\Gamma, \text{t}, \text{Y}_3, C) \)的主解（principal solution），进而可得\( \text{Y}_3 \)为\( \text{t} \)在\( \Gamma \)下的主类型（principal type）。

练习22.5.5

题目：

Combine the constraint generation and unification algorithms from Exercises 22.3.10 and 22.4.6 to build a type-checker that calculates principal types, taking the \( \text{reconbase} \) checker as a starting point. A typical interaction with your typechecker might look like:

\[ \begin{aligned} &\lambda \text{x}: \text{X. } \text{x;} \\ \blacktriangleright &\langle \text{fun} \rangle : \text{X} \to \text{X} \\ &\lambda \text{z}: \text{ZZ. } \lambda \text{y}: \text{YY. } \text{z} \text{ } (\text{y true}) \text{;} \\ \blacktriangleright &\langle \text{fun} \rangle : (?\text{X}_0 \to ?\text{X}_1) \to (\text{Bool} \to ?\text{X}_0) \to ?\text{X}_1 \\ &\lambda \text{w}: \text{W. } \text{if true then false else w false;} \\ \blacktriangleright &\langle \text{fun} \rangle : (\text{Bool} \to \text{Bool}) \to \text{Bool} \end{aligned} \]

Type variables with names like \( ?\text{X}_0 \) are automatically generated.

解答：

ML相关的内容一律跳过。

练习22.5.6

题目：

What difficulties arise in extending the definitions above (22.3.2, etc.) to deal with records? How might they be addressed?

解答：

参考Figure 22-1的约束类型规则CT-APP，容易想到，在遇到形如项\( \text{t}.\text{l}_i \)的时候，我们得新加个约束要求\( \text{t} \)的类型为record，具体类似：

\[ \dfrac{\Gamma \vdash \text{t}: \text{T} \mid_{\mathcal{X}} C}{ \Gamma \vdash \text{t}.\text{l}_i: \text{X} \mid_{\mathcal{X} \cup \{ \text{X} \}} C \cup \{ \text{T} = \{ \text{l}_i: \text{X}, \dots \} \}} \]

这里\( \{ \text{l}_i: \text{X}, \dots \} \)表示任意具有标签\( \text{l}_i \)且标签对应类型为\( \text{X} \)的record类型，这意味着这个record类型是个不确定的类型，但是Figure 22-2的算法是不能处理不确定的类型的，递归调用会不知道该怎么分解下去，所以这是拓展相关定义以及Figure 22-2算法以处理record类型的一个难点。

问题在于我们只知道得要求record类型至少得有域\( \text{l}_i: \text{X} \)， record类型还有什么其他域是不知道/不受限制的，那该怎么解决这个问题呢？还是参考CT-APP，可以看到，它也不知道返回类型该是什么，它的做法是引入一个新的类型变量来代表未知的返回类型，我们也可以这样做，我们引入一个新的变量\( \text{fl} \)（field list的缩写）来代表未知的其他域，便可以得到如下类型规则：

\[ \dfrac{\Gamma \vdash \text{t}: \text{T} \mid_{\mathcal{X}} C}{ \Gamma \vdash \text{t}.\text{l}_i: \text{X} \mid_{\mathcal{X} \cup \{ \text{fl} \}} C \cup \{ \text{T} = \{ \text{l}_i: \text{X}, \dots \text{fl} \} \}} \qquad \text{(CT-PROJ)} \]

这里\( \dots \text{fl} \)代表把\( \text{fl} \)展开，举个例子，假设\( \text{fl} = \{ \text{l}_2: \text{T}_2, \text{l}_3: \text{T}_3 \} \)，则\( \{ \text{l}_i: \text{X}, \dots \text{fl} \} = \{ \text{l}_i: \text{X}, \text{l}_2: \text{T}_2, \text{l}_3: \text{T}_3 \} \)。

还需要考虑，如果有两个约束对\( \text{T} \)的域有要求，那这两个约束怎么合并，具体的，由\( \Gamma \vdash \text{t}.\text{l}_1: \text{X}_1 \)会产生约束 \( C_1 = \{ \text{T} = \{ \text{l}_1: \text{X}_1, \dots \text{fl}_1 \} \} \)， \( \Gamma \vdash \text{t}.\text{l}_2: \text{X}_2 \)则会产生约束 \( C_2 = \{ \text{T} = \{ \text{l}_2: \text{X}_2, \dots \text{fl}_2 \} \} \)，此时对\( \text{T} \)的域有两个要求，这里怎么合并\( C_1, C_2 \)？显然，如果\( \text{l}_1 = \text{l}_2 \)，即标签相同，则明显得应该通过加上约束\( C_3 = \{ \text{X}_1 = \text{X}_2 \} \)来做到合并\( C_1, C_2 \)的效果，即合并后的约束为\( \{ \text{T} = \{ \text{l}_1: \text{X}_1, \dots \text{fl}_1 \}, \text{X}_1 = \text{X}_2 \} \) （或者\( \{ \text{T} = \{ \text{l}_2: \text{X}_2, \dots \text{fl}_2 \}, \text{X}_1 = \text{X}_2 \} \)也行），那如果\( \text{l}_1 \neq \text{l}_2 \)，即标签不同呢？合并后的约束显然得要求\( \text{T} \)同时具有\( \text{l}_1: \text{X}_1 \)以及\( \text{l}_2: \text{X}_2 \)两个域，问题就在于对\( \text{fl}_1, \text{fl}_2 \)的合并了，这里得对两个域列表变量进行修剪，具体的，合并后的约束为\( \{ \text{T} = \{ \text{l}_1: \text{X}_1, \text{l}_2: \text{X}_2, \dots \text{fl}_3 \}, \text{fl}_3 = \text{fl}_1 \setminus \{ \text{l}_2: \text{X}_2 \}, \text{fl}_3 = \text{fl}_2 \setminus \{ \text{l}_1: \text{X}_1 \} \} \)，这里\( \text{fl}_1 \setminus \{ \text{l}_2: \text{X}_2 \} \)代表\( \text{fl}_1 \)去掉域\( \text{l}_2: \text{X}_2 \)。在引入\( \text{fl}_1 \setminus \{ \text{l}_2: \text{X}_2 \} \)这种记号后，替换后会产生形如\( \{ \text{T} = \{ \text{l}_2: \text{X}_2, \dots (\text{fl}_2 \setminus \{ \text{l}_3: \text{X}_3 \}) \} \} \)的约束，于是就得考虑更多种形式约束合并的可能性了，比如\( \{ \text{T} = \{ \text{l}_1: \text{X}_1, \dots \text{fl}_1 \} \} \) 和\( \{ \text{T} = \{ \text{l}_2: \text{X}_2, \dots (\text{fl}_2 \setminus \{ \text{l}_3: \text{X}_3 \}) \} \} \)的合并，这里得考虑\( \text{l}_1 \)是否和\( \text{l}_2 \)相同，\( \text{l}_3 \)是否和\( \text{l}_1 \)相同，以及相同的情况下，哪些类型得约束它们相等，域列表变量又得怎么修改，不同的情况下同理，类似的，还得考虑\( \{ \text{T} = \{ \text{l}_1: \text{X}_1, \dots (\text{fl}_1 \setminus \{ \text{l}_3: \text{X}_3 \}) \} \} \) 和\( \{ \text{T} = \{ \text{l}_2: \text{X}_2, \dots (\text{fl}_2 \setminus \{ \text{l}_4: \text{X}_4 \}) \} \} \)的合并，这些情况合并后还会引入更多需要考虑的情况，会越来越复杂，应该可以通过引入等价性关系，将\( \text{fl}_1 \setminus \{ \text{l}_2: \text{X}_2 \} \)转化成普通的域列表变量，以此来简化处理，这里不再深入讨论下去。

练习22.5.7

题目：

Modify your solution to Exercise 22.5.5 so that it performs unification incrementally and returns principal types.

解答：

ML相关的内容一律跳过。

章节22.7

练习22.7.1

题目：

Implement the algorithm sketched in this section.

解答：

ML相关的内容一律跳过。