Abstract: This paper tries to explain why and how category theory is useful in computing science, by giving guidelines for applying seven basic categorical concepts: category, functor, natural transformation, limit, adjoint, colimit and comma category. Some examples, intuition, and references are given for each concept, but completeness is not attempted. Some additional categorical concepts and some suggestions for further research are also mentioned. The paper concludes with some philosophical discussion. This paper tries to explain why category theory is useful in computing science. The basic answer is that computing science is a young eld that is growing rapidly, is poorly organised, and needs all the help it can get, and that category theory can provide help with at least the following: Formulating de nitions and theories. In computing science, it is often more di cult to formulate concepts and results than to give a proof. The seven guidelines of this paper can help with formulation; the guidelines can also be used to measure the elegance and coherence of existing formulations. Carrying out proofs. Once basic concepts have been correctly formulated in a categorical language, it often seems that proofs just happen": at each step, there is a natural" thing to try, and it works. Diagram chasing see Section 1.2 provides many examples of this. It could almost be said that the purpose of category theory is to reduce all proofs to such simple calculations. Discovering and exploiting relations with other elds. Su ciently abstract formulations can reveal surprising connections. For example, an analogy between Petri nets and the -calculus might suggest looking for a closed category structure on the category of Petri nets 52 . Dealing with abstraction and representation independence. In computing science, more abstract viewpoints are often more useful, because of the need to achieve independence from the often overwhelmingly complex details of how things are represented or implemented. A corollary of the rst guideline given in Section 1 is that two objects are abstractly the same" i they are isomorphic; see Section 1.1. Moreover, universal constructions i.e., adjoints de ne their results uniquely up to isomorphism, i.e., abstractly" in just this sense. The research reported in this paper has been supported in part by grants from the Science and Engineering Research Council, the National Science Foundation, and the System Development Foundation, as well as contracts with the O ce of Naval Research and the Fujitsu Corporation. Category theory can also be abused, and in several di erent s t yles. One style of abuse is specious generality, in which some theory or example is generalised in a way that does not actually include any new examples of genuine interest. A related style of abuse is categorical overkill, in which the language of category theory is used to describe phenomena that do not actually require such an elaborate treatment or terminology. An example is to describe a Galois connection in the language of adjoint functors. Category theory has been called abstract nonsense" by both its friends and its detractors. Perhaps what this phrase suggests to both is that category theory has relatively more form than content, compared to other areas of mathematics. Its friends claim this as a virtue, in contrast to the excessive concreteness and representation dependence of set theoretic foundations, and the relatively poor guidance for discovering elegant and coherent theories that they provide. Section 9 discusses this further. Category theory can also be used in quite concrete ways, because categories are after all just another algebraic structure, generalising both monoids and partial orders see also Example 1.4 below. This paper presents seven guidelines for using category theory, each with some general discussion and speci c examples. There is no claim to originality, because I believe the underlying intuitions are shared by essentially all workers in category theory, although they have been perhaps understandably reluctant to place such dogmatic assertions in textbooks or other written documents 1 . The guidelines are necessarily imprecise, and will seem exaggerated if taken too literally, because they are not objective facts, but rather heuristics for applying certain mathematical concepts. In particular, they may seem di cult to apply, or even impossible, in some situations, and they may need re nement in others. As a reminder that they should not be taken too dogmatically, I will call them dogmas. No attempt is made to be exhaustive. In particular, the technical de nitions are omitted, because our purpose is to provide intuition, and the de nitions can be found in any textbook. Thus, if you are a newcomer to category theory, y ou will need to use some text in connection with this paper. Unfortunately, no existing text is ideal for computing scientists, but perhaps that by Goldblatt 36 comes closest. The classic text by Mac Lane 47 is warmly recommended for those with su cient mathematics background, and Herrlich and Strecker's book 39 is admirably thorough; see also 2 and 45 . The paper 22 gives a relatively concrete and self-contained account o f some basic category theory for computing scientists, using theories, equations, and uni cation as motivation, and many examples from that paper are used here. As far as I know, the rst such attempt is my o wn in 34 , which gives four of the guidelines here. The only other attempt that I know is due to Lambek and Scott 45 , who give a n umberof slogans" in a similar style. The rst dogma is as follows: To e ach species of mathematical structure, there c orresponds a category whose objects have that structure, and whose morphisms preserve it. It is part of this guideline that in order to understand a structure, it is necessary to understand the morphisms that preserve it. Indeed, category theorists have argued that morphisms are more important than objects, because they reveal what the structure really is. Moreover, the category concept can bede ned using only morphisms. Perhaps the bias of modern Western languages and cultures towards objects rather than relationships accounts for this see 50, 64 for some related discussion. By way of notation, we use ;" for composition, and 1 A for the identity morphism at an object A. Now some examples: 1.1 Sets. If we take sets to beobjects, then their morphisms are clearly going to befunctions. A set morphism, however, is not just a set of ordered pairs, because it must also specify particular source and target sets. This is consistent with practice in computation theory which assigns types to functions. The set theoretic representation of functions is an artifact of the set theoretic foundations of mathematics, and like all such representations, has accidental properties beyond those of the concept it is intended to capture. One of those properties is that any two sets of ordered pairs can becomposed to yield a third. The category Set of sets embodies a contrary point of view, that each function has a domain in which its arguments are meaningful, a codomain in which its results are meaningful, and composition of functions is only allowed when meaningful in this sense. See 36 for related discussions. 1.2 Relations. Just as with functions, it seems desirable to take the view that the composition of relations is only meaningful when the domains match. Thus, we m a y de ne a relation from a set A 0 to a set A 1 to be a triple A 0 ; R ; A 1 with R A 0 A 1 , and then allow its composition with B 0 ; S ; B 1 to be de ned i A 1 = B 0 . This gives rise to a category that we denote Rel, of which Set can be considered a subcategory. 1.3 Graphs. A graph G consists of a set E of edges, a set N of nodes, and two functions @ 0 ; @ 1 : E ! N which give the source and target of each edge, respectively. Because the major components of graphs are sets, the major components of their morphisms should be corresponding functions that preserve the additional structure. Thus a morphism from G = E;N;@ 0 ; @ 1 to G 0 = E 0 ; N 0 ; @ 0 0 ; @ 0 1 consists of two functions, f: E ! E 0 and g : N ! N 0 , such that the following diagram commutes in Set for i = 0 ; 1: To show that we h a ve a category Graph of graphs, we m ust show that a composition of two such morphisms is another, and that a pair of identity functions satis es the diagrams and also serves as an identity for composition. Because the major components of automata are sets, the major components of their morphisms should be corresponding functions that preserve the structure. where fg denotes an arbitrary one point set with point . It must be shown that a composition of two such morphisms is another, and that a triple of identities satis es the diagrams and serves as an identity for composition. These checks show that we have a category Aut of automata, and their simplicity increases our con dence in the correctness of the de nitions 18 . 1.6 Types. Types are used to classify things," and according to the rst dogma, they should form a category having types as objects; of course, depending on what is being classi ed, di erent categories will arise. A simple example is nite product types, which are conveniently represented by natural numbers, with morphisms that describe what might be called register transfer operations" among tuples of registers". Thus, n 2 ! indicates an n-tuple ht 1 ; :::; t n i of data items in n registers," and a morphism f : m ! n is a function f1; :::; ng ! f 1; :::; mg indicating that the content of register fi should be transferred to register i, for i = 1 ; :::; n. In fact, if we identify the numbern with the set f1; :::; ng and 0 with ;, then this category is the opposite of a subcategory of Set; let us denote it N. A variant of N has as its objects the nite subsets of a xed countable set X, and as morphisms again the opposites of functions among these, so that we get another opposite of a subcategory of Set, denoted say X. Here, the registers" are denoted by variable symbols" from X, rather than by natural numbers. Going a little further, we can assign sorts from a set S to the symbols in X, and require that the morphisms preserve these sorts. Let us denote this category X S . 4 1.7 Substitutions. Two key attributes of a substitution are the set of variables into which it substitutes, and the set of variables that occur in what it substitutes. Thus, substitutions have natural source and target objects, each a set of variables, as in Example 1.6 above. Clearly there are identity substitutions for each set of variables substituting each variable for itself, and the composition of substitutions is associative when de ned. Thus, we get a category with substitutions as morphisms.
First applications of CT in computer science, and the general claim of CT's extreme usefulness for computer applications should be, of course, attributed to Joseph Goguen REF .
A categorical manifesto
Mathematical Structures in Computer Science
Computer Science Mathematics