For many years, Burstall has been urging computer programmers to look at algebraic constructions to structure their code [1,2]. This book presents computations in categories as algorithms in a modern programming language (the applicative language ML). The authors use these constructions to program examples such as the join of relations and the transitive closure of a graph; they devote one chapter to a categorical unification algorithm. For those more esoterically inclined, they show how the semantics of the specification language Clear can be programmed.
The authors warn that implementations of these constructs may not be very efficient because they use polymorphic high-level functions. They claim that category theory seems to operate on the same level of generality as logic and computer programming. Consequently, the book has to face the disadvantages of any beginning programming book: learning from it is very difficult unless one has both intuition into the basic data types assumed (e.g., integers, reals, and lists in the case of programming) and access to a system on which one can run programs. Assuming one has such a system, this book asks still more. It attempts both to explain category theory and to teach how to program it, which is comparable to a beginning programming book that explains compilation. At the same time, applications of category theory at the basic computer science level are hard to find. I would, therefore, underline the authors’ statement in the preface that the reader “who wishes to learn category theory should have recourse to standard texts . . . but could well find this book a helpful companion text.” Mathematical maturity at the undergraduate level seems to be a prerequisite for this text.
Another audience for the book is theoreticians who want to see how constructive mathematics can be represented in programming. Again, the mathematician who wishes to learn computer programming (in ML, say) is well advised to have a standard ML text and to use this book as a companion.
For those who have some acquaintance with both category theory and computer science, the choices of language and algorithms reveal some interesting design decisions. The major decisions are (a) the representation of categories as types and (b) the representation of universal properties and duality by (higher-order) functions. The references are comprehensive, and the last chapter contains an excellent comparison with other related systems, although I would have liked to see some discussion of Curien’s categorical abstract machine [3].