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”Category: Haskell
Making Haskell lenses less pointless
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).
Probabilistic programming with continuations
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”Subgame perfection made difficult
This is the second post in catching up on aspects of open-games-hs that are ahead of my papers, following open games with stateful payoffs. Subgame perfection has been an embarrassing thorn in my side since 2016 when I had to do major surgery on my PhD thesis because the category of “open games with subgame perfect equilibria” turned out to not be monoidal. Currently there are two approaches: One in iterated open games which is quite pragmatic and requires the “user” specifying an open game to manually mark where the subgames are by applying a functor; and one in morphisms of open games which I find very elegant but requires both an extra categorical dimension and an equivalent amount of effort by the “user”.
I always wanted an “automatic” approach to subgame perfection in open games, like I failed to do in my thesis – just draw the usual string diagram, and get subgame perfect equilibria out. I now have a way to do it, implemented in OpenGames.Engine.SubgamePerfect, which I’ll document here.
Continue reading “Subgame perfection made difficult”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.
Jules Hedges 