Sample Code for this Chapter

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

  1. … has a type.
  2. … may or may not have a value.
  3. … may or may not engender an effect.

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

  1. a type name standing for that type,
  2. a collection of values of that type, and
  3. a collection of operations on values of that type.

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 + 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 + 4
: int
4 div 3
: int
4 mod 3
: int

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

  1. (3+4): int
    1.1 3 : int
    1.2 4 : int
  2. 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
=> 5
(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

  1. (3+2)=> 5
    1.1 3 => 3
    1.2 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
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


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.

Sample Code for this Chapter