Ranta’s aim is to introduce the Martin-Löf theory of types from the point of view of (and with some applications to) linguistics. The author investigates the ways in which such theoretical types manifest themselves in English, especially in “sugaring” procedures, that is, transformations of formal notations into more readable forms.

The author first has to give a presentation of type theory that appeals to non-mathematical readers. This is not an easy task. Because type theory is not a theory in the well-known ordinary predicate calculus, one has to develop an entire (and rather formidable) apparatus to describe it. Nevertheless, the basic idea of Martin-Löf theory is natural. In axiomatic set theory, sets are introduced as contractions of expressions of predicate calculus, for example, “z ∈ A ∪ B” for “z ∈ A or z ∈ B.” The approach of Martin-Löf is exactly inverted. From the intuitive notion of sets as aggregates, one extracts a few basic constructs (the Cartesian product and disjoint union of two sets, and the union and product of a family of sets). These constructs are used for a new foundation of logic, the key idea being that a proposition is the set of its proofs.

Chapter 2 of this book, the most substantial and most directly linked to computer science, gives a good, gradual account of type theory. This chapter may be recommended to anyone who wants an introduction to these ideas. The author scrutinizes the fundamental principle of propositions as types, versus both the classical and intuitionistic notions, leading to constructive interpretations of implication and negation. He also gives an application of the theory to an explicit system of predicate calculus, which may be useful in the current practice of programming.

Chapter 3 discusses examples of the use of the basic operators (existential, universal, Cartesian product, and disjunction) in English, which will help readers understand their meaning. Chapter 7 deals with the use of possible worlds, which are counterparts of models in the classical predicate calculus, and chapter 8 focuses on a reformulation of inference rules through higher-level types.

The other chapters deal with linguistics, but I am not competent to speak on the matter.

This is not a book on computer science, but Martin-Löf types are probably the suitable theoretical background for object-oriented programming, because the four basic concepts--objects, abstract data typing, inheritance, and polymorphism--are easy to formalize in type theory.