iv PREFACE
Outline
It see ms in order to give an overview of the book. Each chapter begins with
a more detailed introduction, so we shall be brief here. We follow this with
a guide on how the book might be approached.
The first three chapters survey the three fields upon which type theory
depends: logic, the λ-calculus and functional programming and construc-
tive mathematics. The surveys are short, establishing terminology, notation
and a general context for the discussion; pointers to the relevant literature
and in particular to more detailed intro ductions are provided. In the second
chapter we discuss some issues in the λ-calculus and functional program-
ming which suggest analogous questions in type theory.
The fourth chapter forms the focus of the book. We give the formal
system for type theory, developing examples of both programs and proofs
as we go along. These tend to be short, illustrating the construct just
introduced – chapter 6 contains many more examples.
The system of type theory is complex, and in chapter which follows we
explore a number of different aspects of the theory. We prove certain results
about it (rather than using it) including the important facts that programs
are terminating and that evaluation is deterministic. Other topics examined
include the variety of equality relations in the system, the addition of types
(or ‘universes’) of types and some more technical points.
Much of our understanding of a complex formal system must derive
from out using it. Chapter six covers a variety of examples and larger
case studies. From the functional programming point of view, we choose to
stress the differences between the system and more traditional languages.
After a lengthy discussion of recursion, we look at the impact of the quan-
tified types, especially in the light of the universes added above. We also
take the opportunity to demonstrate how programs can be extracted from
constructive proofs, and one way that imperative programs c an be seen as
arising. We conclude with a survey of examples in the relevant literature.
As an aside it is worth saying that for any formal system, we can really
only understand its precise details after attempting to implement it. The
combination of symbolic and natural language used by mathematicians is
surprisingly suggestive, yet ambiguous, and it is only the discipline of having
to implement a system which makes us look at some aspects of it. In the
case of T T , it was only through writing an implementation in the functional
programming language Miranda
1
that the author came to understand the
distinctive role of assumptions in T T , for instance.
The system is expressive, as witnessed by the previous chapter, but
are programs given in their most natural or efficient form? There is a
1
Miranda is a trade mark of Research Software Limited
评论0