A monadic solution to the Cartwright-Felleisen-Wadler conjecture

TL;DR

This paper presents a new method for constructing stable monadic denotational semantics for programming languages, addressing the Cartwright-Felleisen-Wadler conjecture by using monad factorizations and fibrations.

Contribution

It introduces a general technique to generate stable models from standard monadic models through monad morphism factorizations, supporting language extension stability.

Findings

Models based on type-and-effect systems are stable under language extension.

Factorizations of monad morphisms induce monads for sets of operations.

Preliminary fibrations work supports correctness of the models.

Abstract

Given a programming language, can we give a monadic denotational semantics that is stable under language extension? Models containing only a single monad are not stable. Models based on type-and-effect systems, in which there is a monad for every set of operations in the language, are. Cartwright and Felleisen, and Wadler, conjectured such monadic semantics can be generated. We describe a new general method of constructing stable models from standard monadic models, based on factorizations of monad morphisms. We show that under certain conditions factorizations induce a monad for every set of operations, and explain why the conditions usually hold. We also describe preliminary work using fibrations for logical relations generated from these factorization systems for proving the correctness of the resulting model.