Technical reports
Non-trivial power types can’t be subtypes of polymorphic types
January 1989, 12 pages
DOI: 10.48456/tr-159
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-159.ps.gz}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-159}, number = {UCAM-CL-TR-159} }