Type-Based Analyses - sumiiのブログ

ちょっと前に「subtypingはプログラム解析でも有用」みたいなことを書きましたが、たとえば（やや古いですが）

http://www.cs.ucla.edu/~palsberg/tba/

にあるような、型を応用したプログラム解析（type-based analysis）のことです。これは何かというと、単に"int"や"float"みたいな型だけでなく、

「（ヒープではなく）スタックに確保できる配列」 $int~array^{stack}$
「自由変数がないのでclosureが不要な関数」 $int \to^{nofv} int$
「メモリ領域ρに格納されているfloat」 $float^\rho$
「一回だけ呼び出される関数」 $int \to^1 int$
「外に漏らしてはいけない（high security）文字列」 $string^H$
「好きなだけreadして、それから必ずcloseしなければならないファイル」 $FILE^{read* ; close}$

みたいな感じで型を拡張して、プログラムのいろいろな性質を解析・検査しよう、というアプローチです。（上の型の書き方はテキトーです。）これらの型は、自分で指定したい場合以外、勝手に推論してもらうこともできます。

で、subtypingがあると、unification（＝の関係）のかわりにinclusion（⊆の関係）によるフロー解析ができるので、精度が向上します。というか、subtypingがないと荒すぎて使い物にならないケースも少なくありません。どういうことかというと、たとえばf(x)=eみたいな関数定義があったとして、f(e1)とf(e2)みたいに二つの関数呼び出しがあるとします。「xの型とe1の型とe2の型はすべて完全に一致しなければならなない」というかわりに、「xの型は、e1の型とe2の型を包含していれば良い」とすることによって、e1とe2を混同せず解析できるようになります。

もちろん、subtypingではなく（parametricな）polymorphismで精度を向上する研究もたくさんあります。