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

- … has a
*type.* - … may or may not have a
*value.* - … 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

- a
*type name*standing for that type, - a collection of
*values*of that type, and - 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`

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

`(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

`5`

=>`5`

=>

2+3`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

`(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`

*exp _{1}*

`else`

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`

*exp _{1}*

`else`

`bool`

and both `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 thenexp1 elseexp2

If you think about it for a moment, this expression is just a longer way of writing

if

expthenexp1 elseexp2

Similarly,

if

exp= false thenexp1 elseexp2

can be abbreviated to

if not

expthenexp1 elseexp2

or, better yet, just

if

expthenexp2elseexp1

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.