Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

A Game Semantics for Generic Polymorphism

Samson AbramskyContact Information and Radha JagadeesanContact Information

(5)  Oxford University Computing Laboratory, Oxford
(6)  DePaul University, Chicago
Abstract
Genericity is the idea that the same program can work at many different data types.Longo,Milsted 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 simple and natural notion of generic strategy. - A “relative polymorphic product”π i (A,B)which expresses 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 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)can be proved for this model.
Samson Abramsky was supported in part by UK EPSRC.
Radha Jagadeesan was supported in part by NSF CCR-020244901.

Contact Information Samson Abramsky
Email: samson@comlab.ox.ac.uk

Contact Information Radha Jagadeesan
Email: rjagadeesan@cs.depaul.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.108 • Server: mpweb17
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)