## Paper: Non trivial power types can't be subtypes of polymorphic types (at LICS 1989)

**Andrew M. Pitts**

### Abstract

A new, limitative relation between the polymorphic lambda calculus and the kind of higher-order type theory embodied in the logic of topoi is established. 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 power types σ→Θ of the topos, in the sense that σ→Θ is a subtype of a polymorphic type only in the case that σ is empty (and hence σ→Θ is terminal). As corollaries, strengthening of the Reynolds result on the nonexistence of set-theoretic models of polymorphism are obtained

### BibTeX

@InProceedings{Pitts-Nontrivialpowertype, author = {Andrew M. Pitts}, title = {Non trivial power types can't be subtypes of polymorphic types}, booktitle = {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)}, year = {1989}, month = {June}, pages = {6--13}, location = {Pacific Grove, CA, USA}, publisher = {IEEE Computer Society Press} }