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にはならない。
- 以上の話がややこしくてよくわからなかったら、大堀先生の「プログラミング言語の基礎理論」なり何なり、ちゃんとした教科書(と原論文)をじっくりと読むのがもっとも確実だろう。「学問に王道なし」というが、そもそもこんな適当な解説だけでわかるわけがないのである、と責任回避。