To a very large extent, category theory deals with “naturality”, i.e., the explicit construction of morphisms. This constructive aspects of the subject is what originally motivated the authors of this interesting book to undertake the project of devising explicit algorithms, in a currently implemented functional programming language (Standard ML), that parallel the usual category-theoretic constructions (e.g., limits, colimits, pullbacks). The idea is to represent categorical concepts as data types in ML, and then to represent constructive proofs of theorems as ML programs. The book is not a report on the (by now widespread) uses of category theory in the theory of programming. However, it is, among other things, a good introduction of category theory for programmers who may desire ultimately to understand such uses. For mathematicians familiar with category theory and with some programming background, the book is an interesting entree into the algebraic development of theoretical computer science. The following is a brief run-down of the chapter contents. Chapter 1 is introductory, lays out the plan of the book, and has a guide to the introductory literature in category theory and in functional programming (including ML references and availability). Chapter 2 is an introduction to programming in ML. The chapter ends with several programming exercises, with solutions given in an appendix. (There are exercises at the end of each of Chapters 3-8, but no solutions are provided.) Chapters 3-7 lay out basic category theory. Topics include limits/colimits, functor categories, adjunctions, and toposes. Chapters 8-9 present applications of categorical programming. Constructions of colimits are used in the unification of terms (arising in the automation of inference), as well as in the construction of algebraic theories. In Chapter 10 the authors discuss the formal (linguistic) aspects of category theory, and list some requirements on a formalism for expressing category-theoretic concepts. They also consider fragments of category theory in formal systems other than ML.
Reviewer: P.Bankston