没有合适的资源？快使用搜索试试~ 我知道了~

首页Type Theory & Functional Programming

资源详情

资源评论

资源推荐

Type Theory & Functional

Programming

Simon Thompson

Computing Laboratory, University of Kent

March 1999

c

Simon Thompson, 1999

Not to be reproduced

i

ii

To my parents

Preface

Constructive Type theory has be en a topic of research interest to computer

scientists, mathematicians, logicians and philosophers for a number of years.

For computer scientists it provides a framework which brings together logic

and programming languages in a most elegant and fertile way: program

development and veriﬁcation can proceed within a single system. Viewed

in a diﬀerent way, type theory is a functional programming language with

some novel features, such as the totality of all its functions, its expressive

type system allowing functions whose result type depends upon the value

of its input, and sophisticated modules and abstract types whose interfaces

can contain logical assertions as well as signature information. A third

point of view emphasizes that programs (or functions) can be extracted

from proofs in the logic.

Up until now most of the material on type theory has only appeared in

proceedings of conferences and in research papers, so it seems appropriate

to try to set down the current state of development in a form accessible to

interested ﬁnal-year undergraduates, graduate students, research workers

and teachers in computer science and related ﬁelds – hence this book.

The book can be thought of as giving both a ﬁrst and a second course in

type theory. We begin with introductory material on logic and functional

programming, and follow this by presenting the system of type theory itself,

together with many examples. As well as this we go further, looking at

the system from a mathematical pe rspective, thus elucidating a number

of its important properties. Then we take a critical look at the profusion

of suggestions in the literature about why and how type theory could be

augmented. In doing this we are aiming at a moving target; it must be

the case that further developments will have been made before the book

reaches the press. Nonetheless, such an survey can give the reader a much

more developed sense of the potential of type theory, as well as giving the

background of what is to come.

iii

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 ﬁrst three chapters survey the three ﬁelds 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 diﬀerent 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 diﬀerences between the system and more traditional languages.

After a lengthy discussion of recursion, we look at the impact of the quan-

tiﬁed 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 eﬃcient form? There is a

1

Miranda is a trade mark of Research Software Limited

剩余377页未读，继续阅读

安全验证

文档复制为VIP权益，开通VIP直接复制

信息提交成功

## 评论0