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. By lifting these restrictions, we introduce ARMM, a computational lambda calculus-style language for arrows that conservatively extends the arrow calculus.
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:40 | Monads and EffectsPOPL at Dortoirs Chair(s): Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg | ||
14:00 25mTalk | An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic TheoriesDistinguished Paper POPL Ohad Kammar University of Edinburgh, Jack Liell-Cock University of Oxford, Sam Lindley University of Edinburgh, Cristina Matache University of Edinburgh, Sam Staton University of Oxford DOI | ||
14:25 25mTalk | Handling Higher-Order Effectful Operations with Judgemental Monadic Laws POPL DOI | ||
14:50 25mTalk | Rows and Capabilities as Modal Effects POPL DOI | ||
15:15 25mTalk | The Relative Monadic Metalanguage POPL Jack Liell-Cock University of Oxford, Zev Shirazi University of Oxford, Sam Staton University of Oxford DOI | ||