Paper: Polymorphism is conservative over simple types (Preliminary Report) (at LICS 1987)

Authors: Val Breazu-Tannen Albert R. Meyer

Abstract

We prove that the addition of the Girad-Reynolds polymorphic constructs to arbitrary simply typed equational lambda theories is conservative. This implies that polymorphism can be superimposed on familiar programming languages without changing their behavior.
Using a purely syntactic method , we give an effective proof of conservative extension in the case of equational reasoning that is complete when all types are assumed non-empty. When polymorphic types may be empty, we prove the stronger result that any model of the simply typed lambda calculus can be fully and faithfully embedded in a model of the polymorphic calculus.

BibTeX

  @InProceedings{BreazuTannenMeyer-Polymorphismisconse,
    author = 	 {Val Breazu-Tannen and Albert R. Meyer},
    title = 	 {Polymorphism is conservative over simple types (Preliminary Report)},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {7--17},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }