From Partial to Monadic: Combinatory Algebra with Effects

TL;DR

This paper introduces Monadic Combinatory Algebras (MCAs), a generalization of Partial Combinatory Algebras (PCAs), to model a broader range of computational effects within a unified algebraic and categorical framework, enhancing realizability theory.

Contribution

It proposes MCAs as a monadic extension of PCAs, supporting various effects and providing a categorical characterization, thus broadening the foundational models of computation.

Findings

MCAs support effects like non-determinism, state, and continuations.

Categorical characterization of MCAs within Freyd Categories.

Construction of effectful realizability models using MCAs.

Abstract

Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped $\lambda$-calculus and serve as the basis for many notions of computability, such as realizability theory. However, PCAs support a very limited notion of computation by only incorporating non-termination as a computational effect. To provide a framework that better internalizes a wide range of computational effects, this paper puts forward the notion of Monadic Combinatory Algebras (MCAs). MCAs generalize the notion of PCAs by structuring the combinatory algebra over an underlying computational effect, embodied by a monad. We show that MCAs can support various side effects through the underlying monad, such as non-determinism, stateful computation and continuations. We further obtain a categorical characterization of MCAs within Freyd Categories, following a similar connection for PCAs. Moreover, we explore the application of MCAs in realizability theory, presenting constructions of effectful realizability triposes and assemblies derived through evidenced frames, thereby generalizing traditional PCA-based realizability semantics. The monadic generalization of the foundational notion of PCAs provides a comprehensive and powerful framework for internally reasoning about effectful computations, paving the path to a more encompassing study of computation and its relationship with realizability models and programming languages.