Type and E ect Systems - Correct System Design: Recent Insights and Advances - page 110

programs are rejected by the type system; in this way types are not only used
for analysing the behaviours of programs but also for enforcing the absence of
certain kinds of dynamic errors.
The overall approach of type systems is to associate types to programs; normally
the types merely describe the form of the data supplied to, and produced by,
programs. The association of types to programs is done by a set of inference rules
that are largely syntax-directed; since subprograms may contain free variables
this needs to be relative to a type environment that maps the free variables
to their types. We express the typing by means of a typing judgement that
is usually a ternary relation on type environments, programs and types; it is
frequently written is the

type environment. The main challenges of devising type systems is (i) to ensure
that they are semantically correct (with respect to some dynamic semantics), (ii)
to ensure that they are decidable so that types can be checked by an algorithm,
and (iii) to ensure that there always is a \best" type, called a principal type, so
that an algorithm can produce the intended type automatically.

Γ ` p : where p is the program, is the type, and Γ

Type and eect systems rene the type information by annotating the types so
as to express further intensional or extensional properties of the semantics of
the program [18,19,20,21]. In Section 2 this takes the form of annotating the
base types or the type constructors. In Section 3 we study eect systems where
the annotations describe certain intensional aspects of the actions taking place
during evaluation. In Section 4 we further enrich the expressivenes of eects
so as to obtain causal information in the manner of process algebras. We then
expose the overall methodology behind type and eect systems in Section 5 and
indicate those combinations of features that challenge state-of-the-art.

Further Reading. A more thorough development of the techniques of static anal-
ysis can be found in [30] (particularly in Chapter 5 that deals with type and eect
systems) as well as in the references given.

2 Annotated Type Systems

Many programming languages incorporate types as a static technique for ensur-
ing that certain operations are only applied to data of the appropriate form; this
is useful for ensuring that the dynamic behaviour satises the specication.

Example 1. A Typed Language.
We shall use the following simple functional language to illustrate the develop-
ment; constructs for iteration, recursion and conditionals present no obstacles
and have only been left out in the interest of brevity. We shall later extend the
language with side eects (as in Standard ML) and communication (as in Con-
current ML) thereby suggesting that type and eect systems apply equally well
to imperative and concurrent languages.