Relational limits in general polymorphism (Q1346668)

Parametric polymorphism, as opposed to what Stachey called `ad hoc' polymorphism, has been a widely studied issue in type theory during the recent years. This paper achieves a categorical answer to this problem, taking Reynolds' concept of parametricity. The construction starts with a generalization of categories based on relations as morphisms, called \(r\)-frames. They are first used to define polymorphic lambda-calculi, and then to provide models of such calculi. This framework already provides parametric models like the parametric per model. A further investigation involves the use of enriched categories and indexed categories: the author introduces notions of cotensor and end, and is able to establish a Kan theorem. From this come numerous consequences on both the logical and the categorical side. Finally he develops the \(\emptyset\)-order minimum model, which has many nice properties, in particular initial and terminal fixed points.