A soft-typing system for Erlang

世間ではErlangがはやっているらしいので、なんとなく最近読んだ論文の話でもしてみる。

http://www.erlang.se/workshop/2003/paper/p56-nystrom.pdf

Soft typingっていうのは、このへんの論文から始まる型システムの話で、要するに「動的型付けの言語(Schemeとか)を型検査してみよう！」という話である。このFaganの論文におけるモチベーションは、動的型付け言語のruntime型検査をできるだけ省略したら速くなるんじゃねえの？というもので、Schemeプログラムで5割以上の型検査を省略できる例が紹介されていたりする。

MLやHaskellなんかの型システムでは、型の不整合によるクラッシュからプログラムを守るすべは型推論、つまりコンパイル時の型検査しかないので、確実に型の整合性が取れているプログラム以外はすべてrejectする。一方soft typingでは、実行時の型検査を仮定するので、別に型の不整合が含まれているプログラムでもコンパイルしちゃって大丈夫と言える。この性質は、とても便利で、つまり型システムとしては健全でなかったとしても、あんまり問題がないわけ。もっと言えば、比較的いい加減に型システムを構成しても、それはそれで便利じゃん？とかなんとか実験によって示せれば、それでよかったりする。もうちょっとまじめに言うと、実際には型システムでは上手く取り扱えないプログラムが書かれているわけで、そういうプログラムをちゃんと型付けできる型システムを開発すべく、世の中の研究者達は脳汁を振り絞っているわけだけど、そういう努力をすっきりと忘れて、「どうせランタイムでも型検査やってるんだからうまくいかなかったらいかなかったでそれでOK」とか言っちゃうのがsoft typingという思想。

ちなみに私の研究(Rubyプログラムの型推論)もこのsoft typingの範疇と捕らえて問題ない。

そういうわけで、やっとErlangの話。

この論文で言うところの「型システム」は、日ごろなじみのあるMLとかHaskellとかあるいはJavaとかのトラディショナルな型システムとは全然違って、フロー解析とかしてやがります。個人的には、そういうアプローチにはあんまり興味がないので、正直アルゴリズムとかまじめに読んでない。というか、それは型システムとは言わない。研究のモチベーションも、Scheme処理系を高速化しよう！というFaganの野心的なsoft typingと違って、なんとなく解析してみてバグが見つかればそれでいいんじゃない？みたいな感じだし。なんだろう、この居心地の悪さは。

そういうわけで、この論文としては、内容ではなく形式にいろいろ感じるところがあったのです。

まず、いきなりErlangの説明から始まります。へー、Erlangのレコードって、プリプロセッサやったんやー。みたいな。いやそれ論文としてどうなん？マイナーな言語を対象にして論文書こうとすると、この辺でいきなり躓くということがわかりました。いまさら気づいてももう遅い。

で、結論というか最後のほうのディスカッションがまた酷い。こういう微妙な感じの研究の論文を書くときには、「ほげほげのプログラムを解析してみたら、ふがふがのバグが見つかりました！」とか言うことで提案する手法の有効さを主張するわけです。ふがふがのバグ、は既知のものでも良い。ところが、型エラーで落ちるプログラムなんて、いまどき世の中には存在しないわけで、つまりこういう弱いモチベーションで研究しようとしても、論文を書けません。みたいな話がずらずら書いてある。論文に。Blogとかじゃなくて論文に。

いやまあ、それはよくわかるんですけど、論文に書くなよ。と。

結論なんかありません。

さっきプロファイルとってみたら、List.assocがえらい時間食ってることが判明しました。ListをHashtblに置き換えてみたら、一気に100倍程度の高速化！やったぜ。