| 研究概要 |
本年度は、研究課題の理論的な側面、特に、多相型の型付けの規則を制約として表し、その制約を解消することによって型推論を行うための一般的な枠組みについて研究を行った。
単相型の型推論については、自然に制約解消の問題に還元することができることが知られているが、多相型に関しては、それを制約を用いて一般的な枠組みの中で表現する方法についてはあまりよく知られていなかった。Odersky,Sulzmann,WherらによるHM(X)がそれに非常に近いものとしてあげられるが、残念ながらHM(X)においては、多相型の型付けは制約式を多相的な型の使用毎にコピーする方法をとっており、多相型の型付け規則を制約の形で表しているわけではない。そのため、HM(X)においては多相型の定義が必ずその型の使用前になければならない。これは、例えば分散アプリケーションやトップダウンのプログラム開発など、必ずしも型の定義が先に得られないような場合に大きな問題となりうる。
本年度の研究では、Hengleinのsemi-unificationを用いた多相型推論の計算量の解析手法からヒントを得て、多相型の型付け規則を制約として表した汎用的な型推論のための枠組みを与え、上記の問題を解決し、また型推論の正しさも証明した。この研究成果は、日本ソフトウェア学会第2回プログラミングおよびプログラミング言語ワークショップで発表され、日本ソフトウェア学会学会誌コンピュータソフトウェアに掲載予定である。
|
