Computation in familiar programming languages such as C is based on the imperative model of computation described in terms of an abstract machine. The meaning of a C program is a state transition function that transforms the initial state of the abstract machine into a final state. The transitions consist of modifications to the memory of the abstract machine (including the registers), and having an effect on the external world (through I/O devices). The constructs of C have the flavor of commands: do something, then do something else for a while, then do something else.
Computation in ML is of an entirely different nature. In ML we compute by calculation of expressions, rather than execution of instructions. (Later in the course we will see that these two viewpoints may be reconciled, but for the time being it is best to keep a clear distinction in mind.) The calculation model is a direct generalization of your experience from high school algebra in which you are given a polynomial in a variable x and are asked to calculate its value at a given value of x. We proceed by "plugging in" the given value for x, and then using the ordinary rules of arithmetic to determine the value of the polynomial. The ML model of computation is essentially just a generalization of this idea, but rather than restrict ourselves to arithmetic operations on the reals, we admit a richer variety of values and a richer variety of primitive operations on them. Much later we will generalize this model a bit further to admit effects on memory and the external world, leading to a reconciliation with the imperative model of computation with which you are familiar.
The unit of evaluation in ML is the expression. Every expression in Standard ML
Roughly speaking, the type of an expression in ML is a description of the sort of value
it yields, should it yield a value at all. For example, if an expression has type int
,
then its values are going to be integers, and similarly, an expression of type real
has real numbers (in practice, floating point numbers) as values. Every expression
is required to have a type; otherwise, it is rejected as ill-typed (with a
suitable explanatory message). A well-typed expression is evaluated (by a
process of calculation) to determine its value, if indeed it has one. An expression
can fail to have a value in several ways, one of which is to incur a run-time error (such
as arithmetic overflow), and another of which is to compute infinitely without yielding a
value. The soundness of the ML type system ensures that if the expression has a
value, then the shape of that value is determined by the type of the expression.
Thus, a well-typed expression of type int cannot evaluate to a string or a floating point
number; it must be an integer. As we will see (much) later it is also possible for
evaluation to engender an effect on the computing environment, for example by
writing to the window system or requesting input from a file. For the time being we
will ignore effects.
What is a type? There are many possible answers, depending on what you wish to emphasize. Here we will emphasize the role of types as determining the set of well-formed programs. Generally speaking, a type consists of
To start off with, let's consider the type of integers. Its name is, appropriately
enough, int
. Values of type int
are the integer numerals
0
, 1
, ~1
, 2
, ~2
, and
so on. Notice that the additive inverse operation in SML is written using a tilde (~
),
rather than a minus sign (-
). Operations on integers include addition and
subtraction, +
and -
, and the operations div
and mod
for dividing and calculating remainders. (See the Standard
ML Basis Library chapter on integers for a complete description.)
Values are one form of atomic expression; others will be introduced later. Compound expressions include atomic expressions, and also include expressions built by applying an operator to other compound expressions. The formation of expressions is governed by a set of typing rules that define the types of atomic expressions and determine the types of compound expressions in terms of the types of their constituent expressions.
The typing rules are generally quite intuitive since they are consistent with our experience in mathematics and in other languages. In their full generality the rules are somewhat involved, but we will sneak up on them by first considering only a small fragment of SML, building up additional machinery as we go along.
Here are some simple arithmetic expressions, written using infix notation for the operations (meaning that the operator comes between the arguments, as is customary in mathematics):
3
3 + 4
4 div 3
4 mod 3
Each of these expressions is well-formed; in fact, they each have type int
.
Writing exp : typ to indicate that the expression exp has the
type typ, we have
:
3
int
:
3 + 4int
:
4 div 3int
:
4 mod 3int
Why? In the case of the value 3
, this is an axiom: integer
numerals have integer type, by definition. What about the expression 3+4
?
Well, the addition operation takes two arguments (written on either side of the plus
sign), each of which must be an integer. Since both arguments are of type int
,
it follows that the entire expression is of type int
. For more complex cases
we proceed analogously, deducing that (3+4) div (2+3)
: int
, for
example, by observing that (3+4)
: int
and (2+3)
: int
.
This kind of reasoning may be summarized by a typing derivation consisting of a
nested sequence of typing assertions, each justified either by an axiom, or a typing rule
for an operation. For example, (3+4) div 5
: int
because
(3+4)
: int
1.1 3
: int
1.2 4
: int
5
: int
Implicit in this derivation is the rule for formation of div
expressions:
it has type int
if both of its arguments have type int
.
Steps (1) and (2) justify the assertion (3+4) div 5
: int
by
demonstrating that the arguments each have type int
. Recursively, we
must justify that (3+4)
: int
, which follows from the
subsidiary steps to step (1). Here we rely on the rule that the addition of two
expressions has type int
if both of its arguments do.
Evaluation of expressions is governed by a similar set of rules, called evaluation rules, that determine how the value of a compound expression is determined as a function of the values of its constituent expressions. Implicit in this description is the call-by-value principle, which states that the arguments to an operation are evaluated before the operation is applied. (While this may seem intuitively obvious, it's worth mentioning that not all languages adhere to this principle.)
We write exp => val to indicate that the expression exp has value val. Informally, it is easy to see that
=>
5
5
=>
2+35
(2+3) div (1+4)
=>1
These assertions can be justified by evaluation derivations, which are similar
in form to typing derivations. For example, we may justify the assertion (3+2) div 5
=> 1
by the derivation
(3+2)
=> 5
1.1 3
=> 3
1.2 2
=> 2
5
=> 5
Some things are left implicit in this derivation. First, it is an axiom that
every value (in this case, a numeral) evaluates to itself; values are fully-evaluated
expressions. Second, the rules of addition are used to determine that adding 3
and 2
yields 5
.
Not every expression has a value. A simple example is the expression 5 div
0
, which is undefined. If you attempt to evaluate this expression it will
incur an execution fault, reflecting the erroneous attempt to divide a number by zero.
The fault is expressed in ML by raising an exception; we will have more to
say about exceptions later in these notes. Another
reason that a well-typed expression might not have a value is that the attempt to evaluate
it leads to an infinite loop. We don't yet have the machinery in place to define
such expressions, but it is indeed possible for an expression to diverge, or run
forever when evaluated.
What types are there besides the integers? Here are a few more base types, summarized briefly by their values and operations:
Type name: real
Values: 3.14
, ~2.17
, 0.1E6
, ...
Operations: +
,-
, *
,/
, =
,
<
, ...
Type name: char
Values: #"a"
, #"b"
, ...
Operations: ord
, chr
, =
, <
,
...
Type name: string
Values: "abc"
, "1234"
, ...
Operations: ^
, size
, =
, <
,
...
Type name: bool
Values: true
, false
Operations: if
exp then
exp1 else
exp2
There are many, many others (in fact, infinitely many others!), but these are enough to
get us started. (See the Basis Library for a complete
description of the primitive types of SML, including the ones given above.) Notice
that some of the arithmetic operations for real numbers are "spelled" the same
way as for integers. For example, we may write 3.1+2.7
to perform a
floating point addition of two floating point numbers. On the other hand division,
which is properly defined for reals, is written as 3.1/2.7
to distinguish it
from the integer division operation div
.
With these types in hand, we now have enough rope to hang ourselves by forming ill-typed expressions. For example, the following expressions are ill-typed:
size 45
#"1" + 1
#"2" ^ "1"
3.14 + 2
The last expression may seem surprising, at first. The primitive arithmetic operations are overloaded in the sense that they apply either to integers or to reals, but not both at once. To gain some intuition, recall that at the hardware level there are two distinct arithmetic units, the integer (or fixed point) unit and the floating point unit. Each has its own separate hardware for addition, and we may not mix the two in a single instruction. Of course the compiler might be expected to sort this out for you, but then there are difficulties with round-off and overflow since different compilers might choose different combinations of conversions and operations. SML leaves this to the programmer to avoid ambiguity and problems with portability between implementations.
The conditional expression if
exp then
exp1
else
exp2 is used to discriminate on a Boolean value.
It has type typ if exp has type bool
and both exp1
and exp2 have type typ. Notice that both
"arms" of the conditional must have the same type! It is evaluated by
first evaluating exp, then proceeding to evaluate either exp1
or exp2, according to whether the value of exp is true
or false
. For example,
if 1<2 then "less" else "greater"
evaluates to "less"
since the value of the expression 1<2
is true.
Notice that the expression
if 1<2 then 0 else 1 div 0
evaluates to 0
, even though 1 div 0
incurs a run-time error.
While it may, at first glance, appear that this is a violation of the call-by-value
principle mentioned above, the explanation is that the conditional is not a primitive
function, but rather a derived form that is explained in terms of other
constructs of the language.
A common "mistake" is to write an expression like this
if exp = true then exp1 else exp2
If you think about it for a moment, this expression is just a longer way of writing
if exp then exp1 else exp2
Similarly,
if exp = false then exp1 else exp2
can be abbreviated to
if not exp then exp1 else exp2
or, better yet, just
if exp then exp2 else exp1
Neither of these examples is really a mistake, but it is rarely clearer to test a Boolean value for equality with true or false than to simply perform a conditional test on the value itself.