Open games with stateful payoffs

I’m starting to worry that my open games implementation is getting ahead of what I’ve written in papers in a few ways, and I should correct that with documentation blog posts. This one is about the module OpenGames.Engine.StatefulPayoffs, which is a pragmatic solution to a fundamental conceptual problem with open games: the identity of agents is not well-defined. Rather the fundamental unit is a decision, and if two decisions are made by the same agent then it is the user’s responsibility to make sure that those decisions have the same payoff, or at least game-theoretically “coherent” payoffs.

For a long time I thought this was a conceptual problem but not a practical one. But recent work with my collaborators Philipp Zahn, Seth Frey and Joshua Tan has stress-tested open games in new ways and revealed it to a problem after all. Specifically, if one agent makes 2 decisions on different sides of an abstraction boundary, then the programmer must explicitly design the boundary to accommodate that agent’s payoff. This feels like an abstraction leak.

Continue reading “Open games with stateful payoffs”

Symmetric polymorphic lenses (maybe)

Whereas ordinary directed lenses go from a source to a view, symmetric lenses relate two different views of an internal source. I’ve been thinking about how to smoosh together symmetric lenses with polymorphic lenses, which are the sort used in functional programming. My actual goal is to invent “symmetric open games” (without relying on non-well-founded recursion like I did in this paper). But with the right definition, I think symmetric polymorphic lenses could be a useful tool to programmers as well.

Normally when I’m playing with an idea like this I mock it up in Haskell and play around with it to check it works, before committing to too much hard work on the proofs. But this would be very difficult (and maybe impossible) to write in Haskell, so the idea of this post is to give enough detail that some folks could try it in Agda or Idris, and give me feedback on whether it feels like something useful. (In the meantime, I will try an extremely fast and loose Haskell version by pretending that pullbacks and pushouts are products and coproducts, and see what happens.)

Continue reading “Symmetric polymorphic lenses (maybe)”

Lenses for philosophers

Lens tutorials are the new monad tutorials, I hear. (This is neat, since monads and lenses were both discovered in the year 1958.) The thing is, after independently rediscovering lenses and working on them for a year and a half before Jeremy Gibbons made the connection, I have a very different perspective on them. This post is based on a talk I gave at the 7th international workshop on bidirectional transformations in Nice. My aim is to move fast and break things, where the things in question are your preconceptions about what lenses are and what they can be used for. Much of this will be a history of lenses, which includes at least 9 independent rediscoveries.

Continue reading “Lenses for philosophers”

Abusing the continuation monad

(Recall that monads are not a good topic for your first blog post.)

I intend to bootstrap a blog by writing about 2 of my old papers, Monad Transformers for Backtracking Search and The Selection Monad as a CPS Transformation. (Wall Street will be spared for the time being.)

I’m going to write about this little bit of Haskell code:

import Control.Monad.Cont
sat n = runCont $ sequence $ replicate n $ cont $ \k -> k $ k True

It’s a SAT solver: you give it a boolean function, and the number of variables to search, and it decides whether that function will ever return true for any values of those variables.

How does this work? Haven’t the foggiest. If anyone can explain what it does at runtime, there’s probably a research paper in it for you. If you can also predict how long it takes, that’s a big deal.

Continue reading “Abusing the continuation monad”