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

Authors: 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}
  }