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

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