In Chapter 3, we presented a model for evaluation of expressions; it was based on the idea of rewrites. This model defined a semantics to which every implementation had to refer. However, an implementation that actually used textual rewrites would be highly inefficient. To achieve reasonable efficiency, we must replace textual rewrites by some other mechanism that simulates it. One possibility is to introduce the idea of an environment.

In this chapter, we present evaluation based on environments. We will write an evaluation function that takes an environment and a Caml expression as its arguments and returns the value of this expression as its result. The ideas for implementing this evaluation function will be refined in Chapter 12 to produce a compiler.

Section 11.1 describes evaluation of expressions with the help of environments. As in Chapter 3, it uses inference rules corresponding to each construction in the language to do so. These inference rules define evaluation by value, the evaluation strategy adopted by Caml. Section 11.2 then shows how to translate these rules into an evaluator written in Caml. Finally, Section 11.3 shows how to modify that evaluator to take into account delayed evaluation rather than evaluation by value.

Evaluation with the Help of Environments

An environment may be regarded as a look-up table in which certain variables are bound to values.

In this chapter, we introduce continuations into the setting of a functional language using eager evaluation. We begin by defining a continuation semantics for the language of the previous chapter. Next, we extend this language by introducing continuations as values. Finally, we derive a first-order semantics that reveals how one might implement the extended language interpretively.

Continuation Semantics

When the evaluation of an expression gives an error or fails to terminate, this “computational effect” is the final result of the entire program. In the direct denotational semantics of Section 11.6, this behavior is expressed by passing err, tyerr, or ⊥ through a chain of *-extended functions that preserve these results.

An alternative approach is to use a continuation semantics, similar to the one discussed in Section 5.7, in which the semantic function, when applied to an expression e, an environment η, and a new argument K called a continuation, produces the final result of the entire program in which e is embedded. If the evaluation of e gives a value, then the final result is obtained by applying K to this value; but if the evaluation gives an error stop or fails to terminate (or executes a throw operation, which we will discuss in the next section), this result is produced directly without using the continuation. This makes it immediately evident that the “rest of the computation”, which is represented by the continuation, has no effect on the final result. (We will use the metavariable K, with occasional primes and subscripts, for continuations.)

Here we describe a variety of general mathematical concepts and notations that are used in this book. (Concepts that are more advanced, or are particular to programming-language theory, are explained in the main text when they are first used.) Even though most of these concepts may be familiar, readers are advised to scan this material, especially since some of the notations are novel.

In fact, modern mathematics gives the writer a surprising degree of freedom in defining its fundamental concepts, as long as the definitions are consistent and lead to entities with appropriate properties. In this book, I have made the following choices:

• Pairs are taken to be a primitive notion rather than being defined in terms of sets.

• Relations are defined as sets of pairs, functions as a special kind of relation, sequences as a special kind of function, and pairs as a special kind of sequence. Since a pair, however, cannot be a set containing itself, we break the inconsistent circle by distinguishing between the pairs 〈x,y) that are sequences and the primitive pairs [x,y] that are members of relations.

• We define relations (including functions) to be sets of primitive argument-result pairs, rather than calling such a set the “graph” of the relation and defining the relation itself to consist of a domain, a codomain, and a graph. Thus, for example, the function on the integers that increases its argument by one is both a function from integers to integers and a function from integers to reals, and also a partial function from reals to reals. (This view of functions is taken by Gleason [1966, Sections 3–4.1 to 3–4.11]. It is a special case of the view that, in category theory, the morphism sets of a category need not be disjoint.)

• […]

Peter Landin remarked long ago that the goal of his research was “to tell beautiful stories about computation”. Since then many researchers have told many such stories. This book is a collection my favorites in the area of languages for programming and program specification.

In 1992, the Computer Science Department of Carnegie Mellon University replaced the preliminary examinations for its doctoral students by a set of required courses, including CS711, simply titled “Programming Languages”, which was intended to be a unified treatment of the basic principles of the subject. Previously, such material had been divided between the programming systems examination and the theory examination, and many important topics had fallen through the cracks between the syllabi. (For example, students were expected to know enough of the theory of program proving to understand Cook completeness, yet they never saw the proof of an actual program beyond a trivial one that computed a square root by iterating over successive natural numbers and squaring them.)

As the most vociferous exponent of such a course, I was put in charge of teaching it, and I soon discovered that there was no suitable textbook. Serious texts in areas such as semantics or verification invariably stressed a particular approach and neglected topics that did not fit well with their point of view. At the opposite extreme, surveys of programming languages usually emphasized superficial differences between languages while slighting more fundamental issues. In effect, what was available were profound novels and journalistic popularizations, but what was needed was a collection of short stories sharing some common characters. Thus I produced extensive class notes, which in a few years grew into this book.

In recent years, the dramatic drop in the cost of computing hardware has made it practical, in an ever-increasing variety of contexts, to execute different parts of a program simultaneously. Many authors use the terms “concurrent” or “parallel” indifferently to describe such computations. Following increasingly common usage, however, we will use concurrent to describe computations where the simultaneously executing processes can interact with one another, and we will reserve parallel to describe computations where the behavior of each process is unaffected by the behavior of the others.

Our present concern is concurrency. In this chapter, we consider an approach where processes communicate through shared variables. This approach mirrors the situation where a common memory, typically containing a shared database, is accessed by several physical processors – or perhaps by a single processor that is time-shared among several logical processes. (An alternative approach to concurrency, where processes communicate by passing messages, will be described in Chapter 9.)

Except in trivial cases, the interaction between concurrent processes will depend on the relative speed of the physical processors or on the decisions by a scheduler of when to switch a physical processor from one logical process to another. Thus concurrent programs are usually nondeterminate. This nondeterminacy makes concurrent programs especially difficult to reason about, since one must consider all possible orders of execution. Moreover, the efficacy of debugging is undermined by the irreproducibility of executions and by the fact that the actual occurrences of obscure and possibly erroneous orders of execution may be very infrequent.

In this chapter, we will explore methods of specifying programs in the simple imperative language and of proving such specifications formally. We will consider both partial correctness, where one specifies that a program will behave properly if it terminates, and total correctness, where one also specifies that a program will terminate. For partial correctness we will use the form of specification invented by C. A. R. Hoare, while for total correctness we will use an analogous form based on the ideas of E. W. Dijkstra.

At the outset, it should be stressed that formal proofs are quite different than the traditional proofs of mathematics. A formal proof is sufficiently detailed that its correctness can be verified mechanically. In contrast, a traditional mathematical proof can be thought of as a blueprint that provides just enough information to allow a well-trained reader to construct a formal proof.

In fact, formal proofs are more prevalent in computer science than in mathematics. The most obvious reason is that only formal methods can be mechanized soundly. A more subtle reason, however, is the different nature of the proof task. Mathematical conjectures often contain no hint of why they might be true, but programs are invariably written by people who have at least a vague idea of why they should work. Thus the task of program proving is not to search over a broad space of arguments, but to refine an already existing argument until all of its flaws have been revealed.

This is not to say that every program merits formal proof. Experience with formal proof methods, however, also increases a programmer's ability to detect flaws in informal arguments.

Many programming languages provide a variety of implicit conversions (sometimes called “coercions”) that serve to make programs more succinct; the most widespread example is the conversion of integers to real (floating-point) numbers. In modern type systems, such conversions are captured by the concept of subtyping.

In this chapter, we extend the simple type system by introducing a subtype relation ≤ between types. When θ ≤ θ′, we say that θ is a subtype of θ′ or, occasionally, that θ′ is a supertype of θ. Syntactically, this relationship implies that any expression of type θ is also an expression of type θ′, and thus can be used in any context that permits an expression of type θ′. In extrinsic semantics, the relationship implies that the set denoted by θ is a subset of that denoted by θ′, and that values which are equivalent for the type θ are also equivalent for θ′; more simply, the partial equivalence relation for θ must be a subset of the partial equivalence relation for θ′. In intrinsic semantics, θ ≤ θ′ implies that there is an implicit conversion function from the meaning of θ to the meaning of θ′.

We will also introduce intersection types, which permit the description of values with more than one conventional type. In extrinsic semantics, the intersection of types is modelled by the intersection of partial equivalence relations, and in intrinsic semantics by a constrained product.

We will find that both extrinsic and intrinsic semantics clarify the subtle interactions between subtypes and generic operators.

In this chapter, we introduce four concepts that pervade the study of programming languages: abstract syntax, denotational semantics, inference rules, and binding. These concepts are illustrated by using them to describe a formal language that is not a programming language: predicate logic.

There are three reasons for the oddity of starting a book about programming languages by defining a logic. First, predicate logic is close enough to conventional mathematical notation that the reader's intuitive understanding is likely to be accurate; thus we will be illustrating novel concepts in a familiar setting. Second, since predicate logic has no concept of nontermination, we will be able to define its denotations in terms of ordinary sets, and postpone the more subtle topic of domains until Chapter 2. Finally, as we will see in Chapter 3, predicate logic plays a pivotal role in the formal specification of simple imperative programs.

Although the syntax and semantics of predicate logic are standard topics in logic, we will describe them in the terminology of programming languages: The types of phrases that a logician would call “terms” and “well-formed formulas” we will call “integer expressions” (abbreviated by “intexp”) and “assertions” (abbreviated by “assert”) respectively. Similarly, “assignments” will be called “states”. Moreover, we will usually interpret the operators used to construct terms in a fixed way, as the familiar operations of integer arithmetic.

Abstract Syntax

It is possible to specify the syntax of a formal language, such as predicate logic or a programming language, by using a context-free grammar (often called BNF or Backus-Naur form) and to define the semantics of the language by a function on the set of strings generated by this grammar.

Rudimentary type systems appeared in even the earliest higher-level programming languages, such as Fortran, Cobol, and Algol 60. Soon it was realized that such systems permitted a wide variety of programming mistakes to be detected during compilation, and provided information that could be used effectively to improve data representations. The consequence, beginning in the late 1960's, was a sequence of languages, such as PL/I, Algol 68, Pascal, and Ada, with extensive and complicated type systems.

Unfortunately, the type systems of these languages had serious deficiencies that limited their acceptance: Many of the languages contained “type leaks” that prevented the compile-time detection of certain type errors, many required so much type information that programs became unworkably verbose, and all imposed constraints that made certain useful programming techniques difficult or impossible.

Meanwhile, however, more theoretically-minded researchers began a systematic study of type systems, particularly for functional languages. Over the last two decades, they have shown that the application of sophisticated mathematical and logical techniques could lead to substantial improvements. Polymorphic systems have been devised that permit a procedure to be applied to a variety of types of parameters without sacrificing compile-time type checking. Type-inference algorithms have been developed that reduce or eliminate the need for explicit type information. (These two developments were central to the design of ML in the late 1970's.)

Other researchers, while exploring the connections between types and constructive logic, discovered that (at least in the setting of functional programming) the distinction between the type of a program and a full-blown logical specification of the program's behavior is one of degree rather than kind.

In this chapter, we introduce a class of languages that combine imperative and functional features in a very different way than the Iswim-like languages of Chapter 13. Algol-like languages are based on normal-order evaluation, and they distinguish two kinds of types, called data types and phrase types. In contrast to Iswim-like languages, they can be implemented by allocating storage on a stack, without any form of garbage collection; thus they are more efficient but more limited in the variety of programs that can be expressed reasonably. They are theoretically cleaner — in particular, β-reduction preserves meaning. Nevertheless, they still exhibit the complications of aliasing that characterized Iswim-like languages.

The original Algol-like language, Algol 60, was (along with Lisp) the earliest language to combine a powerful procedure mechanism with imperative features. By intentionally concentrating on the desired behavior of the language rather than its implementation, the designers of Algol 60 raised problems of implementation and definition that were a fruitful challenge over the following decade. In particular, the language inspired the definitional ideas of Strachey and Landin that, paradoxically, led to Iswim-like languages.

Since then, a few Algol-like languages, such as Algol W and especially Simula 67, have attracted communities of users. At present, however, the acceptance of Iswim-like languages is far wider. Nevertheless, there has been a spate of theoretical interest in the last decade that suggests the Algol framework may inspire new languages which, if they can overcome the limitations of the stack discipline without compromising linguistic cleanliness, will find significant acceptance.