SML# - Foundations/010 Diff

  • Added parts are displayed like this.
  • Deleted parts are displayed like this.

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

!! 歴史的背景と文献

----
内容に関するお断り:本ページの文責は,大堀淳にある.ここに示された見解
や解釈等は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年に発表
された以下の論文である.
* [[Atsushi Ohori and Peter Buneman. ''Type Inference in a Database Programming Language'', Proc. ACM Conference on LISP and Functional Programming, pages 174-183, Snowbird, Utah, 1988.|http://www.pllab.riec.tohoku.ac.jp/~ohori/research/lfp88.pdf]]
この論文は,前年に発表されたWandの
(不完全な{{fn('その技術的に正確な意味は上記論文および以下を参照
[[Wand, M,Corrigendum : Complete type inference for simple object. Proc. LICS, 1988.|http://www.lfcs.inf.ed.ac.uk/events/lics/1988/Wand-Corrigendumcomplete.html]]'}})
レコード計算の理論とは異なる,「型変数に制約を付ける」という考え方を基
礎とし,レコードばかりでなく,データベース演算をも表現可能な型システム
と型推論アルゴリズムの理論を提示している{{fn("大堀による注釈:なお,こ
の論文は,私が初めて書いた,従って当然ながら初めて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 |http://www.lfcs.inf.ed.ac.uk/events/lics/1988/index.html#organisers]] である.味わい深い.")}}.
これは,現在のOCamlが基礎とするRemyの理論の原型(POPL 1989)などとは独
立(かつ時間的に前の)ものである.

さらに,以下の論文で,この型変数の制約の考え方をレコードのみに限定し型
理論を洗練し,型情報を利用しレコード演算のコンパイルを行うという考え方
に基づくコンパイル理論を提案した.
* [[Atsushi Ohori. ''A compilation method for ML-style polymorphic record calculi.'' Proc. ACM POPL Symposium, pages 154-165,1992.|http://www.pllab.riec.tohoku.ac.jp/~ohori/research/ohor92popl.pdf]]
これをバリアントを含むより体系的な理論として完成させたのが以下の論文である.
* [[Atsushi Ohori. ''A polymorphic record calculus and its compilation.'' ACM Transactions on Programming Languages and Systems, vol 17, no 6, pages 844-895, 1995.|http://www.pllab.riec.tohoku.ac.jp/~ohori/research/toplas95.pdf]]
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"}