Rydeheard D.E., Burstall R.M. Computational category theory

Prentice Hall, 1988. — 263 p.
Why should there be a book with such a strange title as this one? Isn't category theory supposed to be a subject in which mathematical structures are analyzed on such a high level of generality that computations are neither desirable nor possible? Historically, category theory arose in algebraic topology as a way to explain in what sense the passages from geometry to algebra in that feld are `natural' in the sense of reflecting underlying geometric reality rather than particular representations in that reality. The success of this endeavor led to many similar studies of geometric and algebraic interrelationships in other parts of mathematics until, at present, there is a large body of work in category theory ranging from purely categorical studies to applications of categorical principles in almost every feld of mathematics. This work has usually been presented in a form that emphasizes its conceptual aspects, so that category theory has come to be viewed as a theory whose purpose is to provide a certain kind of conceptual clarity.
What can all of this have to do with computation? The fact of the matter is that category theory is an intensely computational subject, as all its practitioners well know. Categories themselves are the models of an essentially algebraic theory and nearly all the derived concepts are finitary and algorithmic in nature. One of the main virtues of this book is the unrelenting way in which it proceeds from algorithm to algorithm until all of elementary category theory is laid out in precise computational form. This of course cannot be the whole story because there are some deep and important results in category theory that are non-constructive and that cannot therefore be captured by any algorithm. However, for many purposes, the constructive aspects are central to the whole subject.