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.)
Continue reading “Symmetric polymorphic lenses (maybe)”
Recently open games have reached a state where they realistically might start becoming useful to some people (see this demo). I want to write down the current state of the art, what I believe is possible and what I believe are the limitations of compositional methods. This guides which sorts of situations I believe open games will be applicable to.
First I will say what open games can already do (at least in theory). Then I will say what is awkward and what I think is probably possible with future work, and finally when I think you shouldn’t use open games. This post is written for a hypothetical reader who wants to use game theory as a modelling paradigm.
Continue reading “Are open games useful for my problem?”
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.
Continue reading “Folklore: Monoidal kleisli categories”
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.
Continue reading “Lenses for philosophers”
I feel that having Compositional game theory accepted for publication marks the end of the first chapter for me, and marks open games as a proper research topic. I want to record how open games came to be, told through the story of this paper, which took almost 3 years from writing to acceptance. (That’s roughly the same amount of time as the Higher Order Decisions/Games duo, although they definitely felt longer. Their story can wait for another blog post.)
Continue reading “The pre-history of open games”
The rising sea refers to a particular approach to mathematical problem-solving, in which many small, apparently trivial steps are taken until the solution of a problem becomes itself trivial. It was poetically introduced by Alexander Grothendieck in his beautiful, auto-psychoanalytic Récoltes et Samailles, in which he imagines the mathematical problem as a landmass being swallowed as “the sea advances insensibly in silence”. This makes me think of Xerxes, all-powerful over humans, helpless against the power of the sea. Grothendieck views the mathematician and the problem as complimenting each other, the mathematician using the problem’s natural structure in its solution, rather than striking it with a foreign, invasive method.
(Sadly I’ve only read the small part of Récoltes et Samailles that is translated to English, and that is hard to find. The version which I originally read has disappeared from the internet, and I expect this link to become dead too, so now I’ve kept an offline version to be safe.)
Continue reading “The rising sea in applied mathematics”
I gave a talk last year at Duskofest in Oxford (a workshop celebrating the nth birthday of Dusko Pavlovic, where n is sufficiently large), based on my blog post Breaking the rules.
I have finally remembred to upload my slides here.
This is the only time I can remember enjoying creating slides.