文档介绍:This book is currently out of print. Upon kind permission of the
.-Press, it is available on
All references should be made to the published book.
CATEGORIES
TYPES
AND STRUCTURES
An Introduction to Category Theory for the puter scientist
Andrea Asperti
Giuseppe Longo
FOUNDATIONS PUTING SERIES
. PRESS, 1991
I
INTRODUCTION
The main methodological connection between programming language theory and category theory is
the fact that both theories are essentially “theories of functions.” A crucial point, though, is that the
categorical notion of morphism generalizes the set-theoretical description of function in a very broad
sense, which provides a unified understanding of various aspects of the theory of programs. This is
one of the reasons for the increasing role of category theory in the semantic investigation of programs
pared, say, to the set-theoretic approach. However, the influence of this mathematical
discipline puter science goes beyond the methodological issue, as the categorical approach to
mathematical formalization seems to be suitable for focusing concerns in many different areas of
computer science, such as software engineering and artificial intelligence, as well as automata theory
and other theoretical aspects putation.
This book is mostly inspired by this specific methodological connection and its applications to the
theory of programming languages. More precisely, as expressed by the subtitle, it aims at a self-
contained introduction to general category theory (part I) and at a categorical understanding of the
mathematical structures that constituted, in the last twenty or so years, the theoretical background of
relevant areas of language design (part II). The impact on functional programming, for example, of
the mathematical tools described in part II, is well known, as it ranges from the early dialects of Lisp,
to Edinburgh ML, to the current work i