In mathematical logic, the intersection type discipline is a branch of type theory encompassing type systems that use the intersection type constructor ( ∩ ) {\displaystyle (\cap )} to assign multiple types to a single term. In particular, if a term M {\displaystyle M} can be assigned both the type φ 1 {\displaystyle \varphi _{1}} and the type φ 2 {\displaystyle \varphi _{2}} , then M {\displaystyle M} can be assigned the intersection type φ 1 ∩ φ 2 {\displaystyle \varphi _{1}\cap \varphi _{2}} (and vice versa). Therefore, the intersection type constructor can be used to express finite heterogeneous ad hoc polymorphism (as opposed to parametric polymorphism). For example, the λ-term λ x . ( x x ) {\displaystyle \lambda x.\!(x\;x)} can be assigned the type ( ( α → β ) ∩ α ) → β {\displaystyle ((\alpha \to \beta )\cap \alpha )\to \beta } in most intersection type systems, assuming for the term variable x {\displaystyle x} both the function type α → β {\displaystyle \alpha \to \beta } and the corresponding argument type α {\displaystyle \alpha } . 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 (and often exactly characterize) 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 (such as normalization) 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 ω {\displaystyle \omega } that can be assigned to any λ-term, thereby corresponding to the empty intersection. Using the universal type ω {\displaystyle \omega } 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 infinite intersection type systems is undecidable. However restricting intersection types to finite rank makes their typeability decidable for any finite rank, which is in contrast with system F, where (quantifier) restrictions to finite ranks above 3 still have undecidable typeability. On the other hand, if recursive types are added to a system with rank-2 or higher intersection types, typability becomes undecidable, in general. 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. To deal with the difficulties in applying the Curry-Howard correspondence to intersection types, Kamareddine and Wells have replaced the intersection constructor in the deduction system with finite-set declarations (FSD) for the domain of each variable in a lambda abstraction, turning them into Π types. And they extended the lambda cube to what they call the f-cube, which has with FSD-encoded intersection types at all vertices. Urzyczyn’s term U, which is untypable in the λ-cube, is typable in the f-cube.
Coppo–Dezani type assignment system The Coppo–Dezani type assignment system ( ⊢ CD ) {\displaystyle (\vdash _{\text{CD}})} extends the simply typed λ-calculus by allowing multiple types to be assumed for a term variable.
Term language The term language of ( ⊢ CD ) {\displaystyle (\vdash _{\text{CD}})} is given by λ-terms (or, lambda expressions):
M , N ::= x ∣ ( λ x . M ) ∣ ( M N ) where x ranges over term variables {\displaystyle {\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ where }}x{\text{ ranges over term variables}}\\\end{aligned}}}
… excerpt ends here. Continue reading the full article.
