Background
The interaction between polymorphism and side-effects has
always been a troublesome problem for ML. Here is an example
of a program illustrating the danger:
val r = ref(fn x => x);
r := (fn x => x+1);
!r true;
Under the basic rules of ML type inference (Hindley-Milner type
inference), we would give the local variable r the polymorphic type
r: ('a -> 'a) ref
where the type variable 'a here is implicitly
quantified, meaning the type might be more explicitly
written (in an extended SML type notation) as:
r: (All 'a).('a -> 'a) ref
We will use this explicit quantifier notation when we want to
be particularly clear that we are dealing with a polymorphic type.
Given that r has this polymorphic type, the occurrence of
r in the assignment expression would have the type
(int -> int) ref, while in the third line r
would have the type (bool -> bool) ref. This typing of
the program is clearly unsound, since it allows a function on integers
to be applied to a boolean value.
What is going on here is that a mutable value (here a
ref cell r) is given a polymorphic type. This allows the
mutable value's type to be instantiated differently at the points
where the contents are updated and where they are fetched, with the
consequence that the value stored and retrieved changes type in the
process. The ref cell is acting as a communication channel between
two points in the program that do not agree on the type of the value
being communicated.
Besides ref cells and arrays, another mechanism that can serve as
communication channel between statically uncoordinated parts of a
program are first-class continuations. These can give rise to
the same sort of type unsoundness illustrated above.
This example shows that the simple rule for introducing polymorphism
for let-bound variables, which suffices for purely functional languages,
is not sound in a language with side effects like SML. Somehow the
rule for typing let-bound variables has to be restricted to prevent this
unsoundness.
SML '90 solved this problem by introducing a special, restricted form
of polymorphism expressed through imperative types. An
imperative type is a polymorphic type whose bound type variable is of
a special form, called an imperative type variable. Imperative type
variables are distinguished by an initial underscore in the type
variable name, for example '_a.
Notation: I'll use type variables names with
lower-case names near the beginning of the alphabet like
'a, 'b and '_a for implicitly
generalized type variables in polymorphic types, while capitalized
names near the end of the alphabet like 'X or
'_X will be used for free, or nongeneralized,
type variables. Such free type variables occur during the type
checking process and are sometimes called type metavariables.
They are not allowed to occur in the top-level types produced by
type checking.
In the SML '90 scheme, imperative types are initially associated with
certain primitive functions, such as ref, which has the
imperative polymorphic type:
ref: '_a -> '_a ref
The imperative attribute of a type variable is propagated by
substitution during type checking, so the expression ref(fn x =>
x) has the typing
ref(fn x => x) : ('_X -> '_X) ref
where '_X is a free imperative type variable inheriting
its imperative nature from the '_a in the type of
ref.
The purpose of imperative type variables is to limit the introduction
of polymorphism, i.e. to prevent certain type variables from being
generalized in certain circumstances. In a value declaration like
val y = ref(fn x => x)
we have seen that the type of the right hand side is
('_X -> '_X) ref [1]
We will only be allowed to generalize the imperative type variable
'_X and assign y a polymorphic type if the
defining expression on the right is in some sense safe,
meaning that it cannot create new ref cells that could behave
polymorphically and cause the kind of unsoundness illustrated above.
In this case, the right hand side clearly is not safe since it
directly creates a ref cell. So in this case the type will not be
generalized and y will not have a polymorphic type. In
fact, if the declaration is at top level, y would not be
given a type at all, because types like [1] containing free type
variables such as '_X are not allowed for top-level
bindings.
Determining exactly which expressions are safe, and may therefore have
their types generalized without jeopardizing type soundness, is a very
difficult problem. So we approximate safety with a simple syntactic
notion, that of a nonexpansive expression. Nonexpansive
expressions are
- constants, including nullary constructors (e.g.
3, nil),
- variables (e.g.
x, A.x), or
- function expressions (e.g.
fn x => x).
The evaluation of expressions of any of these forms is
trivial, and in particular cannot entail the creation of new data
structures (other than the benign case of a function closure for
function expressions). All other expressions, including function
applications, let expressions, conditionals, etc., are by definition
expansive, implying that their evaluation may entail
nontrivial computations that might lead to the creation of
ref cells or other mutable data structures.
So to summarize the rule used in SML '90: in a value declaration, we
generalize those free type variables that do not occur free in the
context environment, except that free imperative type
variables can only be generalized (i.e. transformed into bound type
variables of a polymorphic type) if the expression on the right hand
side of the declaration is nonexpansive.
Note: In SML/NJ, the notions of imperative type
variables and nonexpansive expressions were refined into a system of
weak type variables with different degrees of weakness indicated by
a leading integer in the type variable name, e.g. '1a,
'2b. This scheme moderately extended the power of the type
system by allowing the types of certain expansive expressions to be
generalized (e.g. partial applications of polymorphic curried
functions).
One obvious drawback of both imperative types in SML '90 and the
related weak types of SML/NJ (0.93) is that they require a special
kind of type variable. The rules governing their behavior were also
relatively subtle and hard to explain to novices (especially SML/NJ's
weak types).
Another major problem is that imperative types often "infect"
interfaces. A given signature might have two semantically equivalent
implementations written in different styles, one purely functional and
the other using imperative features. The types of the values in the
functional implementation would be normal polymorphic types. However,
even though their behavior is equivalent, the types of the
corresponding values in the imperative implementation might be
imperative polymorphic types. This happens because once a type
variable acquires the imperative attribute through interaction with a
ref cell, the attribute sticks and gets propagated through to the
final type. For example, here are two equivalent implementations of
the identity function:
fun id x = x (* pure *)
idFun : 'a -> 'a
fun id x = !(ref x) (* imperative *)
idImp : '_a -> '_a
A single signature that is meant to describe the common interface of
both implementations must therefore specify the imperative type.
signature S =
sig
val id : '_a -> '_a
end;
If the imperative implementation is introduced after the functional
version already existed, it becomes necessary to go back and revise
the earlier signature to change nonimperative polymorphic types to
imperative types.
Let's consider a slightly more subtle example demonstrating the need
for restricted polymorphism. Under the naive typing rules, (without
imperative types or other restrictions on type generalization), the
following definitions result in the same polymorphic type being
assigned to functions f1 and f2.
fun f1 () =
let val r = ref nil
fun put x = r := x::nil
fun get () = hd(!r)
in (put, get)
end
val f1 = fn : unit -> ('a -> unit) * (unit -> 'a)
fun f2 () : ('a -> unit) * (unit->'a) =
((fn x => ()), (fn () => raise Fail "f2"));
val f2 = fn : unit -> ('a -> unit) * (unit -> 'a)
Again under the naive typing rules, we then have
val (g1,h1) = f1 ()
val g1 = fn : 'a -> unit
val h1 = fn : unit -> 'a
val (g2,h2) = f2 ()
val g2 = fn : 'a -> unit
val h2 = fn : unit -> 'a
Here the polymorphic types for g1 and h1
lead to trouble, because the the last value to which g1
is applied will be the value returned by the next call of
h1:
g1 3; (* stores 3 in the shared ref *)
val it = () : unit
not(h1()); (* apply boolean operation to 3! *)
val it = <> : bool
Because their function bodies both refer to the local variable
r, g1 and h1 are tied together
by hidden shared state, and this is how calls of g1 and
h1 communicate. If g1 and h1
have independent polymorphic types, the the value communicated between
them can change types arbitrarily.
On the other hand, the behavior of g2 and h2 is benign:
g2 3; (* 3 is just discarded *)
val it = () : unit
not(h2()); (* no problem, h1 does not return *)
uncaught exception Fail: f2
because g2 and h2 are independent, and
there is no hidden communication between them.
We note two things about this example: (1) The polymorphic type that
f1 and f2 share does not mention the
ref type constructor, illustrating that there is no
simple way to determine whether shared state and side effects are
involved by looking at the type. (2) Typing is
compositional, meaning that we when we type declarations like
val (g1,h1) = f1 ()
val (g2,h2) = f2 ()
we have only the previously determined types of the component elements
(f1, f2, ()) to work with. Since the types of
f1 and f2 are the same, these two declarations must be
typed the same way, regardless of what may be going on inside of f1
and f2.
In SML '90, the problem is solved by causing f1 and
f2 to have different types. The use of
ref in the definition of f1 introduces an imperative
type variable, and the type checker assigns f1 the type:
val f1 = fn : unit -> ('_a -> unit) * (unit -> '_a)
Note that f1 is still polymorphic because the
declaration of f1 is equivalent to
val f1 = (fn () => ...)
so the right hand side of the declaration is a function expression
and therefore nonexpansive.
Note: I've oversimplified slightly here, since a
fun declaration is actually equivalent to a val
rec, but val rec declarations are by
convention always treated as nonexpansive, since the right hand
sides must all be function expressions.
Now when we type the suspect declaration
val (g1,h1) = f1 ()
the expression f1() on the right gets the type
('_X -> unit) * (unit -> '_X)
and since the right hand side is expansive, the imperative type variable
'_X will not be generalized. This will lead to an
error (at top level), thus preventing the unsound use of g1
and h1. The typing of f2, g2,
and h2 proceeds as in the naive case, since no imperative
type variables arise in those declarations.
Value Polymorphism
In SML '97, we use a different technique to avoid unsoundness. We
drop the distinction between imperative type variables and ordinary
type variables, so once again there is only one flavor of type
variable (ignoring equality type variables). This means that
f1 and f2 have the same polymorphic type, as
with the naive rule. We therefore cannot distinguish between
dangerous (f1()) and safe (f2())
expressions based on type information alone. Also, without imperative
type variables we can't distinguish which type variables are unsafe to
generalize because they are involved in the type of a ref value. So
we conservatively treat all function applications as dangerous and we
do not allow any of the type variables in their types to be
generalized. In effect, we have decided to treat all type
variables as imperative. This new scheme is called value
polymorphism, and it is also known as the value
restriction.
As in SML '90, we approximate the class of safe-to-generalize
expressions conservatively by the simple syntactic notion of a
nonexpansive expression, also known as a value expression
or simply a value. SML '90 defined nonexpansive expressions
to include the following atomic forms:
- constants (e.g.
3),
- nullary constructors (e.g.
nil),
- variables (e.g.
x, A.x),
- function expressions (e.g.
(fn x => x)).
It is clear that the evaluation of any of these forms is
safe because it cannot entail the creation of new data structures
(other than the benign case of creating function closures for
function expressions). To partially compensate for the fact that we
are being more restrictive in our creation of polymorphism, SML '97
enlarges the class of nonexpansive expressions to include some simple
compound expressions:
- records and tuples with nonexpansive fields (e.g.
(3,x,nil)),
- constructors (except
ref) applied to nonexpansive arguments (e.g. x::nil).
All other expressions, including function applications, let
expressions, conditionals, etc., are by definition expansive,
implying that their evaluation may entail nontrivial computations that
might lead to the creation of ref cells or other mutable data
structures.
The value polymorphism rule for typing value
declarations states that in a declaration such as
val pat = exp
the types of the variables appearing in pat can be closed by
generalizing those type variables appearing free in their types but
not in the context if, and only if, the expression on the
right hand side is nonexpansive.
Using the value restriction to control the interaction of polymorphism
and side-effects had been considered during the design of Standard ML,
but it was generally thought to sacrifice too much polymorphism.
However, after several years of investigation of more elaborate
schemes that attempted to weaken the restriction (like the weak types
in SML/NJ), Andrew Wright undertook an empirical investigation
of the consequences of the value restriction ("Simple Imperative
Polymorphism", LISP and Symbolic Computation, 8, 343-355, 1995). He
implemented the value restriction and recorded the changes that were
necessary to convert a large body of existing code (the SML/NJ compiler
and tools, HOL90 and Isabelle theorem provers, etc.). The conclusion
was that surprisingly few changes to the code were needed, and these
changes were mostly fairly simple and local. It turns out that the
imperative types originally adopted were a good example of
premature optimization in language design!
Based on this revelation, we decided to adopt the value restriction
in the revised SML '97 version of the language. This is one of the
most evident and important changes in the language, and it is
important to understand the consequences, and in particular how to
modify old SML code to conform to the new restriction.
We will illustrate below some typical situations where adjustments
are required to conform to the value restriction.
What does it mean in practice?
The value polymorphism scheme is more restrictive than the imperative
type scheme of SML '90 and the weak types of SML/NJ 0.93, so when
converting code from SML '90 to SML '97 you will occasionally need
to rewrite code to satisfy the value restriction. In converting
the 125K lines of SML code in the SML/NJ compiler, there were about 80
cases where code had to be modified for value polymorphism.
The consequences of a failure of the value restriction differ
according to whether the declaration is at top level (in the
interactive system or in the body of a structure), or local to a
let expression or local declaration. How
top-level failures are treated is implementation dependent, but SML/NJ
eliminates any nongeneralized free type variables by instantiating
them to fresh dummy variables. For example
val x = ref nil;
stdIn:6.1-6.8 Warning: type vars not generalized because of
value restriction are instantiated to dummy types (X1,X2,...)
val x = ref [] : ?.X1 list ref
The fresh dummy types that are generated for this purpose are named
X1, X2, X3, etc. Since these dummy types are not the types of any
values, the result of such a declaration is likely to be of little
use. For instance, in the above example, the only value we will
be able to assign to x is nil, and if we fetch the contents of x,
the only thing we will be able to do with this (empty) list is
calculate its length, append it to itself, etc.
If the declaration has local scope (as in a let
expression or local declaration), then all occurrences of
the declared variable must have the same type. The free type
variables left ungeneralized because of the value restriction may be
instantiated by the context in which the declared variable is used,
as in
let val x = ref nil (* x : 'X list ref *)
in x := [3]; (* x : int list ref *)
hd(!x)
end;
val it = 3 : int
Here when the declaration of x is type checked,
x gets the type 'X list ref for some free
type metavariable 'X, but the way x is used
in the body instantiates 'X to be int.
If the type variables are not instantiated locally, they may be
propagated to outer scopes where they are eventually eliminated either
by instantiation or generalization as in the following examples:
fun f y = let val x = ref nil in x end; (* generalized *)
val f = fn : 'a -> 'b list ref
let val y = let val x = ref nil in x end (* instantiated *)
in y := [true];
if hd(!y) then 1 else 2
end;
val it = 1 : int
In the first of these examples the type variable in the type of
x was generalized to 'b when the type of
f was generalized. Note that all "fun"
declarations automatically satisfy the value restriction, so type
variables introduced when typing a "fun" declaration can
always be generalized. In the second example the ungeneralized
(therefore free) type variable shared by the types of x
and y is instantiated to bool when the body
of the let-expression is type checked.
What should you do when the value restriction applies and a formerly
polymorphic declaration fails to be polymorphic? This depends
on whether the polymorphism was actually exploited or not.
Polymorphism not required
If the declaration is local, and the ungeneralized type variables do
not escape (as in the second example above), then nothing need be
done. In fact, one may not even realize that there was a value
restriction failure in such a case unless one has turned on the
message flag Compiler.Control.valueRestrictionLocalWarn,
which causes a warning message to be printed for value restriction
failures in embedded declarations (i.e. declarations local to
expressions or declarations).
If the declaration was at top-level and only a monotype was required,
a type constraint can be added to eliminate the ungeneralized
(escaping) type variable:
val x : int list ref = ref nil;
Polymorphism required
If polymorphism was required, and is no longer achieved because of the
value restriction, then we need to modify the code. A very common
case involves an expansive expression that
computes a function, such as the partial application of a curried
function to an incomplete list of arguments.
fun f x y = y;
val f = fn : 'a -> 'b -> 'b
val g = f 3;
stdIn:7.1-7.12 Warning: type vars not generalized because of
value restriction are instantiated to dummy types (X1,X2,...)
val g = fn : ?.X1 -> ?.X1
In SML '90, g would have the type 'a -> 'a
because there are no imperative type variables involved, but now in
SML '97 the value restriction comes into play, forcing g
to have a monomorphic type (containing a dummy type X1 to
boot!). We can fix the definition of g to restore the
polymorphic type by converting the expression f 3 into a
value expression using eta-expansion. Eta-expansion
transforms an function valued expression e into (fn
x => (e) x) (choosing the new variable x to make
sure that it is not free in e). In this case, we
eta-expand the definition of g to:
val g = (fn y => (f 3) y);
val g = fn : 'a -> 'a
or, equivalently:
fun g y = f 3 y;
val g = fn : 'a -> 'a
In this case, the eta-expanded definition of g is entirely
equivalent to the original one. But in general we have to be careful,
because the eta-expansion of an expression is not always semantically
equivalent to that expression.
One problem is termination. It may be that the expression defining
g loops or raises an exception:
fun f (x::l) = (fn y => y);
stdIn:14.1-14.27 Warning: match nonexhaustive
x :: l => ...
val f = fn : 'a list -> 'b -> 'b
val g = f nil;
stdIn:15.1-15.14 Warning: type vars not generalized because of
value restriction are instantiated to dummy types (X1,X2,...)
uncaught exception nonexhaustive match failure
raised at: stdIn:14.16
fun g y = f nil y;
val g = fn : 'a -> 'a
With this eta-expanded definition of g, the raising of
the nonexhaustive match exception is delayed from when g
is defined to when g is applied to an argument.
Another situation where eta-expansion does not preserve semantics
is where partial application causes side-effects, as the following
example (borrowed from Andrew Wright) shows.
val counter = ref(ref 0);
val counter = ref (ref 0) : int ref ref
fun mkCountF f =
let val x = ref 0
val f2 = fn z => (x := !x + 1; f z)
in counter := x; (* call counter returned via global counter *)
f2
end;
val mkCountF = fn : ('a -> 'b) -> 'a -> 'b
When applied to a function, mkCountF returns a new
function that behaves like the argument except that a counter records
the number of times it is called. The counter is returned via the
global reference counter. If we define a function by
partially applying mkCountF:
fun pair x = (x,x);
val pair = fn : 'a -> 'a * 'a
val cpair = mkCountF pair;
val cpair = fn : ?.X1 -> ?.X1 * ?.X1
val cpairCalls = !counter (* obtain the counter for cpair *)
val cpairCalls = ref 0 : int ref
the function cpair is not polymorphic. Recovering
polymorphism by eta-expansion changes the behavior:
val cpair' = (fn y => mkCountF pair y)
val cpair' = fn : 'a -> 'a * 'a
Now cpair' is polymorphic, but no counter is produced
when cpair' is defined. Instead, a new counter is produced every time
cpair' is applied, which is not what we want.
Another problem with eta-expansion is the potential for severe
performance penalties.
fun id x = x
val id = fn : 'a -> 'a
fun g f = (heavy(); f)
val g = fn : 'a -> 'a
val id1 = g id
val id1 = fn : ?.X1 -> ?.X1
val id2 = (fn x => g id x)
val id2 = fn : 'a -> 'a
Here the definition of id1 causes heavy
to be called once, but id1 is not polymorphic, while the
function id2 defined by eta-expansion is polymorphic, but
heavy is called every time id2 is applied.
If heavy is a very expensive function, this will probably
not be acceptable.
In the examples given here, the algorithmic differences between the
original function and its eta-expanded version are obvious, but in
real programs, the difference may be rather subtle and easily
overlooked (as I found on at least one occasion when converting the
SML/NJ compiler to obey the value restriction).
So eta-expansion is not a universal solution for restoring
polymorphism to computed functions. When eta-expansion is not
appropriate, one can sometimes rewrite the code more globally to
work around the problem; e.g. by lifting a side-effect or expensive
computation out of the function definition. In the very rare cases
where this fails, and one can't achieve a polymorphic definition, the
last resort is to duplicate code and have multiple definitions. At
least one is no worse off than one would be with a language like
Pascal that does not support polymorphism!
Computed Polymorphic data
There are cases where in SML '90 one might use a non-value expression
to compute a polymorphic data structure. For instance, in SML '90
the declaration
val x = rev []
yields the polymorphic typing x : 'a list. Since
rev [] is not a value expression, x will
not get a polymorphic type in SML '97. If the polymorphic type of
such a data structure declaration was needed, we cannot restore it
by the technique of eta expansion that usually works for function
declarations. As for computed function declarations where eta
expansion is not appropriate, some global rewriting of the code
may be required, including possibly duplicating the declaration.
Fortunately this situation seems to rarely arise in practice.
Treatment of local vs top level declarations
When the type of a variable fails to generalize in a local declaration
because of the value restriction, the ungeneralized free type variables in
its type may be instantiated later on when the variable is used in
the body. In the following expression,
let val r = ref(fn x => x)
in !r 5
end;
the local variable r initially gets the type:
r : ('X -> 'X) ref
Then when the body expression !r 5 is type
checked 'X is unified with int and thereby
eliminated. Thus r ends up with the type int ->
int and the whole let expression has type int.
Since r has only one type in its scope, it cannot be used
inconsistently, so
let val r = ref(fn x => x)
in !r 5; !r true
end;
will cause a type error in the expression !r true
(assuming left to right expression traversal by the type checker).
It is also possible that a free type variable in a local variable's
type will be generalized in a more global scope, as illustrated by
the declaration
fun f () =
let val r = ref(fn x => x)
in !r
end;
where the free type variable 'X in the type r : ('X
-> 'X) ref gets eliminated by polymorphic generalization in the
typing of the declaration of f, with the resulting typing:
val f : unit -> 'a -> 'a
But how do we deal with type variables that remain free in the type
of top-level declarations because of the value restriction? We could
just leave the free type variables in the type as we do for local
declarations, but this would lead to inscrutable behavior at best
or type unsoundness at worst, depending on how these free type
variables are treated. In SML/NJ, our solution is to eliminate
residual free type variables in top-level declarations by
instantiating them to new dummy types. We also print a warning
message indicating that type generalization failed.
val x = ref(fn x => x);
stdIn:1.1-2.18 Warning: type vars not generalized because of
value restriction are instantiated to dummy types (X1,X2,...)
val x = ref fn : (?.X1 -> ?.X1) ref
The new dummy type X1 introduced for this purpose will
not match the type of any value, so there is very little one can
do with the value of x. Nevertheless, we consider it
to be more informative to produce a dummy typing rather than a type
error. There are also situations where the dummy typing doesn't
matter, such as
OS.Process.exit(OS.Process.failure);
stdIn:1.1-19.12 Warning: type vars not generalized because of
value restriction are instantiated to dummy types (X1,X2,...)
where
OS.Process.exit: OS.Process.status -> 'a
In this case, having the value restriction generate a static error
would prevent the execution of the expression, thus preventing the exit
command from taking effect.
The warning message for top-level value restriction violations can be
suppressed by setting the appropriate compiler control flag to false
(the default value is true):
Compiler.Control.valueRestrictionTopWarn := false;
On the other hand, if you also want to see warning messages when local
declarations fail to generalize because of the value restriction, you
can set another flag to true:
Compiler.Control.valueRestrictionLocalWarn := true;
However, these additional warning messages for local declarations are
not very useful in our experience.
Old imperative or weak type variable notation in SML '97
How are the old "imperative" ('_a) or "weak"
('1a) type variables treated? The special annotation
of an underscore or digit following the apostrophe has no significance
in SML '97, so these will be treated as ordinary type variables;
the value restriction means that all type variables are effectively
treated like imperative type variables in SML '90. However, it is
a good idea to remove these annotations from your SML '97 code to
avoid possible confusion.
A declaration such as:
val [x] = nil::nil
is known as a refutable pattern binding since an exception can
potentially be raised depending on the value of the right hand side.
In SML/NJ, the value restriction rule has been tightened to disallow
generalization for such bindings, even though the defining expression
for x can be statically determined to be a value.
This is a minor deviation from the SML '97 definition. The main
justification is the simplicity it provides in the type-theoretic
interpretation. The potential raising of the Bind exception can
be regarded as a side-effect, and a strict version of the value
restriction will suppress type generalization in these cases too.
Formally, one can associate polymorphic generalization with the
introduction of an explicit type abstraction. The type checker
would implicitly transform the declaration
val I = fn x => x
into the explicitly typed version
val I = (FN 'a => fn (x: 'a) => x) : (All 'a). 'a -> 'a
where "FN 'a" is an explicit type abstraction.
If such an explicit type abstraction is suspending (i.e.
suspends evaluation of its body like a normal variable abstraction)
then the abstracted expression should have no computational effect,
including the potential of raising an exception.
Consider
val [x] = nil
which is equivalent to
val x = hd(nil) [1]
which could translate into the explicit form
val x = (FN 'a => hd(nil)) [2]
If the type abstraction is suspending, then versions [1] and [2] are
not equivalent, because [1] raises the Empty exception while [2] does
not. There are technical advantages for this interpretation, which
corresponds closely with the typed internal language used in SML/NJ
(FLINT), so we have adopted this stricter version of the value
restriction.
Nonreturning expressions
It would be possible (that is, we believe it would be sound) to weaken
the value restriction by allowing generalization of types that consist
of a single free type variable. For instance, in the declaration
val x = raise Fail "foo";
the type of the right hand side is 'X (where
'X again represents a free type variable). This can
safely be generalized to the polymorphic type (All
'a). 'a, because the expression does not return a value,
and hence the variable x is not bound to a value and will not be
used. This would also apply to applications of functions like
fun loop () = loop ()
or OS.Process.exit of type (All 'a). t -> 'a for some
domain type t.
We do not admit this weakening of the value restriction in SML '97,
partly because it is not consistent with the suspending type
abstraction model discussed in the previous point.