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:
let
val m:int = 3
val n:int = m*m
in
m*n
end
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 =
let
val m:int=3
val n:int=m*m
in
m*n
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:
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.