Computer Laboratory

Technical reports

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

Andrew M. Pitts

January 1989, 12 pages


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

  author =	 {Pitts, Andrew M.},
  title = 	 {{Non-trivial power types can't be subtypes of polymorphic
  year = 	 1989,
  month = 	 jan,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-159}