1 Answers
In mathematical logic, the intersection type discipline is a branch of type theory encompassing type systems that use the intersection type constructor {\displaystyle } 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}} .Therefore, the intersection type constructor can be used to express finite heterogeneous ad hoc polymorphism.For example, the λ-term λ x . {\displaystyle \lambda x.\!} can be assigned the type ∩ α ] → β {\displaystyle \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 normalization properties of λ-terms under β-reduction.
In programming languages, such as TypeScript and Scala, intersection types are used to express ad hoc polymorphism.