Route 477

■ [types] 型推論のある言語作った

まだλ計算に毛が生えたようなものなので、Hello Worldくらいしか動かないですが。

https://github.com/yhara/boom

TAPLを読んだからには*1静的型付け言語の一つでも作らなければならないと思って、とりあえず動くとこまで実装した。Boomという名前は適当に付けたのであとで変えるかもしれない。 最初はTAPLのfullreconをベースにしようと思ったのだけど、動かしてみたらこいつは多相型が実装されてなくて(練習問題になってた)、pi8027さんのtypeinferをベースにすることにした。

動かし方

Ruby 2.1が必要*2。

 $ git clone https://github.com/yhara/boom
 $ gem i bundler
 $ bundle install
 $ bundle exec rspec
 $ echo 'print("hi")' | bundle exec rake run
 hi

これだけだと型推論どこ？っていう感じですが、以下のようにするとちゃんとエラーが出ます(printはstring -> stringなのにintを渡してるので)。

 $ echo 'print(1)' | bundle exec rake run

参考文献

以下はいずれもHindley-Milnerという、MLやHaskellで使われている型推論の仕組みを対象としている。

4274069117

いわゆるTAPL。PDF版もある。高いけど、この本が母国語で読めるのは幸せなことだと思う。

型にまつわるいろんな仕組みの話が出てくるけど、型推論の話は22章のみ(つまり必ずしも全部を読破する必要はない。序文ix参照)。

4781912850

10章が型推論の話。

• https://github.com/pi8027/typeinfer

アルゴリズムWの解説と、OCamlによる実装。

• http://d.hatena.ne.jp/takuto_h/20110401/ibis

JSによる実装。

• https://sites.google.com/site/scalajp/home/documentation/scala-by-example/chapter16

Scalaによる実装？(これは後から見つけたので読んでいない)

感想

型推論というとrocket scienceなイメージがあったけど、実際にはコアの部分は80行程度しかない。 各文献はだいたい数学的な記法で書かれていて読むのが大変だったけど、ibis-rb、tapl-ruby、boomと似たようなものを3回移植したらなんとなく分かってきた気がする(まだ分かってないとこもあるけど)。

今後の予定

気分が続けば機能を足すかも？