| Semantic Orthogonality of Type Disciplines (1997) | |||||||||||||||
Abstract | |||||||||||||||
| We consider a version 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 additions to the type systems are orthogonal to the original language. 1 Introduction Type systems for programming languages are rarely monolithic: although a type system may be composed of many parts, each part can usually be understood on its own. Consider, for instance, the programming language Standard ML (SML) [22]. SML's type system includes base types of integers, reals, strings, and characters, and type constructors for lists, functions, tuples, references, exceptions, user-defined recursive datatypes, and polymorphism. On a syntactic level, the type rules of the parts do not interfere with one another: the type-checking rule for application, for example, uses only the fact that the operator is... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||