TaPL読書録 #6
前回:
今回は7章、8章。
7章は実装章である。個人的には小ステップの実装をするところまでで終わり。大ステップには変換しなかった。もうひとり書いてきた人のと小ステップ・大ステップでの差異をかるく比較して終わり。実装したのは2人だったが、「実装したからといって理解したとは限らない」のであった。
8章からは「型つき算術式」ということでようやく型がついた。長く苦しい戦いだった(マジ)
以前は「行き詰まり状態」というものを導入して評価をとめていたが、それらを実行前に静的に解釈して行き詰まり状態であることを検査したい。そのため型 Nat, Bool を導入する。
検査は「保守的」に行われることに注意。すなわち if 項 if t1 then t2 else t3 において、 t1 が「明らかに」真である場合にも t3 の型情報も用いる、という話である。ここでは t2 と t3 についてユニオンしたような型の導入は行わない1
補題8.2.2.「型付け関係の逆転」
逆転が成り立つのは、ある値が複数の型に解釈される可能性がないからである。すなわち 1 が型 Nat であり、かつ型 Rational でもあるような値が今の所存在しないことが前提となっている。これは定理 8.2.4. 「型の一意性」にて言及されている。
演習8.2.3.
「正しく片付けされた項」の「正しく」ってなんだっけ、というメモがあったが定義 8.2.1 に「項 t にたいしてある型 T が存在して t: T となるとき t は型付け可能(または正しく型付けされている)という」と書いてあった。
解答してはだいたい自明で、筆者のメモでは「規則に従ってるので規則が正しく型付けされていること・保守的に評価することを考えたら自明」とある。はい。おそらく正式に書く場合には逆転補題についてそれぞれ追えばよい。
定理8.2.4「型の一意性」
余談として部分型(で合ってたか少し自信がないが)についての話が出てきた。以下のようなクラス、関数を考える。記法は独自文法であるが意味はおそらくとれるとおもう2。
class A x: int end class B x: int y: int end func f(a: A) -> int return a.x * 2 end
上記の関数 f について、仮引数 a として B のインスタンスをいれることが可能なのか、という話。この場合 B ⊂ A なので、使えてもいいよね、という話をした。
ここでダイヤモンド継承の話もした。ダイヤモンド継承をして同名メソッドがあったときには、シグネチャさえ同じならば型システム的にはおkになりそうだよねー、実装的にはどっちにとぶか決められなくてつらそうだよねーなど。
8.3.
型の安全性とは進行と保存である。
演習 8.3.4. スキップ
演習 8.3.5.
俺のメモでは pred 0 で行き詰まるので pred nv の nv は「0 ではない numeric value」という型情報をもたないと型システムが健全じゃなくなるので無理、と書いてあった。
演習 8.3.6.
良問では？という話になった。
メモでは「型付けされていて、型が2つしかないから保存の定理の対偶から明らか」とあるが、実際のところは if true then 0 else false みたいな項が反例となる。
演習 8.3.7.
大ステップにおける「最終的に値になる」という制約が強いのだなあ、ということを確認して終わり。
次回 chap9 全部。
