9.1 Rank 1 polymorphism

Polymorphic types Standard ML type system can infer are those whose type variables are bound at the top-level. For example, for a function

fun f x y = (x, y)

the following type is inferred.

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

In contrast, SML# infers the following nested polymorphic type

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

This type can be think of as a type function that receives a type $\tau$ through type variable ’a and return a polymorphic type [’b. ’b -> $\tau$ * ’b]. It behaves as follows.

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

Let $t$ represent type variables, $\tau$ monomorphic types (possibly including type variables), and let $\sigma$ polymorphic types. Then the set of polymorphic types Standard ML can infer is roughly given by the following grammar.

	$\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$

We call this set rank 0 types.

In contract, SML# can infer the following set called rank 1 types.

	$\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$

We have introduced this as a technical extension for making compilation of record polymorphism more efficient. In a type system for pure ML term without imperative feature, this extension does not increase the expressive power of ML. However, with the value restriction introduced in the revision of Standard ML type system, rank 1 extension become important extension. Next section explain this issue.