9.1 ランク１多相性

Standard MLの多相型システムが推論できる多相型は，すべての多相型変数が最も外側で束縛される型です．例えば関数

fun f x y = (x, y)

に対しては，

val f = fn : [’a, ’b. ’a -> ’b -> ’a * ’b]

の型が推論されます． SML#では，このような関数に対して以下のようなネストした多相型を推論可能に拡張しています．

# fun f x y = (x, y);
val f = fn : [’a. ’a -> [’b. ’b -> ’a * ’b]]

この型は，’aとしてある型 $\tau$ を受け取って多相関数 [’b. ’b -> $\tau$ * ’b]を返す関数型です．実際，以下のような動作をします．

# f 1;
val it = fn : [’b. ’b -> int * ’b]
# it "ML";
val it = (1, "ML") : int * string

型変数を $t$ ，種々の型にインスタンス化ができない単相型を $\tau$ ，多相型を $\sigma$ で表すと，Standard ML言語の多相型はおおよそ以下のように定義されるランク０と呼ばれる型です．

	$\displaystyle\tau$	$\displaystyle::=$	$\displaystyle t\mbox{\ $\|$\ }b\mbox{\ $\|$\ }\tau\rightarrow\tau\mbox{\ $\|$\ }% \tau*\tau$
	$\displaystyle\sigma$	$\displaystyle::=$	$\displaystyle\tau\mbox{\ $\|$\ }\forall(t_{1},\ldots,t_{n}).\tau$

これに対して，SML#で推論可能な多相型は，多相型が関数の引数の位置以外の位置にくることを許す以下のようなランク１と呼ばれる型です．

	$\displaystyle\tau$	$\displaystyle::=$	$\displaystyle t\mbox{\ $\|$\ }b\mbox{\ $\|$\ }\tau\rightarrow\tau\mbox{\ $\|$\ }% \tau*\tau$
	$\displaystyle\sigma$	$\displaystyle::=$	$\displaystyle\tau\mbox{\ $\|$\ }\forall(t_{1},\ldots,t_{n}).\tau\mbox{\ $\|$\ }% \tau\rightarrow\sigma\mbox{\ $\|$\ }\sigma*\sigma$

この拡張は，もともとレコード多相性の効率的な実現を目指した技術的な拡張であり，純粋なMLの型理論の枠組みでは殆ど違いはありません．しかし，Standard MLの改訂版で導入された値多相性制約のもとでは，重要な拡張となっています．次節で値多相性とランク１多相性の関連を解説します．