Sample Code for this Chapter

Just as in any other programming language, values may be assigned to variables that may be used in an expression to stand for that value.  However, in sharp contrast to more familiar languages, variables in SML do not vary (!).  Values are bound to variables using value bindings; once a variable is bound to a value, it is bound for life.  There is no possibility of changing the binding of a variable after it has been bound.  In this respect variables in SML are more akin to variables in mathematics than to variables in languages such as C.  Similarly, types may be bound to type variables using type bindings; the type variable so defined stands for the type bound to it and can never stand for any other type.

A binding (either value or type) introduces a "new" variable, distinct from all other variables of that class, for use within its range of significance, or scope.   Scoping in SML is lexical, meaning that the range of significance of a variable is determined by the program text, not by the order of evaluation of its constituent expressions.  (Languages with dynamic scope adopt the opposite convention.)  For the time being variables will have global scope, meaning that the range of significance of the variable is the "rest" of the program --- the part that lexically follows the binding.  We will introduce mechanisms for delimiting the scopes of variables shortly.

Any type may be give a name using a type binding. At this stage we have so few types that it is hard to justify binding type names to identifiers, but we'll do it anyway because we'll need it later. Here are some examples of type bindings:

type float = real

type count = int and average = real

The first type binding introduces the type variable float, which subsequently is synonymous with real.  The second introduces two type variables, count and average, which stand for int and real, respectively.  In general a type binding introduces one or more new type variables simultaneously in the sense that the definitions of the type variables may not involve any of the type variables being defined.  Thus a binding such as

type float = real and average = float

is nonsensical (if taken in isolation) since the type variables float and average are introduced simultaneously, and hence cannot refer to one another.  The syntax for type bindings is type var1 = typ1 and ... and varn = typn, where each vari is a type variable and each typi is a type expression.

Similarly, value variables are bound to values using value bindings. Here are some examples:

val m : int = 3+2

val pi : real = 3.14 and e : real = 2.17

The first binding introduces the variable m, specifying its type to be int and its value to be 5.  The second introduces two variables, pi and e, simultaneously, both having type real, and with pi having value 3.14 and e having value 2.17.   Notice that a value binding specifies both the type and the value of a variable.   The syntax of value bindings is val var1 : typ1 = exp1 and ... and varn : typn = expn, where each vari is a variable, each typi is a type expression, and each expi is an  expression.

As you have no doubt surmised, value bindings are type-checked by comparing the type of the right-hand side with the specified type to ensure that they coincide. If a mismatch occurs, the value binding is rejected as ill-formed. Well-typed bindings are evaluated according to the bind-by-value rule: the right-hand side of the binding is evaluated, and the resulting value (if any) is bound to the given variable.

The purpose of a binding is to make a variable available for use within its scope.   In the case of a type binding we may use the type variable introduced by that binding in type expressions occurring within its scope.  For example, in the presence of the type bindings above, we may write

val pi : float = 3.14

since the type variable float is bound to the type real, the type of the expression 3.14.  Similarly, we may make use of the variable introduced by a value binding in value expressions occurring within its scope.   Continuing from the preceding binding, we may use the expression

sin pi

to stand for 0.0 (approximately), and we may bind this value to a variable by writing

val x : float = sin pi

As these examples illustrate, type checking and evaluation are context dependent in the presence of type and value bindings since we must refer to these bindings to determine the types and values of expressions.  For example, to determine that the above binding for x is well-formed, we must consult the binding for pi to determine that it has type float, consult the binding for float to determine that it is synonymous with real, which is necessary for the binding of x to have type float.

The rough-and-ready rule for both type-checking and evaluation is that a bound variable is implicitly replaced by its binding prior to type checking and evaluation.   This is sometimes called the substitution principle for bindings.    For example, to evaluate the expression cos x in the scope of the above declarations, we first replace both occurrences of x by its value (approximately 0.0), then compute as before, yielding (approximately) 1.0.   Later on we will have to refine this simple principle to take account of more sophisticated language features, but it is useful nonetheless to keep this simple idea in mind.

Bindings may be combined to form declarations.  A binding is an atomic declaration, even though it may introduce many variables simultaneously.  Two declarations may be combined by sequential composition by simply writing them one after the other, optionally separated by a semicolon. Thus we may write the declaration

val m : int = 3+2
val n : int = m*m

which binds m to 5 and n to 25. Subsequently, we may evaluate m+n to obtain the value 30.   In general a sequential composition of declarations has the form dec1 ... decn, where n is at least 2.  The scopes of these declarations are nested within one another: the scope of dec1 includes dec2 ... decn, the scope of dec2 includes dec3 ... decn, and so on.

One thing to keep in mind is that binding is not assignment. The binding of a variable never changes; once bound to a value, it is always bound to that value (within the scope of the binding). However, we may shadow a binding by introducing a second binding for a variable within the scope of the first binding.  Continuing the above example, we may write

val n : real = 2.17

to introduce a new variable n with both a different type and a different value than the earlier binding.  The new binding eclipses the old one, which may then be discarded since it is no longer accessible.  (Later on, we will see that in the presence of higher-order functions shadowed bindings are not always discarded, but are preserved as private data in a closure.  One might say that old bindings never die, they just fade away.)

The scope of a variable may be delimited by using let expressions and local declarations. A let expression has the form let dec in exp end, where dec is any declaration and exp is any expression. The scope of the declaration dec is limited to the expression exp.   The bindings introduced by dec are (in effect) discarded upon completion of evaluation of exp.  Similarly, we may limit the scope of one declaration to another declaration by writing local dec in dec' end.  The scope of the bindings in dec is limited to the declaration dec'.  After processing dec', the bindings in dec may be discarded.

The value of a let expression is determined by evaluating the declaration part, then evaluating the expression relative to the bindings introduced by the declaration, yielding this value as the overall value of the let expression. An example will help clarify the idea:

    val m:int = 3
    val n:int = m*m

This expression has type int and value 27, as you can readily verify by first calculating the bindings for m and n, then computing the value of m*n relative to these bindings. The bindings for m and n are local to the expression m*n, and are not accessible from outside the expression.

If the declaration part of a let expression eclipses earlier bindings, the ambient bindings are restored upon completion of evaluation of the let expression. Thus the following expression evaluates to 54:

val m:int = 2
val r:int =
        val m:int=3
        val n:int=m*m
    end * m

The binding of m is temporarily overridden during the evaluation of the let expression, then restored upon completion of this evaluation.

To complete this chapter, let's consider in more detail the context-sensitivity of type checking and evaluation in the presence of variable bindings.  The key ideas are:

  1. Type checking must take account of the declared type of a variable.
  2. Evaluation must take account of the declared value of a variable.

This is achieved by maintaining environments for type checking and evaluation. The type environment records the types of variables; the value environment records their values.   For example, after processing the compound declaration

val m : int = 0
val x : real = sqrt(2)
val c : char = #"a",

the type environment contains the information

val m : int
val x : real
val c : char

and the value environment contains the information

val m = 0
val x = 2.14…
val c = #"a".

In a sense the value declarations have been divided in "half", separating the type from the value information.

Thus we see that value bindings have significance for both type checking and evaluation.  In contrast type bindings have significance only for type checking, and hence contribute only to the type environment.  A type binding such as

type float = real

is recorded in its entirety in the type environment, and no change is made to the value environment.  Subsequently, whenever we encounter the type variable float in a type expression, it is replaced by real in accordance with the type binding above.

Earlier we introduced two relations, the typing relation, exp : typ, and the evaluation relation, exp => val.  These two-place relations were sufficient for variable-free expressions, but in the presence of declarations these relations must be extended to account for the type and value environments.  This is achieved by expanding the typing relation into a three-place relation typenv |- exp : typ, where typenv is a type environment, exp is an expression and typ is a type.   (The turnstile symbol, "|-", is a punctuation mark separating the type environment from the expression and its type.)  The type of a variable is determined by consulting the type environment; in particular, we have the following typing axiom:

... val x : int ... |- x : int

Similarly, the evaluation relation is enriched to take account of the value environment.  We write valenv |- exp => val to indicate that exp evaluates to val in the value environment valenv.  Variables are governed by the following axiom:

... val x = val ... |- x => val

There is an obvious similarity between the two relations.

Sample Code for this Chapter