English

The Relative Monadic Metalanguage

Programming Languages 2025-12-15 v1 Category Theory

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.

Keywords

Cite

@article{arxiv.2512.11762,
  title  = {The Relative Monadic Metalanguage},
  author = {Jack Liell-Cock and Zev Shirazi and Sam Staton},
  journal= {arXiv preprint arXiv:2512.11762},
  year   = {2025}
}

Comments

41 pages. Published in Proceedings of the ACM on Programming Languages (POPL 2026)

R2 v1 2026-07-01T08:22:32.101Z