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 = 	 {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}
}