Category Theory - An Axiomatic Theory of Structure

--- tags: programming languages, category theory, monoids, haskell, monads --- # Category Theory - Axiomatic Theory of Structure (formerly entitled **A Short Introduction to Monads**) *(These are notes to a course taught in interterm January 2020 to a small number of students who took my course on Programming Languages, had discovered monads in Haskell and wanted to learn about monads in mathematics. I wrote the notes while giving the course and never refined them afterwards. But I would be happy to add material if anybody was interested.)* ... *(Maybe I should change the title, the notes are not so short anymore.)* Addressed (mainly, but not exclusively) to undergraduate computer science students who encountered monads in Haskell and want to see how they arise in mathematics. [^monadsinhaskell] I will write some of the mathematics in Haskell. We will use only a very small fragment of Haskell, so you can give it a try even if you have not seen Haskell before. [Get in touch](mailto:akurz@chapman.edu?subject=Monads) if you have any questions. [^haskell] The perspective on Haskell I take in this course is the one of a mathematician using Haskell to illustrate and implement mathematics. I try to avoid Haskell idiosyncrasies as much as possible. There are many Haskell monad tutorials available.  I will label some exercises as "programming exercises" and some as "maths exercises". The aim is that these notes will benefit equally a reader who just does the programming exercises and a reader who just does the maths exercises. Programming exercises require implementation, maths exercises require proof. There are also general exercises that require neither. I made an introductory video on [What is algebraic structure?](https://youtu.be/kgr3R2Bwhgs) I wrote an [introduction to the introduction](https://hackmd.io/@alexhkurz/ryhYFFtmD).  ## Abstract 1) [Monoids](https://hackmd.io/@alexhkurz/B1oIuXxRv) Monoids play a major role in computer science. In fact, one could characterise the difference between "physics maths" and "computer science maths" by the difference between groups and monoids. Groups are crucial in physics because all fundamental physical laws are reversible. If we drop the axiom of reversibility, we obtain monoids instead of groups. Examples of (variations of) monoids are automata (finite state machines) and many fundamental data structures such as lists, strings, various systems of numbers, etc. And, of course, the (untyped) lambda calculus. 2) [Structure Preserving Maps](https://hackmd.io/@alexhkurz/BJppGrxRD) Structure and patterns is what makes science work. So it makes sense to study structure in its own right. Can we define what structure is? Is there a general theory of structure? Here we will look at a first clue, namely the idea of a structure preserving map. Structure preserving maps are a very general idea. They are what makes abstraction work, whether it is in mathematics or software engineering. They also arise when we give meaning to syntax in logic or programming languages. 3) **An Axiomatic Theory of Structure:** [Categories, Functors, Natural Transformations](https://hackmd.io/@alexhkurz/BktmSSgCP) Category theory is one of the areas of maths that provides a general language for problem solving (other examples are logic, probability theory, differential equations). From that point of view, category theory is great for solving problems that are best dealt with using types, structure preserving maps, and different modes of composition. But a category is also a simple mathematical structure in its own right: - A category is a typed (or many-sorted) monoid. - A category is a directed graph in which any two edges can be composed. - A category is an ordered structure in which there is more than one way that one element can be smaller than another. In addition, from a logical point of view, one can think of a category as an axiomatic theory of structure. 3) (b) [Yoneda Lemma](https://hackmd.io/@alexhkurz/HyMzQZLJu) The previous two lectures involved quite a bit of programming and only suggested some optional excursions into mathematical proofs. This lecture focusses on the mathematics side and is not needed in the next section. The main aim is to use the Yoneda lemma to prove that there are rather fewer polymorphic functions than one might expect at first sight. But we also prove the Yoneda lemma itself and explain its importance to category theory. 4) [Monads](https://hackmd.io/@alexhkurz/HkH8SBxAw) One of the benefits of an axiomatic theory of structure is that the same axioms appear again and again on different levels of abstraction. A famous example is the definition of a monad as a monoid in the category of endofunctors. Just from this short definition, one would not expect that that monads encompass a wide variety of structures such as - monads in functional programming - monoids, groups, rings, algebras, ... - abstract data types - algebraic data types - reflexive and transitive relations - categories and many more. **Remarks on teaching:** In my experience this course can fit (without the excursion to the Yoneda lemma) into 4 x 90min lectures for computer science undergraduates who know some Haskell and want to learn more about the mathematical side. The Haskell concepts of algebraic data types and monads are related to universal algebra and category theory, respectively. But no prior knowledge of universal algebra or category theory was expected. The lectures did not cover everything in the notes, rather I tried to convey the important ideas and left the notes for reference/further reading. I tried to strike a balance between lecturing and developing the material with the audience. A largely student led exploration would have taken maybe twice as much time. While interleaving math with programming was one of the ideas of these notes from the beginning, only while teaching it, I started to think of the course as having two projections $$Programming \longleftarrow Course \longrightarrow Mathematics$$ When I will have more time again, my plan is to rework these notes so that the reader can project out either a course that only has programming and no math or a course that only has math and no programming. There should be a sequence of "programming exercises" and a sequence of "math exercises" which are entirely independent, the course making sense for readers who are only taking one set of exercises. This should also help to clarify the interplay between mathematics and programming more generally. ## Introduction It is good to have a unifying theme for all lectures. I will take this to be the axiomatic method. It will follow the following pattern. 1. Examples 2. Axioms 3. More Examples 4. Theory 5. Applications The axiomatic method has been applied succesfully to answer, amongst others, the following questions. - What is geometry? (Euclid, Hilbert, Klein, ...) - What are numbers? (Dedekind, Peano, ...) - What is probability? (Kolmogorov, ...) - What is causality? (Pearl, ...) In this course, we will be concerned with the question - What is structure? On the way, we will shed light on related questions such as the following. What is algebraic structure? What is induction? ... ## Acknowledgements Thanks to Dan Haub and Matt Raymond for feedback and comments. ## References For a quick introduction to Haskell, my [Very Short Introduction to Automata and Haskell](https://hackmd.io/@alexhkurz/HylLKujCP) should suffice (let me know ...). ... more references and further reading should be added ... [^monadsinhaskell]: If you have not seen monads in Haskell a good place to start is Graham Hutton's video [What is a Monad? - Computerphile](https://www.youtube.com/watch?v=t1e8gqXLbsU). If you want a general introduction to monads for imperative programmers try the video which starts from the idea of [Controlling Complexity in Software Engineering](https://www.youtube.com/watch?v=ZhuHCtR3xq8#t=16m26s). [^haskell]: See also my [short introduction to automata and Haskell](https://hackmd.io/@alexhkurz/HylLKujCP) and my list of resources at [first steps in Haskell](https://hackmd.io/@alexhkurz/SJgHGZ_nw)