Paper: Functional parametricity (at LICS 1992)

Authors: Peter J. Freyd Edmund P. Robinson Giuseppe Rosolini

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 = 	 {Peter J. Freyd and Edmund P. Robinson and Giuseppe Rosolini},
    title = 	 {Functional parametricity},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {444--452},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }