日々の流転

λ. 継承とサブタイプ

暗黙のselfを受け取るメンバ関数のサブタイピングは、操作的意味論を考えるだけならば、確かにそんなに問題では無い気がします。ただ、この議論はこの体系が「二階ラムダ計算＋サブタイプ」へ素直には埋め込めないということを言っているわけで、既存の理論を直接応用できないという点で痛いんじゃないかと。例えば、モデルの存在は自明ではないと思うし、特にパラメトリシティ等の良い性質を持ったモデルを構築できるかどうかも気になります。

Extensible Objects: a Tutorial, Viviana Bono を読まねば……

λ. 「〜」ってなんて読むの？

やっぱ「にょろ」でしょう。それしか考えられん。変換するときも「にょろ」。

λ. Theorems for free!. Philip Wadler

を読んだ。不動点コンビネータを導入する場合には、パラメトリシティを適用できる関係は、単に連続な関係であるだけでなく正格な関係でなくてはならないというのに少し驚いた。