The Relative Monadic Metalanguage
summary
Generalises the monadic metalanguage to a relative setting and gives a complete semantics using a new definition of strong relative monads. Builds a first‑order calculus separating ground types and effect types, implements finite probabilistic programming with a built‑in coin and axioms that recover finite stochastic matrices, and constructs LNL‑RMM for graded monads plus ARMM for arrows. Proves the semantics is sound and complete and both language embeddings are conservative, so the constructions behave as claimed.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:49Ground vs effect types
- 3:55Relative monads in programming
- 6:07Finite probabilistic programs
- 9:41Effect vs ground types
- 13:34Strong relative monads
- 16:25Graded monads in RMML
- 21:02Controlling computation
- 21:46Summary
- 22:29Q&A
related talks
17mNotions of Stack-manipulating Computation and Relative Monads
36mDependently Typed Multi-Stage Programming, Revisited
49mSemantic Foundations for Probabilistic Programming
15mStable Relations and Abstract Interpretation of Higher-Order Programs
16mA metalanguage for multi-phase modularity
27mPractical Extensions for Graded Monads
49mFinite functional programming via graded effects and relevance types
29mMechanized monadic equational reasoning for ML references