Handling the Selection Monad (Full Version)
Gordon Plotkin, Ningning Xie
TL;DR
This work presents a novel integration of the selection monad with algebraic effect handlers by introducing choice continuations that expose future losses to programmer-defined operations. The λC language formalizes this design with a deterministic, progressive small-step semantics, a termination guarantee for a safe subset, and a denotational model based on augmented selection monads, establishing soundness and adequacy results. The authors provide a Haskell library and a diverse set of programming examples, including greedy strategies, optimizations, hyperparameter tuning, and two-player games, illustrating the expressiveness and practicality of loss-aware effect handling. This framework enables programmable, loss-aware selection within modular effects, with potential applications in optimization, learning, game-playing, and beyond. The approach advances the theory and practice of effect handlers by enabling explicit access to loss information through choice continuations, offering a flexible foundation for future extensions and integrations with ML and AI tooling.
Abstract
The selection monad on a set consists of selection functions. These select an element from the set, based on a loss (dually, reward) function giving the loss resulting from a choice of an element. Abadi and Plotkin used the monad to model a language with operations making choices of computations taking account of the loss that would arise from each choice. However, their choices were optimal, and they asked if they could instead be programmer provided. In this work, we present a novel design enabling programmers to do so. We present a version of algebraic effect handlers enriched by computational ideas inspired by the selection monad. Specifically, as well as the usual delimited continuations, our new kind of handlers additionally have access to choice continuations, that give the possible future losses. In this way programmers can write operations implementing optimisation algorithms that are aware of the losses arising from their possible choices. We give an operational semantics for a higher-order model language $λC$, and establish desirable properties including progress, type soundness, and termination for a subset with a mild hierarchical constraint on allowable operation types. We give this subset a selection monad denotational semantics, and prove soundness and adequacy results. We also present a Haskell implementation and give a variety of programming examples.