Handling the Selection Monad

on YouTube ↗21m

" summary

Designs effect handlers that expose loss continuations derived from the selection monad, letting handlers observe per-choice losses and resume computations with chosen results. Formalizes a core language λC, gives operational semantics, and proves progress, type soundness, and termination under a mild hierarchy constraint; offers a denotational semantics with soundness and adequacy proofs. Ships a Haskell library and working examples: binary-search choices, gradient updates for linear regression, two-player games and hyperparameter tuning.

AI-written summary · about

" chapters (9)

1. 0:00Selection monad intro
2. 2:58Algebraic effect handlers
3. 10:25Formal semantics
4. 11:49Loss continuations
5. 12:32Selection monads + handlers
6. 14:19Minimizer handler example
7. 16:01Linear regression with losses
8. 17:27Formal development
9. 18:31Q&A

" related talks

• 01h 17mSmart Handlers: Handling the selection monadNingning Xie · HOPE 2025
• 36mFlexible Instruction-Set Semantics via Abstract MonadsAdam Chlipala, Thomas Bourgeat, Andres Erbsen, Samuel Gruetter, Ian J Clester, Pratap Singh, Andy Wright · ICFP 2023
• 02h 50mIntro to Type Systems and Operational SemanticsAndres Löh · ZuriHac 2022
• 15mEffect Handlers, EvidentlyNingning Xie, Jonathan Immanuel Brachthäuser, Philipp Schuster, Daniel Hillerström · ICFP 2020
• 15mLatent Effects for Reusable Language ComponentsTom Schrijvers, Casper Bach Poulsen, Nicolas Wu, Birthe van den Berg · APLAS 2021
• 34mGraded Monads and Type-Level Programming for Dependence AnalysisFinnbar Keating · Haskell Symposium 2021
• 08mLightning Talk: Designing a Language for Learning ContinuationsYouyou Cong · Scheme 2023
• 54mRevisiting the Evolution of Effects (Invited Talk)Nicolas Wu · PEPM 2026