Game Semantics for a Polymorphic Programming Language

This article presents a game semantics for higher-rank polymorphism, leading to a new model of the calculus System F, and a programming language which extends it with mutable variables. In contrast to previous game models of polymorphism, it is quite concrete, extending existing categories of games by a simple development of the notion of question/answer labelling and the associated bracketing condition to represent "copycat links" between positive and negative occurrences of type variables. Some well-known System F encodings of type constructors correspond in our model to simple constructions on games, such as the lifted sum. We characterize the generic types of our model (those for which instantiation reflects denotational equivalence), and show how to construct an interpretation in which all types are generic. We show how mutable variables (a la Scheme) may be interpreted in our model, allowing the definition of polymorphic objects with local state. By proving definability of finitary elements in this model using a decomposition argument, we establish a full abstraction result.