TAPLを見てます。
コンパイラを作るには型理論を理解しているとよいそうなのでTAPLを読んでいます。最初からまじめに読もうとすると反射的に眠くなって駄目です。難しい。大学の時の代数学とかを思い出します。大学の時に勉強した数学は苦手ですっかり忘れてしまいました。かといって読まないと進まないので理論的な所は飛ばして全体的に何を書いてあるのかを先に把握しようとしています。評価戦略でいうと、call by need、必要になったら読みます戦略です。理論は必要になったら読みます。良く言うとトップダウンで見ていこうとしているわけです。
まず、目次を眺めたりパラパラ本をめくって何かいてあるかだけ摘み読みしているうちに眠くなって寝ました。次に何度も例えると第何部はCの実装みたいな物みたいに例えてみました。6部構成で32章あるということを覚えて寝ました。小さい体系からだんだん大きくして行っていて、最初に理論があり実装する事を繰り返している事が分かりました。ソースもWebサイトにある事も分かりました。インターネットで探すとScalaの実装も見つかって寝ました。
とにかく、眠いです。うーむ。眠い。笑。受け入れがたい事だらけなので眠いんだろうと思います。もう、すぐ拒絶反応が起こるんで大変です。寝て脳内GCして受け入れて、ちょっと進んで拒絶反応が起きて、寝てGCして、受け入れてっていう事の繰り返しなのかなと思います。
次にScalaのソースを拾ってきました。意味も分からず動かしてみました。動かしかたは分かったので寝ました。次にScalaのソースを１つずつ把握しながら動かしてみています。そして、ソースをちょっとだけ弄ってコンパイルし直して動くのをみたり、exampleのプログラムを書き足して理解を深めたりしています。ちょっと進んで、すぐ休憩です。
実装出来たからと言って理解したとは限らないんですけど実装が分かればかなり理解が進んでいると思えるはずです。現状はarithとuntyped,fulluntypedの実装が80%くらい分かった感じです。
1. arithが算術式
2. untypedが型無しラムダ計算
3. fulluntypedが型無しラムダ計算にifとかletとかrecordとかstringとかを加えたもののようです。
4. tyarithが型付き算術式
5. simpleboolが型付きラムダ計算
6. fullsimpleが更に色々加えた型付きラムダ計算
7. fullrefがfullsimpleに参照を加えた型付きラムダ計算
8. fullerrorがsimpleboolにエラー処理付きな型付きラムダ計算
:
23. fullfomsubref Scala版では最終ボス
26. fullupdateがたぶん本当の最終ボス
fomega,letexercise,joinexerciseはおまけ？
という感じで、全部でsbtで動かせるソースが21個ほどあります。どれもインタプリタの実装なのでコンパイラを作るのに比べれば簡単です。（それでも難しいですけど）
１章を読んで、全てを理論的にゼロから構築して行った美しい世界と、なんとなく実装した物とは違うってことは分かりました。理論的に積み上げた物は、正しく動く事が証明できていればバグが無い事が明らかなので、100%安心と言える訳です。
だから、SMLのほうが仕様が決まっていて標準化もされているので安心だ。OCamlは仕様も良くわからないので信頼できない。という主張も分かる気がしました。OCamlも仕様を明確にして標準化することは可能でしょうから別にOCamlが駄目とかではないのですが、発展途上であれば仕様を明確にするより新しい機能を追加して試して、よりよい物に近づけていく事も必要なはずです。高速に動く事の方が重要だったりもします。
三角関数を回転するアニメーションを作って覚えたように、理論的な事も何かしら実装をしながら理解したいところです。ところが三角関数を使えばいいっていう単純な話ではなくて、三角関数をどう考えたかみたいなレベルの話をプログラミングするってことは、普通のプログラミング言語では難しそうです。
Coqという言語を使うと理論を実装しながら勉強出来そうです。なのでTAPLの実装をみながら、同時並行でCoqを勉強してます。TAPL脳とCoq脳は別な領域を使えるようなので、たぶん、学習効率がいいんです。
TAPLをCoqで理解するようなもの無いのかとググってみると「定理証明支援器「Coq」によるプログラミング言語理論の定式化チュートリアル」というものをPOPLの2008年に併設されていたそうです。参考にするといいのかもと思いましたが、実装は分かっても理論もCoqも英語も分からないので難しすぎました。残念
http://d.hatena.ne.jp/sumii/20080109/p1
日本語に翻訳されているCoqでラムダ計算まで勉強出来るサイトを見つけたのでそちらを先にやってから、TAPLに戻ってくれば、分からないのは英語だけになるのでずっと楽に読めるのではないかと思います。
http://proofcafe.org/sf/
いきなりCoqでラムダ計算もしんどそうです。Coqだけとりあえず入門するだけのほうが無難かもしれません。
http://www.iij-ii.co.jp/lab/techdoc/coqt/
ああ、でも、Coq覚える事多すぎるー。（泣）頭悪いといろいろ大変ですが、急がば回れなんだなぁ。素直に読んだ方がずっと早い気もしてきます。Coqは理論を実装しながら覚えられそうなのは魅力なので頑張って覚えようと思います。
ということで、TAPLは非常に読む環境も整っていて素晴らしいと思うのですが、普通のプログラマに取っては、まだまだ、難しいと思うのでした。
こんなん、なんで理解出来るだよ。頭おかしいよ。と思うのでした。
