Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Category theory for computing science
Barr M. (ed), Wells C. (ed), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990. Type: Book (9780131204867)
Date Reviewed: Nov 1 1993
Comparative Review

About 35 years ago I had a discussion with some graduate students at my alma mater about problems I was having formulating questions about function composition in relationship to Algol. They said that little was understood about such general compositions. At that time hardly anyone knew about category theory and Kan had only just published his seminal paper on adjoint functors [1]. Today the effectiveness of category theory in explicating concepts based upon composition is widely recognized. The applications range from dynamical systems through rewrite rules and programming languages to structures within logic that profoundly alter our conceptions of constructive foundations.

As computation is so deeply intertwined with the very conception of composition, the universals that arise in the study of categories apply to all technical aspects of computer science, computer engineering, software engineering, and all other technical forms of computer practice. In any discipline, appropriate theory codifies the experimentation and practice. We now understand the role of categories and category theory in providing a clean, uniform, cohesive framework giving great insight into appropriate computational structures.

Lawvere and Schanuel

F. William Lawvere’s Ph.D. dissertation originated the categorical view of algebras that strongly influenced the development of abstract data types. He invented distributive categories as an explication for aspects of computation. His work with Myles Tierney gave rise to the great foundational explorations of toposes. Written by masters, Conceptual mathematics is for all of us who want to learn a new, clear, clean, crisp, and wonderfully refreshing way of looking at the world. Not specifically just for computer scientists, this elementary text could serve as the lecture notes for a freshman course. It offers a perspective upon the world that, provided you persevere, will enable you to see order and beauty where previously there was none. The book is full of the beginnings of topics that are ordinarily considered advanced but are not actually that difficult, as this book demonstrates. These topics include the important notions of inverse images and fibers, but also factorizations and a touch of toposes. Categories of structured sets and universal mapping properties are introduced.

All of this is done for beginners with small, well-motivated examples. The book has lots of discourse with students, plenty of repetition, and ample examples. This gem is suitable for self-study or the classroom, and for the sheer joy of discovery I had trouble putting it down.

Walters

Many years ago, Alfred North Whitehead wrote in The aims of education [2] that the step in learning after discovery was to build toward mastery. Walters’s text, a reworking of lecture notes for a junior course at the University of Sydney, continues the discovery of the applicability of categories in computer science and begins building toward mastery. The examples are drawn from elementary topics in circuits and flowcharts and also in automata and formal languages. They build toward the distributive categories just touched upon in Lawvere and Schanuel’s work. Within the setting of distributive categories, nicely explained here, one sees data structure abstractions done properly. The example of queues is the most compelling in that all of the structure of distributive categories is used.

The concept of freedom is central to the understanding of many matters in category theory and in computer science. This concept, closely akin to generating graphs, is explicated well here. Perhaps one needs to carefully remember the distinction between a category and the presentation of a category via multidigraphs and relations. The automata and formal language concepts fit in beautifully here. Kleene’s theorem requires but a page for statement and proof after the categorical background perfectly sets the stage.

The concluding chapter takes on two procedures of great import: Knuth-Bendix and the left Kan extension. Both are explained well. The left Kan extension has many important uses within computer science as well as computer and software engineering--vastly more than the text hints at. Programs in the book and correction details for the book are available by anonymous ftp from maths.su.oz.au:pub/sydcat.

Conceptual mathematics and Categories and computer science have been used together for an upperclass or graduate course for computer scientists to good effect. I strongly recommend both books.

Pierce

The next volume for our growing mastery of the subject is Basic category theory for computer scientists. This pleasant little volume introduces more of the universal constructions than the previous two books, as well as introducing adjoints. There are many examples of adjoints. For example, the two books reviewed above contain many instances of adjoints without defining the concept. The applications discussed in this volume are all closely related to programming language semantics, but even if this topic does not particularly appeal to you, I recommend this book; the uses of Cartesian closed categories and recursive domain equations, both treated here, extend throughout computation studies and will amply repay the effort. The book closes with an extremely useful chapter about other textbooks, introductory articles, reference books, and some selected research papers. Pierce writes in the preface that he wrote this book as a graduate student, and I think that is an appropriate audience for this friendly, helpful book with lots of examples. This book is also recommended as an introduction for all computer scientists who want to read either of the next two books in this review.

Barr and Wells

Rather more mature as a text, and so requiring greater maturity and thought from readers, is Category theory for computing science. Here one sees Cartesian closed categories from a different perspective, and is introduced to sketches and to locally Cartesian closed categories. The chapter on fibrations harkens back to ideas not seen in the volumes in this review since Conceptual mathematics, as does the chapter on toposes. This chapter provides a brief, clear introduction to the important concept of sheaf. For more on this subject, try MacLane and Moerdijk [3] or Barr and Wells[4].

Fibrations and the Grothendieck construction of fibrations are important ideas. A fibration is a generalization of the inverse of a function. The generalization occurs repeatedly in the structuring of data and programs. With mastery, obtainable by the study of this volume, you will recognize fibrations and the Grothendieck construction again and again in computational settings.

This is the first book in this review to treat the concept of “triple,” also called “monad” by computer scientists following the usage in MacLane [5]. This concept is a vast generalization of the idea of an algebra, in the sense of universal algebra. So the “abstract data types” are often monads; various domain constructions are monads; certain topological concepts are monads; and so on. A more advanced discussion may be found in Barr and Wells [4].

This book lightly treats many other ideas having applications in software engineering and computer science. I consult it frequently for both areas. I recommend it highly for the more mature and patient readers who are ready to draw diagrams, do exercises, and otherwise attend to the discipline of learning a science from the writings of masters.

The book is maintained with a list of errata and additions available by postal service or email from the authors via barr@triples.math.mcgill.ca or cfw2@po.cwru.edu.

Asperti and Longo

This text is the most advanced of these five books. It treats, with thorough rigor, all the previously mentioned topics except distributive categories and sketches. This text uses indexed categories rather than fibrations. As this book is a semantically and foundationally oriented advanced text, readers should be aware that, in an important foundational sense, indexed categories need to be replaced by fibrations. Making this (not difficult) mental change as one reads will make the close relationship between indexed categories and fibrations completely clear.

The authors emphasize internal category theory, that is, categories within categories as foundations. This beautiful idea from topos theory helps to build the deep and interesting understanding of types as objects. This is the purpose of the second half of this book. Finally, at the end, we see internal models for types-as-objects done in a way that appears to provide satisfying closure about this aspect of expressibility. Once one has read the book, there is more food for thought, including predicates as fibrations (see Pavlovic [6]) and subtyping judgments for object languages and databases.

Comparison

Having fully mastered this part of conceptual mathematics, we can bring our mastery to bear upon important, practical questions of the day. For some, the first two volumes of this review series will suffice. Others may want to continue further with MacLane and Moerdijk [3], Lambek and Scott [7], and Barr and Wells [4], perhaps contributing to applications of categories by writing their own book, exemplified for the purposes of this review by Gunter [8], Manes [9], and Bloom and Esik [10]. Many topics in object databases, distributed computation, logic programming, and document preparation systems exist for which such books could be written.

I will conclude with a word about errors and notations. Every one of these books surely contains errors. Every one contains a few quirks of notation or terminology peculiar to the author or authors. The closest thing to a standard in this field is MacLane [5], and even that volume has a few mistakes. The important thing about categories is the concepts; they are what makes studying categories so refreshing.

Reviewer:  David B. Benson Review #: CR117439
1) Kan, D. M. Adjoint functors. Trans. Am. Math. Soc. 87 (1958), 299–329.
2) Whitehead, A. N. The aims of education and other essays. Macmillan, New York, 1929.
3) MacLane, S. and Moerdijk, I. Sheaves in geometry and logic: a first introduction to topos theory. Springer-Verlag, New York, 1992.
4) Barr, M. and Wells, C. Toposes, triples, and theories. Springer-Verlag, New York, 1985.
5) MacLane, S. Categories for the working mathematician. Springer-Verlag, New York, 1971.
6) Pavlovic, D. Predicates and fibrations. Ph.D. thesis, Rijksuniversiteit Utrecht, Utrecht, The Netherlands, 1990.
7) Lambek, J. L. and Scott, P. J. Introduction to higher order categorical logic. Cambridge University Press, New York, 1986.
8) Gunter, C. A. Semantics of programming languages: structures and techniques. MIT Press, Cambridge, MA, 1992.
9) Manes, E. G. Predicate transformer semantics. Cambridge University Press, New York, 1992.
10) Bloom, S. L. and Esik, Z. Iteration theories: the equational logic of iterative processes. Springer-Verlag, New York, 1993.
Comparative Review
This review compares the following items:
  • Category theory for computing science:
  • Basic category theory for computer scientists:
  • Categories, types, and structures:
  • Conceptual mathematics:
  • Categories and computer science:
  • Bookmark and Share
     
    Algebraic Approaches To Semantics (F.3.2 ... )
     
     
    Abstract Data Types (D.3.3 ... )
     
     
    Automata (F.1.1 ... )
     
     
    Control Primitives (F.3.3 ... )
     
     
    Type Structure (F.3.3 ... )
     
     
    Formal Definitions And Theory (D.3.1 )
     
      more  
    Would you recommend this review?
    yes
    no
    Other reviews under "Algebraic Approaches To Semantics": Date
    A basic abstract semantic algebra
    Mosses P.  Semantics of data types (, Sophia-Antipolis, France, Jun 27-29, 1984)1081984. Type: Proceedings
    Jun 1 1985
    Continuations in possible-world semantics
    Tennent R., Tobin J. Theoretical Computer Science 85(2): 283-303, 1991. Type: Article
    Sep 1 1992
    Soundness and completeness of the Birkhoff equational calculus for many-sorted algebras with possibly empty carrier sets
    Manca V., Salibra A. Theoretical Computer Science 94(1): 101-124, 1992. Type: Article
    Jun 1 1993
    more...

    E-Mail This Printer-Friendly
    Send Your Comments
    Contact Us
    Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
    Terms of Use
    | Privacy Policy