Logic in Computer Science (LICS 1989)

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