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

Authors:**Pitt, A.M.**

### 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{Pitt-Nontrivialpowertype, author = {Pitt, A.M.}, title = {Non trivial power types can't be subtypes of polymorphic types}, booktitle = {Proceedings of the Fourth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1989}, year = 1989, editor = {Rohit Parikh}, month = {June}, pages = {6--13}, location = {Pacific Grove, CA, USA}, publisher = {IEEE Computer Society Press} }