BackgroundThe 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 typer: ('a -> 'a) refThen in the body of the let declaration the type of the first occurrence of r could be instantiated as
(int -> int) ref, while the second occurrence could have the type (bool -> bool) ref. This typing is clearly unsound, since it allows a function on integers to be applied to a boolean value.
More generally, what is going on here is that a mutable value (here a ref cell) is given a polymorphic type. This allows the type of the mutable value to be instantiated differently at a point 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 which 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 unconnected 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 normal rule for introducing polymorphism for let-bound variables that suffices for purely functional languages is not adaquate in a language like ML with side effects. 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 was a polymorphic type whose bound type variable was of a special form, called an imperative type variable, distinguished by an initial underscore in the type variable name, for example
The imperative types were associated with certain primitive functions. The type of
refwas an imperative type:ref: '_a -> '_a refThe imperative attribute of a type variable was propagated by substitution during type checking, so the expression
ref(fn x => x)would have the typingref(fn x => x) : ('_b -> '_b) refwhere the imperative type variable
'_bis free, not quantified. Thus the effect of imperative type variables was to limit the introduction of polymorphism. In a value declaration, free imperative type variables could 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 was "nonexpansive", meaning that it was a function expression (i.e. a lambda abstraction). Thus typing the declarationval y = ref(fn x => x);would yield a nonpolymorphic type
('_X -> '_X) reffor
ycontaining a free imperative type variable
'_X. If the declaration is at top level this would cause an error message, indicating that the imperative type variable
'_Xcould not be generalized, because
ref(fn x => x)is a function application, and therefore expansive.
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 entended the power of the type system by allowing the types of certain expansive expressions to be generalized (e.g. partial application of some polymorphic curried functions). The drawbacks of both the imperative type and the related weak type schemes were that they required a special kind of type variable and were relatively complicated and hard to explain to novices (especially SML/NJ's weak types).
Another major problem was that imperative types would infect interfaces. That is, a given signature might be have semantically equivalent implementations written in two different styles, one functional and the other using imperative features. The types of the components in the functional implementation would be normal polymorphic types. However, even though their behavior was equivalent, the types of the corresponding components of the imperative implementation might be imperative polymorphic types, because of the conservative character of the restriction. For example, here are two equivalent implementations of the identity function:fun idFun x = x idFun : 'a -> 'a fun idImp x = !(ref x) idImp : '_a -> '_aA single signature that is meant to describe the common interface of both implementations must therefore specify the imperative type. If the imperative version is introduced after the functional version already existed, it becomes necessary to go back and revise the earlier signature to change polymorphic types to imperative types.
An simpler approach to controlling the interaction of polymophism and side-effects had been considered during the design of Standard ML. The idea was to disallow the generalization of all type variables for expansive expressions (we'll call this the "value resriction" method), which is equivalent to having all type variables be imperative variables. This solution avoided the need for a separate variaty of imperative type variables, but it was thought to be too restrictive. However, after several years of investigation of more elaborate schemes that attempted to weaken the restriction (like the weak type system in SML/NJ), Andrew Wright decided to do 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 investegated what changes were required to covert 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.
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. But first we need to be precise about what the value restriction means.
What is a value?
An expression is nonexpansive if it is (ignoring any explicit type constraints):
The value polymorphism rule is then that in a declaration such as
- a literal constant (e.g.
- a variable (e.g.
- nullary data constructor (e.g.
- an atomic function expression (e.g.
(fn x => x)),
- a tuple or record of nonexpansive expressions,
- a data constructor applied to a nonexpansive argument expression (e.g.
ref).val pat = expthe 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. We shall also speak of this as the value restriction.
This is roughly equivalent to modifying the old imperative type scheme by treating every type variable as an imperative variable. As with the older scheme, the intent and consequence is to prevent the creation of mutable values (like refs and arrays) with polymorphic types that could be instantiated differently when values are stored and retrieved.
What does it mean in practice?The value polymorphism scheme is strictly more restrictive than the imperative types scheme of SML '90 (and the weak types that SML/NJ has used as a generalization of imperative types). When converting code from SML '90 to SML '97, there will be occasional need to rewrite code to conform to 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
localdeclaration. 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
localdeclaration), then all occurences 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 = in x := ; = hd(!x) = end; val it = 3 : intHere when the declaration of x is type checked, x gets the type
'X list reffor some free type metavariable
'X, but the way
xis used in the body instantiates
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:
Example 1- fun f y = let val x = ref nil in x end; val f = fn : 'a -> 'b list ref Example 2- let val y = let val x = ref nil in x end = in y := [true]; = if hd(!y) then 1 else 2 = end; val it = 1 : intIn the first of these examples the type variable in the type of x was generalized to
'bwhen the type of f was generalized. Note that all "
fun" declarations satisfy the value restriction, so variables declared in "
fun" declarations can always be polymorphic. In the second example the ungeneralized (therefore free) type variable shared by the types of
yis instantiated to
boolwhen the body of the
let-expression is type checked.
What should one do when the value restriction applies? This depends on whether a polymorphic type was required or not.
Polymorphism not required.If the declaration is local, and the ungeneralized type variables do not escape (as in Example 3), 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. The most common situation this occurs is a nonvalue (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 -> ?.X1Here would like g to have the type
'a -> 'a, as it would have in SML 90 because there are no imperative type variables involved. We can fix the definition of g to restore the polymorphic type by converting the expression
f 3into a value expression using eta expansion, which transforms an expression
(fn x => (e) x)(making sure that the variable
xdid not appear 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 -> 'aor, equivalently:- fun g y = f 3 y; val g = fn : 'a -> 'aIn this case, the second definition of g is entirely equivalent to the first. But there are some possible pitfalls, 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 -> 'aWith 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.val counter = ref(ref 0); 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;When applied to a function, mkCountF returns a new function that behaves like the argument except that a counter (
int ref) records the number of times it is called. The counter is returned via the global reference
counter(thanks to Andrew Wright for this example). If we define a function by partially applying mkCountFfun pair x = (x,x); val cpair = mkCountF pair; val cpairCalls = !counterthe function
cpairis not polymorphic. Recovering polymorphism by eta-expansion changes the behavior:val cpair' = (fn y => mkCountF pair y)We see that no counter is produced when cpair' is defined, but a new counter is produced every time cpair' is applied.
Another problem with eta-expansion is the potential for severe performance penalties.fun id x = x fun g f = (expensive(); f) val id1 = g id val id2 = (fn x => g id x)Here the definition of
expensiveto be called once, but
id1is not polymorphic, while the function
id2defined by eta-expansion is polymorphic, but expensive is called every time
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 coverting 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 dataThere 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,
xwill 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 declarationsWhen 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
rinitially gets the typer : ('X -> 'X) refwhere I am adopting the convention that a capitalized type variable such as
'Xis free rather than bound (i.e. polymorphic or generalized). Then when the body expression
!r 5is type checked
'Xis unified with
intand thereby eliminated. Thus
rends up with the type
int -> intand the whole let expression has type
rhas only one type in its scope, it cannot be used inconsistenly, solet 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 declarationfun f () = let val r = ref(fn x => x) in !r end;where the free type variable
'Xin the type
r : ('X -> 'X) refgets 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 unsoundess 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) refThe new dummy type
X1introduced 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 bogus typing rather than a type error. There are also situations where the bogus 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,...)whereOS.Process.exit: OS.Process.status -> 'aIn this case, a value restriction error would prevent the execution of the expression, preventing the exit command from taking place.
The top-level value restriction warning message can be suppressed by setting the appropriate 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 the flag
Compiler.Control.valueRestrictionLocalWarnto 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 '97How 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.
Nonrefutable pattern restrictionA declaration such as:val [x] = nil::nilis 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 binding to 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 declarationval I = fn x => xinto the explicitly typed versionval I = (FN 'a => fn (x: 'a) => x) : (All 'a). 'a -> 'awhere "
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. Considerval [x] = nilwhich is equivalent toval x = hd(nil) (* 1 *)which could translate into the explicit formval 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, so we have adopted this stricter version of the value restriction.
Nonreturning expressionsIt would be possible (i.e. 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 declarationval x = raise Fail "foo";the type of the right hand side is
'Xagain 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 likefun loop () = loop ()or OS.Process.exit of type
(All 'a). τ -> 'a)for some domain type τ.
We do not admit this weakening of the value restriction, partly because it is not consistent with the suspending type abstraction model discussed in the previous point.
SML '97 supports multiple precisions of integers (Int31.int, Int32.int) and words (Word8.word, Word31.word, Word32.word) (and potentially floating reals). It is convenient to overload integer literals (e.g.
3), and word literals (e.g.
0w3, so SML '97 supports this.- 3; val it = 3 : int (* int = Int.int = Int31.int *) - 3 : Int31.int; val it = 3 : int - 3 : Int32.int; val it = 3 : Int32.int - 0w3; val it = 0wx3 : word (* word = Word.word = Word31.word *) - 0w3 : Word8.word; val it = 0wx3 : Word8.word - 0w3 : Word31.word; val it = 0wx3 : word - 0w3 : Word32.word; val it = 0wx3 : Word32.word - 0w3 :Word.word; val it = 0wx3 : wordAs this illustrates, if the context does not explicitly or implicitly determine the type of a literal, it is assigned a default type:
Int.intfor integer literals and
Word.wordfor word literals.
Like SML '90, SML '97 provides a fixed set of overloaded functions, including arithmetic operators such as
+and relational operators such as
>. In SML '90, the context has to provide enough type information to resolve the overloaded operator (i.e. to assign it exactly one of the possible types that the operator is capable of assuming). If the overloaded operator is not resolved, an SML '90 compiler generates an error message:- fun f x = x + x; std_in:10.13 Error: overloaded variable cannot be resolved: +In SML '97, an overloaded function that is not resolved by its context is assigned a default type (normally the integer version of the operator).- fun f x = x + x; val f = fn : int -> intIf you don't want the default type, you must override it by adding explicit type constraints, as in:- fun f (x: real) = x + x; val f = fn : real -> real
When a programmer uses a type variable in a type constraint in an expression or declaration, there is a natural, but fairly complicated rule that determines where that type variable is implicitly bound.
For instance, in the codeval x = (let val id : 'a -> 'a = fn z => z in Id Id end, fn y => y);the type variable
'aused in the type of
idis implicitly bound at the declaration
val id, so
idhas a polymorphic type. However, if we add another occurence of 'a, as inval x = (let val id : 'a -> 'a = fn z => z in id id end, fn (y: 'a) => y);now
'ais implicitly bound at the
val xdeclaration. This means that
idis no longer polymorphic, because
'aacts like a monomorphic type identifier within the body of its binding scope, and so the later declaration will not type check.
Since the application of the scoping rule for such explicit type variables is a bit tricky, it would be preferable to be able to explicitly determine where the type variable is bound. SML '97 provides a notation for this. Here are some examples:fun 'a id(z: 'a) = z val 'a id : 'a -> 'a = fn z => z fun ('a, 'b) pair (x: 'a) (y: 'b) = (x,y)So using this notation, the first example above becomesval x = (let val 'a id : 'a -> 'a = fn z => z in Id Id end, fn y => y);while the second, which still doesn't type check, becomesval x = (let val id : 'a -> 'a = fn z => z in id id end, fn (y: 'a) => y);Note: There is a descrepancy between the syntax supported by SML/NJ and that of the Definition in the case of explicit type variable bindings in
val recdeclarations. SML/NJ supports the notationval rec 'a f = (fn x: 'a => x);while the Definition would haveval 'a rec f = (fn x: 'a => x);
In the SML '90 formal definition, there were deficiencies in the way that new type names (i.e. internal type identifiers) were managed. These deficiencies would allow a generative type name to be reused for another type while values of the original type were still in the environment. Thus according to the Definition, an expression such aslet datatype A = C of bool in fn (C x) = not x (* : A -> bool *) end let datatype B = C of int in C 2 (* : B *) endcould be successfully type checked because the internal type name for
Acould be reused for
B, meaning that types
Bwould agree and the application would be accepted. This is unsound of course, because it is equivalent to
Implementations (e.g. SML/NJ) typically implement generative type declarations (datatypes and abstypes) by ensuring that unique names are assigned to each declared type, so this problem does not apply to implementations, but is an artifact of the way the formal definition was designed. Since the SML '97 Definition is still vulnerable to this problem, the language has been restricted to ensure soundness of the Definition. The language restrictions ensure that a locally declared datatype cannot escape from the static scope of its declaration. Thus in a
let dec in exp end, the type of the let expression, which is the type of
expcannot contain any generative types declared in
dec. This means that an expression likelet datatype t = C in C endshould not type check in SML '97.
Another way that a local generative type could escape from it's scope is through type unification, as in the following expression.fn x => let datatype t = C val _ = if true then x else C in 5 endBecause of the conditional expression,
xgets the type t, and the entire function expression gets the type
t -> int, even though it extends outside the scope of the declaration of
t. So this sort of expression is also not allowed in SML '97.
SML/NJ Deviation: Currently, SML/NJ still type checks both the above forms of expression, so the new restriction is not currently enforced. As we noted before, this relates to an unsoundness in the Definition that does not affect implementation (unless they adhere too slavishly to the Definition!).
In SML '90, there was no direct way for one module to inherit a datatype as a datatype from another module. For instance, suppose I have a datatype
tin a structure
A:structure A = struct datatype t = C | D of t endI can define a new structure
Bthat contains an alias of
tas follows:structure B = struct type t = A.t endbut then
Bhave provide access to the data constructors of
t. If I define
Basstructure B = struct type t = A.t val C = A.C val D = A.D endI gain access to the constructors
Das values, but I still can't use them in patterns.
In SML '90, one gets around this problem by using the
opendeclaration:structure B = struct open A endand if A has additional components that
Bis not supposed to gain access to you have to use a signature constraint on
Bto filter them out. This is not an ideal solution, because it unnecessarily polutes the name space within the body of
Bwith all the component names in A.
To support the sharing of datatypes between modules directly, without the use of
open, SML '97 introduces a new form of datatype declaration: the datatype replication declaration. Its syntax isdatatype tycon = datatype longtyconwhere (as the the Definition),
tyconis an identifier naming a type constructor (in the TyCon name space), and
longtyconis a symbolic path (e.g.
A.t) ending in a type constructor name. A datatype replication makes the tycon be an alias for the datatype named by longtycon, and in addition implicitly declares the data constructor names for longtycon. Sostructure B = struct datatype t = datatype A.t endis equivalent to the declaration of
Bversion about using
B.Dare defined as constructors and can be used in patterns.
A common error with datatype replication declarations is to leave out the
datatypekeyword on the right hand side, as instructure B = struct datatype t = A.t endThis causes A.t to be treated as a constructor declaration, and an error results because a qualified name is illegal in this case. But if I had writtenstructure B = struct open A datatype t = t endThere would be no complaint from the compiler, because the
ton the right hand side would be treated as a valid data constructor name having nothing to do with the datatype
As we will see in the chapter on modules, there is an analogous datatype replication specification for use in signatures.
SML '97 uses the IEEE semantics for floating point operations. Equality for floating point numbers in the IEEE standard does not behave the way equality is expected to behave in SML. For instance,
x = xis not always true for floating point numbers, because
nan = nanis false.
Real.==implements IEEE equality for reals, but because of its unusual behavior we no longer treat
Real.realas an equality type. For consistency, we also reject real literals as constants in patterns. This means that an expression likex = 5.6has to be rewritten asReal.==(x,5.6),and a case expression likecase x of 5.6 => 0 | 3.2 => 1 | ~1.7 => 2 | _ => 3has to be rewritten using conditionals like this:if Real.==(x,5.6) then 0 else if Real.==(x,3.2) then 1 else if Real.==(x,~1.7) then 2 else 3