制約に基づく汎用型推論モジュールの研究

Research Project

Project/Area Number	12780216
Research Category	Grant-in-Aid for Encouragement of Young Scientists (A)
Allocation Type	Single-year Grants
Research Field	計算機科学
Research Institution	Kyoto University
Principal Investigator	西村進京都大学, 数理解析研究所, 助手 (10283681)
Project Period (FY)	2000 – 2001
Project Status	Completed (Fiscal Year 2001)
Budget Amount *help	¥2,600,000 (Direct Cost: ¥2,600,000) Fiscal Year 2001: ¥1,400,000 (Direct Cost: ¥1,400,000) Fiscal Year 2000: ¥1,200,000 (Direct Cost: ¥1,200,000)
Keywords	型推論 / 多相型 / 制約解消 / 制約
Research Abstract	型推論は、プログラム中に潜むエラーを実行前の段階で捕捉するための重要な技術である。しかし、従来の型推論のアルゴリズムは、対象とする個々の型体系に対して与えられ、しかもそれは型体系がより豊かになればなるほど複雑になる傾向にあった。とくに、多相型を含む型体系において、多相型の型推論を一般的に記述する方法が求められていた。このような問題を解決するため、Odersky, Sulzmann, Wherらは、制約系をベースとしたより一般的な型体系の枠組みであるHM(X)を提案した。しかしながら、HM(X)では、多相型の型付けは制約系によっては特徴づけられていなかった。本研究では、Odersky, Sulzmann, Wherらの研究をふまえ、多相型の型付けをも制約系によって特徴づけするような、型体系を記述する一般的な枠組みを提案した。この枠組みの中では、適切な制約系とその制約解消器を与えれば自動的に型推論アルゴリズムが得られる。この枠組みのなかでは、多相型の型付けを表す汎用的な制約が導入され、この制約を解くことにより型推論を行うことができる。この汎用的型推論の枠組みにおいては、型推論はより柔軟な多相型の使用を可能にする。例えば、分散アプリケーションやトップダウンのプログラム開発など、必ずしも型の定義が先に得られないような場合でも、多相型を扱うことができるようになる。これらの結果を著した論文は、日本ソフトウェア学会学会誌に採録された。