A game semantics for generic polymorphism

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

categorical model of program polymorphism game semantics generic polymorphism second-order \(\lambda\)-calculus System F

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

f o r a l l 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 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.

Review text

In this paper, a categorical model of program polymorphism, based on game semantics, is constructed. The construction uses the idea of genericity, that is the idea that the same program can work at many different data types. The categorical model contains a large collection of generic types which provide a clear meaning of type independence especially for the case of programs containing higher-order types. In Section 2, the System F is recalled, see also [\textit{J.-Y. Girard, P. Taylor} and \textit{Y. Lafont}, Proofs and types. Cambridge: Cambridge Univ. Press (1989; Zbl 0671.68002)]. Section 3 introduces a direct interpretation of variable types as games with a natural notion of substitution of games. This interpretation allows moves in games \(A[T]\) to be decomposed into the generic part from \(A\) and the part pertaining to the instance \(T\). In Section 4, two orderings on games are defined. Also, a relative polymorphic product \(\Pi_i(A,B)\) is specified for the purpose of expressing quantification over the type variable \(X_i\) in the variable type \(A\) with respect to a universe which is explicitly given as an additional parameter. Finally, in Section 4, a domain equation for variable games of System F is presented. Section 5 deals with generic strategies and defines a cartesian closed category of games as constructed by taking partial equivalence classes of strategies. In Section 6, the categorical model is built. For this purpose, the authors employ hyperdoctrines, cf. [\textit{R. L. Crole}, Categories for types, Cambridge: Cambridge Univ. Press (1993; Zbl 0837.68077)]. In Section 7, a notion of homomorphism between games is defined. Section 8 contains examples of generic types in the model. In Section 9, the authors prove full completeness for ML types, that is universal closures of quantifier-free types. In the proof, the decomposition of intuitionistic implication into linear logic connectives is performed, and the domain equation is carried over to variable games of second-order types.

Recommendations

Cites work

Cited in

(9)

Describes a project that uses

Uses Software

Esterel

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)