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

2005 Fiscal Year Annual Research Report

• Project/Area Number: 16700011
• Research Institution: Nagoya University
• Principal Investigator: GARRIGUE Jacques 名古屋大学, 大学院・多元数理科学研究科, 助教授 (80273530)
• Keywords: 多相型 / 部分型 / 抽象型 / 推論的多相性

Research Abstract

本年度は主に抽象型と構造的多相性の組み合わせを調べた.
ML系の言語では抽象型が様々な役割を果している.一つは,データ構造の実装を隠すことである.古くから抽象データ型と言われる概念で,ライブラリーのユーザーにはデータ型の定義を見せずに,それを扱う関数群だけを与える.これによって実装とインターフェースが明確に別れ,丈夫なプログラムが構築できる.もう一つはファンクターの引数として抽象型と関数をもらい,ファンクターの中でそれを利用する.ファンクターを使うときに抽象型に複数の型が代入できるので,この構造が再利用を促す.とても役に立つ二つの機能だが,今までは構造的多相性と混ぜることができなかった.抽象化された型について構造が全く分からないので,それを使えない.プライベート列型という部分的に抽象化された型を新しく導入することで,その組み合わせを可能にした.関数型言語Objective Camlでそれを実装し,PPL2006で報告した.型推論の妨げにならないように配慮した.
この組み合わせは部分型とも深い関係をもっている.データ型の知られている構造を段階的に増やしていけるが,構造がより正確に分かったデータ型がちょうど曖昧なものの部分型(またはその逆関係)になる.その性質を利用して,「式の問題」というプログラミング言語の表現力を測る有名な問題をプライベート列型と再帰モジュールによって解決した.今まで提案されたオブジェクト指向言語を使った解では知られた型の部分型になる抽象型が使われていたが,ここでは再帰モジュールがクラスの役割を果し,プライベート列型が部分型の役割を担う.この解が問題の本質をより忠実に表現していると思う.