Inmathematical logic, theintersection type discipline is a branch oftype theory encompassingtype systems that use theintersection type constructor${\displaystyle (\cap )}$ to assign multiple types to a single term.^[1]In particular, if a term${\displaystyle M}$ can be assignedboth the type${\displaystyle {\phi }_1}$ and the type${\displaystyle {\phi }_2}$, then${\displaystyle M}$ can be assigned theintersection type${\displaystyle {\phi }_1\cap {\phi }_2}$ (and vice versa).Therefore, the intersection type constructor can be used to express finite heterogeneousad hoc polymorphism (as opposed toparametric polymorphism).For example, theλ-term${\displaystyle \lambda x.(xx)}$ can be assigned the type${\displaystyle ((\alpha \to \beta )\cap \alpha )\to \beta }$ in most intersection type systems, assuming for the term variable${\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,^[2] the Barendregt-Coppo–Dezani type assignment system,^[3] and the essential intersection type assignment system.^[4]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^[5] and Scala,^[6] intersection types are used to expressad hoc polymorphism.

The intersection type discipline was pioneered by Mario Coppo,Mariangiola Dezani-Ciancaglini, Patrick Sallé, and Garrel Pottinger.^[2][7][8]The underlying motivation was to study semantic properties (such asnormalization) of theλ-calculus by means oftype theory.^[9]While the initial work by Coppo and Dezani established a type theoretic characterization of strong normalization for the λI-calculus,^[2] Pottinger extended this characterization to the λK-calculus.^[7]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.^[8]Using the universal type${\displaystyle \omega }$ allowed for a fine-grained analysis of head normalization, normalization, and strong normalization.^[10]In collaboration withHenk 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 isundecidable. However restricting intersection types to finite rank makes their typeability decidable for any finite rank, which is in contrast withsystem F, where (quatifier) restrictions to finite ranks above 3 still have undecidable typeability.^[11] On the other hand, ifrecursive types are added to a system with rank-2 or higher intersection types, typability becomes undecidable, in general.^[12]

Complementarily,undecidability of the dual problem oftype inhabitation in prominent intersection type systems was proven by Paweł Urzyczyn.^[13]Later, this result was refined showingexponential space completeness of rank 2 intersection type inhabitation andundecidability of rank 3 intersection type inhabitation.^[14]Remarkably,principal type inhabitation is decidable inpolynomial time.^[15]

To deal with the difficulties in applying theCurry-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 thelambda 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.^[16]

TheCoppo–Dezani type assignment system${\displaystyle ({⊢}_{\text{CD}})}$ extends thesimply typed λ-calculus by allowing multiple types to be assumed for a term variable.^[2]

The term language of${\displaystyle ({⊢}_{\text{CD}})}$ is given byλ-terms (or,lambda expressions):

The type language of${\displaystyle ({⊢}_{\text{CD}})}$ is inductively defined by the following grammar:

The intersection type constructor (${\displaystyle \cap }$) is taken modulo associativity, commutativity andidempotence.

Thetyping rules${\displaystyle (\to \text{I})}$,${\displaystyle (\to \text{E})}$,${\displaystyle (\cap \text{I})}$, and${\displaystyle (\cap \text{E})}$ of${\displaystyle ({⊢}_{\text{CD}})}$ are:

Typability and normalization are closely related in${\displaystyle ({⊢}_{\text{CD}})}$ by the following properties:^[2]

• Subject reduction: If${\displaystyle \mathrm{\Gamma }{⊢}_{\text{CD}}M:\sigma }$ and${\displaystyle M{\to }_{\beta }N}$, then${\displaystyle \mathrm{\Gamma }{⊢}_{\text{CD}}N:\sigma }$.
• Normalization: If${\displaystyle \mathrm{\Gamma }{⊢}_{\text{CD}}M:\sigma }$, then${\displaystyle M}$ has aβ-normal form.
• Typability ofstrongly normalizing λ-terms: If${\displaystyle M}$ isstrongly normalizing, then${\displaystyle \mathrm{\Gamma }{⊢}_{\text{CD}}M:\sigma }$ for some${\displaystyle \mathrm{\Gamma }}$ and${\displaystyle \sigma }$.
• Characterization of λI-normalization:${\displaystyle M}$ has a normal form in the λI-calculus, if and only if${\displaystyle \mathrm{\Gamma }{⊢}_{\text{CD}}M:\sigma }$ for some${\displaystyle \mathrm{\Gamma }}$ and${\displaystyle \sigma }$.

If the type language is extended to contain the empty intersection, i.e.${\displaystyle \sigma ={\phi }_1\cap \cdots \cap {\phi }_n\text{ where }n=0}$, then${\displaystyle ({⊢}_{\text{CD}})}$ is closed under β-equality and is sound and complete for inference semantics.^[17]

TheBarendregt–Coppo–Dezani type assignment system${\displaystyle ({⊢}_{\text{BCD}})}$ extends the Coppo–Dezani type assignment system in the following three aspects:^[3]

• ${\displaystyle ({⊢}_{\text{BCD}})}$ introduces theuniversal type constant${\displaystyle \omega }$ (akin to the empty intersection) that can be assigned to any λ-term.
• ${\displaystyle ({⊢}_{\text{BCD}})}$ allows the intersection type constructor${\displaystyle (\cap )}$ to appear on the right-hand side of the arrow type constructor${\displaystyle (\to )}$.
• ${\displaystyle ({⊢}_{\text{BCD}})}$ introduces theintersection type subtyping${\displaystyle (\le )}$ partial order on types together with a corresponding typing rule.

The term language of${\displaystyle ({⊢}_{\text{BCD}})}$ is given byλ-terms (or,lambda expressions):

The type language of${\displaystyle ({⊢}_{\text{BCD}})}$ is inductively defined by the following grammar:

Intersection typesubtyping${\displaystyle (\le )}$ is defined as the smallestpreorder (reflexive andtransitive relation) over intersection types satisfying the following properties:

Intersection type subtyping is decidable in quadratic time.^[18]

Thetyping rules${\displaystyle (\to \text{I})}$,${\displaystyle (\to \text{E})}$,${\displaystyle (\cap \text{I})}$,${\displaystyle (\le )}$,${\displaystyle (\text{A})}$, and${\displaystyle (\omega )}$ of${\displaystyle ({⊢}_{\text{BCD}})}$ are:

• Semantics:${\displaystyle ({⊢}_{\text{BCD}})}$ 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.^[3]
• Subject reduction: If${\displaystyle \mathrm{\Gamma }{⊢}_{\text{BCD}}M:\sigma }$ and${\displaystyle M{\to }_{\beta }N}$, then${\displaystyle \mathrm{\Gamma }{⊢}_{\text{BCD}}N:\sigma }$.^[3]
• Subject expansion: If${\displaystyle \mathrm{\Gamma }{⊢}_{\text{BCD}}N:\sigma }$ and${\displaystyle M{\to }_{\beta }N}$, then${\displaystyle \mathrm{\Gamma }{⊢}_{\text{BCD}}M:\sigma }$.^[3]
• Characterization ofstrong normalization:${\displaystyle M}$ is strongly normalizing wrt. β-reduction, if and only if${\displaystyle \mathrm{\Gamma }{⊢}_{\text{BCD}}M:\sigma }$ is derivable without rule${\displaystyle (\omega )}$ for some${\displaystyle \mathrm{\Gamma }}$ and${\displaystyle \sigma }$.^[19]
• Principal pairs (also known as "principal typings"^[20]): If${\displaystyle M}$ is strongly normalizing, then there exists a principal pair${\displaystyle (\mathrm{\Gamma },\sigma )}$ such that for any typing${\displaystyle {\mathrm{\Gamma }}^{\prime }{⊢}_{\text{BCD}}M:{\sigma }^{\prime }}$ the pair${\displaystyle ({\mathrm{\Gamma }}^{\prime },{\sigma }^{\prime })}$ can be obtained from the principal pair${\displaystyle (\mathrm{\Gamma },\sigma )}$ by means of type expansions, liftings, and substitutions.^[21]

• Type theory
• Type systems
• Lambda calculus
• Theory of computation
• Polymorphism (computer science)

• Articles with short description
• Short description matches Wikidata