Promotors: Prof. Dr. W. Fokkink, Prof. Dr. H. Hansen
Co-Promotor: Dr. J. Endrullis
This thesis explores two applications of category theory in computer science. Part I presents theorems that provide uniform algebraic presentations of monads. Part II presents methods for identifying quasitoposes in graph rewriting. These concepts will be explained in more detail in the remainder of this chapter. 1.1 Two Applications of Category Theory in Computer Science Category theory is a field of mathematics that focuses on abstract structures and relationships between them. It offers an abstract framework that enables the unification and generalisation of mathematical definitions and theorems. At its core, category theory is about identifying and analysing patterns of relationships. We assume that the reader is familiar with the basic concepts of category theory, such as categories, functors, and natural transformations. Appendix A contains a reminder of all basic, but also more advanced, concepts in category theory used in this thesis. 1.1.1 Part I: Uniform Algebraic Presentation of Monads Monads are a categorical concept in algebra. Moggi [Mog89; Mog91] introduced their use in computer science as a unifying theory for modelling various notions of computation in functional programming, such as partiality, nondeterminism, exceptions, and side-effects. A function is partial if it is not defined for all inputs, nondeterministic if it returns multiple possible outcomes, and it handles exceptions by allowing errors to propagate while preserving its normal flow. The side effects are, for instance, having states or input/output. Plotkin and Power [PP02] built on Moggi’s work, renaming “notion of computation” as computational effect, and emphasised the algebraic view of monads. This algebraic view derives 1 2 Chapter 1. Introduction from the correspondence between (finitary) monads and algebraic theories [AR94, Section 3.18]. When an algebraic theory corresponds to a monad, it is said to be an algebraic presentation of the monad [Man76]. The development and use of monads have led to their incorporation into several functional programming languages, including Haskell, Scala, and OCaml, and later into some imperative languages, such as Python and JavaScript. Monad compositions provide a structured approach to reasoning about programs that combine several computational effects. Methods to compose monads are complex, require sometimes lengthy axioms to be checked, and sometimes even fail [KS18; Zwa20; JD93]. Recent research has shown that composing certain monads via distributive laws is impossible, correcting several mistakes in the literature [Zwa20; ZM22; KS18]. Understanding the conditions under which monads can be composed, particularly through the use of distributive laws, remains an active area of research. Studying distributive laws algebraically has proven to be a productive approach to understand when and how monads can be composed [Zwa20; Par20]. Section 1.2 provides a more detailed overview of the background regarding monads, algebraic presentations, and distributive laws. Section 1.3 outlines the novel contributions of Part I. Section 1.4 reviews related work relevant to Part I. 1.1.2 Part II: Quasitoposes in Graph Rewriting Graph rewriting is about transforming graphs according to a given set of rules. It generalises term rewriting [Ter03], a formalism where terms —constructed from variables, constants, and function symbols —are transformed based on specified rewrite rules. Since terms can be represented as trees, which are a special kind of graph, graph rewriting extends term rewriting by allowing for the manipulation of more complex structures. Graphs provide a visual way to represent data and are often more suitable than terms, as they can naturally incorporate references and pointers. There are many different types of graphs: multigraphs, hypergraphs, bipartite graphs, coloured graphs, labelled graphs, bouquets, etc. The variety of graph definitions poses a problem in graph rewriting, as it is impractical to develop a rewriting formalism for each type of graphs separately. The framework of algebraic graph rewriting solves this problem by using category theory to define rewriting formalisms for arbitrary categories, which can later be instantiated with any desired category of graphs [EEPT06]. Moreover, the categorical approach to graph rewriting allows for a general study of meta theorems—such as termination, concurrency, congruence, parallelism —in terms of the properties of the category at hand, see e.g. [LD94; Plu95; Cor96; BHK21]. Over the years, new categorical definitions have been introduced with applications in graph rewriting in mind, including adhesive categories and multiple variations of it. One purpose of adhesivity was to ensure the applicability of the Double Pushout (DPO) rewriting formalism [LS04; LS05]. More recently, a new interest 1.1. Two Applications of Category Theory in Computer Science 3 in algebraic graph rewriting has emerged for toposes and quasitoposes, which are existing mathematical notions that have been extensively studied, see e.g. [Joh02; Wyl91; MM94; McL92]. Quasitoposes have proven fruitful in graph rewriting, as they possess properties that facilitate the applicability and comparison of graph rewriting formalisms, enable operations such as relabelling, and ensure the validity of meta-theorems like concurrency and termination [BHK21; OER23; OE23b]. Part II of this thesis investigates techniques for establishing that certain graph categories are quasitoposes. Section 1.5 provides a more detailed overview of the background regarding graph rewriting, rewriting graph with labels, and (quasi)toposes. Section 1.6 outlines the novel contributions of Part II. Section 1.7 reviews related work relevant to Part II.