Inspired by Plotkin and Power’s algebraic treatment of computational effects and the principle of notions of computations as monoids, we propose a categorical framework for equational theories and models of monoids equipped with operations. This framework generalises Plotkin and Power’s algebraic treatment of effectful operations taking or returning values as input or output to operations that may take or return computations as input or output. Additionally, to give semantic models of computational effects in a modular way, we introduce a formal theory of modular constructions of algebraic structures based on the framework of lifting functors along fibrations.

The formal theory of monads shows that much of the theory of monads can be developed in the abstract at the level of 2-categories. This means that results about monads can be established once and for all and simply instantiated in settings such as enriched category theory. Unfortunately, these results can be hard to reason about as they involve more abstract machinery. In this paper, we present the formal theory of monads in terms of string diagrams — a graphical language for 2-categorical calculations. Using this perspective, we show that many aspects of the theory of monads, such as the Eilenberg–Moore and Kleisli resolutions of monads, liftings, and distributive laws, can be understood in terms of systematic graphical calculational reasoning. This paper will serve as an introduction both to the formal theory of monads and to the use of string diagrams, in particular, their application to calculations in monad theory.

Deep learning, despite its remarkable achievements, is still a young field. Like the early stages of many scientific disciplines, it is marked by the discovery of new phenomena, ad-hoc design decisions, and the lack of a uniform and compositional mathematical foundation. From the intricacies of the implementation of backpropagation, through a growing zoo of neural network architectures, to the new and poorly understood phenomena such as double descent, scaling laws or in-context learning, there are few unifying principles in deep learning. This thesis develops a novel mathematical foundation for deep learning based on the language of category theory. We develop a new framework that is a) end-to-end, b) unform, and c) not merely descriptive, but prescriptive, meaning it is amenable to direct implementation in programming languages with sufficient features. We also systematise many existing approaches, placing many existing constructions and concepts from the literature under the same umbrella. In Part I we identify and model two main properties of deep learning systems parametricity and bidirectionality by we expand on the previously defined construction of actegories and Para to study the former, and define weighted optics to study the latter. Combining them yields parametric weighted optics, a categorical model of artificial neural networks, and more. Part II justifies the abstractions from Part I, applying them to model backpropagation, architectures, and supervised learning. We provide a lens-theoretic axiomatisation of differentiation, covering not just smooth spaces, but discrete settings of boolean circuits as well. We survey existing, and develop new categorical models of neural network architectures. We formalise the notion of optimisers and lastly, combine all the existing concepts together, providing a uniform and compositional framework for supervised learning.

Inspired by algebraic effects and the principle of notions of computations as monoids, we study a categorical framework for equational theories and models of monoids equipped with operations. The framework covers not only algebraic operations but also scoped and variable-binding operations. Appealingly, in this framework both theories and models can be modularly composed. Technically, a general monoid-theory correspondence is shown, saying that the category of theories of algebraic operations is equivalent to the category of monoids. Moreover, more complex forms of operations can be coreflected into algebraic operations, in a way that preserves initial algebras. On models, we introduce modular models of a theory, which can interpret abstract syntax in the presence of other operations. We show constructions of modular models (i) from monoid transformers, (ii) from free algebras, (iii) by composition, and (iv) in symmetric monoidal categories.

Effect handlers can be composed by applying them sequentially, each handling some operations and leaving other operations uninterpreted in the syntax tree. However, the semantics of composed handlers can be subtle—it is well known that different orders of composing handlers can lead to drastically different semantics. Determining the correct order of composition is a non-trivial task. To alleviate this problem, this paper presents a systematic way of deriving sufficient conditions on handlers for their composite to correctly handle combinations, such as the sum and the tensor, of the effect theories separately handled. These conditions are solely characterised by the clauses for relevant operations of the handlers, and are derived by fusing two handlers into one using a form of fold/build fusion and continuation-passing style transformation. As case studies, the technique is applied to commutative and distributive interaction of handlers to obtain a series of results about the interaction of common handlers: (a) equations respected by each handler are preserved after handler composition; (b) handling mutable state before any handler gives rise to a semantics in which state operations are commutative with any operations from the latter handler; (c) handling the writer effect and mutable state in either order gives rise to a correct handler of the commutative combination of these two theories.