SML# - Foundations/020 Diff

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

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

----
内容に関するお断り:本ページの文責は,大堀淳にある.ここに示された見解
や解釈等は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多相性の型推論の基礎は以下の論文に示されている.
* [[Atsushi Ohori and Nobuaki Yoshida.. ''Type Inference with Rank 1 Polymorphism for Type-Directed Compilation of ML'', Proc. ACM ICFP Conference, pages 161-171, 1999.|http://www.pllab.riec.tohoku.ac.jp/~ohori/research/icfp99.pdf]]

この論文で提案されたランク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の型システムで推
論した型は,プログラムが実際に計算する値の型とは異なり,実行時に型エラー
を引き起こしシステムが停止すてしまうことがある.
(健全かつ完全な型推論等の概念の正確な理解のためには,例えば,
* [[「プログラミング言語の基礎理論」(情報数学講座9),大堀 淳,共立出版|http://www.pllab.riec.tohoku.ac.jp/~ohori/texts/index.html]]
* [[コンピュータサイエンス入門,「アルゴリズムとプログラミング言語」大堀淳,ジャック ガリグ(雅利賀 惹玖) ,西村 進,岩波書店や|http://www.pllab.riec.tohoku.ac.jp/~ohori/texts/index.html]]
* 「チュートリアル:SML#で学ぶ型理論の基礎」(SML#のチュートリアルページに執筆予定)
などを参照.)

この問題点は,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にまで遡る手続き的機能に関する多相型理論の長い研究の
歴史は,この値多相性制約に勝る解決法が困難であることを示唆している
{{fn('もちろん,未だ発見されていない優れたアイデアによる画期的な解決法
があるかもしれない.手続き型言語の多相型システムの問題自体は分かりやす
く単純であるので,MLに興味を持つ方はぜひ考えてみられることを勧める.よ
りよい解決方法が構築できたら,SML#チームにもお教え願えれば幸である.')}}.

!!ランク1多相性の理論

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

値多相性制約は,値式ではない
makeObj {Name = "Amy", Age = 26, Office = "S401"}
のような式に対しては多相型は与えられない,
という制約である.
ここで,「多相型は与える」とは,
この式の型を推論した結果えられる型の中の型変数を多相型に昇格させる操作
である.
この過程を吟味してみよう.
[[レコード多相性の理論|Foundations/010]]で概説したとおり,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の多相型束縛機能