let多相についてのメモ

October 3, 2017

TaPLの22章で紹介されている let多相 について、そもそもどんなものか非MLユーザーにはよくわからなかったのでメモ。

Milner先生のこの論文が元らしい。

「多相性(polymorphism)」について

TaPLの説明がとてもわかりやすいのでそのまま引用。

多相性という言葉は、プログラムの一部分を、異なる文脈では異なる型として用いることを可能にする各種言語機能を指す。

(22.7 let多相より)

パラメトリック多相やらアドホック多相やらいろいろあるけれど、すべて「別の場所では別の型として扱う」を実現していることがわかる。 今回はその中のlet多相 (もしくはDamas–Milner多相、ML式多相) の話。

let束縛

部分式に対して名前をつけることで、繰り返しを避けたり、式を読みやすくできる。そのための仕組みとしてlet束縛がある。

let x = t1 in t2

「式t1を評価し、その結果の値に名前xを束縛した状態でt2を評価せよ」という意味。

let多相 (let polymorphism)

名前の通り let束縛項を多相にする。もうちょっと具体的に書くと

let x = t1 in t2

について、let束縛項x が多相になる。例を見てみる。

let id = λa . a in ...

のようにidλa . aが束縛されているとして、このidは多相だろうか? TaPLの22章までで紹介してきた規則だと、単相になる。

直観的には id の型は型変数 X を導入して X -> X となるが、以下のようになってしまう。

id true // ここで idは X == Boolの制約が追加されてしまう
id 1    // 型検査失敗 

定義通り、異なる文脈では異なる型として扱えていない。 シンプルなアイディアとしてxt1代入することで多相性を持たせるというものがあり、これをlet多相と呼ぶらしい。

// idに代入される
(λa . a) true
(λa . a) id

let多相の実用的な実装

代入による方式だと、let束縛項の出現のたびにlet束縛の右辺全体が検査されることになってしまい効率が悪い。

これを解決するために以下のようにする。

MLの多相型推論は、let x = eのような宣言があったら、eの型を推論して、「決まらなかった」部分は「何でもよい」と解釈し、具体化されなかった型変数について∀を先頭を追加する。

http://d.hatena.ne.jp/sumii/20061028/1162000645

プログラムのサイズに対して最悪指数関数的になるが、基本的には線形であり、単純な代入形式より実用的になる。

副作用のある場合のlet多相と値制限

TaPLの例をそのまま持ってくる。

let r = rf (λx. x) in
(r:=(λx:Nat. succ x);
	(!r)true);
  • 上で紹介した実用的な実装だと、この式を評価するとsucctrueに適用する、となってしまいおかしくなる
  • 評価規則を変更してrをそのままその定義に置き換えると問題ないが、1つ目と2つ目は別の参照を指すことになってしまい、よくわからない意味論になってしまう。

これの問題を解決するために「右辺が構文的に値であるときのみ、let束縛は多相に扱える」というアプローチをWrightが導入し、この制約を値制限という。この制約があっても実用上は大きな問題がない、とTaPLでは紹介されている。

まとめ

let x = t1 in t2

について

  • xを多相にしたい
  • t2中のxt1を代入することにより多相性を実現
  • けど効率が悪いので、「決まらない型変数には∀をつける」方式を実際には採用
  • 副作用を伴う場合は問題が起こるので値制限を導入する

参考

このエントリーをはてなブックマークに追加