Structure and language of higher-order algebraic effects
File(s)
Author(s)
Yang, Zhixuan
Type
Thesis
Abstract
The research programme of algebraic effects studies non-pure features in programming languages, commonly referred to as computational effects, through the lens of algebraic theories of effectful operations. The free algebra monad induced by an algebraic theory provides the necessary structure for interpreting the computational effect in a programming language. Moreover, the universal property of free algebras can be internalised in programming languages as a useful programming construct known as effect handlers.
This thesis presents a generalisation of algebraic effects, called higher-order algebraic effects in this thesis, widening the range of effects that can be treated algebraically. The central idea is to shift focus from algebraic theories of operations to algebraic theories of monads equipped with operations, or more generally, theories of monoids equipped with operations in a monoidal category.
Part I of the thesis first develops a convenient categorical framework and a syntactic language for presenting algebraic theories of operations on monoids, and categorical properties of such theories are studied within this framework. Additionally, a formal theory of modular constructions of algebraic structures is proposed, based on lifting functors along fibrations.
In Part II of the thesis, a programming language with higher-order impredicative polymorphism and a restricted form of higher-order algebraic effects is presented. The consistency and the computational interpretation of the language are given by a realizability model. The canonicity of closed terms is proven using synthetic Tait computability. An extension of the language with general recursion is considered and is modelled using synthetic domain theory.
This thesis presents a generalisation of algebraic effects, called higher-order algebraic effects in this thesis, widening the range of effects that can be treated algebraically. The central idea is to shift focus from algebraic theories of operations to algebraic theories of monads equipped with operations, or more generally, theories of monoids equipped with operations in a monoidal category.
Part I of the thesis first develops a convenient categorical framework and a syntactic language for presenting algebraic theories of operations on monoids, and categorical properties of such theories are studied within this framework. Additionally, a formal theory of modular constructions of algebraic structures is proposed, based on lifting functors along fibrations.
In Part II of the thesis, a programming language with higher-order impredicative polymorphism and a restricted form of higher-order algebraic effects is presented. The consistency and the computational interpretation of the language are given by a realizability model. The canonicity of closed terms is proven using synthetic Tait computability. An extension of the language with general recursion is considered and is modelled using synthetic domain theory.
Version
Open Access
Date Issued
2024-09-28
Date Awarded
01/01/2025
License URL
Advisor
Wu, Nicolas
Sponsor
Engineering and Physical Sciences Research Council
Huawei-Edinburgh Joint Lab (Firm)
Grant Number
EP/S028129/1
Publisher Department
Computing
Publisher Institution
Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)