PMTT本など

基本的に毎日やったことを、日付が過ぎても書いておくことにする（いまこれを書いてるのは金曜日）。そのほうが精神的に落ち着く。

水曜日は午後から来客があった。木曜日は特に何にもなかったような気がするが家に帰った16時以降やることがいろいろとあって、2日ともそんなに作業はしてない。が、火曜日に引き続いてPMTT本*1の読解。

PMTT本をざっと読んでいて思ったが、結局のところ型理論自体はΠ-typeとΣ-typeという２つの型があることが特筆すべきである以外は、そんなに「これは難しくて意味不明」な内容はない気がした。圏論の本みたいには。

結局のところ型理論というのは、型というのがあって、これとこれからはこの式が導出できますよ、というjudgement form（判断形式、とでも訳すのだろうか。いろいろググってもわからん）がある、以上。というものなのではないかと思う。*2

ぼくが最近読んでいた論文というのは、そのMartin-Löf型理論をインタラクティブなプログラムに適用するとどうなるか、という話で、型理論のちょっとした応用？みたいなことである。ので、PMTT本をめっちゃ読みこんでも新しいネタは出てこないような気がした。あくまでも基礎の積み上げである*3。

今日はこのあと関数型言語とは何か、というのをもうちょっと実感をもってつかめるようにOCamlで遊んでみる予定。

*1:Programming in Martin-Löf's type theoryのことをこう呼ぶことにする

*2:まだ理解が浅いので間違っているかもしれない

*3:それが大事なのは間違いないのだが