Types are the central organizing principle of the theory of programming languages. Language features are manifestations of type structure. The syntax of a language is governed by the constructs that define its types, and its semantics is determined by the interactions among those constructs. The soundness of a language design—the absence of ill-defined programs—follows naturally.

The purpose of this book is to explain this remark. A variety of programming language features are analyzed in the unifying framework of type theory.Alanguage feature is defined by its statics, the rules governing the use of the feature in a program, and its dynamics, the rules defining how programs using this feature are to be executed. The concept of safety emerges as the coherence of the statics and the dynamics of a language.

In this way, we establish a foundation for the study of programming languages. But why these particular methods? The main justification is provided by the book itself. The methods we use are both precise and intuitive, providing a uniform framework for explaining programming language concepts. Importantly, these methods scale to a wide range of programming language concepts, supporting rigorous analysis of their properties. Although it would require another book in itself to justify this assertion, these methods are also practical in that they are directly applicable to implementation and uniquely effective as a basis for mechanized reasoning. No other framework offers as much.

Being a consolidation and distillation of decades of research, this book does not provide an exhaustive account of the history of the ideas that inform it. Suffice it to say that much of the development is not original but rather is largely a reformulation of what has gone before. The notes at the end of each chapter signpost the major developments but are not intended as a complete guide to the literature. For further information and alternative perspectives, the reader is referred to such excellent sources as Constable (1986, 1998), Girard (1989), Martin-Löf (1984), Mitchell (1996), Pierce (2002, 2004), and Reynolds (1998).

The book is divided into parts that are, in the main, independent of one another. Parts I and II, however, provide the foundation for the rest of the book and must therefore be considered prior to all other parts.

It often arises that the values of a type are partitioned into a variety of classes, each classifying data with distinct internal structure. A simple example is provided by the type of points in the plane, which are classified according to whether they are represented in cartesian or polar form. Both are represented by a pair of real numbers, but in the cartesian case, these are the x and y coordinates of the point, whereas in the polar case, these are its distance r from the origin and its angle θ with the polar axis. A classified value is an object, or instance, of its class. The class determines the type of the classified data, the instance type of the class; the classified data itself is the instance data of the object.

Methods are functions that act on classified values. The behavior of a method is determined by the class of its argument. The method dispatches on the class of the argument. Because the selection is made at run-time, it is called dynamic dispatch. For example, the squared distance of a point from the origin is calculated differently according to whether the point is represented in cartesian or polar form. In the former case, the required distance is x2 + y2, whereas in the latter it is simply r2. Similarly, the quadrant of a cartesian point can be determined by examining the sign of its x and y coordinates, and the quadrant of a polar point can be calculated by taking the integral part of the angle θ divided by π/2.

Dynamic dispatch is often described in terms of a particular implementation strategy, which we will call the class-based organization. In this organization, each object is represented by a vector of methods specialized to the class of that object. We may equivalently use a method-based organization in which each method branches on the class of an object to determine its behavior. Regardless of the organization used, the fundamental idea is that (a) objects are classified and (b) methods dispatch on the class of an object. The class-based and method-based organizations are interchangeable and, in fact, related by a natural duality between sum and product types.We explain this symmetry by focusing first on the behavior of each method on each object, which is given by a dispatch matrix.

A reference to an assignable a is a value, written &a, of reference type that determines the assignable a. A reference to an assignable provides the capability to get or set the contents of that assignable, even if the assignable itself is not in scope when it is used. Two references can be compared for equality to test whether they govern the same underlying assignable. If two references are equal, then setting one will affect the result of getting the other; if they are not equal, then setting one cannot influence the result of getting from the other. Two references that govern the same underlying assignable are aliases. Aliasing complicates reasoning about programs that use references, because any two references may refer to the assignable.

Reference types are compatible with both a scoped and a scope-free allocation of assignables. When assignables are scoped, the range of significance of a reference type is limited to the scope of the assignable to which it refers. Reference types are therefore immobile, so that they cannot be returned from the body of a declaration, nor stored in an assignable. Although ensuring adherence to the stack discipline, this restriction precludes using references to create mutable data structures, those whose structure can be altered during execution. Mutable data structures have a number of applications in programming, including improving efficiency (often at the expense of expressiveness) and allowing cyclic (self-referential) structures to be created. Supporting mutability requires that assignables be given a scope-free dynamics, so that their lifetime persists beyond the scope of their declaration. Consequently, all types are mobile, so that a value of any type may be stored in an assignable or returned from a command.

Capabilities

The commands get[a] and set[a](e) in MA operate on statically specified assignable a. Even to write these commands requires that the assignable a be in scope where the command occurs. But suppose that we wish to define a procedure that, say, updates an assignable to double its previous value, and returns the previous value. We can write such a procedure for any given assignable, a, but what if we wish to write a generic procedure that works for any given assignable?

Most programming languages are safe (or, type safe, or strongly typed). Informally, this means that certain kinds of mismatches cannot arise during execution. For example, type safety for E states that it will never arise that a number is added to a string, or that two numbers are concatenated, neither of which is meaningful.

In general, type safety expresses the coherence between the statics and the dynamics. The staticsmay be seen as predicting that the value of an expression will have a certain form so that the dynamics of that expression is well–defined. Consequently, evaluation cannot “get stuck” in a state for which no transition is possible, corresponding in implementation terms to the absence of “illegal instruction” errors at execution time. Safety is proved by showing that each step of transition preserves typability and by showing that typable states are well–defined. Consequently, evaluation can never “go off into the weeds” and, hence, can never encounter an illegal instruction.

Type safety for the language E is stated precisely as follows:

Theorem 6.1 (Type Safety).

1. 1. If e : τ and e ⟼ e', then e': τ.

2. 2. If e : τ, then either e val, or there exists e' such that e ⟼ e'.

The first part, called preservation, says that the steps of evaluation preserve typing; the second, called progress, ensures that well–typed expressions are either values or can be further evaluated. Safety is the conjunction of preservation and progress.

We say that an expression e is stuck iff it is not a value, yet there is no e' such that e ⟼ e'. It follows from the safety theorem that a stuck state is necessarily ill–typed. Or, putting it the other way around, that well–typed states do not get stuck.

Preservation

The preservation theorem for E defined in Chapters 4 and 5 is proved by rule induction on the transition system (rules (5.4)).

Theorem 6.2 (Preservation). If e : τ and e ⟼ e', then e': τ.

Many programs are instances of a pattern in a particular situation. Sometimes types determine the pattern by a technique called (type) generic programming. For example, in Chapter 9, recursion over the natural numbers is introduced in an ad hoc way. As we shall see, the pattern of recursion on values of an inductive type is expressed as a generic program.

To get a flavor of the concept, consider a function f of type ρ → ρ', which transforms values of type ρ into values of type ρ'. For example, f might be the doubling function on natural numbers.We wish to extend f to a transformation from type [ρ/t]τ to type [ρ'/t]τ by applying f to various spots in the input, where a value of type ρ occurs to obtain a value of type ρ', leaving the rest of the data structure alone. For example, τ might be bool × t, in which case f could be extended to a function of type bool × ρ → bool × ρ' that sends the pairs ⟨a, b⟩ to the pair ⟨a, f (b⟩.

The foregoing example glosses over an ambiguity arising from the many-one nature of substitution. A type can have the form [ρ/t]τ in many different ways, according to how many occurrences of t there are within τ. Given f as above, it is not clear how to extend it to a function from [ρ'/t]τ to [ρ/t]τ. To resolve the ambiguity, we must be given a template that marks the occurrences of t in τ at which f is applied. Such a template is known as a type operator, t.τ, which is an abstractor binding a type variable t within a type τ. Given such an abstractor, we may unambiguously extend f to instances of τ given by substitution for t in τ.

The power of generic programming depends on the type operators that are allowed. The simplest case is that of a polynomial type operator, one constructed from sum and product of types, including their nullary forms. These are extended to positive type operators, which also allow certain forms of function types.