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

第13章

章节13.1

练习13.1.1

题目：

Draw a similar diagram showing the effects of evaluating the expressions \( \text{a} = \{ \text{ref } 0, \text{ref } 0 \} \) and \( \text{b} = (\lambda \text{x}: \text{Ref Nat. } \{ \text{x}, \text{x} \}) \text{ } (\text{ref } 0) \).

解答：

练习13.1.2

题目：

If we defined update more compactly like this \[ \begin{aligned} \text{update} = \lambda &\text{a}: \text{NatArray. } \lambda \text{m}: \text{Nat. } \lambda \text{v}: \text{Nat. } \\ &\quad \text{a} := (\lambda \text{n}: \text{Nat. } \text{if equal m n then v else } (!\text{a}) \text{ } \text{n})\text{;} \end{aligned} \] would it behave the same?

解答：

不一样，这样修改之后，函数体中的\( !\text{a} \)解引用得到的值就是\( \text{a} \)的当前值，故如果传递给\( !\text{a} \)的参数\( \text{n} \neq \text{m} \)，则\( (!\text{a}) \text{ } \text{n} \)会不停调用自身，无法终止。

综上，我们在覆盖旧函数前应该先保存旧函数，并在fallback情况下使用旧函数而不是新函数。

练习13.1.3

题目：

Show how this can lead to a violation of type safety.

附注：

这里问的是：不用垃圾回收来回收内存，而是采用手动管理内存的方式是怎样违反类型安全性的。

解答：

我们使用\( \text{free 引用cell} \)来释放引用cell对应的存储空间并以trivial的\( \text{unit} \)作为返回值，则例子如下：

\[ \begin{aligned} &\text{let } \text{r} = \text{ref 0} \text{ in} \\ &\quad \text{let } \text{s} = \text{r} \text{ in} \\ &\quad \quad \text{free r}; \\ &\quad \quad \text{let } \text{t} = \text{ref false} \text{ in} \\ &\quad \quad \quad \text{succ } !\text{s} \end{aligned} \]

上面的例子通过\( \text{free r} \)释放掉了\( \text{s, r} \)共用指向的引用cell的存储空间\( \text{a} \)，接着我们通过\( \text{ref false} \)为\( \text{t} \)分配一个类型为\( \text{Ref Bool} \)的引用cell，这里假设内存管理器复用之前刚释放掉的存储空间\( \text{a} \)，则\( \text{succ } !\text{s} \)将求值成停滞项\( \text{succ } \text{false} \)，但我们的类型系统却可能推导出\( \text{s} \)的类型为\( \text{Ref Nat} \)，进而推导出\( \text{succ } !\text{s} \)的类型是\( \text{Nat} \)，即\( \text{succ } !\text{s} \)是类型良好的项，但在类型安全的语言中，类型良好的项不应该能求值成停滞项，故上述例子可能违反了类型安全性。实际上，我们不应该对已释放的存储空间的内容有任何假设， \( !\text{s} \)就应该直接视为未定义的，进而\( \text{succ } !\text{s} \)也是未定义的，然而类型良好的项也不应该求值成未定义的项，也违反了类型安全性。

上面的例子中，虽然通过\( \text{free r} \)，我们有办法推导出\( \text{r} \)在\( \text{free r} \)语句之后就非法了，不能再被使用，但还有一个别名\( \text{s} \)指向了相同的存储空间，这个例子比较简单，我们还是有办法推导出\( \text{s, r} \)指向相同的存储空间，进而可以限制\( \text{free r} \)语句之后\( \text{s,r } \)均不能再使用，但在有大量复杂表达式+副作用的情况下，别名分析是个困难的工作，此时我们就不一定能分析出两个变量指向相同的存储空间了。

章节13.3

练习13.3.1

题目：

How might our evaluation rules be refined to model garbage collection? What theorem would we then need to prove, to argue that this refinement is correct?

解答：

我们这里形式化一个简单的追踪式（trace）垃圾回收器，我们假定内存是无限的，从而避免需要处理内存不足的异常情况，读者可能会有疑问，如果内存无限多的话，那要垃圾回收器干嘛？首先，这只是一个理论模型，现实中虽然内存均是有限的，但是我们可以通过不断扩充内存以近似无限内存，从而达到和我们理论模型差不多的效果，其次，简单的垃圾回收器模型假设有限内存并不会带来特别大的好处，并不会有什么特别有用的理论结果，也就多了对内存不足情况的描述（注：这里是针对我们这种简单的垃圾回收器模型来说的，如果你想研究内存不足情况下的内存使用策略，那模型就必须假定有限内存）。

注：给定存储\( \mu \)，则我们记\( dom(\mu) \)为\( \mu \)当前已用的内存位置的集合，虽然内存是无限的，但是当前已用的内存位置的集合始终是有限的，故\( dom(\mu) \)是有限集。

首先，给定项\( \text{t} \)以及记录了当前内存所有内容的存储\( \mu \)，我们希望知道\( \text{t} \)直接或间接引用了哪些内存位置，我们称这些内存位置为从\( \text{t} \)可达的内存位置（reachable），记为\( reachable(\text{t}, \mu) \) 举几个例子：

1. 令\( \mu = (l_0 \mapsto \text{true}), \text{t} = l_0 \)，则\( reachable(\text{t}, \mu) = l_0 \)。
2. 令\( \mu = (l_0 \mapsto \{ \text{false}, l_1 \}, l_1 \mapsto \text{true}), \text{t} = l_0 \)，则\( reachable(\text{t}, \mu) = l_0, l_1 \)，这里\( l_1 \)是间接引用到的。
3. 令\( \mu = (l_0 \mapsto \text{true}), \text{t} = \text{ref 0} \)，则\( reachable(\text{t}, \mu) = \empty \)，这是虽然执行\( \text{ref 0} \)会创建一个新的内存位置，但是\( \text{ref 0} \)还没被执行，故还没在\( \mu \)中创建新的内存位置，进而\( \text{t} \)没有引用到任何内存位置。

现在，我们希望通过递归定义来定义\( reachable \)，但引用链是图结构（可能包含环）而不是树等结构，比较适合通过闭包算法描述，而不适合用递归定义，故我们采用其他方法，首先，我们先定义直接可达（direct reachable），直接可达关系是树状结构，适合用递归定义描述。

定义1（direct reachable）：

给定项\( \text{t} \)以及存储\( \mu \)，归纳假设，针对\( \text{t} \)的所有直接子项\( \text{t}' \)， \( dreachable(\text{t}', \mu) \)均已定义，我们按如下规则定义\( dreachable(\text{t}, \mu) \) （注：虽然上面举例用了布尔和乘积，但我们目前的系统是纯\( \lambda \)+Unit类型+引用）：

1. 如果\( \text{t} = \text{x} \)，则\( dreachable(\text{t}, \mu) = \empty \)，这是因为：
   1. 变量代表了未知项，我们无法知道未知项引用了哪些内存位置。
   2. 变量会在使用E-APPABS求值规则后，被替换成实际项，在那之后，变量就不见了，故我们不需要知道变量引用了哪些内存位置。
2. 如果\( \text{t} = \lambda \text{x}: \text{T. } \text{t}_1 \)，则令\( dreachable(\text{t}, \mu) = dreachable(\text{t}_1, \mu) \)。
3. 如果\( \text{t} = \text{t}_1 \text{ } \text{t}_2 \)，则令\( dreachable(\text{t}, \mu) = dreachable(\text{t}_1, \mu) \cup dreachable(\text{t}_2, \mu) \)。
4. 如果\( \text{t} = \text{unit} \) ，则\( dreachable(\text{t}, \mu) = \empty \)。
5. 如果\( \text{t} = \text{ref } \text{t}_1 \)，则令\( dreachable(\text{t}, \mu) = dreachable(\text{t}_1, \mu) \)，注意，这里\( \text{ref} \)语句还没有执行，故还没创建新的内存位置。
6. 如果\( \text{t} = !\text{t}_1 \)，则令\( dreachable(\text{t}, \mu) = dreachable(\text{t}_1, \mu) \)。
7. 如果\( \text{t} = \text{t}_1 := \text{t}_2 \)，则令\( dreachable(\text{t}, \mu) = dreachable(\text{t}_1, \mu) \cup dreachable(\text{t}_2, \mu) \)。
8. 如果\( \text{t} = l \)，则\( l \in dom(\mu) \)（注：内存位置无法由程序员直接书写创建，而是程序员通过\( \text{ref} \)间接创建的，故不会出现\( l \notin dom(\mu) \)，即非法内存位置的情况），我们令\( dreachable(\text{t}, \mu) = \{ l \} \)。

定义1完毕。

有了\( dreachable \)的定义后，我们可以定义\( reachable \)了，不过不像上面，\( reachable \)的定义不是构造性的定义（等下我们再讲怎么处理非构造性的问题）。

定义2 (reachable)：

给定项\( \text{t} \)以及存储\( \mu \)，令\( reachable(\text{t}, \mu) = \{ l \in dom(\mu) \mid \exists \text{t}_1, \text{t}_2, \dots, \text{t}_{n_l}, \text{t}_1 = \text{t}, l \in dreachable(\text{t}_{n_l}), \forall 1 \leq i < n_l, \exists l_i \in dreachable(\text{t}_i), \mu(l_i) = \text{t}_{i + 1} \} \)。

定义2完毕。

简而言之，\( reachable(\text{t}, \mu) \)为所有从\( \text{t} \)经有限步骤可达的内存位置。

上述\( reachable \)的定义非构造性定义，不过很容易给出计算\( reachable \)的闭包算法，故\( reachable \)可以视为显式函数而非隐式函数，下面给出\( reachable \)计算的闭包算法。

算法3 (reachable)：

首先，注意到\( dreachable \)是递归定义，很容易直接转换成递归算法，故我们这里可以直接调用\( dreachable \)。

给定项\( \text{t} \)以及存储\( \mu \)，我们按如下规则计算 \( reachable(\text{t}, \mu) \)：

1. 初始化，令\( reachable(\text{t}, \mu) = dreachable(\text{t}, \mu) \)。
2. 令\( oldreachable(\text{t}, \mu) = reachable(\text{t}, \mu) \)，
3. \( \forall l \in reachable(\text{t}, \mu) \)，令\( \text{t}_l = \mu(l) \)，更新\( reachable(\text{t}, \mu) = reachable(\text{t}, \mu) \cup dreachable(\text{t}_l, \mu) \)。
4. 如果\( reachable(\text{t}, \mu) = oldreachable(\text{t}, \mu) \)，即前一步我们没有得到新的可达内存位置，则算法停止，否则回到第2步继续执行。

易证上述算法必定停止，且计算的\( reachable(\text{t}, \mu) = \)定义2中的\( reachable(\text{t}, \mu) \)。

算法3完毕。

接下来直观地演示下怎么通过\( reachable \)来进行垃圾回收：

1. 令初始项\( \text{t}_0 = (\lambda \text{x}: \text{Ref Unit. } !x) \text{ } (\text{ref unit}) \)，一开始存储是空的，故初始存储\( \mu_0 \)为空函数，或者直观点写就是\( \mu_0 = \empty \)，此时有\( reachable(\text{t}_0, \mu_0) = \empty \)。
2. 使用E-REFV进行单步求值，可得\( \text{t}_0 \mid \mu_0 \rightarrow \text{t}_1 \mid \mu_1 \)，其中，\( \text{t}_1 = (\lambda \text{x}: \text{Ref Unit. } !x) \text{ } l_0 \)， \( l_0 \)为新创建的内存位置，更新后的存储\( \mu_1 = (l_0 \mapsto \text{unit}) \)，此时有\( reachable(\text{t}_1, \mu_1) = \{ l_0 \} \)，刚好\( reachable(\text{t}_1, \mu_1) = dom(\mu_1) \)，没有不使用的内存位置，不需要进行垃圾回收。
3. 使用E-APP2进行单步求值，可得\( \text{t}_1 \mid \mu_1 \rightarrow \text{t}_2 \mid \mu_2 \)，其中，\( \text{t}_2 = !l_0 \)，存储没有被修改，故\( \mu_2 = \mu_1 \)，此时仍然是\( reachable(\text{t}_2, \mu_2) = \{ l_0 \} \)，还是刚好\( reachable(\text{t}_2, \mu_2) = dom(\mu_2) \)，不需要进行垃圾回收。
4. 使用E-DEREFLOC进行单步求值，可得\( \text{t}_2 \mid \mu_2 \rightarrow \text{t}_3 \mid \mu_3 \)，其中，\( \text{t}_3 = \text{unit} \)，存储没有被修改，故\( \mu_3 = \mu_2 \)，此时\( reachable(\text{t}_3, \mu_3) = \empty \)，可得\( reachable(\text{t}_3, \mu_3) \subsetneq dom(\mu_3) \)，这意味着\( dom(\mu_3) \)中存在没有用的内存位置，需要进行垃圾回收，这里\( dom(\mu_3) \setminus reachable(\text{t}_3, \mu_3) = \{ l_0 \} \)就是要回收的内存位置的集合，垃圾回收完，\( \mu'_3 = \empty \)且\( \text{t}_3 \)已经是值了，不需要进一步求值。

上述例子并不严格，下面，我们严格定义垃圾回收步骤。

定义4（垃圾回收步骤）：

给定项\( \text{t} \)以及存储\( \mu \)，则\( \text{t} \mid \mu \xrightarrow{gc} \text{t} \mid \mu' \)，这里\( \mu' \)为\( \mu \)回收掉\( dom(\mu) \setminus reachable(\text{t}, \mu) \)中所有内存位置后得到的新存储。

定义4完毕。

我们希望在求值过程中穿插垃圾回收步骤，并不一定要每步求值后都进行一次垃圾回收，可以两步求值后垃圾回收一次，等等。为此，我们定义一个新的求值关系，如下：

定义5（穿插垃圾回收的求值步骤）：

\( \text{t} \mid \mu \xrightarrow{gc}^* \text{t}' \mid \mu' \)当且仅当存在\( n \geq 1 \)个项\( \text{t}_1, \text{t}_2, \dots, \text{t}_n \)、 \( n \)个存储\( \mu_1, \mu_2, \dots, \mu_n \)，它们满足： \( \text{t}_1 = \text{t}, \text{t}_n = \text{t}', \mu_1 = \mu, \mu_n = \mu' \)，且\( \forall 1 \leq i < n \)，有\( \text{t}_i \mid \mu_i \rightarrow \text{t}_{i + 1} \mid \mu_{i + 1} \)或\( \text{t}_i \mid \mu_i \xrightarrow{gc} \text{t}_{i + 1} \mid \mu_{i + 1} \)。

定义5完毕。

为了说明穿插垃圾回收的求值步骤不影响求值结果，我们需要证明如下命题：

命题6（穿插垃圾回收的求值步骤不影响求值结果）：

1. 如果\( \text{t} \mid \mu \xrightarrow{gc}^* \text{t}' \mid \mu' \)，则\( \exists \mu'', \text{t} \mid \mu \rightarrow^* \text{t}' \mid \mu'' \)，这里\( dom(\mu') \subseteq dom(\mu'') \)且\( \forall l \in dom(\mu'), \mu'(l) = \mu''(l) \)。
2. 如果\( \text{t} \mid \mu \rightarrow^* \text{t}' \mid \mu' \)，则\( \exists \mu'', \text{t} \mid \mu \xrightarrow{gc}^* \text{t}' \mid \mu'' \)，这里\( dom(\mu'') \subseteq dom(\mu') \)且\( \forall l \in dom(\mu''), \mu''(l) = \mu'(l) \)。

命题6完毕。

以上就是我们对垃圾回收的简单形式化，不过得注意该形式化缺少很多垃圾回收应该考虑的东西，比如：

1. 如果语言有弱引用的概念，则如果一个内存位置仅被弱引用引用，该内存位置也应该被回收，这是我们的形式化没有考虑到的东西。
2. 我们的形式化没有考虑不同类型对象所需的存储空间大小不同的问题，无法用于研究如何紧凑地使用内存等问题。
3. 我们的形式化将内存位置看成一个抽象的、没有结构的实体，然而实际垃圾回收算法使用的内存位置的表示非常可能会有特定的结构，比如有tag记录存储的对象的类型等。

章节13.4

练习13.4.1

题目：

Can you find a term whose evaluation will create this particular cyclic store?

解答：

\[ \begin{aligned} &\text{let } \text{f}_1 = \text{ref } (\lambda \text{x}: \text{Nat. } \text{x}) \text{ in} \\ &\quad \text{let } \text{f}_2 = \text{ref } (\lambda \text{x}: \text{Nat. } (!\text{f}_1) \text{ } \text{x}) \text{ in} \\ &\quad \quad (\text{f}_1 := \lambda \text{x}: \text{Nat. } (!\text{f}_2) \text{ } \text{x}); \text{ } \text{f}_1 \end{aligned} \]

章节13.5

练习13.5.2

题目：

Can you find a context \( \Gamma \), a store \( \mu \), and two different store typings \( \Sigma_1 \) and \( \Sigma_2 \) such that both \( \Gamma \mid \Sigma_1 \vdash \mu \) and \( \Gamma \mid \Sigma_2 \vdash \mu \)?

解答：

令 \[ \begin{aligned} \Gamma &= \empty \\ \mu &= (l_0 \mapsto \lambda \text{x}: \text{Unit. } (!l_0) \text{ x}) \\ \Sigma_1 &= l_0: \text{Unit} \to \text{Unit} \\ \Sigma_2 &= l_0: \text{Unit} \to (\text{Unit} \to \text{Unit}) \end{aligned} \] 则\( \Sigma_1 \neq \Sigma_2 \)且\( \Gamma \mid \Sigma_1 \vdash \mu, \Gamma \mid \Sigma_2 \vdash \mu \)。

练习13.5.8

题目：

Is the evaluation relation in this chapter normalizing on well-typed terms? If so, prove it. If not, write a well-typed factorial function in the present calculus (extended with numbers and booleans).

解答：

明显本章不是所有类型良好的项都是终止的，比如练习13.4.1给出的函数就是类型良好的，且随便给一个类型匹配的参数调用都是非终止的，不过那里用到了\( \text{let} \)，我们desugar一下、把\( \text{Nat} \)改成\( \text{Unit} \)、加上对函数的调用，就可以得到类型良好的、非终止的项，不过desugar后可读性会下降，故我们下面仅仅把\( \text{Nat} \)改成\( \text{Unit} \)并加上对函数的调用：

\[ \begin{aligned} &\text{let } \text{f}_1 = \text{ref } (\lambda \text{x}: \text{Unit. } \text{x}) \text{ in} \\ &\quad \text{let } \text{f}_2 = \text{ref } (\lambda \text{x}: \text{Unit. } (!\text{f}_1) \text{ } \text{x}) \text{ in} \\ &\quad \quad (\text{f}_1 := \lambda \text{x}: \text{Unit. } (!\text{f}_2) \text{ } \text{x}); \text{ } ((!\text{f}_1) \text{ } \text{unit}) \end{aligned} \]

接下来，我们给出\( \text{factorial} \)函数的定义，其实重点就是我们要把函数存在引用里面，从而做到能引用自己以调用自己而已，我们这里就不用\( \text{let} \)语句了，直接在脑中desugar一下：

\[ \begin{aligned} \text{factorial} &= \\ &(\lambda \text{rf}: \text{Ref } \text{Nat} \to \text{Nat.} \\ &\quad \text{rf} := (\lambda \text{n}: \text{Nat. } \text{if } (\text{iszero n}) \text{ then } 1 \text{ else } (\text{times } \text{n} \text{ } ((!\text{rf}) \text{ } (\text{pred n})))); \\ &\quad !\text{rf}) \\ &(\text{ref } (\lambda \text{n}: \text{Nat. } 1)) \end{aligned} \]