Quartz 4

Using the selection monad

2 min read

Abstract

In 2010, Martin and Paulo Oliva invented the selection monad
S(X) = (X → R) → R. Then, in 2017, they showed how to combine the selection monad with an auxiliary monad T to obtain the extended selection monad
S_T(X) = (X → R) → T(R), with R a T-algebra. These monads have applications to game theory, search algorithms, and proof theory.

Martin Abadi suggested a natural optimization interpretation of the selection monad: a selection function i.e., an element of S(X) chooses an element of X, given a loss (or profit) function γ : X → R that gives the loss (or profit) associated with a particular choice. Argmax provides a natural example of such a selection function: it makes optimal choices.

We illustrated this idea via a programming language for making optimal choices combined with probabilistic ones. Its denotational semantics uses the selection monad combined with an auxiliary monad for probability and nondeterminism. It has an operational semantics involving games against nature. And there are adequacy and (limited) full abstraction theorems for expectedly optimal selection functions.

However, in practice, one cannot, of course, make optimal choices, and programmers must employ learning algorithms such as reinforcement learning or gradient descent. I hint at a selection monad approach to this problem. It combines the selection monad with (a monad for) algebraic effects to obtain algebraic effects with choice continuations (work with Ningning Xie).

Talk Details

Speaker: Gordon Plotkin (Google Deepmind)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Wednesday 17 December 2025
Time: 16:15 (remote)
Slides: Available

Key Topics

  • Selection monad
  • Extended selection monad
  • Game theory
  • Search algorithms
  • Optimization
  • Reinforcement learning
  • Gradient descent
  • Algebraic effects
  • Denotational semantics
  • Probability and nondeterminism

Collaborators

  • Ningning Xie

Graph View

Backlinks