Lax Trans formationを用いたPolymorphismの意味づけ

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

総称関数とは、複数の引数の型に対して適用可能な関数のことである。型つきのオブジェクト指向言語の動作を、総称関数を用いて表現し、その性質を調べ、新しい言語の設計に対する指針を与えようというのが、この研究の目標である。そのような計算として、λ-mergeや、オーバーロードの機構を改良し、Lax Transformationに対応する動作をするものに制限したλmについて研究してきた。λ-mergeのオーバーロードの機能は、一種のアドホックな多相(Polymorphism)と考えることができる。この多相では、どの型に対しても統一的な動作をするパラメトリックな多相に対応したものは表現できなかった。このことは、遅延束縛を表現できないことを意味し、オブジェクト指向に対応する型システムとして用いるための、大きな障害となっていた。そこで、オブジェクト指向に対応するλ-mergeの部分計算に型変数を導入し、パラメトリックな多相を表現できるようにすることにより、遅延束縛の動作を表現できる計算を考えた。ここでは、全ての型が、exactに表現されており、オブジェクト指向に対する静的解析、プログラム変換などへの応用が期待される。型変数をレコードに制限し、また、高階な関数の利用も制限したため、string Normalizationが成り立ち、自然なファンクタによる領域の上で意味を与えることができる。この結果については、Workshopにおいて発表を行なった。