動的メソッドを扱うオブジェクト指向言語の型システム

点击翻译按钮获取中文摘要

今年度は多相型を制約として表す型システムおよびその型推論アルゴリズムに関して研究を行った。多相型システムとは、一つのメソッドあるいは関数を、複数の異なる型に対して適応することを許すような型システムを言う。多相型についてはよく研究されてきており、通常のプログラミング言語における多相型の型推論アルゴリズムについてもよく知られている。しかしながら、この研究のテーマとなっている動的メソッド呼び出しのためには、従来のアルゴリズムでは不十分である。なぜなら、従来のアルゴリズムでは、多相的なメソッドの型はそれが実際に使われる前に決定していなければならないからである。動的メソッドの型は実行時に初めてわかるので、このような状況を仮定するのは困難である。本研究ではこの問題を、多相的な型付けを制約として表すことで解決できることを示した。すなわち、型推論時にはメソッドのもつ多相型とそれが使われる時の型が充たすべき関係を制約式として生成し、メソッドが実際に使われるときに型が制約を充足するかどうか調べることによって、動的メソッドが多相型を持つことを許すことができる。従来の研究に対する本研究の利点は、制約システムを使うことにより、多相型を含む型システムが完全に宣言的に定義され、そのため型推論も非常に単純な制約生成および制約解消の手続きとして理解できることである。この結果は、いくつかの研究集会などで発表済み/予定であり、雑誌等への出版の用意を進めているところである。また、昨年度独国Saarbrucken大学のMartin Muller氏と行った研究の成果はInternational Journal of Foundations of Computer Scienceに近日掲載予定である。