「Featherweight Javaのための漸進的型付け」を読む

• http://www.nue.riec.tohoku.ac.jp/ppl2008/program.html より
  • http://www.nue.riec.tohoku.ac.jp/ppl2008/proceedings/1-09.pdf

「漸進的型付け」というのはgradual typingのこと。Top Type(意味的には、全オブジェクトの具体クラスとして成り立つ型とでもいえばいいかな)である?型を導入した型システムのこと。

この論文で定義してるモデルFJ?はFeatherweight Javaをそれで拡張したもの。

Featherweight Javaは、メソッドの中が１つの式のみで、メソッドは引数と戻り値が必ずひとつづつある、などで制限したJavaの意味論モデル。そのGenericsバージョン(同一論文)は、Java 5のGenericsの意味論にもなっている。

Siek氏が、STLC（単純型付ラムダ計算）やその後のECMAScript風オブジェクトシステムに対して行ったやり方とほぼ同様で、?型に対しては推移律を持たないconsistencyでのみ対処している。またサブタイプ関係が成り立てばconsistencyでもある。

FJへの追加ルールは、

• ? は何でもキャストできるし、暗黙的にキャストもされる
• ? はどんなフィールドでも呼べ、その型は?
• ? はどんなメソッドでも呼べ、戻り値の型は?

直感的には、?を境界に構文的に型整合性が取れる(明示的に？でない型がついてる部分は型安全で、?のところは実行時キャストが正しければ正しい、という意味になる)、という感じ。

サブタイプ関係もextendsでの関係のみで、

• http://ece-www.colorado.edu/~siek/gradual-obj.pdf

のような、オブジェクトの構造を見るところまでは入っていない(FJのサブクラス関係の仕様上というのもあるだろう)のでかなりシンプルなルールになっている。

さらに、このFJ?を、全体的に型安全なFJreflに変換する。FJreflは、(構文的に解決できる)リフレクション機能をつけたFJの拡張構文。FJ?からFJreflへの変換は、FJな部分はほぼそのままで、FJ?の?が絡む部分の部分を、FJreflのリフレクションを使ったプログラムに（型チェックつきで）変換するものになっている。

FJreflは静的にリフレクションコードの整合性をチェックする。とはいえ、安全性を保持するには、FJreflの構文チェックから、そのコードの実行までの間で、クラスメンバーが変更されない必要がある。そのため、Java的に考えればクラスロード時のチェック手段のひとつにできる。

関連研究を知っていれば、内容的にはわかりやすいが、よくまとまっていると思った。