The notion of a \emph{free extension} of an algebra serves as the foundation for an expressive framework, abstractly characterising algebras of terms over an algebraic structure — e.g., the ring of polynomials over a ring. This framework finds applications in the optimisation of algebraic computations in meta-programming; in the theory of normalisation by evaluation for first-order term languages; and in proof-synthesis in dependent-type theories. However, the current theoretical treatment of free extensions is limited to universal algebraic structures, whilst many structures of interest in programming language theory cannot be captured universal algebraically.

I present my ongoing work to generalise free extensions to broader classes of equational structures. Here, I focus on \emph{generalised algebraic theories} (GATs) à la Cartmell. Observing that the dependent sorting of GATs precludes a notion of free extension by a \emph{set} of variables, I instead develop a notion of free extension by a \emph{context}. This requires a strict generalisation of the universal property of free extensions, which I show specialises to the usual notion of free extension when applied to a universal algebraic theory (UAT). I conclude by summarising ongoing work to construct effective descriptions of generalised free extensions of structured categories.

Nathan Corbyn is a second-year DPhil student at the University of Oxford. His research interests span programming language theory, type theory, category theory, and compiler construction with a particular interest in the intersection. His recent work has focused on the theory and applications of free extensions of algebras.