Abstract

Game semantics has been used to define denotational models of a wide variety of programming languages with stateful effects, including locally bound integer and general references, dynamically bound procedures,​ coroutines and message-passing between concurrent threads. These are typically given by directly defining the interpretation of key stateful objects (such as reference cells) as “history sensitive” strategies, for which the whole history of play can act as an internal state. Relating these to more explicit representations of state such as the side-effect monad is useful, both for understanding the model itself (for example, showing correspondence with the operational semantics) and beyond game semantics, in giving new principles for constructing and reasoning about objects with local state.

To achieve this, we investigate the underlying structure of game semantics using the sequoid, a novel connective which allows us to construct and deconstruct history sensitive strategies. The sequoid A⊘B represents a game in which play in B has some causal dependency in A: it is interpreted as an action of a monoidal category, together with a map in the category of such actions into the canonical action of the monoidal category on itself. We may observe sequoidal structure in each of the various categories of games which have been used for denotational semantics, and relate it to other key structuring principles such as linear logic and CPS . Each imperative effect may be identified with particular categorical properties of the sequoid, which we can use to define equational theories and canonical representations for elements in the corresponding model.

A key example is that in categories of games and history sensitive strategies, a final coalgebra for the functor A⊘_ has the structure of the cofree commutative comonoid on A (giving an interpretation of the “bang” of linear logic). So in particular, if we have a strategy on S 􏰉 􏰉→ (A ⊘ S), corresponding to an object of type A with explicit input and output states of type S (cf. the side-effect monad) we may “encapsulate” its state as a coalgebra morphism S → !A which shares internal state between its threads, and which comes with a corresponding set of coinductive reasoning principles.​