A Game Semantics for Generic Polymorphism

Genericity is the idea that the same program can work at many different data types. Longo, Milstead and Soloviev proposed to capture the inability of generic programs to probe the structure of their instances by the following equational principle: if two generic programs, viewed as terms of type ∀X. A[X], are equal at any given instance A[T], then they are equal at all instances. They proved that this rule is admissible in a certain extension of System F, but finding a semantically motivated model satisfying this principle remained an open problem. In the present paper, we construct a categorical model of polymorphism, based on game semantics, which contains a large collection of generic types. This model builds on two novel constructions: • A direct interpretation of variable types as games, with a natural notion of substitution of games. This allows moves in games A[T] to be decomposed into the generic part from A, and the part pertaining to the instance T. This leads to a sim...

• Type: Conference
• Year: 2003
• Where: FOSSACS
• Authors: Samson Abramsky, Radha Jagadeesan
• Keywords: Applied Computing, Different Data Types, FOSSACS 2003, Generic Programs, Variable Type