Geometry of Interaction (also known as the Int-construction) is an important construction in category theory that shows up the semantics of concurrency. It’s also a contender for my favourite thing in category theory. It’s one member of a whole zoo of things that look kinda like lenses but are a bit different. Back around 2017 when I was writing The game semantics of game theory I asked myself whether Int was an optic, and concluded it probably wasn’t, but recently I was thinking about the question with my PhD student Riu Rodríguez Sakamoto and we realised that it actually is. In this post I’ll sketch the construction in the terms of Haskell’s Lens library. None of the proofs are done yet, and all of this ought to work in a general categorical setting, but what I wrote here demonstrably works by testing. The source code can be found here.Continue reading “Geometry of interaction is the optic for copointed functors”
Fair warning: this post assumes some familiarity with Haskell’s
Control.Lens library. Source code for this post can be found here.
Recently I’ve been working on a major rewrite of the open game engine, based on some newer theoretical ideas such as this paper. A major objective is to no longer require a custom DSL, removing the dependency on Template Haskell and especially the need to maintain a parser. For reasons that are brutally obvious to anyone who’s ever programmed with open games, it’s a hard requirement to have a syntax based on name-binding: working with point-free combinators is not humanly possible at this scale. This post is a spin-off from that work, explaining how to use Haskell’s Lens library in a name-binding rather than point-free style.
The key idea is that if you have a lens of type
Lens s t a b, and you want to treat it as though it’s a function, then the corresponding notion of “value” is something of type
(s, t -> r). That is, it’s an input for the lens’ getter, together with a continuation from the output of the setter. Given a lens and such a value-continuation pair, you can get an “output value” of type
(a, b -> r).
In this post I’ll explain something folkloric: that you can pretend that the continuation monad is a probability monad, and do probabilistic programming in it. Unlike more obvious representations of probability like the one in Numeric.Probability.Distribution via lists, this way works equally well for continuous as for discrete distributions (as long as you don’t mind numerical integration). The post is a literate Haskell program, which is an expanded version of this repository. It’s a sort of sequel to my very first blog post, Abusing the continuation monad.
I mentally call this idea “synthetic measure theory” or sometimes “synthetic probability”, although as far as I know it is not related to various Google hits for those terms such as this, or this. (But one of the hits is this paper, which is probably related.)Continue reading “Probabilistic programming with continuations”
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”
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.)
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.
(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.