ランク1多相性の理論

ランク1多相性を可能にした理論である.


内容に関するお断り:本ページの文責は,大堀淳にある.ここに示された見解や解釈等は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.


文献

ランク1多相性の型推論の基礎は以下の論文に示されている.

この論文で提案されたランク1多相性の理論とその実現メカニズムそのものは,現在理解されている型理論の体系からみると単純なものであるが,この機能が現実の言語に必用とされた理由を理解するには,その導入の背景となったMLの型推論に関する問題点を理解する必用があると思われる.

このランク1多相性は,言わば,

  • より柔軟な多相型システム
  • MLの値多相性制約
  • 効率よい型主導コンパイル

をともに実現するための"妥協の産物"と言える.

以下,いささか解説風になるが,これら背景を概観したのち,ランク1多相性の理論とその実装方式の概要を説明する.

MLの多相型型推論

MLの型推論が基礎とする理論はDamasとMilnerが以下の論文で定式化した理論にほぼ準拠している.

Damas, L. and Milner, R. Principal type-schemes for functional programs ACM POPL, 207-212, 1982

この枠組みでは,型集合は以下の2つのクラスに分けられる.

  • (monotype) T ::= int | bool ...(その他種々の原子型)| α (型変数)| T * T | T -> T
  • (polytype) S ::= T | ∀α.S

ここで,∀t.Sが多相型である.このシステムでは多相関数は例えば,

 fn x => x : ∀α.α -> α
 fn x => fn y => (x,y) : ∀α.∀β.α -> β -> α * β

のような型をもつ.既存のML処理系では,

- fn x => x;
val it = fn : 'a -> 'a
- fn x => fn y => (x,y);
val it = fn : 'a -> 'b -> 'a * 'b

のように表示される.

この型体系は,ラムダ計算を(多相関数の定義構文である)val宣言やfun宣言を許すlet式で拡張した言語に対して健全かつ完全であることが証明されている.しかしながら,手続き型言語の機能を含む現実のML言語に対しては,その健全性さえ成立しない.すなわち,ある種のプログラムに対しては,DamasとMilnerの型システムで推論した型は,プログラムが実際に計算する値の型とは異なり,実行時に型エラーを引き起こしシステムが停止すてしまうことがある.(健全かつ完全な型推論等の概念の正確な理解のためには,例えば,

などを参照.)

この問題点は,LCFシステムのメタ言語(LCF ML)としての出発点からすでに存在し,認識されていたものである.(ちなみに,LCF MLにおける解決方法は,以下に延べる値制約による方法とは異なるものであった.)

MLの手続き的機能とそ型

MLは,その出生時点ですでに,現在のStadnard MLに受け継がれる副作用を含むプリミティブを有する手続き型言語であった.現在のMLの標準仕様であるthe Definition of Standard MLでは,以下のプリミティブ演算が提供されている.

type 'a ref                  (ポインタ型)
val ! : 'a ref -> 'a            (ポインタの指す値取り出し)
val ref : 'a -> 'a ref          (ポインタの生成)
val op := : 'a * 'a ref -> unit (ポインタの変更)

これらプリミティブは,以下の動作から確認されるように確に多相性を持つ.

 # val x = ref 1;
 val x = ref 1 : int ref
 # !x;
 val it = 1 : int
 # val y = ref "Ridge Geyserville";
 val y = ref "Ridge Geyserville" : string ref
 # y := "Mount Eden";
 val it = () : unit
 # !y;
 val it = "Mount Eden" : string

しかしながら,他の多相型を持つプリミティブのように,これらプリミティブを含む式に対して系統的に型を推論すると,実行時の型エラーが起ってします.

そこで,まず,ポインタ型を含まない多相関数の例を考えてみよう.

fun id x = x;
fun addOne x = x + 1;
val funList = [id];
addOne :: funList;
(hd funList) true;

funListには('a -> 'a) listのような多相型が与えられ,この変数が,addOne :: funListでは(int -> int) list型として,(hd funList) trueでは(bool -> bool) list型として使われる.このプログラムの構造は,型のみを考えた場合,ポインタを扱う以下のプログラムと同一である.

fun id x = x;
fun addOne x = x + 1;
val funRef = ref id;
funRef := addOne;
(!funRef) true;

従って,標準の型推論を行えば.上記同様に,funRefに('a -> 'a) refという多相型が与えられ,それがfunRef ;= addOne;では(int -> int) ref型として,また,(!funRef) trueでは,(bool -> bool) ref型として使われることになる.しかし,その動作を考えると,2行目でポインタfunRefの指す内容がaddOneに変更されているので,3行目でtrueへの加算が行われ,型エラーとなってしまう.

MLの値多相性制約とその問題点

この問題を解決するための多くの試みがなされたが,型理論的にきれいな,すなわち,ある妥当な型システムにたいして健全かつ完全な,解決策は見いだせなかった,というのがおそらく妥当な見方であろう.この問題の詳細な分析と現在にいたるまでの研究の過程の詳細は他に譲ることにし,ここでは,現在採用されている解決策を概観する.

上記の不整合の原因は,多相型を持つオブジェクトへのポインタが生成されてしまうことである.そのようなポインタが生成されないかぎり,多相型の中にref型が現れても問題は起らない.例えば,関数定義

fun makeRef x = ref x

はポインタを生成しないので,'a -> 'a refのような多相型を与えても問題ない.ところが

ref (fn x => x)

ではポインタを生成するrefプリミティブが実行されポインタが作られるので,上記のような不整合を生じる恐れがある.この点に着目すると,不整合の問題を回避する一つ方法として,

プリミティブrefが実行されない式に限り多相型を与える

とすることが考えられる.しかし,高階の関数を自由に使えるMLでは,「ある式を実行するとき,その中でrefプリミティブが実行されるか否か」は簡単には判定できない.そこで,この考え方を極端に単純化し,

いかなる演算も実行しない式に限り多相型を与える

とする方式が提案された.以下のように定義される値式の集合は,「いかなる演算も実行しない」という条件満たす.

  • 関数式(関数を定義するのみであり,その本体は実行されない.)
  • 定数式
  • 変数式
  • 以上をタプルやデータ構成子を使って組み合わせるだけの式

これら値式にのみ多相型を許すように制限するのが,MLにおける値多相性制約である.The Definition of Standard MLでは,この制約が採用されている.

この値多相性制約は,refプリミティブを実行する式に多相型を与えることがないのでポインタの変更に伴う不整合を防ぐことができるが,当然,ポインタの操作は伴わないが値式ではない多くの式が多相型を持つことを禁止してしまう.しかも残念なことに,禁止される式は,多相型をもつ高階の関数によって生成されるようなMLの利点を生かして書かれたプログラムであることが多い.例えば,以下のように,種々のviewメッソドを受け取るオブジェクトを生成する多相関数makeObjを定義し,種々の型のオブジェクトを生成するプログラムを書いたとする.

val makeObj = fn state => fn view => view state;
val person = makeObj {Name = "Amy", Age = 26, Office = "S401"};
val nameAndAge = (person (fn {Name,Age, Office} => Name),
                  person (fn {Name,Age,Office} => Age));

ここでmakeObjはオブジェクトの状態を受け取り,viewメソッドに応答するオブジェクトを生成する高階の関数である.生成されたpersonオブジェクトは,種々の型のviewメッソドを受け取り,それをオブジェクトの状態に適用し結果を返す高階の多相関数である.このコードは,典型的な相型を持つ高階関数の定義と利用の例であり,何の不整合も含まない.しかし,makeObj {Name = "Amy", Age = 26, Office = "S401"} は値式では無いため,現在のML系言語では,その結果のperson関数に多相型が与えることができず,それに続くnameAndAgeの計算は型エラーとなる.

この例から理解される通り,値多相性制約は,手続き的機能を安全に型付けるために,必用な条件を極端に単純化した苦肉の解決法といえる.残念ながら,LFC MLにまで遡る手続き的機能に関する多相型理論の長い研究の歴史は,この値多相性制約に勝る解決法が困難であることを示唆している*1

ランク1多相性の理論

ランク1多相性を含む型システムの目的の一つは,この値多相性の制約下でも,makeObjのような高階の関数の返す値に対しても多相型を許すことである.

値多相性制約は,値式ではないmakeObj {Name = "Amy", Age = 26, Office = "S401"} のような式に対しては多相型は与えられない,という制約である.ここで,「多相型は与える」とは,この式の型を推論した結果えられる型の中の型変数を多相型に昇格させる操作である.この過程を吟味してみよう.レコード多相性の理論で概説したとおり,MLの型推論の最初のステップは,まず,プログラムの部分式の型をとりあえず「なにか分からない型」を表す変数と仮定することである.しかし,その部分式がmakeObjのように既に定義された変数であれば,型変数ではなく,その変数に対して推論された型とする.さらにその際,もしその型が多相型であれば,その多相型型変数を,なにか分からない型を表す型変数で置き換えて得られる型とする.makeObjに対して推論された型は,

∀α.∀β.α -> (α -> β) -> β

であるので,多相型型変数αとβを型変数に'Aと'Bに置き換え,makeObjの型を,

 'A -> ('A -> 'B) -> 'B

と置き,その他の部分式の型とともに推論を進め,最終的に残った型変数を改めて多相型に昇格させる.関数適用式makeObj {Name = "Amy", Age = 26, Office = "S401"} の場合,推論の結果'Aはレコード型{Name:string, Age:int, Office:int} に置き換えられるが,'Bは何ら制約が課されないので.最終的な型は,

({Name:string, Age:int, Office:int} -> 'B) -> 'B

となり,'Bがそのまま残る.値多相性制約がないシステムでは,残った'Bを再び多相型に昇格させ,∀α.({Name:string, Age:int, Office:int} -> α) -> α なる型を得るが,値多相性制約の下では,このステップが実行できなず,この結果の関数に多相型を与えることができない.

(続く...)

型主導コンパイルとMLの多相型束縛機能

Last modified:2008/02/05 00:55:24
Keyword(s):
References:[SML#の理論的基礎]

*1 もちろん,未だ発見されていない優れたアイデアによる画期的な解決法があるかもしれない.手続き型言語の多相型システムの問題自体は分かりやすく単純であるので,MLに興味を持つ方はぜひ考えてみられることを勧める.よりよい解決方法が構築できたら,SML#チームにもお教え願えれば幸である.