The 1996 revision of Standard ML [7]
adopts value polymorphism, discarding the distinction between
imperative ('_a) and applicative ('a) type variables,
and generalizing type variables only in non-expansive expressions.
Consider a val-binding
[
With value polymorphism, the free type variables in the type of x are generalized only if the right-hand side e is non-expansive. This is a purely syntactic criterion: an expression is non-expansive if it has the form nexp, defined by the grammar below:
Roughly, a non-expansive expression is just a value, that is, an expression in normal form. For example, the right-hand side length below is an identifier, and so is non-expansive. Hence the free type variable 'a in the type 'a list -> int of x becomes generalized:
On the other hand, the right-hand side (fn f => f) length below, although it evaluates to the same value as the previous one, is expansive: it is not derivable from the above grammar. Hence the type variable 'a will not be generalized, and type checking will fail:
In Standard ML, all type variables in types reported at top-level must be universally quantified; there must be no free type variables. When type checking fails for this reason, there are two remedies: Either (1) insert a type constraint to eliminate the type variables, or (2) eta-expand the right-hand side to make it non-expansive:
In Moscow ML versions prior to 1.40, the type checker would distinguish imperative and applicative type variables, generalize all applicative type variables, and generalize imperative type variables only in non-expansive expressions, as required by the 1990 Definition [6]. To reinstate this behaviour, invoke mosml or mosmlc with the option -imptypes. This is useful for compiling old programs.