Categories, types, and structures. An introduction to category theory for the working computer scientist. (English) Zbl 0783.18001

MIT Press Series in the Foundations of Computing. Cambridge, MA: The MIT Press. 325 p. (1991).
From the introduction: “This book \(\dots\) 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 in polymorphisms and modularity. Recent applications, such as CAML, which will be described, use categorical formalization for the purposes of implementation.\(\;\dots\) The first part of this book should encourage even the reader with no specific interest in programming language theory to acquire at least some familiarity with the categorical way of looking at formal descriptions. The explicit use of deeper facts is a further step, which becomes easier with access to this information. Part II and some chapters in part I are meant to take this further step, at least in one of the possible directions, namely the mathematical semantics of data types and programs as objects and morphisms of categories.\(\;\dots\) We were urged to write the general introduction contained in part I, since most available books in category theory are written for the “working mathematician” and, as the subject is greatly indebted to algebraic geometry and related disciplines, the examples and motivations can be understood only by readers with some acquaintance with nontrivial facts in algebra or geometry. For most computer scientists, it is not much help in the understanding of “natural transformations” to see an involved example based on tensor products in categories of sheaves. Thus our examples will be based on elementary mathematical notions, such as the definition of monoid, group, or topological space, say, and on structures familiar for readers with some acquaintance with the tools in programming language semantics. In particular, partial orders and the various categories of domains for denotational semantics will often be mentioned or introduced, as well as basic results from computability theory.”
Contents: Part I, Categories and structures: 1. Categories (categories, diagrams, special morphisms), 2. Constructions (special objects, special limits, topoi), 3. Functors and natural transformations (including Yoneda Lemma, examples of Cartesian closed categories), 4. Categories derived from functors and natural transformations (monads, monoidal categories, closed categories), 5. Universal arrows and adjunctions, 6. Cones and limits, 7. Indexed and internal categories. – Part II, Types as objects: 8. Formulae, types, and objects (typed lambda calculus, sequent calculus, cut-elimination, categorical semantics), 9. Reflexive objects and the type-free lambda calculus, 10. Recursive domain equations, 11. Second- order lambda calculus, 12. Examples of internal models (provable retractions, PER inside \(\omega\)-Set, PL-categories inside their Grothendieck completion).


18-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to category theory
03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing