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: category theory
Selection functions and lenses
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.
Continue reading “Selection functions and lenses”Towards dependent optics
There are two different generalises of lenses that are important in my research. One is optics, which are a non-obvious generalisation of lenses that work over a monoidal category (whereas lenses only work over a finite product category). We use optics in Bayesian open games, over the category of Markov kernels (kleisli category of probability). The other is dependent lenses, also known as containers and equivalent to polynomial functors. These haven’t appeared in a game theory paper yet, but I use them privately to handle external choice of games better than lenses do.
An interesting and probably-hard question is to find a common generalisation of optics and dependent lenses. In this post I’ll outline the problem and explain a (probable) partial solution that might be useful for somebody, but doesn’t appear useful in game theory. This post will be heavy on category theory: I assume knowledge of fibred categories and the Grothendieck construction.
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”Lax functors describe emergent effects
In this post I’ll describe something that’s kind of common knowledge among applied category theorists, that when you describe behaviour via a (pseudo)functor to the category of relations, emergent effects are described by the failure of that functor to be strong, ie. to be an actual functor. This is more or less in Seven Sketches (Fong and Spivak say “generative effects”, which as far as I can tell is an exact synonym for emergent effects), but I’ll write it in one place and in my own words.
Suppose we have a domain-specific category 
Categorical cybernetics: A manifesto
(Image credit: H.R. Grant / SaurianDandy)
I suddenly became obsessed with cybernetics (exactly) 2 weeks ago when I learned what the word actually means, closely followed by this tweet bring my attention to the following line from the beginning of Kenneth Boulding’s classic (1956) paper General Systems Theory: “The developments of a mathematics of quality and structure is already on the way, even though it is not as far advanced as the “classical” mathematics of quantity and number.” Which sounds like category theory to me. (I think it’s extremely unlikely Boulding had category theory in mind – Eilenberg and Mac Lane’s General Theory of Natural Equivalences was published in 1945; for comparison the first textbook on graph theory was published in 1936.)
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.)
Folklore: Monoidal kleisli categories
I’ve been threatening a few times recently to blog about bits of mathematical folklore that I use, i.e. important things that aren’t easy to find in the literature. I’m going to start with an easy one that won’t take me long to write.
Theorem: Given a commutative strong monad on a symmetric monoidal category, the kleisli category is symmetric monoidal in a canonical way.
Jules Hedges 