23に必要そうだったので読んだ。let-polymorphism とは初耳。morph と form、音の並びが逆だ。
ゼノブレ2のセーブデータ持ってたボーナスで金たくさんもらったので早速水着買ってフィオルンのケツ見てた。これがリアル。
再帰型が登場すると 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 のアプリで読めたわ。ｱﾋﾋ
先週末は極まった精神状態でホントひどいもんで、やはり月曜の朝の動悸が特徴的だったので、久しぶりにFitbitを装着しだした。これによるとおれは朝から脂肪燃焼してるらしい。……。先週のうちに懸念が半分くらいは解けてきて、今はマシ。でも嫌な気持ちはある。
