Logic in Computer Science (LICS 1992)

Paper: Functional parametricity (at LICS 1992)

Authors: Freyd, P.J. Robinson, E.P. Rosolini, G.

Abstract

The authors consider the idea of treating a parametrized type as an arbitrary functor from some parametrizing category to a category of types, and giving elements semantics as natural transformations. They show that under reasonable hypotheses this is only possible when the parametrizing category is a groupoid. This suggests a semantics for a semiparametric form of polymorphism. They discuss the interpretation of this form of parametricity in a PER model, and show that it coincides with the ostensibly stronger form derived from dinaturality

BibTeX

  @InProceedings{FreydRobinsonRosoli-Functionalparametri,
    author = 	 {Freyd, P.J. and Robinson, E.P. and Rosolini, G.},
    title = 	 {Functional parametricity},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {444--452},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }