Intersection type discipline

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.^[1] In particular, if a term ${\displaystyle M}$ can be assigned both the type ${\displaystyle \varphi _{1}}$ and the type ${\displaystyle \varphi _{2}}$, then ${\displaystyle M}$ can be assigned the intersection type ${\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 ${\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 ${\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 express ad hoc polymorphism.