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

とした。

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

ML多相の続き

  • さて、Wrightの論文の当時は、value restrictionは妥当な制限だった。なぜならば、value restrictionのせいで型付けできなくなる主なケースは、多相関数の部分適用がまた多相関数になる(はずの)場合ぐらいで、それはlet x = eのeをfun y -> e yのように書き換えること(η展開)で回避できたからである。
  • ところが、SML#のような多相レコード、OCamlのような多相オブジェクトないし多相バリアントを利用すると、value restrictionが本当に問題になってくる。たとえば
# let f x = `V x ;;
val f : 'a -> [> `V of 'a ] = <fun>
# let v = f 1 ;;

などで、vがpolymorphicにならないとしたら、「(実質的に)多相バリアントを返す関数は書けない」ことに(事実上)なってしまう。

  • そこで、OCamlでは「let x = eのeが値でなくても、正位置にしか現れない型変数については∀をつける」という拡張が実装された(正位置とは、大雑把にいえば、reference cellの中身や関数の引数にならない位置のこと)。したがって、上の例のvなども、ちゃんと
val v : [> `V of int ] = `V 1

とpolymorphicになる。この拡張が健全であることの「証明」は「簡単」で、正位置にしか出現しない型変数であれば、ボトムで具体化してから、subtyping(というかsubsumption)により任意の型に"upcast"できる、という「だけ」である。

  • 一方、SML#では「先頭にしか∀をつけられない」というML多相の制限を緩和して、「→の右側やlistの要素の型にも∀をつけられる」ようにした。したがって、たとえば、fn x => fn y => (x, y)の型は∀α.∀β.(α→β→α×β)ではなく、∀α.(α→∀β.(β→α×β))となる。
> smlsharp
restoring static environment...done
restoring dynamic environment...done
# fun f x y = (x, y) ;
val f = fn : ['a .'a  -> ['b .'b  -> 'a * 'b]]

よって、f 1の型も∀β.(β→int×β)となる。

# val f1 = f 1 ;
val f1 = fn : ['a .'a  -> int * 'a]
  • ちなみに、SML#でもvalue restrictionは存在する。
# val r = ref [] ;
stdIn:3.1-3.14 Warning:
  dummy type variable(s) X0 are introduced due to value restriction
val r = ref [] : X0 list ref
# r := [1] ;
stdIn:4.1-4.8 Error:
  operator and operand don't agree
  operator domain: X0 list ref * X0 list
  operand: X0 list ref * 'A#{int, largeInt} list

これは上の話と矛盾しない。value restrictionは、あくまでlet x = eのeが値でなければxの型に∀をつけ加えないという話であって、「∀β.(β→int×β)」の∀βは「(加えなくても)すでについている」ためである。

  • そういうと、ひょっとしたら「∀α.∀β.α→β→α×βの∀βも『すでについている』ではないか」と思う人もいるかもしれないが、SMLにせよOCamlにせよSML#にせよ、let x = eのxが後で出現するごとに先頭の∀を外してそのxの出現の型とするので、SMLやOCamlでは、f 1の型はあくまでmonomorphicであって、polymorphicにはならない。
  • 以上の話がややこしくてよくわからなかったら、大堀先生の「プログラミング言語の基礎理論」なり何なり、ちゃんとした教科書(と原論文)をじっくりと読むのがもっとも確実だろう。「学問に王道なし」というが、そもそもこんな適当な解説だけでわかるわけがないのである、と責任回避。