Polymorphic types and parametric limits
In giving a set-theoretic semantics to the polymorphic lambda calculus, John Reynolds has noted that a polymorphic type such as FORALL X. F(X) does not represent arbitrary families of elements of sets F(X), but rather only the parametric families that behave in a uniform way for all X. In his characterization, parametric families have components that preserve all possible relations between sets chosen for X. On the surface, one finds that the notion of limits in category theory is very similar to this, where LIM X. F(X) consists of families that preserve all possible morphisms between objects chosen for X.
In this talk, we make this connection concrete by characterizing polymorphic types as form of limits (called parametric limits) in a suitable setting of categories. This enables us to generalize Reynolds's semantics to categorical level so that the ideas of polymorphism and parametricity can be interpreted in arbitrary categories with the requisite structure. We axiomatize the requisite structure so that representation results concerning polymorphic types for initial algebras and final coalgebras follow from the axioms.
This talk represents joint work with Brian Dunphy.