Introduction to type inference

by syoyo

JS 実装をしようかな、と思い立ち、
まずは型推論の知識をしっかり取得するところから初めようと考えています.

そもそも、型推論とはなんぞや、というところからおさらいしてみます.

私が型推論について知りたいことの一番の目的は、
「型推論を行うことで動的言語の事前コンパイルを可能にしプログラムの実行を早くすることができるのではないか」,
ということになりますので、それに特化した内容になっています.
もちろん型推論には、プログラムを早くするという以外の目的もありますが、
ここではそれらは取り上げないことにします.

型推論(type inference)とは、簡単に言うと、


var muda = 7

というコードがあったら、

「変数 muda って Int 型(整数型)じゃね?」

とコンパイラがよろしく変数の型を決定してくれる(推測してくれる)機能になります.

静的な関数型言語(Ocaml, Haskell)などでは、変数(関数)には型を通常プログラマが指定しませんが、コンパイラが型推論を用いて型を割り付け、文法にエラーが無いかの判断などに使ったり、最適なアセンブラコードの選択に使ったりします.

動的言語でも、この型推論を行うことで、実行時にエラーが起きるようなスクリプトを、あらかじめ実行前にエラー判定したり、実行前に型が不変であることが分かれば事前にコードパスを特定の型に特化してコンパイルすることで、実行時の処理速度を上げることができます.

たとえば,


def muda(a):
  print a

muda(10)

というようなスクリプトがあった場合、muda() 関数の引数 a の型は int しかとらないことが分かるので、int に特化したネイティブコードをあらかじめスクリプト実行前(JIT コンパイルでもよし)に生成することができます.

型推論のアルゴリズム

では実際に、型推論ってどうやればいいのでしょうか?
推論っていうくらいだから、なにか AI みたいなことをするのでしょうか?
(実はしません)

ひとまず型推論のアルゴリズムについて調べてみました.

Hindley-Milner

関数型言語向けでは、Hindley-Milner のアルゴリズムが基本になるそうです.

Damas, Luis & Milner, Robin (1982), “Principal type-schemes for functional programs”, POPL ’82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, pp. 207–212.
http://groups.csail.mit.edu/pag/6.883/readings/p207-damas.pdf

イメージとしては再帰的に式をたどって型を割り当てていく感じ?
py2llvm で実装した型推論の方法と似ているかな?
(こういう車輪の再発明なことをして時間の無駄をしたくないから、既存研究を調べるわけです.
先人たちのほうがきちんと sophisticate された体系としてまとめてくれているわけですから)

CPA

オブジェクト指向言語向けには、CPA と呼ばれる Cartesian Product Algorithm から入っていくのがよさそうです.

http://research.sun.com/self/papers/cpa.html

イメージとしては、取りうる型の組み合わせをどんどん狭めていってひとつの型を導きだすという感じでしょうか.
たとえば最初は変数 muda は [String, Number, Boolean] のいずれか、とセットアップしておき、
いろいろ周りの状況をみて候補を絞っていって、 muda : Number とするような感じ?

Java や JavaScript(?) の基礎になった Self 言語の型推論エンジンとして使われたという実績があります.

また、Starkiller と呼ばれる Python 向けの型推論にも使われているアルゴリズムです.

http://salib.com/writings/thesis/thesis.pdf

DDP

オブジェクト指向言語向けにもう少し発展した型推論として、DPP というアルゴリズムがあります.

DDP: Demand-Driven Analysis with Goal Pruning
http://www.lexspoon.org/ti/

SmallTalk の型推論向けに開発されました.
DDP は CPA よりも、大規模なプログラムに対してスケールしやすいことを挙げています.

DDP ベースの型推論を Ruby に組み込もうとした SoC があり、
http://soc.jayunit.net/
成果は Ruby 向けコード補完として Aptana に取り込まれたそうです.
(ところで、この SoC プロジェクトのメンターだったのは Chris Williams なのですね.
JDK6 の JIT を書いたひと. いろんなところでつながっているんだなぁ.)

まとめ

JS 実装という観点からは、まずは CPA からいろいろ調べていくとよさそう.

Advertisements