Where is relational parametricity in hyperdoctrine or topos models explored?

Question

Reynolds originally proposed a relational semantics for the second order polymorphic lambda calculus[1]. However he later showed[2] that this approach was inconsistent with classical set theory. Pitts described the framework of hyperdoctrine models and topos models[3] which are consistent with constructive logic.

Presumably relational hyperdoctrine and topos models were then developed. Where can I read about them?

• [1] Types, abstraction and parametric polymorphism
• [2] Polymorphism is not set-theoretic
• [3] Polymorphism is set theoretic, constructively

Answer 1

• For technical reasons, there hasn't been much work on parametric topos models. The internal logic of a topos is a form of set theory, and F-style impredicative indexing and the powerset axiom are incompatible. See Andy Pitts's Non-trivial Power Types Can't Be Subtypes of Polymorphic Types:

  This paper establishes a new, limitative relation between the polymorphic lambda calculus and the kind of higher-order type theory which is embodied in the logic of toposes. It is shown that any embedding in a topos of the cartesian closed category of (closed) types of a model of the polymorphic lambda calculus must place the polymorphic types well away from the powertypes, P(X), of the topos, in the sense that P(X) is a subtype of a polymorphic type only in the case that X is empty (and hence P(X) is terminal). As corollaries, we obtain strengthenings of Reynolds' result on the non-existence of set-theoretic models of polymorphism.

  As a result, even though you can give a universe interpreting F's types in topos logic, you can't let it interact in interesting ways with the full universe of sets. However, all is not lost!

  1. The fact that a (non-parametric) universe of sets interpreting System F means that you can give a parametric model of System F in the internal logic of the topos, much more easily than you can in ordinary set theory. Essentially, you don't have to muck around with PERs, since you can just assume that you have a suitable collection of sets. Bob Atkey used this idea in his paper Relational Parametricity for Higher Kinds, where he worked out parametricity for $F_\omega$ by working in the impredicative calculus of constructions.

  2. Another reaction to Pitts's result is to not work with a set theory, but a dependent type theory. Since there's no power type former in dependent type theory, you don't have to worry about the interaction of power types and polymorphism. See Atkey, Ghani and Johann's A Relationally Parametric Model of Dependent Type Theory.

• However there are no such obstacles to building hyperdoctrine-ish models, where terms of System F are objects of the logic. Research along these lines was probably initiated by Abadi and Plotkin in their seminal paper A Logic for Parametric Polymorphism. Lars Birkedal and his collaborators have worked heavily on formulating categorical models for this and similar logics --- see in particular Birkedal, Møgelberg, and Petersen's Category-Theoretic Models of Linear Abadi and Plotkin Logic, which gives a logic for reasoning about linear System F, plus a proof that it is sound and complete with respect to a certain class of categorical models.