System F

日曜日までお腹下して家でお休みしてました。カンボジアでなんかくらったらしいです。でも、もう治った(気がする)。胃腸の弱い僕だが、これくらいですんでよかった。白湯で乗り切りました。(いつものことだが)

System F は、いつもの難しい話ですが。といっても、System T みたいに、再帰で自然数やリストの計算をするみたいな話で簡単って言えば簡単。電卓っぽい。

System F は、二階の型付きλ式にエンコードしていくのですが、これが、

C++ の template
Java の Generic

とかと、そっくり。True / False とかは、Smalltalk 方式で、True にブロックを投げると eval ってくれるみたいな感じです。

Prolog の unification だけで、再帰抜きにプログラミングしていくみたい、と言っても誰もわからないか。λをfunctorで書いて eval を書くあれです。

そんな感じで、シェムリアップにいる間に、ほとんど Agda で書いちゃったんですが、結構、癖があるな。論文には「これで何でも書ける」的に書いてありますが、関数の組み合わせとかに制約が多くて大変そう。

まぁ、でも、だいたいの感じはわかりました。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/45130bd669ca/system-f.agda