I’ve been wondering for several years how selection functions and lenses relate to each other, I felt intuitively that there should be some connection – and not just because they both show up in the foundations of game theory. Last night I came up with an answer, which isn’t a complete answer but looks like the starting point for a complete answer.
A selection function is a function of type . The canonical example is , after choosing a single maximiser for every function (say that is a finite set to avoid worrying about existence of a maximiser). is a strong monad, closely related to the continuation monad, with a highly non-obvious monad structure. Combining argmaxen using the monadic bind makes the backward induction algorithm from game theory fall out of pure category theory – see a string of papers by Martín Escardó and Paulo Oliva, especially Sequential games and optimal strategies for a good introduction.
Meanwhile, the category of lenses has as objects pairs of sets , and its morphisms consist of pairs of functions and . The identity lens on consists of an identity function and a projection, and the composition of and consists of and . Lenses also play a deep role in the foundations of game theory, via open games.
What I noticed is that there is a functor , taking the object to the set of selection functions . Given a selection function and a lens , we can “push forward” the selection function along the lens, to obtain a selection function using the formula . This turns out to be functorial – pushing forward a selection function along the identity lens does nothing, and pushing forward a selection function along two lenses is the same as pushing forward along the composed lens.
The slick way to see this is to notice that there is a natural isomorphism – in other words, a selection function is a way to turn costates into states in the category of lenses. These two representable functors already play a deep role in open games.
I wanted to write a short blog post just to explain this much; how this connects to the monad structure of , and what are the implications for game theory, remain to be seen. To me, this functor feels close to the beating heart of game theory.