In mathematical logic, the intersection type discipline is a branch of type theory encompassing type systems that use the intersection type constructor to assign multiple types to a single term. In particular, if a term can be assigned both the type and the type, then can be assigned the intersection type . Therefore, the intersection type constructor can be used to express finite heterogeneous ad hoc polymorphism. For example, the λ-term can be assigned the type in most intersection type systems, assuming for the term variable both the function type and the corresponding argument type. Prominent intersection type systems include the Coppo–Dezani type assignment system, the Barendregt-Coppo–Dezani type assignment system, and the essential intersection type assignment system. Most strikingly, intersection type systems are closely related to normalization properties of λ-terms under β-reduction. In programming languages, such as TypeScript and Scala, intersection types are used to express ad hoc polymorphism.
History
The intersection type discipline was pioneered by Mario Coppo, Mariangiola Dezani-Ciancaglini, Patrick Sallé, and Garrel Pottinger. The underlying motivation was to study semantic properties of the λ-calculus by means of type theory. While the initial work by Coppo and Dezani established a type theoretic characterization of strong normalization for the λI-calculus, Pottinger extended this characterization to the λK-calculus. In addition, Sallé contributed the notion of the universal type that can be assigned to any λ-term, thereby corresponding to the empty intersection. Using the universal type allowed for a fine-grained analysis of head normalization, normalization, and strong normalization. In collaboration with Henk Barendregt, a filter λ-model for an intersection type system was given, tying intersection types ever more closely to λ-calculus semantics. Due to the correspondence with normalization, typability in prominent intersection type systems is undecidable. Complementarily, undecidability of the dual problem of type inhabitation in prominent intersection type systems was proven by Paweł Urzyczyn. Later, this result was refined showing exponential space completeness of rank 2 intersection type inhabitation and undecidability of rank 3 intersection type inhabitation. Remarkably, principal type inhabitation is decidable in polynomial time.
Coppo–Dezani type assignment system
The Coppo–Dezani type assignment systemextends the simply typed λ-calculus by allowing multiple types to be assumed for a term variable.
Term language
The term language of is given by λ-terms :
Type language
The type language of is inductively defined by the following grammar: The intersection type constructor is taken modulo associativity, commutativity and idempotence.
Type rules
The type rules,,, and of are:
Properties
Typability and normalization are closely related in by the following properties:
Subject reduction: If and, then.
Normalization: If, then has a β-normal form.
Typability of strongly normalizing λ-terms: If is strongly normalizing, then for some and.
If the type language is extended to contain the empty intersection, i.e., then is closed under β-equality and is sound and complete for inference semantics.
Barendregt–Coppo–Dezani type assignment system
The Barendregt–Coppo–Dezani type assignment system extends the Coppo–Dezani type assignment system in the following three aspects:
introduces the universal type constant that can be assigned to any λ-term.
allows the intersection type constructor to appear on the right-hand side of the arrow type constructor.
introduces the intersection type subtypingpartial order on types together with a corresponding typing rule.
Term language
The term language of is given by λ-terms :
Type language
The type language of is inductively defined by the following grammar:
Intersection type subtyping is defined as the smallest preorder over intersection types satisfying the following properties: Intersection type subtyping is decidable in quadratic time.
Type rules
The type rules,,,,, and of are:
Properties
Semantics: is sound and complete wrt. a filter λ-model, in which the interpretation of a λ-term coincides with the set of types that can be assigned to it.
Subject reduction: If and, then.
Subject expansion: If and, then.
Characterization of strong normalization: is strongly normalizing wrt. β-reduction, if and only if is derivable without rule for some and.
Principal pairs: If is strongly normalizing, then there exists a principal pair such that for any typing the pair can be obtained from the principal pair by means of type expansions, liftings, and substitutions.
