関数型言語における多相型と部分型の関係および型推論の強化

本年度は主に抽象的な多相ヴァリアント型の拡張性について調べた.前年度に調べたプライベート列型は構造的多相性と抽象型の間に立ち,多相オブジェクト型や多相ヴァリアント型のファンクターでの使用を可能にした.これによって型システムの表現力が高まり,モジュールを使ったプログラムが拡張しやすくなる.「式の問題」の新しい解を与えることでそのアプローチの有用性も証明できた.しかし,プライベート列型だけでは,抽象的な多相型の和などは表現できない.具体的には,完全に知られている二つの多相ヴァリアント型を与えられたら,簡単にその和が取れて,実際のプログラミングでもとても役に立つ.しかし,どちらかのヴァリアント型が抽象的な部分を持つと,和の無矛盾性は保証できなくなり,和を取ることが簡単にできない.Romain Bardouというフランスの学生と一緒にこの問題に取り組み,互換性という新しい概念を型システムに入れることで,抽象的な多相ヴァリアント型の和を可能にした.抽象的な互換性は完全に調べることができるので,ごく自然な形でプログラムに使える.この互換性の問題が解決されると,型推論の拡張に大きな問題がないので,近い将来にObjective Camlでの実装を目指す.京都大学の中田景子氏とも協力を続け,一緒に自由な再帰を許したモジュールシステムを設計した.MLを拡張した再帰モジュールの提案は既にいくつかあるが,我々のものは二つの面で利便性を向上させている.まず,ほぼ完全な適用性を実現している.適用性がより複雑な構造の柔軟な構築を可能にするが,その代表格であるObjective Camlでさえ部分的にしか実現されておらず,我々の提案は大幅な改善になる.さらに,他の再帰モジュールを許したシステムに見られない型推論機能も実現できた.

本年度は主に抽象的な多相ヴァリアント型の拡張性について調べた.前年度に調べたプライベート列型は構造的多相性と抽象型の間に立ち,多相オブジェクト型や多相ヴァリアント型のファンクターでの使用を可能にした.これによって型システムの表現力が高まり,モジュールを使ったプログラムが拡張しやすくなる.「式の問題」の新しい解を与えることでそのアプローチの有用性も証明できた.しかし,プライベート列型だけでは,抽象的な多相型の和などは表現できない.具体的には,完全に知られている二つの多相ヴァリアント型を与えられたら,簡単にその和が取れて,実際のプログラミングでもとても役に立つ.しかし,どちらかのヴァリアント型が抽象的な部分を持つと,和の無矛盾性は保証できなくなり,和を取ることが簡単にできない.Romain Bardouというフランスの学生と一緒にこの問題に取り組み,互換性という新しい概念を型システムに入れることで,抽象的な多相ヴァリアント型の和を可能にした.抽象的な互換性は完全に調べることができるので,ごく自然な形でプログラムに使える.この互換性の問題が解決されると,型推論の拡張に大きな問題がないので,近い将来にObjective Camlでの実装を目指す.京都大学の中田景子氏とも協力を続け,一緒に自由な再帰を許したモジュールシステムを設計した.MLを拡張した再帰モジュールの提案は既にいくつかあるが,我々のものは二つの面で利便性を向上させている.まず,ほぼ完全な適用性を実現している.適用性がより複雑な構造の柔軟な構築を可能にするが,その代表格であるObjective Camlでさえ部分的にしか実現されておらず,我々の提案は大幅な改善になる.さらに,他の再帰モジュールを許したシステムに見られない型推論機能も実現できた.