Technical reports

# Non-trivial power types can’t be subtypes of polymorphic types

**Andrew M. Pitts**

January 1989, 12 pages

## Abstract

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 σ→Ω of the topos, in the sense that σ→Ω is a subtype of a polymorphic type only in the case that σ isempty (and hence σ→Ω is terminal). As corollaries we obtain strengthenings of Reynold’s result on the non-existence of set-theoretic models of polymorphism.

## Full text

PS (0.1 MB)

## BibTeX record

@TechReport{UCAM-CL-TR-159, author = {Pitts, Andrew M.}, title = {{Non-trivial power types can't be subtypes of polymorphic types}}, year = 1989, month = jan, url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-159.ps.gz}, institution = {University of Cambridge, Computer Laboratory}, number = {UCAM-CL-TR-159} }