At the seminar a fortnight ago, Sophie asked a question that is much more profound than she probably realised: "What is 'lookup'? I did not answer at the time as it would have been too great a digression, but I promised another talk about it, and this is it.
We have been told for over 30 years that one may model state by use of the "state" or "side-effects" monad, (Sx-)^S for a countable set S, but the situation is more subtle than that, and category theory can help to illuminate some of the structure.
There are natural operations and equations that generate the monad (Sx-)^S, which I shall describe. The operations may be described as lookup:X^S→X and update:X→X^S. However, lookup is of countable arity, whereas programming languages do not have operations of countable arity in general. That concern led Plotto to define a notion of "generic effect", that being equivalent to giving an operation. The underlying category theory of the correspondence is routine, but the computational significance is profound. It amounts to adding a new type to the language to represent an arity, then adding a constant of that type to represent an operation of the corresponding arity. The correspondence makes lookup and update into familiar programming constructs.
Beyond that, in practice, a state is typically a function from a finite set Loc of locations into a countable set Val of values, with lookup meaning looking up a location, and update meaning updating a value. The state monad is predicated upon that, with (Sx-)^S referring to "global" state. However, typically, a program may also add locations using, for example, a block operation. So we studied lookup, update and block, yielding a more subtle monad on a presheaf category, modelling the computationally more natural "local" state. There is an oversight in the paper (my mistake), and more importantly, I do not believe there has been a definitive semantic account of local state yet, but we made substantial progress, which I shall describe.