Programming with intersection types, union types, and polymorphism

Abstract: "Type systems based on intersection types have been studied extensively in recent years, both as tools for the analysis of the pure [lambda]-calculus and, more recently, as the basis for practical programming languages. The dual notion, union types, also appears to have practical interest. For example, by refining types ordinarily considered as atomic, union types allow a restricted form of abstract interpretation to be performed during typechecking. The addition of second-order polymorphic types further increases the power of the type system, allowing interesting variants of many common datatypes to be encoded in the "pure" fragment with no type or term constants.This report summarizes a preliminary investigation of the expressiveness of a programming language combining intersection types, union types, and polymorphism.