MLのlet多相とか値制限とかよく分からなかったので調べてみた

世間はもうすぐ予定されているTAPLの日本語版の発刊に色めき立ってますね。関数型都市と呼ばれていた(る？)なごやでは、いいかげん動的型の言語ばっかやってられない雰囲気をヒシヒシと感じてるので、ぼちぼちと静的型付言語の勉強を進めています。
で、このエントリでは、今までなんだか分かったような分からないような感じのままになっていた、ML系言語のlet多相とか値制限とかその辺りについて調べたときに、参考になったweb上の文献等をまとめるのをメインにしつつ、自分の中での理解なんかをチョロチョロっと書いていこうかなぁと思います。

全体を通した話としては、住井先生のこの辺りの記事が時系列で書かれてるし、分かりやすいと思いました。

• ML多相 - sumiiの日記
• ML多相の続き - sumiiの日記

このエントリは、基本的に上の記事の劣化コピーでしかないので、上の記事を見て理解できれば、以降は読む必要ないでしょう:P

let多相

let多相については、上の住井先生の記事に端的な説明があります。

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

ML多相 - sumiiの日記

「型の多相性がどこで与えられるか」に対するMLでの答えがlet多相なんだと理解してます。型推論的には、letは特別な扱いを受けています。たとえば、OCamlでは

# let f = fun x -> x in (f 1, f true);;
- : int * bool = (1, true)

に型がつきます。fは多相的な関数で、let内でint->intとしてもbool->boolとしても使えていることに注意。一方で、上のコードをfunを使って書き直してみると、

# (fun f -> (f 1, f true)) (fun x -> x);;
Error: This expression has type bool but an expression was expected of type
         int

このように型エラーになってしまいます*1。

let多相の概要はそんな感じですが、詳しくは実際に型推論アルゴリズムにあたるのが遠回りではあるけど確実なアプローチかなと思います。let多相を含む型推論については、以下の五十嵐先生の講義資料が分かりやすかったです。

• 型推論機構の実装

型スキーム('a -> 'aみたいな多相な型を、∀で明示して∀α.α→αと表す表現)なんかは他のところでも散々出てくるので知っておいた方がいいと思います。
また、@pi8027さんが書かれた Algorithm W 入門 は、まさに型推論アルゴリズムについて書かれている薄い本で、let多相についても説明がされています。

• Algorithm W 入門 今は購入不可だけど、@pi8027さんに頼めば買える？(未確認)
• pi8027/typeinfer · GitHub 一応、GitHubからソースは見られるけど…？。

値制限

で、純粋な言語であればlet多相でOKなわけですが、破壊的操作が可能な言語では型安全でないようなケースが出てくるようです。このようなケースが生じないようにする回避策はいろいろ考えられたようですが、現在ではAndrew Wrightが考案した値制限という比較的単純な方法をベースとした方法が広く使われています。
値制限は、let x = e でlet多相によってeに多相性を持たせる場合の制限で、eとして数値や文字列といったリテラルやコンストラクタの呼び出し等、実行を伴わない「値」(syntactic value)しか許さないというものです。この辺りの制限がどうやって導かれたかについては、SML#のrank-1 多相性の理論の解説ページに詳しく書かれています。
値制限は単純である反面、必要以上に厳しい制限です。特に、関数適用がsyntactic valueとして扱われないことが非常に大きな制限になります。たとえば、以下のような場合、

# let f = List.map (fun x -> Some x);;
val f : '_a list -> '_a option list = <fun>

fに束縛される List.map (fun x -> Some x) という式は関数適用であるため、値制限により多相になりません。OCamlでは、値制限によって多相にならなかった場合、'_aのような型変数が割り付けられますが、このような型変数は一度ある型で具体化されてしまうと他の型になることができなくなります。

# f [1; 2; 3];;
- : int option list = [Some 1; Some 2; Some 3]
# f;;
- : int list -> int option list = <fun>
# f [true; true; false];;
Error: This expression has type bool but an expression was expected of type
         int

一応、この場合には、いわゆるη展開によってfに多相性を持たせることができます。

# let f xs = List.map (fun x -> Some x) xs;;
val f : 'a list -> 'a option list = <fun>
(* 上は以下と等価 *)
# let f = fun xs -> List.map (fun x -> Some x) xs;;
val f : 'a list -> 'a option list = <fun>
(* 関数抽象はsyntactic valueとして扱われるため、値制限を回避できる *)

とはいえ、いちいちη展開をするのは、高階関数を使いまくるときなんかにはだるいですね。これまで見てきた例に限らず、値制限は不便な点が多いため、値制限をベースにしつつ、実際には各言語で制限を緩めるような拡張がなされています。

各言語での拡張

有名どころでは以下のような拡張があるみたいです。

• OCamlのRelaxed value restriction
  • Relaxing the Value Restriction (PDF)
• SML#のrank-1 多相
  • Type Inference with Rank 1 Polymorphism for Type-Directed Compilation of ML (PDF)
  • ランク１多相性 in Ch.5. SML#の拡張機能：その他の型の拡張 in プログラミング言語SML#解説

OCamlのRelaxed value restrictionはよく分かっておらず。共変な型変数ならsubtypingによって多相性が回復するといいますが。。。
それから、SML#のrank-1 多相について。もともと、MLの多相性はrank-1 多相というクラスに属していますが、その中でも∀が先頭にのみ現れる∀α.(α→α)や∀α.∀β.(α→β→α*β)といった型だけが許されています。SML#のrank-1 多相ではこの制限を緩めて、∀α.(α→∀β.(β→α*β))といったように、∀が→の右側に現れるのを許すようになっています(というか、そういう型に推論されるようになっている？)。これによって、上で挙げた部分適用された関数を束縛する例を含むいくつかのケースで、値制限を回避して多相性をもつことができるようです。

まとめ

• let多相は型に多相性を与えるための型推論の仕組み
• 値制限は純粋でない言語でlet多相の型安全性を保証するために広くとり入れられている方法
• 値制限は厳しいので、各言語で値制限をベースにしつつ、制限を緩めるような拡張がなされている

よく分からず書いている部分も多く、間違った記述があるかもしれません。間違いを見つけた場合は*お手柔らかに*ご指摘いただけると幸いです。

*1:rank-2 多相を使うと書けるという話もありますが、それはまた別の話。