Category Theory for Computing Science

by Michael Barr and Charles Wells

Category Theory for Computing Science is a textbook in basic category theory, written specifically to be read by researchers and students in computing science.  You may read the excerpts from the Preface to find out more about it.

The third edition is now available from Centre de recherches mathématiques, or by email to crmbooks@crm.umontreal.ca . This edition contains all the material dropped from the second edition (with corrections) and the answers to all the exercises.

About earlier editions

Some of the chapters in the first edition were dropped from the second edition in order to make room for new material. Revised and corrected versions of the omitted chapters may now be found in an electronic supplement to the text. We also provide corrections and additions to the first edition and corrections to the second edition.

Preface

 

This book is a textbook in basic category theory, written specifically to be read by researchers and students in computing science.  We expound the constructions we feel are basic to category theory in the context of examples and applications to computing science.  Some categorical ideas and constructions are already used heavily in computing science and we describe many of these uses.  Other ideas, in particular the concept of adjoint, have not appeared as widely in the computing science literature.  We give here an elementary exposition of those ideas we believe to be basic categorical tools, with pointers to possible applications when we are aware of them.

 

In addition, this text advocates a specific idea:  the use of sketches as a systematic way to turn finite descriptions into mathematical objects.  This aspect of the book gives it a particular point of view.  We have, however, taken pains to keep most of the material on sketches in separate sections. It is not necessary to read to learn most of the topics covered by the book.

 

As a way of showing how you can use categorical constructions in the context of computing science, we describe several examples of modeling linguistic or computational phenomena categorically.  These are not intended as the final word on how categories should be used in computing science; indeed, they hardly constitute the initial word on how to do that!  We are mathematicians, and it is for those in computing science, not us, to determine which is the best model for a given application.

 

The emphasis in this book is on understanding the concepts we have introduced, rather than on giving formal proofs of the theorems. We include proofs of theorems only if they are enlightening in their own right.  We have attempted to point the reader to the literature for proofs and further development for each topic.

 

In line with our emphasis on understanding, we frequently recommend one or another way of thinking about a concept.  It is typical of most of the useful concepts in mathematics that there is more than one way of perceiving or understanding them.  It is simply not true that everything about a mathematical concept is contained in its definition.  Of course it is true that in some sense all the theorems are inherent in its definition, but not what makes it useful to mathematicians or to scientists who use mathematics.  We believe that the more ways you have of perceiving an idea, the more likely you are to recognize situations in your own work where the idea is useful.

 

We have acted on the belief just outlined with many sentences beginning with phrases such as `This concept may be thought of as …'.  We have been warned that doing this may present difficulties for a non-mathematician who has only just mastered one way of thinking about something, but we feel it is part of learning about a mathematical topic to understand the contextual associations it has for those who use it.

 

About categories

 

Categories originally arose in mathematics out of the need of a formalism to describe the passage from one type of mathematical structure to another.  A category in this way represents a kind of mathematics, and may be described as category as mathematical workspace.

 

A category is also a mathematical structure.  As such, it is a common generalization of both ordered sets and monoids (the latter are a simple type of algebraic structure that include transition systems as examples), and questions motivated by those topics often have interesting answers for categories.  This is  category as mathematical structure.

 

A third point of view is emphasized in this book.  A category can be seen as a structure that formalizes a mathematician's description of a type of structure.  This is the role of  category as theory.  Formal descriptions in mathematical logic are traditionally given as formal languages with rules for forming terms, axioms and equations.  Algebraists long ago invented a formalism based on tuples, the method of signatures and equations, to describe algebraic structures.  In this book, we advocate categories in their role as formal theories as being in many ways superior to the others just mentioned.  Continuing along the same path, we advocate sketches as finite specifications for the theories.

 

Topics

Chapter 1 contains preliminary material on graphs, sets and functions. The reader who has taken a discrete mathematics course may wish to skip this chapter.  However, some fine points concerning sets and functions are discussed that may be worth looking at.

 

Chapter 2 introduces categories and gives many examples.  We also give certain simple constructions on categories and describe elementary properties of objects and arrows.

 

Chapter 3 introduces functors, which are the mappings that preserve the structure of categories.  We make certain constructions here that will be needed in later chapters.

 

Chapter 4 deals with three related topics: diagrams, natural transformations and sketches.  Probably the first thing noncategorists notice about category theory is the proliferation of diagrams:  here we begin the heavy use of diagrams in this book.  We discuss representable functors, universal objects and the Yoneda embedding, which are fundamental tools for the categorist.  We also introduce 2-categories in this chapter, as well as a very weak version of sketch called a linear sketch.

 

Chapter 5 introduces products and sums.  This allows one to use categories, in their role as theories, to specify functions of several variables and to specify alternatives.  In programming languages these appear as record structures and variant records.

 

Chapter 6 is an introduction to cartesian closed categories, which have been a major source of interest to computer scientists because they are equivalent in theoretical power to typed lambda calculus.  In this chapter, we outline briefly the process of translating between typed lambda calculus and cartesian closed categories. Normally, in learning a new language, one should plunge right in speaking it instead of translating.  However, it may be helpful for the suspicious reader to see that translation is possible.  We outline two translation processes in this book:  the one mentioned here and another in Chapter 7. Except for those two places, category theory is everywhere presented in its own terms. 

 

Chapter 7 introduces finite product sketches, which have the expressive power of multisorted universal algebra. These sketches provide a formalism for universal algebra that provide a natural definition of models in categories other than the category of sets, and being based on graphs, they also incorporated multisortedness into the definition in an intrinsic way. In this chapter, a method is given for translating between finite product sketches and the formalism of signatures and equations used in traditional universal algebra. More expressive types of sketches are described in Chapters 8, 10 and 11.  

 

Chapter 8 introduces finite discrete sketches, which have more expressive power than universal algebra, in that they allow one to express alternatives.  

 

Chapter 9  introduces the general concepts of limit and colimit.  These are basic constructions in category theory that allow the formation of equationally defined subtypes and quotients. We describe unification in terms of coequalizers of free models of a certain kind of theory (free theory).

 

Chapter 10 describes finite limit sketches, which are more powerful than universal algebra in a different way from the finite discrete sketches of Chapter 8, allowing partial operations, but only those whose domain can be described equationally. These sketches have somewhat more expressive power than universal Horn theories. We also describe briefly the most general types of sketches.

 

Chapter 11 introduces mappings between sketches, which are applied to the description of parametrized data types. In this chapter, sketches are also shown to be institutions in the sense of Goguen and Burstall.

 

Chapter 12 describes fibrations and the Grothendieck construction, which have applications to programming language semantics. We also consider wreath products, a type of fibration which has been used in the study of automata.

 

Chapter 13 discusses the concept of adjointness, which is one of the grand unifying ideas of category theory.  It is closely related to two other ideas: representable functors and the Yoneda Lemma.  Many of the constructions in preceding chapters are examples of adjoints.

 

Chapter 14 contains a miscellany of topics centered around the idea of the algebra for a functor.  We use this to define fixed points for a functor, to introduce the notion of a triple (monad) and to develop the Smyth-Plotkin technique for constructing Scott domains.

 

Chapter 15 introduces toposes.  A topos is a kind of generalized set theory in which the logic is intuitionistic instead of classical.  Toposes (or computable subcategories thereof) have often been thought the correct arena for programming language semantics.  Categories of fuzzy sets are recognized as almost toposes, and modest sets, which are thought by many to be the best semantic model of polymorphic lambda calculus, live in a specific topos.

 

Chapter 16 introduces monoidal categories, *autonomous categories and the Chu construction. The latter form a model of linear logic. 

 

Most sections have exercises which provide additional examples of the concepts and pursue certain topics further.  Many exercises can be solved by carefully keeping track of the definitions of the terms involved.  A few exercises are harder and are marked with a dagger. Some of those so marked require a certain amount of ingenuity (although we do not expect the reader to agree in every case with our judgment on this!).  Others require familiarity with some particular type of mathematical structure.  For example, although we define monoids in the text, a problem asking for an example of a monoid with certain behavior can be difficult for someone who has never thought about them before reading this book.

 

The third edition contains solutions to all the exercises. The solutions to the easy exercises, especially in the early chapters, go into considerable detail.  The solutions to the harder exercises often omit routine verifications.


Charles Wells' Home Page -- CWRU Mathematics Department Home Page