Computational Category Theory D.E. Rydeheard R.M. Burstall University of Manchester University of Edinburgh v This is a version of Computational Category Theory that is available for personal use only. Distributing copies, multiple downloads, availabil- ity at other websites, or use of any of the text for commercial purposes is strictly forbidden. Full copyright remains with the authors. vi Contents 1 Introduction 1 1.1 The contents 4 1.2 Accompanying texts 6 1.2.1 Textbooks on category theory 6 1.2.2 ML references and availability 7 1.2.3 A selection of textbooks on functional programming 7 1.3 Acknowledgements 8 2 Functional Programming in ML 9 2.1 Expressions, values and environments 11 2.2 Functions 13 2.2.1 Recursive de(cid:12)nitions 14 2.2.2 Higher order functions 14 2.3 Types 15 2.3.1 Primitive types 16 2.3.2 Compound types 16 2.3.3 Type abbreviation 17 2.4 Type polymorphism 17 2.5 Patterns 20 2.6 De(cid:12)ning types 21 2.7 Abstract types 24 2.8 Exceptions 26 2.9 Other facilities 27 2.10 Exercises 27 3 Categories and Functors 35 3.1 Categories 35 vii viii CONTENTS 3.1.1 Diagram chasing 38 3.1.2 Subcategories, isomorphisms, monics and epis 39 3.2 Examples 40 3.2.1 Sets and (cid:12)nite sets 40 3.2.2 Graphs 40 3.2.3 Finite categories 41 3.2.4 Relations and partial orders 41 3.2.5 Partial orders as categories 42 3.2.6 Deductive systems 42 3.2.7 Universal algebra: terms, algebras and equations 43 3.2.8 Sets with structure and structure-preserving arrows 46 3.3 Categories computationally 47 3.4 Categories as values 49 3.4.1 The category of (cid:12)nite sets 49 3.4.2 Terms and term substitutions: the category T Fin 50 (cid:10) 3.4.3 A (cid:12)nite category 52 3.5 Functors 53 3.5.1 Functors computationally 54 3.5.2 Examples 54 3.6 Duality 55 3.7 An assessment(cid:3) 57 3.8 Conclusion 60 3.9 Exercises 60 4 Limits and Colimits 65 4.1 De(cid:12)nition by universality 67 4.2 Finite colimits 68 4.2.1 Initial objects 69 4.2.2 Binary coproducts 70 4.2.3 Coequalizers and pushouts 72 4.3 Computing colimits 74 4.4 Graphs, diagrams and colimits 79 4.5 A general construction of colimits 82 4.6 Colimits in the category of (cid:12)nite sets 88 4.7 A calculation of pushouts 90 4.8 Duality and limits 93 4.9 Limits in the category of (cid:12)nite sets 95 4.10 An application: operations on relations 97 4.11 Exercises 100 CONTENTS ix 5 Constructing Categories 103 5.1 Comma categories 104 5.1.1 Representing comma categories 105 5.2 Colimits in comma categories 107 5.3 Calculating colimits of graphs 109 5.4 Functor categories 113 5.4.1 Natural transformations 113 5.4.2 Functor categories 114 5.5 Colimits in functor categories 116 5.6 Duality and limits 118 5.7 Abstract colimits and limits(cid:3) 120 5.7.1 Abstract diagrams and colimits 121 5.7.2 Category constructions 122 5.7.3 Indexed colimit structures 123 5.7.4 Discussion 123 5.8 Exercises 124 6 Adjunctions 127 6.1 De(cid:12)nitions of adjunctions 128 6.2 Representing adjunctions 130 6.3 Examples 131 6.3.1 Floor and ceiling functions: converting real num- bers to integers 132 6.3.2 Components of a graph 132 6.3.3 Free algebras 134 6.3.4 Graph theory 136 6.3.5 Limits and colimits 138 6.3.6 Adjunctions and comma categories 138 6.3.7 Examples from algebra and topology 139 6.4 Computing with adjunctions 140 6.5 Free algebras 142 6.5.1 Constructing free algebras 143 6.5.2 A program 144 6.5.3 An example: transitive closure 146 6.5.4 Other constructions of free algebras 149 6.6 Exercises 152 7 Toposes 155 7.1 Cartesian closed categories 156 7.1.1 An example: the category of (cid:12)nite sets 157 7.2 Toposes 159 x CONTENTS 7.2.1 An example: the topos of (cid:12)nite sets 161 7.2.2 Computing in a topos 162 7.2.3 Logic in a topos 164 7.2.4 An example: a three-valued logic 166 7.3 Conclusion 170 7.4 Exercises 171 8 A Categorical Uni(cid:12)cation Algorithm 173 8.1 The uni(cid:12)cation of terms 174 8.2 Uni(cid:12)cation as a coequalizer 175 8.3 On constructing coequalizers 176 8.4 A categorical program 180 9 Constructing Theories 187 9.1 Preliminaries 188 9.2 Constructing theories 190 9.3 Theories and institutions 194 9.4 Colimits of theories 197 9.5 Environments 199 9.6 Semantic operations 200 9.7 Implementing a categorical semantics 201 10 Formal Systems for Category Theory 203 10.1 Formal aspects of category theory 204 10.2 Category theory in OBJ 207 10.3 Category theory in a type theory 216 10.4 Categorical data types 218 A ML Keywords 223 B Index of ML Functions 225 C Other ML Functions 229 D Answers to Programming Exercises 231 FOREWORD xi Foreword John W. Gray 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 struc- tures 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 (cid:12)eld are ‘natural’ in the sense of re(cid:13)ecting 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, atpresent, there isalarge bodyofworkincategory theoryranging frompurelycategorical studiestoapplicationsofcategorical principlesin almost every (cid:12)eldof mathematics. Thiswork hasusually beenpresented inaformthat emphasizesitsconceptual aspects, sothatcategory 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 (cid:12)nitary and algorithmic in nature. One of the main virtues of this book is the unrelenting way in which it proceeds from algorithm to algorithm untilallofelementarycategorytheoryislaidoutinprecisecomputational 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 manypurposes,theconstructiveaspectsarecentraltothewholesubject. This is important for several reasons. First of all, one of the most xii FOREWORD importantfeaturesofcategory theoryisthatitisaguide to computation. The conceptual clarity gained from a categorical understanding of some particular circumstance in mathematics enables one to see how a com- putation of relevant entities can be carried out for special cases. When the special case is itself very complex, as frequently is the case, then it is a tremendous advantage to know exactly what one is trying to do and in principle how to carry out the computation. The idea of mechanizing such computations is very intriguing. The present book, of course, does not enable one to do this, but it can be viewed as an essential precur- sor of developments that will lead to such mechanization. Categories themselves must be present in the computer as well as many particular examples of them before mechanical computation of categorical entities can be carried out. Secondly, the fact that category theory is essentially algebraic means that it can be learned by learning these basic constructions. It comes as something of a shock to realize that one aspect of category theory is that it is ‘just’ a collection of ML-algorithms. However, it is particu- larly important for computer scientists and students of computer science that there issucha programminglanguage representation ofthe subject. Becausemathematicianshaveaccumulatedgeometric andalgebraicintu- itions, many things can be elided in presenting category theory to them. But computer scientists generally lack these intuitions, so these elisions can present a great di(cid:14)culty for them. Computer code does not permit such elisions and thus presents the basic material in a form that reas- sures computer scientists and allows them to use their intuitions for and understanding of programs to gain an advantage similar to the mathe- maticians’ advantage from their knowledge of geometry and algebra. Of course, all of this is beside the point unless there is a reason for computer scientists to need to learn category theory. However, the reasons are easily found by looking into almost any issue of a journal in theoretical computer science. Either the category theory is explicitly there or should be there and is missing only at the expense of devious circumlocutions. It really cannot be avoided in discussing the semantics of programming languages. The most dramatic instance of this arises in thesemanticsofthepolymorphiclambdacalculuswhichunderliesML.It really is an engaging thought that one needs category theory to explain ML, while in turn ML is a vehicle for explaining category theory. That brings up the last point. There is another audience for this book; namely, category theorists who want to understand theoretical computerscience sothattheycanparticipate intheexciting interactions FOREWORD xiii that aretaking place between thesetwo (cid:12)elds. Onevery importantentry pointintotheproblemsoftheoreticalcomputerscienceisjusttoexamine computer programs and to wonder what they mean. There probably is no (cid:12)nal answer to this question, but along the way, this book can serve as an invaluable stimulus to further research.