Since late 2023 I have been regularly posting on the CyberCat Institute blog at https://cybercat.institute/
Blog
The cursed families fibration
This post is describing a simple construction I worked out while trying to understand the semantics of quantitative type theory. It is a variant of the families fibration, a well known construction in category theory, which is sensitive to the way that sets are made out of elements, and allows fibres to overlap. Hence it is “cursed”, which is like evil but more.
Let’s begin by recalling how the families fibration works. For any category 
There is a functor 
Monadic lenses are the optic for right monad modules III
This post picks up where the exposition in the first installment left off, before the sideline development in the second installment. I never intended to make a blog post in sonata form, but there we are. Code for this post can be found here.
If we’d like both our forwards and backwards passes to live in our monad then this is the simplest case that there is no possible concrete description, without using any quantification. If we naively put the monad on both the forwards and backwards passes, so we have 
The solution, which is the main topic of Mitchell Riley’s important paper, is to use coend optics in the kleisli category. Using this to repair my thesis eventually led to the paper Bayesian Open Games, which went on to be by far the most useful version of open games in practice. The motivation behind this post is to use my “less pointless lenses” trick with the “diegetic” variant of Bayesian open games in order to get a domain specific language written directly in native Haskell rather than compiled via templates, which would have several practical advantages. This is one of several steps needed to get to that point.
Continue reading “Monadic lenses are the optic for right monad modules III”Monadic lenses are the optic for right monad modules II
This was originally intended to be a 2-part blog post, but a sideline into the interaction of monad modules and distributive laws turned into something of blog length, making this part 2 of 3. But it should be possible to read it independently of the previous installment.
Previously we saw that monadic lenses (where the forwards part is pure, but the backwards part lives in a monad) can be defined in van Laarhoven style by quantifying over all functors which are right modules of the monad, that is, they have a natural transformation 
If we want to also have the monad on the forwards pass then the concrete get/put definition of lenses is no longer possible, and the fundamental definition is kleisli optics, which involve an existential type. Their van Laarhoven encoding, which will be the topic of part 3, is functors which are both a right module and also which the monad distributes over. The topic of this post is exploring what this means and how these two structures interact. This is a currently half-baked theory of “distributive bimodules”.
Continue reading “Monadic lenses are the optic for right monad modules II”Monadic lenses are the optic for right monad modules I
I figured out encoding of 2 more lens-like constructions in the “van Laarhoven” (functor quantification) style used by Haskell’s Control.Lens. The first is monadic lenses, which allow your backwards pass to have side effects from a monad, and the second is the far more subtle monadic optics, which allow effects on both the forwards and backwards passes. I was originally surprised to find neither of these in the monolith-with-included-batteries that is Control.Lens. To summarise my findings:
- Monadic lenses are the optic for right modules of the monad
- Monadic optics are the optic for right modules of the monad that additionally the monad distributes over
Source code for this post can be found here. As usual I didn’t prove correctness of either of these, they’re only conjectures that seem to check out in code. In this post I’ll cover the first one, and then part II will be about the second, which is a lot more complicated. Let’s dive in.
Continue reading “Monadic lenses are the optic for right monad modules I”Geometry of interaction is the optic for copointed functors
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”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”
Jules Hedges 