2 RESULTS ON SET-THEORETIC POLYMORPHISM

Moggi and Hyland showed how to model various polymorphic lambda-calculi inside the effective topos and other realizability toposes; types are modelled by the so-called modest sets, which form an internal category Mod in the topos that is, in a certain sense, complete. Polymorphic types are modelled as products indexed by the object of modest sets. The same idea lets us model polymorphism in reflective subcategories of the category of modest sets-for example, the categories of synthetic domains studied by various authors. This paper presents two alternative interpretations of polymorphic types. The first is the groupoid interpretation. Unlike the Moggi-Hyland interpretation, it is stable under equivalence; but it is also very easy to define, and makes sense for any small 'complete' category in a topos. The second is the uniformized interpretation applicable to reflective subcategories of Mod. It clarifies the way in which they can be regarded as PER models, and has applications to the interpretation of subtyping and bounded quantification.