お茶の水大学 Agda Implementers Meeting

お茶の水大学は久しぶりだが、何回か行ったことがあります。

一階上が伊藤先生の研究室なので、噂の扉を見に行きましたが、本人にも会えました。

　　「So, what do you want to do in code splint?」
...
「Me?」

え、僕から? copy term みたいなのが欲しいとか言ったんですが、Andreas　「どれ、見せてみろ」というので、

　　System F の実装を復習

する羽目に。Andreas 超親切。

Parametricity がどうとか言ってましたが、やっぱりできないらしい。Church Calculus とかいうらしいんですが、
どうも、同じ問題をやっていた人がいるらしく、変数を入れ替える型推論を入れるらしい。なので、簡単にはできないらしいです。

Code Split って、ハッカソンみたいなものなのね。時間、結構あるので、もう少し Agda の中身を見てみようかな。