2004 Fiscal Year Annual Research Report
関数型言語における多相型と部分型の関係および型推論の強化
| Project/Area Number |
16700011
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
GARRIGUE Jacques 名古屋大学, 大学院・多元数理科学研究科, 助教授 (80273530)
|
|---|
| Keywords | 多相型 / 部分型 / モジュル / 関数型言語 |
|---|
| Research Abstract |
本年度はいくつかの観点から多相型と部分型の関係を追求して来た.
値多相性の緩和
値多相性を緩和する方法をFLOPS2004で発表した.その方法はObjective Camlで実装されている.そのときには,型定義における型変数の共変性が重要な問題になるが,それをさらに解析することになった.元々共変性は定義が与えられている型についてのみ考えられていたが,共変性を明示することによって抽象型にも書けるようにした.共変性が明示しなければならない場合が他にいくつかある.例えば,型変数が型の定義の中に出現しない場合,その共変性を推論することができない.特に,型制約によってその型変数が出現している変数と関連付けられている場合,ただし共変性の指定が健全性のために必要になる.
ファンクターと部分型
MLの多相性は通常,型変数によって表されるが,型を引数として取るファンクターも同じ力をもっている.特にStandard MLの場合では,多相性を使った全てのプログラムはファンクターのみ(型変数なし)で表現できることが知られている.Objective Camlでは部分型に似た特別な構造を持った多相ヴァリアント型やオブジェクト型があるので,それが不可能になっている.その型に秘められた列変数を抽象化できるようにすることで,Standard MLよ同じ性質に近付けている.面白いことに,この抽象化がScalaなどが持っている抽象部分型と同様の利用ができる.
ファンクターと部分型と再帰
中田恵子氏と伊藤徹氏との共同研究で,再帰を含んだモジュールシステムでの部分型関係の清楚な定義を調べた.FOOL2005に報告されているように,清楚性を保証するためにモジュールシステムに関して自明でない性質を調べなければならない.この問題は型変数による多相性とは一見無関係に見えるが,ファンクターの扱いが難しいことからやはり多相性と再帰に関連性を試すものでもある.
|
