The Relative Monadic Metalanguage

TL;DR

This paper extends the monadic metalanguage to a relative setting using strong relative monads, generalizing existing calculi and providing complete semantics for graded monads and arrows.

Contribution

It introduces the relative monadic metalanguage, generalizes two existing calculi, and offers complete semantics for graded monads and arrow calculus.

Findings

LNL-RMM is a conservative extension of the graded monadic metalanguage.

Complete semantics for the arrow calculus as a restricted relative monadic metalanguage.

Introduction of ARMM, a lambda calculus-style language for arrows.

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.