Types and Programming Languages习题的参考解答及思考（第18章）
第18章
章节18.6
练习18.6.1
题目：
Write a subclass of \( \text{resetCounterClass} \) with an additional method \( \text{dec} \) that subtracts one from the current value stored in the counter. Use the \( \text{fullref} \) checker to test your new class.
解答：
\[ \begin{aligned} &\text{DecCounter} = \{ \text{get}: \text{Unit} \to \text{Nat}, \text{inc}: \text{Unit} \to \text{Unit}, \text{dec}: \text{Unit} \to \text{Unit}, \text{reset}: \text{Unit} \to \text{Unit} \} \\ &\text{decCounterClass} = \\ &\hphantom{aa} \lambda \text{r}: \text{CounterRep. } \\ &\hphantom{aaaa} \text{let super} = \text{resetCounterClass r} \text{ in} \\ &\hphantom{aaaaaa} \{ \text{get} = \text{super}.\text{get}, \\ &\hphantom{aaaaaa\{} \text{inc} = \text{super}.\text{inc}, \\ &\hphantom{aaaaaa\{} \text{dec} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{x} := \text{pred}(!(\text{r}.\text{x})), \\ &\hphantom{aaaaaa\{} \text{reset} = \text{super}.\text{reset} \} \\ &\text{newDecCounter} = \\ &\hphantom{aa} \lambda \text{\_}: \text{Unit. } \text{let r} = \{ \text{x} = \text{ref 1} \} \text{ in } \text{decCounterClass r} \end{aligned} \]
练习18.6.2
题目：
The explicit copying of most of the superclass fields into the record of subclass methods is notationally rather clumsy—it avoids explicitly re-entering the code of superclass methods in subclasses, but it still involves a lot of typing. If we were going to develop larger object-oriented programs in this style, we would soon wish for a more compact notation like “\( \text{super with } \{ \text{reset} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{x} := 1 \} \),” meaning “a record just like super but with a field reset containing the function \( \lambda \text{\_}: \text{Unit. } \text{r}.\text{x} := 1 \).” Write out syntax, operational semantics, and typing rules for this construct.
解答：
语法：
\[ \text{t} \text{ with } \text{t} \]
等下会有相关规则确保\( \text{with} \)左右侧的项均为record， 我们允许两个record间有相同标签 ，针对重复/冲突的标签，在求值规则中优先取右侧record的值，在类型规则中则优先取右侧record的类型，但是在规则中我们不会明确写明该要求，不然规则的可读性会变差。至于这里为什么不直接假定两个record之间没有相同的标签，是因为子类覆盖（override）父类的方法是个非常常用的操作。
求值规则：
首先，要让\( \text{with} \)左侧的项能求值成值，增加如下规则：
\[ \dfrac{\text{t}_1 \rightarrow \text{t}'_1}{ \text{t}_1 \text{ with } \text{t}_2 \rightarrow \text{t}'_1 \text{ with } \text{t}_2} \qquad (\text{E-RCD-OVERRIDE-LEFT}) \]
接着，我们得确保\( \text{with} \)左侧的项求值成值后，才去求值右侧的项，求值顺序是固定的，增加如下规则：
\[ \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{ \text{v}_1 \text{ with } \text{t}_2 \rightarrow \text{v}_1 \text{ with } \text{t}'_2} \qquad (\text{E-RCD-OVERRIDE-RIGHT}) \]
上面规则我们没有限制\( \text{v}_1 \)必须为record，实际上也可以限制它为record，因为\( \text{v}_1 \)不为record的情况下会是非类型良好的（由我们之后添加类型规则保证），而我们只需要确保类型良好的项不停滞即可，故上述规则也可以改成如下：
\[ \dfrac{\text{t}_2 \rightarrow \text{t}'_2}{ \{ \text{l}_i = \text{v}_i \ ^{i \in 1 \dots n} \} \text{ with } \text{t}_2 \rightarrow \{ \text{l}_i = \text{v}_i \ ^{i \in 1 \dots n} \} \text{ with } \text{t}'_2} \qquad (\text{E-RCD-OVERRIDE-RIGHT2}) \]
这里还是采用简单点的E-RCD-OVERRIDE-RIGHT规则。
最后，当\( \text{with} \)的左右侧都求值成record后（非record不管，为停滞项），可以进一步求值成两个record的合并record，如下：
\[ \{ \text{l}_i = \text{v}_i \ ^{i \in 1 \dots n_1} \} \text{ with } \{ \text{k}_j = \text{v}_j \ ^{j \in 1 \dots n_2} \} \rightarrow \{ \text{l}_i = \text{v}_i \ ^{i \in 1 \dots n_1} \ \text{k}_j = \text{v}_j \ ^{j \in 1 \dots n_2} \} \qquad (\text{E-RCD-OVERRIDE-MERGE}) \]
类型规则：
直接要求\( \text{with} \)的左右侧均为record，类型则为合并record的类型，如下：
\[ \dfrac{\Gamma \vdash \text{t}_1: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n_1} \} \quad \Gamma \vdash \text{t}_2: \{ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n_2} \}}{ \Gamma \vdash \text{t}_1 \text{ with } \text{t}_2: \{ \text{l}_i: \text{T}_i \ ^{i \in 1 \dots n_1} \ \text{k}_j: \text{S}_j \ ^{j \in 1 \dots n_2} \}} \qquad (\text{T-RCD-OVERRIDE}) \]
章节18.7
练习18.7.1
题目：
Define a subclass of \( \text{backupCounterClass} \) with two new methods, \( \text{reset2} \) and \( \text{backup2} \), controlling a second “backup register.” This register should be completely separate from the one added by \( \text{backupCounterClass} \): calling \( \text{reset} \) should restore the counter to its value at the time of the last call to \( \text{backup} \) (as it does now) and calling \( \text{reset2} \) should restore the counter to its value at the time of the last call to \( \text{backup2} \). Use the \( \text{fullref} \) checker to test your class.
解答：
\[ \begin{aligned} &\text{BackupCounter2} = \begin{aligned} \{ &\text{get}: \text{Unit} \to \text{Nat}, \text{inc}: \text{Unit} \to \text{Unit}, \\ &\text{reset}: \text{Unit} \to \text{Unit}, \text{backup}: \text{Unit} \to \text{Unit}, \\ &\text{reset2}: \text{Unit} \to \text{Unit}, \text{backup2}: \text{Unit} \to \text{Unit} \} \end{aligned} \\ &\text{BackupCounter2Rep} = \{ \text{x}: \text{Ref Nat}, \text{b}: \text{Ref Nat}, \text{b2}: \text{Ref Nat} \} \\ &\text{backupCounter2Class} = \\ &\hphantom{aa} \lambda \text{r}: \text{BackupCounter2Rep. } \\ &\hphantom{aaaa} \text{let super} = \text{backupCounterClass r} \text{ in} \\ &\hphantom{aaaaaa} \{ \text{get} = \text{super}.\text{get}, \\ &\hphantom{aaaaaa\{} \text{inc} = \text{super}.\text{inc}, \\ &\hphantom{aaaaaa\{} \text{reset} = \text{super}.\text{reset}, \\ &\hphantom{aaaaaa\{} \text{backup} = \text{super}.\text{reset}, \\ &\hphantom{aaaaaa\{} \text{reset2} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{x} := \ !(\text{r}.\text{b2}), \\ &\hphantom{aaaaaa\{} \text{backup2} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{b2} := \ !(\text{r}.\text{x}) \} \\ &\text{newBackupCounter2} = \\ &\hphantom{aa} \lambda \text{\_}: \text{Unit. } \text{let r} = \{ \text{x} = \text{ref 1}, \text{b} = \text{ref 0}, \text{b2} = \text{ref 0} \} \text{ in } \text{backupCounter2Class r} \end{aligned} \]
章节18.11
练习18.11.1
题目：
Use the \( \text{fullref} \) checker to implement the following extensions to the classes above:
- Rewrite \( \text{instrCounterClass} \) so that it also counts calls to \( \text{get} \).
- Extend your modified \( \text{instrCounterClass} \) with a subclass that adds a \( \text{reset} \) method, as in \( \S \text{18.4} \).
- Add another subclass that also supports backups, as in \( \S \text{18.7} \).
解答：
解答1：
\[ \begin{aligned} &\text{instrCounterClass} = \\ &\hphantom{aa} \lambda \text{r}: \text{InstrCounterRep. } \\ &\hphantom{aaaa} \lambda \text{self}: \text{Unit} \to \text{InstrCounter. } \\ &\hphantom{aaaaaa} \lambda \text{\_}: \text{Unit. } \\ &\hphantom{aaaaaaaa} \text{let super} = \text{setCounterClass r self unit} \text{ in} \\ &\hphantom{aaaaaaaaaa} \{ \text{get} = \lambda \text{\_}: \text{Unit. } (\text{r}.\text{a} := \text{succ}(!(\text{r}.\text{a})); \text{super}.\text{get } \text{unit}), \\ &\hphantom{aaaaaaaaaa\{} \text{set} = \lambda \text{i}: \text{Nat. } (\text{r}.\text{a} := \text{succ}(!(\text{r}.\text{a})); \text{super}.\text{set } \text{i}), \\ &\hphantom{aaaaaaaaaa\{} \text{inc} = \text{super}.\text{inc}, \\ &\hphantom{aaaaaaaaaa\{} \text{accesses} = \lambda \text{\_}: \text{Unit. } !(\text{r}.\text{a}) \} \end{aligned} \]
解答2：
\[ \begin{aligned} &\text{ResetInstrCounter} = \begin{aligned} \{ &\text{get}: \text{Unit} \to \text{Nat}, \text{set}: \text{Nat} \to \text{Unit}, \\ &\text{inc}: \text{Unit} \to \text{Unit}, \text{accesses}: \text{Unit} \to \text{Nat}, \\ &\text{reset}: \text{Unit} \to \text{Unit} \} \end{aligned} \\ &\text{resetInstrCounterClass} = \\ &\hphantom{aa} \lambda \text{r}: \text{InstrCounterRep. } \\ &\hphantom{aaaa} \lambda \text{self}: \text{Unit} \to \text{ResetInstrCounter. } \\ &\hphantom{aaaaaa} \lambda \text{\_}: \text{Unit. } \\ &\hphantom{aaaaaaaa} \text{let super} = \text{instrCounterClass r self unit} \text{ in} \\ &\hphantom{aaaaaaaaaa} \{ \text{get} = \text{super}.\text{get}, \\ &\hphantom{aaaaaaaaaa\{} \text{set} = \text{super}.\text{set}, \\ &\hphantom{aaaaaaaaaa\{} \text{inc} = \text{super}.\text{inc}, \\ &\hphantom{aaaaaaaaaa\{} \text{accesses} = \text{super}.\text{accesses}, \\ &\hphantom{aaaaaaaaaa\{} \text{reset} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{x} := 0 \} \\ &\text{newResetInstrCounter} = \\ &\hphantom{aa} \lambda \text{\_}: \text{Unit. } \text{let r} = \{ \text{x} = \text{ref 1}, \text{a} = \text{ref 0} \} \text{ in } \\ &\hphantom{aaaa} \text{fix } (\text{resetInstrCounterClass r}) \text{ } \text{unit} \end{aligned} \]
解答3：
\[ \begin{aligned} &\text{BackupInstrCounter} = \begin{aligned} \{ &\text{get}: \text{Unit} \to \text{Nat}, \text{set}: \text{Nat} \to \text{Unit}, \\ &\text{inc}: \text{Unit} \to \text{Unit}, \text{accesses}: \text{Unit} \to \text{Nat}, \\ &\text{backup}: \text{Unit} \to \text{Unit}, \text{reset}: \text{Unit} \to \text{Unit} \} \end{aligned} \\ &\text{BackupInstrCounterRep} = \{ \text{x}: \text{Ref Nat}, \text{a}: \text{Ref Nat}, \text{b}: \text{Ref Nat} \} \\ &\text{backupInstrCounterClass} = \\ &\hphantom{aa} \lambda \text{r}: \text{BackupInstrCounterRep. } \\ &\hphantom{aaaa} \lambda \text{self}: \text{Unit} \to \text{BackupInstrCounter. } \\ &\hphantom{aaaaaa} \lambda \text{\_}: \text{Unit. } \\ &\hphantom{aaaaaaaa} \text{let super} = \text{resetInstrCounterClass r self unit} \text{ in} \\ &\hphantom{aaaaaaaaaa} \{ \text{get} = \text{super}.\text{get}, \\ &\hphantom{aaaaaaaaaa\{} \text{set} = \text{super}.\text{set}, \\ &\hphantom{aaaaaaaaaa\{} \text{inc} = \text{super}.\text{inc}, \\ &\hphantom{aaaaaaaaaa\{} \text{accesses} = \text{super}.\text{accesses}, \\ &\hphantom{aaaaaaaaaa\{} \text{backup} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{b} := \ !(\text{r}.\text{x}), \\ &\hphantom{aaaaaaaaaa\{} \text{reset} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{x} := \ !(\text{r}.\text{b}) \} \\ &\text{newBackupInstrCounter} = \\ &\hphantom{aa} \lambda \text{\_}: \text{Unit. } \text{let r} = \{ \text{x} = \text{ref 1}, \text{a} = \text{ref 0}, \text{b} = \text{ref 0} \} \text{ in } \\ &\hphantom{aaaa} \text{fix } (\text{backupInstrCounterClass r}) \text{ } \text{unit} \end{aligned} \]
章节18.13
练习18.13.1
题目：
Another feature of objects that is useful for some purposes is a notion of object identity — an operation \( \text{sameObject} \) that yields \( \text{true} \) if its two arguments evaluate to the very same object, and \( \text{false} \) if they evaluate to objects that were created at different times (by different calls to \( \text{new} \) functions). How might the model of objects in this chapter be extended to support object identity?
解答：
最简单的方法就是维护一个全局的计数器，然后所有对象的实例变量record都添加一个叫\( \text{id} \)的域，与此同时，所有类的构造函数\( \text{newXX} \)都在创建对象时将计数器的当前值赋给\( \text{id} \)，并将计数器的值递增，这样不同时间创建的对象会有不同的\( \text{id} \)，进而我们\( \text{sameObject} \)比较\( \text{id} \)就可以确认是否为同一个对象。
但是上述做法不太可靠，某个构造函数\( \text{newXX} \)容易漏掉对\( \text{id} \)的赋值，或者赋值了，但是忘了递增全局计数器等，整个过程是易错的，解决方法就是利用引用的别名特性，增加一个类型为\( \text{Ref Nat} \)的域\( \text{id} \)，如果两个对象\( \text{a}, \text{b} \)真的是同一个对象，则对\( \text{a}.\text{id} \)赋值后，\( !(\text{b}.\text{id}) \)会拿到一样的值，具体如下：
\[ \begin{aligned} &\text{IdCounter} = \begin{aligned} \{ &\text{get}: \text{Unit} \to \text{Nat}, \text{inc}: \text{Unit} \to \text{Unit}, \\ &\text{id}: \text{Unit} \to \text{Nat}, \text{setid}: \text{Nat} \to \text{Unit} \} \end{aligned} \\ &\text{IdCounterRep} = \{ \text{x}: \text{Ref Nat}, \text{id}: \text{Ref Nat} \} \\ &\text{idCounterClass} = \\ &\hphantom{aa} \lambda \text{r}: \text{IdCounterRep. } \\ &\hphantom{aaaa} \{ \text{get} = \lambda \text{\_}: \text{Unit. } !(\text{r}.\text{x}), \\ &\hphantom{aaaa\{} \text{inc} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{x} := \text{succ }(!(\text{r}.\text{x})), \\ &\hphantom{aaaa\{} \text{id} = \lambda \text{\_}: \text{Unit. } !(\text{r}.\text{id}), \\ &\hphantom{aaaa\{} \text{setid} = \lambda \text{i}: \text{Nat. } \text{r}.\text{id} := \text{i} \} \\ &\text{newIdCounter} = \\ &\hphantom{aa} \lambda \text{\_}: \text{Unit. } \text{let r} = \{ \text{x} = \text{ref 1}, \text{id} = \text{ref 0} \} \text{ in } \text{idCounterClass r} \\ &\text{sameObject} = \\ &\hphantom{aa} \lambda \text{a}: \{ \text{id}: \text{Unit} \to \text{Nat}, \text{setid}: \text{Nat} \to \text{Unit} \} \text{. } \\ &\hphantom{aa} \lambda \text{b}: \{ \text{id}: \text{Unit} \to \text{Nat}, \text{setid}: \text{Nat} \to \text{Unit} \} \text{. } \\ &\hphantom{aaaa} \text{a}.\text{setid } 1; \text{b}.\text{setid } 0; \text{iszero } \text{a}.\text{id} \end{aligned} \]
或者，更紧凑点的实现，如下：
\[ \begin{aligned} &\text{IdCounter} = \{ \text{get}: \text{Unit} \to \text{Nat}, \text{inc}: \text{Unit} \to \text{Unit}, \text{id}: \text{Unit} \to \text{Ref Nat} \} \\ &\text{IdCounterRep} = \{ \text{x}: \text{Ref Nat}, \text{id}: \text{Ref }(\text{Ref Nat}) \} \\ &\text{idCounterClass} = \\ &\hphantom{aa} \lambda \text{r}: \text{IdCounterRep. } \\ &\hphantom{aaaa} \{ \text{get} = \lambda \text{\_}: \text{Unit. } !(\text{r}.\text{x}), \\ &\hphantom{aaaa\{} \text{inc} = \lambda \text{\_}: \text{Unit. } \text{r}.\text{x} := \text{succ }(!(\text{r}.\text{x})), \\ &\hphantom{aaaa\{} \text{id} = \lambda \text{\_}: \text{Unit. } !(\text{r}.\text{id}) \} \\ &\text{newIdCounter} = \\ &\hphantom{aa} \lambda \text{\_}: \text{Unit. } \text{let r} = \{ \text{x} = \text{ref 1}, \text{id} = \text{ref }(\text{ref 0}) \} \text{ in } \text{idCounterClass r} \\ &\text{sameObject} = \\ &\hphantom{aa} \lambda \text{a}: \{ \text{id}: \text{Unit} \to \text{Ref Nat} \} \text{. } \\ &\hphantom{aa} \lambda \text{b}: \{ \text{id}: \text{Unit} \to \text{Ref Nat} \} \text{. } \\ &\hphantom{aaaa} \text{a}.\text{id} := 1; \text{b}.\text{id} := 0; \text{iszero } (!\text{a}.\text{id}) \end{aligned} \]