Three approaches to type structure

Abstract

We examine three disparate views of the type structure of programming languages: Milner's type deduction system and polymorphic let construct, the theory of subtypes and generic operators, and the polymorphic or second-order typed lambda calculus. These approaches are illustrated with a functional language including product, sum and list constructors. The syntactic behavior of types is formalized with type inference rules, but their semantics is treated intuitively.