The Relative Monadic Metalanguage
Abstract
Relative monads provide a controlled view of computation. We generalise the monadic metalanguage to a relative setting and give a complete semantics with strong relative monads. Adopting this perspective, we generalise two existing program calculi from the literature. We provide a linear-non-linear language for graded monads, LNL-RMM, along with a semantic proof that it is a conservative extension of the graded monadic metalanguage. Additionally, we provide a complete semantics for the arrow calculus, showing it is a restricted relative monadic metalanguage. This motivates the introduction of ARMM, a computational lambda calculus-style language for arrows that conservatively extends the arrow calculus.
Fields of Study & Subjects
Logic
programming
and type systems
Reasoning
and Knowledge
Natural Language Processing Techniques
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Volume
- 10
- Issue
- POPL
- Pages
- 1730–1758
- Publication date
- 8 January 2026
- Language
- EN