酒を飲まずに寝たら久しぶりに夢を見た。また移動に関する夢。明日東京に出張しなければならない。が、なぜか今夜のホテルをこちらに取っている。用事は朝からあるので、できれば今日のうちに移動しておけると都合がいいのだけど、もう予約しているので金が無駄になってしまう。悩んだ末誰かに相談して、その日はこちらのホテルで寝ることにする。あるフロアを拠点にしていて、近くにいた同僚にこの階に夕飯を取れるところがあるか訊くが、地図を見たところほとんどが呉服屋とかそういった類の店で、ひとつだけ違うのは駄菓子屋だった。駄菓子を夕飯にするわけにもいかないが、その後どうしたかはわからない。
TAPL §22 Reconstruction
23に必要そうだったので読んだ。let-polymorphism とは初耳。morph と form、音の並びが逆だ。
■
ゼノブレ2のセーブデータ持ってたボーナスで金たくさんもらったので早速水着買ってフィオルンのケツ見てた。これがリアル。
TAPL §20 Recursive Types
再帰型が登場すると strong normalization が破綻する、normalization の中身読んでないので空気を読むと、型がついてても発散する項がありえるって話に驚き。あと D = μX.X→X（= D→D）と言う型で型無しラムダ計算を埋め込めてしまう……。無限はヤバイ。
Iso-recursive アプローチに登場する unfold [T] は recursive type を1段階展開する。fold [T] はその逆。実装が面倒そうなのだけど、この型をもった項を「作る」ときと「使う」ときにそれぞれ fold, unfold が対応するので、実際には破滅的に難しいというわけではなさそうだ。（p. 278）
Metatheory はスキップするつもりだけど、むしろここがおもしろそうなので 16, 21 章は後で読む。
■
数年ぶりにTAPLの続きを読んでる。こういう人生の諸問題から＊完全に＊切り離された抽象的な事象を扱うコトはリフレクシュアである。心なしか人生の諸問題（このフレーズが好きになった）を捉えなおす手助けになっていると思えなくもない。基本的な章はすでに読んでいた（らしい）ので、あとは興味あるところを飛ばし飛ばしに。ひとまず 15 Subtyping を読み終えたところ。Variant、これなんと訳すのかわからんのだが、タグが増えるほど super であるってのは不思議さが少しある。ちょっとまだ気持ちがわかってない。Kindle デバイスでも読めないしくらうどりーだーでもアレなので辟易していたんだけど今見たら macOS のアプリで読めたわ。ｱﾋﾋ
