レコード多相性の理論

レコード多相性を可能にした理論である.

歴史的背景と文献


内容に関するお断り:本ページの文責は,大堀淳にある.ここに示された見解や解釈等はSML#開発チーム全体を代表するものでは必ずしもない.不正確な表現や見方の責は大堀淳にある.

論文の著作件に関するお断り:The documents made available in this page are the author's verisons of published articles. They are included here by the author as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


レコード多相性を持つレコード演算を実用言語に導入するには,レコードオペレータの型に関する理論とそのコンパイルに関する理論を完成させる必用があった.SML#が基礎とする型に関するレコード多相性の型理論の原型は1988年に発表された以下の論文である.

この論文は,前年に発表されたWandの(不完全な*1)レコード計算の理論とは異なる,「型変数に制約を付ける」という考え方を基礎とし,レコードばかりでなく,データベース演算をも表現可能な型システムと型推論アルゴリズムの理論を提示している*2.これは,現在のOCamlが基礎とするRemyの理論の原型(POPL 1989)などとは独立(かつ時間的に前の)ものである.

さらに,以下の論文で,この型変数の制約の考え方をレコードのみに限定し型理論を洗練し,型情報を利用しレコード演算のコンパイルを行うという考え方に基づくコンパイル理論を提案した.

これをバリアントを含むより体系的な理論として完成させたのが以下の論文である.

SML#の多相型レコード演算は,ここに提示された型システムとコンパイルアルゴリズムをほぼ忠実に実現したものである.

理論の概要

MLにレコードを導入するには,(1)MLの多相型システムの拡張と(2)レコード式のコンパイル理論の構築の二つが必用である.以下それぞれの概要を説明する.

レコード多相性の型理論の概要

レコード多相性の型推論を理解するために,まず,MLの多相型推論の基本的な考え方はを振り返っておこう.

1. プログラムの(すべての各部分式の)型を,とりあえず,それぞれ「なにか分からない型」を表す変数'A,'B,...と置いていく.

val f = fn (x:'A) => fn (y:'B) => (x : 'A, (y : 'B + 1) : 'C) : 'D

2. プログラムの部分間の関連によって,各型変数に関する制約を等式として書出し,解く.

'B = int
'C = int
'D = 'A * 'C

3. その結果を代入し,主要な型を求める.

val f : 'A -> int -> 'A * int

4. 最後まで残った型変数'Aは,何も制約も付かに「どの型でもよい」型であるから,多相型に昇格させる.

val f : ['a. 'a -> int -> 'a * int]

この過程は,論理学の以下の全称命題の推論法則に相当する.

P(x)がxに関して何の制約も付かずに証明できるなら,(∀x)P(x)が証明できる.

しかしこのこの考え方だけでは,ある特定のラベルを持つレコードに対してだけ多相性を持つレコード演算 #name は表現できない.演算 #name を表現するためには,「name を含むレコード型の中でなにか分からない型」を表す変数があればよい.そこで,この演算を,「種類制約付き型変数」を用いて,以下のように型付ける.

 #name : ('A::{name:'B}) -> 'B

ここで,'A::{name:'B} は型変数であるが,何か分からない型を表す通常の型変数と異なり,「フィールド name:'B を含むレコード型の中で何か分からない型」を表す.

MLの型推論ステップの2の制約を書出していく所で,以下のようにこの種類制約も同時に書出していけば,レコード多相性を反映した主要な型を推論できる.

1. プログラムの(すべての各部分式の)型を,とりあえず,それぞれ「なにか分からない型」を表す変数と置いていく.

val f = fn (x:'C) => ((#name: ('A::{name:'B}) -> 'B) (x:'C)) : 'D

2. プログラムの部分間の関連によって,各型変数に関する等式制約と種類制約を書出し解く.

'C::{name:'B}
'C = 'A
'D = 'B

3. その結果を代入し,主要な型を求める.

val f : 'A::{name:'B} -> 'B

4. 何も制約も付かに最後まで残った種類付き型変数'Aは,「種類制約の範囲でどの型でもよい」と考え,種類付き多相型に昇格させる.

val f : ['b,'a#{name:'b}.'a -> 'b]

多相型レコード演算のコンパイル理論

以上の種類付き型変数を使ったレコード多相性の型理論を応用すれば,多相型レコード演算を効率よいコードにコンパイルする方式を導くことができる.

この問題を理解するために,まず,Cのレコード演算を考えてみよう.

typedef struct {char * address; char * name;} person;
char * name(person P) {
  return (P.name);
}

Pはaddressとnameをメンバーとするレコード(構造体)であり,P.nameはレコードの中のnameフィールドの取りだしである.コンパイラは,nameのオフセット位置を自動的に計算し,((char **)P)[1] のような効率よいコードを出す.ここで,1はnameフィールドの先頭からのワード数である.多相型を持たない言語では,このようなコンパイルが可能であり,この性質により,レコードは効率よい基本データ構造として使われている.

しかし,多相型言語であるMLでは,

fn x => #name x

のような関数は,定義した時点ではレコードの中のnameフィールドの位置が不明であり,効率よいコードへのコンパイルができない.Lispなどの静的型を持たない動的な言語でも同様な問題がある.動的なスクリプト言語などでは,レコードのフィールド文字列を実行時まで取っておき,実行時にnameフィールドをサーチするという方法が取られることが多いが,そのような方式では,レコードを使用したプログラムの効率よい実行は望めない.

上記論文(POPL1992,TOPLAS1995)では,型を推論すると同時に,その型推論の過程で得られる型情報を利用しコンパイルを同時に行うという考え方を提唱し,この問題を解決した.

1.まず型を計算する.

val name = fn (x:'A::{name:'B}) => #name (x: 'A#{name:'B})

2.フィールド取りだし演算を配列のオフセットアクセス演算x[i]にコンパイルする.その際,オフセットが不明であれば,そのオフセットを表す仮引数を導入し,その型を記録する.

val name = fn (I:offset('A::{name:'B}, name)) =>
              fn (x:'A::{name:'B}) => (x : 'A::{name:'B})[I]

3.多相型に昇格させ,追加した引数の型を含む多相型を記録する.

val name : ['b, 'a::{name:'b}.offset('a,name) -> 'a -> 'b]

ここで,offset('a,name)は,型'aのフィールドnameのオフセットを表す型である.

4.この関数を適用する際,コンパイラが追加した引数を補う.

この過程を

name {address = "Katahira 2-1-1", name = "Atsushi"}

を例にトレースしてみる.

4.1 まず,この適用における多相関数nameの型を計算する.

name : offset({address:string, name:string},name)
         -> {address:string, name:string}  -> string

4.2 多相関数が使われている具体的型から,挿入すべき追加引数を決定しその値を計算する.この例の場合,最初の引数は,その型offset({address:string, name:string},name)から,コンパイラが挿入した引数であることが分かる.さらに,この型の持つ値は{address:string, name:string}レコードの中の.nameフィールドのオフセット位置,つまり1であることがわかる.そこで,以下のようなコードを生成する.

name  1 {address = "Katahira 2-1-1", name = "Atsushi"}
Last modified:2011/06/25 17:31:03
Keyword(s):
References:[SML#の理論的基礎] [ランク1多相性の理論]

*1 その技術的に正確な意味は上記論文および以下を参照Wand, M,Corrigendum : Complete type inference for simple object. Proc. LICS, 1988.

*2 大堀による注釈:なお,この論文は,私が初めて書いた,従って当然ながら初めてrejectされた,国際会議論文である.ちなみに「当然ながら」は「rejectされた」に係る.さらにちなみに,その最初の投稿先はLICS 1988である.この時の,その大部分を私がこころから尊敬するプログラム委員会メンバーはProgram Chair:Yuri Gurevich, Program Committee:M. Dezani; J. Halpern; G. Huet; C.A.R. Hoare; P. Kanellakis; J.-L. Lassez; J. Mitchell; R. Platek; G. Plotkin; S. Rosenschein; A. Sistla; J. Tiuryn; M. Wand である.味わい深い.