Ulrich Schöpp, Playing Games with Effects
Playing Games with Effects
(Work in Progress)
Game semantics is traditionally concerned with the interpretation of programming languages and for reasoning about programs by looking at their interpretation. It is also interesting to use ideas from game semantics in the reverse direction: start with a programming language and use it to implement the plays of a game model. The structure that one finds in the game model can then be used to devise a language for meta-programming in the original language. This approach is interesting, since a very simple language is often enough to implement game-like models, which on the other hand often support very rich structure, such as higher-order functions or complicated control flow such as coroutines.
Two recent examples of work that may be considered an instance of this approach are the Geometry of Synthesis of Ghica and the language IntML for sublinear space programming of Dal Lago and Schöpp. In the Geometry of Synthesis one starts with digital circuits described in Verilog and uses them to implement a game model. The game model is then used to interpret a variant of Idealized Algol as a language for meta-programming circuits. In IntML a simple first-order programming language is used as the basis of a game model, in which a typed higher-order functional language is implemented. This functional language can be used to implement plays in the style of AJM-games. It provides type constructors such as tensor, linear functions and (bounded) duplication.
In this talk I will examine how a programming language with effects can be used as the basis for constructing of a game model that supports a type theory like that of IntML. Interesting effects in this context include store -- the Geometry of Synthesis uses stateful circuits -- and nondeterminism. I will argue that a variant of the Enriched Effect Calculus (EEC) of Egger, Mogelberg and Simpson provides a good basis for such a construction. The Enriched Effect Calculus is a type theory close to Levy's Call-by-Push-Value; it simplifies the syntax and adds new types for enriched structure such as copowers. I will consider a variant of EEC without function types, which are not needed, but with sum types and a Conway operator instead. It turns out that the enriched structure captured by EEC provides a particularly good fit for the construction of a game-like model and the interpretation of an IntML-like type theory therein.