SML '97 Types and Type Checking

Type Checking

Value Polymorphism

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
Then 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 '_a.
The imperative types were associated with certain primitive functions. The type of ref was an imperative type:
    ref: '_a -> '_a ref
The imperative attribute of a type variable was propagated by substitution during type checking, so the expression ref(fn x => x) would have the typing
    ref(fn x => x)  : ('_b -> '_b) ref
where the imperative type variable '_b is 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 declaration
    val y = ref(fn x => x);
would yield a nonpolymorphic type ('_X -> '_X) ref for y containing 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 '_X could 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 -> '_a
A 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):

a literal constant (e.g. 3),
a variable (e.g. x),
nullary data constructor (e.g. nil),
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. x::nil) (excluding ref).
The value polymorphism rule is then 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. 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 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 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 := [3];
    =    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:
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 : 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 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 x and y is instantiated to bool when 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 -> ?.X1
Here 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 3 into a value expression using eta expansion, which transforms an expression e into (fn x => (e) x) (making sure that the variable x did 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 -> 'a
or, equivalently:
    - fun g y = f 3 y;
    val g = fn : 'a -> 'a
In 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 -> '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.
    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 mkCountF
    fun pair x = (x,x);
    val cpair = mkCountF pair;
    val cpairCalls = !counter
the function cpair is 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 id1 causes expensive to be called once, but id1 is not polymorphic, while the function id2 defined by eta-expansion is polymorphic, but expensive is called every time id2 is applied.
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 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
where I am adopting the convention that a capitalized type variable such as 'X is free rather than bound (i.e. polymorphic or generalized). 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 inconsistenly, 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 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) 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 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,...)
where
    OS.Process.exit: OS.Process.status -> 'a
In 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.valueRestrictionLocalWarn to 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.

Nonrefutable pattern restriction
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 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 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, so we have adopted this stricter version of the value restriction.
Nonreturning expressions
It 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 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). τ -> '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.

Overloaded literals

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 : word
As this illustrates, if the context does not explicitly or implicitly determine the type of a literal, it is assigned a default type: Int.int for integer literals and Word.word for word literals.

Overloaded functions with defaults

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 -> int
If 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

Explicit type variable binding

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 code
    val x = (let val id : 'a -> 'a = fn z => z in Id Id end,
	     fn y => y);
the type variable 'a used in the type of id is implicitly bound at the declaration val id, so id has a polymorphic type. However, if we add another occurence of 'a, as in
    val x = (let val id : 'a -> 'a = fn z => z in id id end,
	     fn (y: 'a) => y);
now 'a is implicitly bound at the val x declaration. This means that id is no longer polymorphic, because 'a acts 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 becomes
    val 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, becomes
    val 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 rec declarations. SML/NJ supports the notation
    val rec 'a f = (fn x: 'a => x);
while the Definition would have
    val 'a rec f = (fn x: 'a => x);

Local datatypes

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 as
  let datatype A = C of bool
   in fn (C x) = not x         (* : A -> bool *)
  end
  let datatype B = C of int
   in C 2                      (* : B *)
  end
could be successfully type checked because the internal type name for A could be reused for B, meaning that types A and B would agree and the application would be accepted. This is unsound of course, because it is equivalent to not(2).
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 expression let dec in exp end, the type of the let expression, which is the type of exp cannot contain any generative types declared in dec. This means that an expression like
  let datatype t = C in C end
should 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
	  end
Because of the conditional expression, x gets 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!).

Datatype replication declarations

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 t in a structure A:
  structure A =
  struct
    datatype t = C | D of t
  end
I can define a new structure B that contains an alias of t as follows:
  structure B =
  struct
    type t = A.t
  end
but then B have provide access to the data constructors of t. If I define B as
  structure B =
  struct
    type t = A.t
    val C = A.C
    val D = A.D
  end
I gain access to the constructors C and D as values, but I still can't use them in patterns.
In SML '90, one gets around this problem by using the open declaration:
  structure B =
  struct
    open A
  end
and if A has additional components that B is not supposed to gain access to you have to use a signature constraint on B to filter them out. This is not an ideal solution, because it unnecessarily polutes the name space within the body of B with 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 is
  datatype tycon = datatype longtycon
where (as the the Definition), tycon is an identifier naming a type constructor (in the TyCon name space), and longtycon is 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. So
  structure B =
  struct
    datatype t = datatype A.t
  end
is equivalent to the declaration of B version about using open, i.e. B.C and B.D are defined as constructors and can be used in patterns.
A common error with datatype replication declarations is to leave out the datatype keyword on the right hand side, as in
  structure B =
  struct
    datatype t = A.t
  end
This 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 written
  structure B =
  struct
    open A
    datatype t = t
  end
There would be no complaint from the compiler, because the t on the right hand side would be treated as a valid data constructor name having nothing to do with the datatype t in A.
As we will see in the chapter on modules, there is an analogous datatype replication specification for use in signatures.

real not an equality type

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 = x is not always true for floating point numbers, because nan = nan is false.
The function Real.== implements IEEE equality for reals, but because of its unusual behavior we no longer treat Real.real as an equality type. For consistency, we also reject real literals as constants in patterns. This means that an expression like
    x = 5.6
has to be rewritten as
    Real.==(x,5.6),
and a case expression like
    case x
      of 5.6 => 0
       | 3.2 => 1
       | ~1.7 => 2
       | _ => 3
has 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

Dave MacQueen

Last modified: Wed Mar 4 12:39:46 EST 1998

SML '97 Types and Type Checking

Background

What is a value?

What does it mean in practice?

Polymorphism not required.

Polymorphism required.

Computed Polymorphic data

Treatment of local vs top level declarations

Old imperative or weak type variable notation in SML '97

Nonreturning expressions