A game semantics for generic polymorphism

From MaRDI portal


DOI10.1016/J.APAL.2004.10.002MaRDI QIDQ1772770zbMATH OpenOpenAlexWikidataFDO

Authors Samson Abramsky, Radha Jagadeesan

Publication date 21 April 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1312.1120


zbMATH Keywords

game semanticsSystem Fsecond-order \(\lambda\)-calculuscategorical model of program polymorphismgeneric polymorphism

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Categorical logic, topoi (03G30) Semantics in the theory of computing (68Q55)


Abstract: 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 forallX.,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 simple and natural notion of generic strategy. -- A "relative polymorphic product" which expresses quantification over the type variable X in the variable type A with respect to a "universe'" which is explicitly given as an additional parameter B. We then solve a recursive equation involving this relative product to obtain a universe in a suitably "absolute" sense. Full Completeness for ML types (universal closures of quantifier-free types) is proved for this model.


Recommendations


Cites work


Cited in
(9)


Describes a project that uses

Uses Software





This page was built for publication: A game semantics for generic polymorphism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1772770)

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=A_game_semantics_for_generic_polymorphism&oldid=68920407"
Powered by MediaWiki