Extensions to type systems can preserve operational equivalences

Abstract

We consider call-by-name, call-by-value, and lazy versions of PCF, and prove, using both syntactic and semantic means, that the operational equivalences of the base language are preserved when the language is extended with sum and product types, with polymorphic types, and with recursive types. These theorems show that the type systems of the extended languages are orthogonal to the type systems of the original languages.