So far we have mainly studied the statics and dynamics of programs in isolation, without regard to their interaction with the world. But to extend this analysis to even the most rudimentary forms of input and output requires that we consider external agents that interact with the program. After all, the whole purpose of a computer is, ultimately, to interact with a person!

To extend our investigations to interactive systems, we begin with the study of process calculi, which are abstract formalisms that capture the essence of interaction among independent agents. The development will proceed in stages, starting with simple action models, then extending to interacting concurrent processes, and finally to synchronous and asynchronous communication. The calculus consists of two main syntactic categories, processes and events. The basic form of process is one that awaits the arrival of an event. Processes are closed under parallel composition (the product of processes), replication, and declaration of a channel. The basic forms of event are signaling on a channel and querying a channel; these are later generalized to sending and receiving data on a channel. Events are closed under a finite choice (sum) of events. When enriched with types of messages and channel references, the process calculus may be seen to be universal in that it is at least as powerful as the untyped λ-caclulus.

Up to this point we have frequently encountered arbitrary choices in the dynamics of various language constructs. For example, when specifying the dynamics of pairs, we must choose, rather arbitrarily, between the lazy dynamics, in which all pairs are values regardless of the value status of their components, and the eager dynamics, in which a pair is a value only if its components are both values. We could even consider a half-eager (or, equivalently, half-lazy) dynamics, in which a pair is a value only if, say, the first component is a value, but without regard to the second.

Similar questions arise with sums (all injections are values, or only injections of values are values), recursive types (all folds are values, or only folds of values are values), and function types (functions should be called by-name or by-value). Whole languages are built around adherence to one policy or another. For example, Haskell decrees that products, sums, and recursive types are to be lazy and functions are to be called by name, whereas ML decrees the exact opposite policy. Not only are these choices arbitrary, but it is also unclear why they should be linked. For example, we could very sensibly decree that products, sums, and recursive types are lazy, yet impose a call-by-value discipline on functions. Or we could have eager products, sums, and recursive types, yet insist on call-by-name. It is not at all clear which of these points in the space of choices is right; each has its adherents, and each has its detractors.

A subtype relation is a preorder (reflexive and transitive relation) on types that validates the subsumption principle:

The subsumption principle relaxes the strictures of a type system to permit values of one type to be treated as values of another.

Experience shows that the subsumption principle, although useful as a general guide, can be tricky to apply correctly in practice. The key to getting it right is the principle of introduction and elimination. To determine whether a candidate subtyping relationship is sensible, it suffices to consider whether every introductory form of the subtype can be safely manipulated by every eliminatory form of the supertype. A subtyping principlemakes sense only if it passes this test; the proof of the type safety theorem for a given subtyping relation ensures that this is the case.

A good way to get a subtyping principle wrong is to think of a type merely as a set of values (generated by introductory forms) and to consider whether every value of the subtype can also be considered to be a value of the supertype. The intuition behind this approach is to think of subtyping as akin to the subset relation in ordinary mathematics. But, as we subsequently see, this can lead to serious errors, because it fails to take account of the eliminatory forms that are applicable to the supertype.

The types nat → nat and nat list may be thought of as being built from other types by the application of a type constructor, or type operator. These two examples differ from each other in that the function space type constructor takes two arguments, whereas the list type constructor takes only one. We may, for the sake of uniformity, think of types such as nat as being built by a type constructor of no arguments. More subtly, we may even think of the types ∀(t · τ) and ∃(t. τ) as being built up in the same way by regarding the quantifiers as higher-order type operators.

These seemingly disparate cases may be treated uniformly by enriching the syntactic structure of a language with a new layer of constructors. To ensure that constructors are used properly (for example, that the list constructor is given only one argument and that the function constructor is given two), we classify constructors by kinds. Constructors of a distinguished kind T are types, which may be used to classify expressions. To allow for multiargument and higher-order constructors, we also consider finite product and function kinds. (Later we consider even richer kinds.)

The distinction between constructors and kinds on one hand and types and expressions on the other reflects a fundamental separation between the static, and the dynamic phase of processing of a programming language, called the phase distinction. The static phase implements the statics, and the dynamic phase implements the dynamics.

A reference to an assignable a is a value, written as & a, of reference type that uniquely 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 at the point at which it is used. Two references may also 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 said to be aliases. The possibility of aliasing complicates reasoning about the correctness of code that uses references, for we must always consider for any two references whether they might be aliases.

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 must be limited to the scope of the assignable to which it refers. This may be achieved by declaring that reference types are immobile, so that they cannot be returned from the body of a declaration or stored in an assignable. Although ensuring adherence to the stack discipline, this restriction precludes the use of references to create mutable data structures, those whose structure can be altered during execution.

A future is a computation whose evaluation is initiated in advance of any demand for its value. Like a suspension, a future represents a value that is to be determined later. Unlike a suspension, a future is always evaluated, regardless of whether its value is actually required. In a sequential setting futures are of little interest; a future of type τ is just an expression of type τ. In a parallel setting, however, futures are of interest because they provide a means of initiating a parallel computation whose result is not needed until (presumably) much later, by which time it will have been completed.

The prototypical example of the use of futures is to implementing pipelining, a method for overlapping the stages of a multistage computation to the fullest extent possible. This minimizes the latency caused by one stage waiting for the completion of a previous stage by allowing the two stages to proceed in parallel until such time as an explicit dependency is encountered. Ideally, the computation of the result of an earlier stage is completed by the time a later stage requires it. At worst the later stage must be delayed until the earlier stage completes, incurring what is known as a pipeline stall.

A speculation is a delayed computation whose result may or may not be needed for the overall computation to finish. The dynamics for speculations executes suspended computations in parallel with the main thread of computation, without regard to whether the value of the speculation is actually required by the main thread.

In the language ℒ{num str} we may perform calculations such as the doubling of a given expression, but we cannot express doubling as a concept in itself. To capture the general pattern of doubling, we abstract away from the particular number being doubled by using a variable to stand for a fixed, but unspecified, number to express the doubling of an arbitrary number. Any particular instance of doublingmay then be obtained by substituting a numeric expression for that variable. In general an expression may involve many distinct variables, necessitating that we specify which of several possible variables is varying in a particular context, giving rise to a function of that variable.

In this chapter we consider two extensions of ℒ{num str} with functions. The first, and perhaps most obvious, extension is by adding function definitions to the language. A function is defined by binding a name to an abt with a bound variable that serves as the argument of that function. A function is applied by substituting a particular expression (of suitable type) for the bound variable, obtaining an expression.

The domain and range of defined functions are limited to the types nat and str, as these are the only types of expression. Such functions are called first-order functions, in contrast to higher-order functions, which permit functions as arguments and results of other functions. Because the domain and range of a function are types, this requires that we introduce function types whose elements are functions.

Modularity is the most important technique for controlling the complexity of programs. Programs are decomposed into separate components with precisely specified, and tightly controlled, interactions. The pathways for interaction among components determine dependencies that constrain the process by which the components are integrated, or linked, to form a complete system. Different systems may use the same components, and a single system may use multiple instances of a single component. Sharing of components amortizes the cost of their development across systems and helps limit errors by limiting coding effort.

Modularity is not limited to programming languages. In mathematics the proof of a theorem is broken down into a collection of definitions and lemmas. Cross references among lemmas determine a dependency structure that constrains their integration to form a complete proof of the main theorem. Of course, one person's theorem is another person's lemma; there is no intrinsic limit on the depth and complexity of the hierarchies of results in mathematics. Mathematical structures are themselves composed of separable parts, as, for example, a Lie group is a group structure on a manifold.

Modularity arises from the structural properties of the hypothetical and general judgments. Dependencies among components are expressed by free variables whose typing assumptions state the presumed properties of the component. Linking consists of substitution and discharge of the hypothesis.

A symbol is an atomic datum with no internal structure. Whereas a variable is given meaning by substitution, a symbol is given meaning by a family of operations indexed by symbols. A symbol is therefore just a name, or index, for an instance of a family of operations. Many different interpretations may be given to symbols according to the operations we choose to consider, giving rise to concepts such as fluid binding, dynamic classification, mutable storage, and communication channels. With each symbol is associated a type whose interpretation depends on the particular application. The type of a symbol influences the type of its associated operations under each interpretation. For example, in the case of mutable storage, the type of symbol constrains the contents of the cell named by that symbol to values of that type. It is important to bear in mind that a symbol is not a value of its associated type, but only a constraint on how that symbol may be interpreted by the operations associated with it.

In this chapter we consider two constructs for computing with symbols. The first is a means of declaring new symbols for use within a specified scope. The expression v a:ρ in e introduces a “new” symbol a with associated type ρ for use within e. The declared symbol a is new in the sense that it is bound by the declaration within e, and so may be renamed at will to ensure that it differs from any finite set of active symbols.

The semantics of many control constructs (such as exceptions and coroutines) can be expressed in terms of reified control stacks, a representation of a control stack as an ordinary value. This is achieved by allowing a stack to be passed as a value within a program and to be restored at a later point, even if control has long since returned past the point of reification. Reified control stacks of this kind are called continuations; they are values that can be passed and returned at will in a computation. Continuations never “expire,” and it is always sensible to reinstate a continuation without compromising safety. Thus continuations support unlimited “time travel”—we can go back to a previous point in the computation and then return to some point in its future, at will.

Why are continuations useful? Fundamentally, they are representations of the control state of a computation at a given point in time. Using continuations we can “checkpoint” the control state of a program, save it in a data structure, and return to it later. In fact, this is precisely what is necessary to implement threads (concurrently executing programs)—the thread scheduler must be able to checkpoint a program and save it for later execution, perhaps after a pending event occurs or another thread yields the processor.