ML多相

というわけで大体の解説。

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

だったら、fun y -> yの型がα→αのように推論されるので、idの型は∀α.α→αになる。ただし、OCamlやSML/NJでは、∀α.は省略され、表示されない。

  • ところが、破壊的代入やcall-with-current-continuationなど「副作用」のある言語では、上述の型推論は不健全になる。たとえば
let polyref = ref []

においてpolyrefの型が∀α.α list refと推論されてしまったら、

polyref := [true]

と

123 + List.hd !polyref

が両方とも型付けできてしまい、明らかに困る。

  • この問題を回避するために、過去に様々なアプローチが提案・実装されたが（後述の論文で引用されている文献などを参照）、どれも複雑だった。
  • そこで、Andrew Wrightが「let x = eのeが値(syntactic value)でなかったら、xの型に∀をつけない」という単純なアプローチを考案し、（当時の）多数のプログラムを調査して、そのような制限があっても支障はないと主張した。いわゆるvalue restrictionである。
  • ただし、値(syntactic value)とは、たとえば「1」「(2, 3)」「fun y -> y」など、それ以上の評価ができず、評価の結果が自分自身と等しい式のことである（だから副作用もない）。したがって、関数適用は値ではない。
  • value restrictionは広く受け入れられ、SMLやOCamlでも採用された。この点においてはSMLもOCamlも同じだった。
  • ただし、SMLは「具体化されておらず∀もついていない型変数は、他のすべての型と異なるダミーの型（?.X1等）でおきかえる」
> sml
Standard ML of New Jersey, Version 110.0.7, September 28, 2000 [CM;
autoload enabled]
- fun f x y = (x, y) ;
val f = fn : 'a -> 'b -> 'a * 'b
- val f1 = f 1 ;
stdIn:18.1-18.13 Warning: type vars not generalized because of
  value restriction are instantiated to dummy types (X1,X2,...)
val f1 = fn : ?.X1 -> int * ?.X1
- f1 2 ;
stdIn:19.1-19.5 Error: operator and operand don't agree [literal]
 operator domain: ?.X1
 operand:         int
 in expression:
   f1 2

OCamlの対話環境は「具体化されておらず∀もついていない型変数は、とりあえず'_a等として残しておき、後で決める」

# let f x y = (x, y) ;;
val f : 'a -> 'b -> 'a * 'b = <fun>
# let f1 = f 1 ;;
val f1 : '_a -> int * '_a = <fun>
# f1 2 ;;
- : int * int = (1, 2)
# f1 ;;
- : int -> int * int = <fun>
# f1 true ;;
Characters 3-7:
  f1 true ;;
     ^^^^
This expression has type bool but is here used with type int

OCamlのバッチコンパイラは「具体化されておらず∀もついていない型変数が残ったら型エラー」

> cat foo.ml
let f x y = (x, y)
let f1 = f 1
> ocamlc foo.ml
File "foo.ml", line 2, characters 9-12:
The type of this expression, '_a -> int * '_a,
contains type variables that cannot be generalized

とした。

ここまでが基本的歴史。（暇があれば）続く。