An interface is a contract that specifies the rights of a client and the responsibilities of an implementor. Being a specification of behavior, an interface is a type. In principle, any type may serve as an interface, but in practice it is usual to structure code into modules consisting of separable and reusable components. An interface specifies the behavior of a module expected by a client and imposed on the implementor. It is the fulcrum balancing the tension between separation and integration. As a rule, a module ought to have a welldefined behavior that can be understood separately, but it is equally important that it be easy to combine modules to form an integrated whole.

A fundamental question is, what is the type of a module? That is, what form should an interface take? One long-standing idea is that an interface is a labeled tuple of functions and procedures with specified types. The types of the fields of the tuple are often called function headers, because they summarize the call and return types of each function. Using interfaces of this form is called procedural abstraction, because it limits the dependencies between modules to a specified set of procedures. We may think of the fields of the tuple as being the instruction set of a virtual machine. The client makes use of these instructions in its code, and the implementor agrees to provide their implementations.

The problem with procedural abstraction is that it does not provide as much insulation as one might like. For example, a module that implements a dictionary must expose in the types of its operations the exact representation of the tree as, say, a recursive type (or, in more rudimentary languages, a pointer to a structure that itself may contain such pointers). Yet the client ought not depend on this representation: the purpose of abstraction is to get rid of pointers. The solution, as discussed in Chapter 17, is to extend the abstract machine metaphor to allow the internal state of the machine to be hidden from the client. In the case of a dictionary, the representation of the dictionary as a binary search tree is hidden by existential quantification. This concept is called type abstraction, because the type of the underlying data (state of the abstract machine) is hidden.

Writing the second edition to a textbook incurs the same risk as building the second version of a software system. It is difficult to make substantive improvements, while avoiding the temptation to overburden and undermine the foundation on which one is building.With the hope of avoiding the second system effect, I have sought to make corrections, revisions, expansions, and deletions that improve the coherence of the development, remove some topics that distract from the main themes, add new topics that were omitted from the first edition, and include exercises for almost every chapter.

The revision removes a number of typographical errors, corrects a few material errors (especially the formulation of the parallel abstract machine and of concurrency in Algol), and improves the writing throughout. Some chapters have been deleted (general pattern matching and polarization, restricted forms of polymorphism), some have been completely rewritten (the chapter on higher kinds), some have been substantially revised (general and parametric inductive definitions, concurrent and distributed Algol), several have been reorganized (to better distinguish partial from total type theories), and a new chapter has been added (on type refinements). Titular attributions on several chapters have been removed, not to diminish credit, but to avoid confusion between the present and the original formulations of several topics. A new system of (pronounceable!) language names has been introduced throughout. The exercises generally seek to expand on the ideas in the main text, and their solutions often involve significant technical ideas that merit study. Routine exercises of the kind one might include in a homework assignment are deliberately few.

My purpose in writing this book is to establish a comprehensive framework for formulating and analyzing a broad range of ideas in programming languages. If language design and programming methodology are to advance from a trade-craft to a rigorous discipline, it is essential that we first get the definitions right. Then, and only then, can there be meaningful analysis and consolidation of ideas. My hope is that I have helped to build such a foundation.

I am grateful to Stephen Brookes, Evan Cavallo, Karl Crary, Jon Sterling, James R. Wilcox and Todd Wilson for their help in critiquing drafts of this edition and for their suggestions for modification and revision. I thank my department head, Frank Pfenning, for his support ofmy work on the completion of this edition.

The dynamics of a language describes how programs are executed. The most important way to define the dynamics of a language is by the method of structural dynamics, which defines a transition system that inductively specifies the step–by–step process of executing a program. Another method for presenting dynamics, called contextual dynamics, is a variation of structural dynamics in which the transition rules are specified in a slightly different way. An equational dynamics presents the dynamics of a language by a collection of rules defining when one program is definitionally equivalent to another.

Transition Systems

A transition system is specified by the following four forms of judgment:

1. s state, asserting that s is a state of the transition system.

2. s final, where s state, asserting that s is a final state.

3. s initial, where s state, asserting that s is an initial state.

4. s ⟼ s', where s state and s' state, asserting that state s may transition to state s'.

In practice, we always arrange things so that no transition is possible from a final state: if s final, then there is no s' state such that s ⟼ s'. A state from which no transition is possible is stuck.Whereas all final states are, by convention, stuck, theremay be stuck states in a transition system that are not final. A transition system is deterministic iff for every state s there exists at most one state s' such that s ⟼ s'; otherwise, it is non-deterministic.

A transition sequence is a sequence of states s0, …, sn such that s0 initial, and si ⟼ si+1 for every 0 ≤ i < n. A transition sequence is maximal iff there is no s such that sn ⟼ s, and it is complete iff it is maximal and sn final. Thus, every complete transition sequence is maximal, but maximal sequences are not necessarily complete. The judgment s ↓ means that there is a complete transition sequence starting from s, which is to say that there exists s' final such that s ⟼*s'.

In Chapter 23, we demonstrated that dynamic typing is but a mode of use of static typing, one in which dynamically typed values are of type dyn, a particular recursive sum type. A value of type dyn is always of the form new[c](e), where c is its class and e is its underlying value. Importantly, the class c determines the type of the underlying value of a dynamic value. The type system of the hybrid language is rather weak in that every dynamically classified value has the same type, and there is no mention of the class in its type. To correct this shortcoming it is common to enrich the type system of the hybrid language to capture such information, for example, as described in Section 24.2.

In such a situation, subtyping is used to resolve a fundamental tension between structure and behavior in the design of type systems. On the one hand, types determine the structure of a programming language and, on the other, serve a behavioral specifications of expressions written in that language. Subtyping attempts to resolve this tension, unsuccessfully, by allowing certain forms of retyping. Although subtyping works reasonably well for small examples, things get far more complicated when we wish to specify the deep structure of a value, say, that it is of a class c and its underlying value is of another class d whose underlying value is a natural number. There is no limit to the degree of specificity one may wish in such descriptions, which gives rise to endless variations on type systems to accommodate various special situations.

Another resolution of the tension between structure and behavior in typing is to separate these aspects by distinguishing types from type refinements. Type refinements specify the execution behavior of an expression of a particular type using specifications that capture whatever properties are of interest, limited only by the difficulty of proving that a program satisfies the specification given by a refinement.

Certain limited forms of behavioral specifications can express many useful properties of programs while remaining mechanically checkable. These include the fundamental behavioral properties determined by the type itself but can be extended to include sharper conditions than just these structural properties. In this chapter, we will consider a particular notion of refinement tailored to the hybrid language of Chapter 23.