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”Blog
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).
PhD position at the University of Strathclyde, Glasgow
Update: This position has now been filled
This is an update to my previous posting, refer to that post for most of the details.
I am reopening applications for one of these positions (the other is filled). This time there will be no deadline, instead I will keep applications open indefinitely, and then edit this post when it’s filled.
Continue reading “PhD position at the University of Strathclyde, Glasgow”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”Free publishing
This post is a manifesto for a very simple idea: the phrase “open access” should be replaced with “free publishing”. I am asking you, the reader, to make this change. The rest of this post will try to explain why.
The fundamental reason is that the phrase “open access” has already been compromised through contact with corporate interests that are not in the interest of science. The fact that extra adjectives such as diamond open access, platinum open access and fair open access are required shows that the words “open access” have lost their useful meaning. The pledge that I am a signatory of, No Free View? No Review!, does not consider gold open access and other hybrid models to count as true open access.
Continue reading “Free publishing”Two PhD positions at the University of Strathclyde, Glasgow
I have two PhD studentships (** huge caveat about funding follows **) in the Mathematically Structured Programming group at Strathclyde
Position 1: Is for a fixed project jointly with the National Physical Laboratory, to do with category-theoretic techniques for Bayesian inference and estimation in complex systems. Some programming experience is preferred for this project.
Position 2: Has no fixed project attached, feel free to propose a research project roughly within my interests of applied category theory + economics, machine learning and optimisation/control, or to discuss with me. (See https://julesh.com/ for details.)
To apply, email a CV plus any another documents to me at jules.hedges@strath.ac.uk . If you’d like to discuss with me then you can email me, or use any other public channel you can find me on (Zulip, Twitter). I’m happy to arrange a Zoom call if you prefer that.
I enthusiastically encourage anyone to apply who considers themselves part of a minority group within academia
Arbitrary application deadline is January 31st 2021. Start date is flexible
The MSP group at Strathclyde is an exciting group to be part of, focussing on type theory, category theory and their applications. Faculty is: Neil Ghani, Conor McBride, Glynn Winskel, Radu Mardare, Clemens Kupke, Ross Duncan, Bob Atkey, Fredrik Norvall Forsberg and me. See http://msp.cis.strath.ac.uk/index.html
(Caveat: The funding situation is extremely complicated and uncertain because of Brexit. For UK citizens these positions are definitely fully-funded. For Europeans the official position is “it’s very complicated” and “we haven’t decided yet”. Here are direct quotes from a recently-circulated email: “Scholarships for PGR [postgraduate researcher = PhD student] EU fee status students are still being considered, with further information expected early in the new year… Determining which EU students will continue to be eligible for home fees, and which will fall into the new EU fee status is very complex, and depends on aspects such as family members, residency, and settled or pre settled status, and we’re waiting on further guidance from the government on some of these elements too. So it’s worth being aware that it’s not as straight forward as that if a student is from the EU they will definitely fall into the new EU fee status from 2021-22. We won’t have a full understanding of how many EU students will come under this new fee category until much closer to the 2021 intake.“
There are no eligibility requirements on the position, but those not eligible for “home fees” will require a secondary source of funding. In some cases it is possible (but not guaranteed) the the university can find extra funding for a strong applicant.
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”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”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”
Jules Hedges 