A game semantics for generic polymorphism (Q1772770)

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.