論文メモ: Towards a Theory of Type Structureを読もうとして挫折した話
プログラミング言語理論に関係する論文を結構読み散らかしているのだが、あまりしっかりアウトプットする機会もないので読み込みも甘いし記憶も曖昧になる。
というわけで面白そうなやつは、内容・背景・感想などをブログにメモとして残していこうと考えた。
Types and Programming Languages作者のBenjamin Pierceが2004年に知り合いの研究者たちに聞いてリストアップした「プログラミング言語関連で重要な論文」リストを最近見ていて：
この中からJohn ReynoldsのTowards a Theory of Type Structureを読んでみよう、と思ったのだが歯が立たず挫折した。再度挑戦するときのためにもメモっておく。
内容
型付きラムダ計算に無制限な多相を導入したSystem Fはほぼ同時期に論理学者Girardとプログラミング言語理論研究者Reynoldsによって別々に発見された（Girardは1972、Reynoldsは1974）。Towards a Theory of Type StructureはReynoldsの発見を発表したもので、この時点ではSystem FではなくPolymorphic Lambda Calculusという名前で呼ばれている。
参考文献を抜かすと16ページで、まあ読みやすい長さの論文ではある。
最初の6ページまでは、「引数が『多相な関数』な関数」の型を表現する、などのPolymorphic Lambda CalculusのSTLCに対する違い（ここら辺の問題意識はStratcheyから来ているとのこと）からはじめて、Polymorphic Lambda Calculusの構文を定義している。微妙な違い（というか後世による整理）があるとはいえ、基本的にTaPLの23章で見た内容なのですんなり読める。
しかし7ページ目からSemanticsの項に入り、まったく歯が立たなくなる。最初の文章が：
Semantics: We will interpret our language in terms of the lattice theoretic approach of D. Scott. Intuitively the effect of a type expression is to produce a Scott domain given an assignment of a domain to each free type variable occurring in the type expression.
となっていて、基本的にこれ以降はlattice theoryとScott domainについてそれなりに知識がないとほぼすべての部分が意味がわからなくなる。さらに特定の文字が手書きでなんと読めばいいかわからなくなり、私の理解のカオスっぷりに拍車がかかる。
ドメイン理論と表示的意味論を少ししっかり読み込んでからもう一度挑戦するのが良さそうだ。
Polymorphic Lambda Calculusは以前ブログで書いたとおりImpredicativeな性質（自己言及性？）があり、その型のモデルを考慮する場合ラッセルのパラドックスをどうにか回避しないといけない、的な話が出ており理解できればなかなか面白そうではある。ただしこの論文ではうまく回避できたかは定かではない、と書いてある。またFull Semantics of Type Expressionsという章以降（11~14ページ）では"In order to extend the semantic function B, we first note that the combination of domains and representations forms a category"とはじまる圏論的な話題も出てくる。やはりかなり数学的素養を要求してくる論文である。
著者について
著者のJohn ReynoldsはSystem Fの発見者の一人である以外でも、Separation LogicというHoare Logicの拡張を打ち出したことでも知られる。POPLやICFPのAccepted Papersを見てもSeparation Logic関連の話題は豊富で、プログラミング言語研究に関しては非常に大きな貢献のようだ。（私はまだSeparation Logicについては全然理解できていないが・・・）
ISWIMベースの言語の最古参の一つであるGEDANKENの開発者でもある。
Reynoldsの功績に関しては2013年に亡くなった時に出た追悼論文に詳しい。
