Object-oriented languages can be roughly divided into two classes: those inspired by Simula, where messages are always sent to a unique receiver and methods are associated with a unique class of objects, and those that ascribe to the style of Common Lisp Object System (CLOS), where messages may be sent to several objects and methods are global. The study of polymorphism observes the same dichotomy, between parametric and overloading polymorphism. While parametric polymorphism has been extensively studied, overloading, while it has become a fundamental programming language feature, has been considered too ad hoc to merit the same level of attention. This text remedies this situation.

In the foreword, Luca Cardelli observes that “this book presents a compelling framework for the study of run-time overloading and its interactions with subtyping and with parametric polymorphism.” The text is essentially an extended and revised version of the author’s Ph.D. thesis. As such, it is easy to agree with Castagna’s observation that the “more than three hundred pages of interconnected chapters does not present an easy read.” It is harder to agree that “the book is self-contained,” unless the reader is very well versed in programming language theory. The author makes every effort to aid the reader, both by suggesting differing approaches for practitioners, teachers, and scholars, and by indicating parts of the book that are detours or can be skipped.

The text is divided into four sections: “Introduction” (chapters 1 and 2), “Simple Typing” (chapters 3 through 10), “Second Order” (chapters 11 through 14), and “Appendices.” All or part of most chapters has been published elsewhere; the exceptions are chapters 1, 2, and 9.

Chapter 1, “Background and Notation,” briefly introduces &lgr;-notation, type theory, &lgr;-calculus, subtyping, type systems, and type-checking algorithms. This material might not be sufficient for less experienced readers.

Chapter 2 is a general survey of the book. The first section provides the context for the research described here, with subsequent sections outlining the significant points made, chapter by chapter. This chapter is valuable in orienting the reader to the material.

Chapter 3, “Object-Oriented Programming,” describes object-oriented languages via the toy language KOOL (kernel object-oriented language). This language is deliberately kept simple, in order to emphasize the unified foundation of Simula-like and CLOS-like languages. The appendices provide a formal specification and translation of KOOL. The essential idea of this chapter is to identify the mechanism of message passing with overloading and late binding.

Chapter 4, “The &lgr;&-Calculus,” introduces an extension of the simply typed &lgr;-calculus to model the mechanisms of overloading and late binding. The &lgr;&-calculus is formally defined, relevant properties are proven, and connections to KOOL are made.

Chapter 5, “Covariance and Contravariance: Conflict Without a Cause,” immediately discusses a primary contribution of the &lgr;&-calculus model: clarifying the roles of covariance and contravariance in subtyping. The author shows that the controversy is a false problem created by confusing the mechanisms of substitutivity and overriding.

Chapter 6, “Strong Normalization,” observes that the &lgr;&-calculus is not strongly normalized, and the model presented here does not require this property. However, as strongly normalized subsystems of &lgr;&-calculus that are expressive enough to model object-oriented systems are of interest, the properties of such a subsystem are explored.

Chapter 7, “Three Variations on the Theme,” modifies, extends, and reformulates &lgr;&-calculus in three ways. First, the calculus is extended to allow explicit coercions. A second variant provides more freedom in the application of reduction rules. Last, a pure system of overloaded functions is created.

Chapter 8, “Interpretation of Object-Oriented Languages,” shows how the &lgr;&-calculus can be used to model object-oriented programming languages. As &lgr;& is by itself inadequate to formally model the relevant properties, the author derives the operational semantics of a kernel language &lgr;_object that has the requisite properties.

Chapter 9, “Imperative Features and Other Widgets,” defines an imperative &lgr;&-calculus in order to more faithfully implement the behaviors being modeled. Until this point, the framework was purely functional, but that approach is insufficient for the precise modeling of assignment  operations. 

Chapter 10, “Semantics,” defines the semantics of &lgr;&, with particular attention to the problems of pre-order, type-dependent execution, late binding, and  impredicativity. 

Chapter 11, “Introduction to Part III,” introduces second-order formalisms that allow a deeper understanding of the mathematical meaning of late binding. Polymorphism in a calculus with type-dependent computations is a neglected area, as is the integration of this ad hoc polymorphism with parametric polymorphism. This chapter also uses the second-order formalism to address the “loss of information” problem.

Chapter 12, “Second Order Overloading,” extends the previous work by describing a calculus in which overloaded functions are applied to types and the selection is based on the type at the argument (as opposed to the type of the argument).

Chapter 13, “Second Order Overloading and Object-Oriented Programming,” employs the second-order formalisms of chapter 12 in modeling both varieties of object-oriented languages. The author also identifies some new features suggested by this formalism that could be added to existing object-oriented paradigms.

Chapter 14 provides conclusions and motivation for future work. Appendix A is a “Specification of KOOL,” and Appendix B contains a “Formal Definition of the Translation.” The book ends with a 149-item bibliography and an index.

The major contribution of the research described here is to unify the previously disconnected worlds of Simula and CLOS and to show that this unified view can be integrated into a language where the two styles coexist. The book is important to graduate students and professionals in object-oriented programming languages and type theory. While much of the text is theoretical, many of the implications will interest practitioners.