Parametricity as a notion of uniformity in reflexive graphs
Uday S. Reddy, Brian Patrick Dunphy · 2002
Uniformity is an important concept in good computer programming practice. Reflexive graph categories provide an abstract setting where uniformity can be characterized as parametric transformations, that is, collections of morphisms that respect edges. This permits one to give categorical characterizations of uniformity for type constructs that do not form functors, such as function types. We give additional axioms on reflexive graph categories to ensure that parametricity provides a reasonable notion of uniformity. The strength of this notion of uniformity can be exhibited by way of “representation results”. We show that the possible parametric transformations of certain type correspond to the intuitively uniform families of functions of that type. Thus abstract models of polymorphic programming languages are produced. Some programming language features, such as state and recursion, provide modeling complications when combined with polymorphism. We show that representation results are still obtainable for polymorphic programming languages with state or recursion.