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 $(\cap )$ to assign multiple types to a single term. In particular, if a term $M$ can be assigned both the type $\varphi _{1}$ and the type $\varphi _{2}$, then $M$ can be assigned the intersection type $\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 $\lambda x.\!(x\;x)$ can be assigned the type $((\alpha \to \beta )\cap \alpha )\to \beta$ in most intersection type systems, assuming for the term variable $x$ both the function type $\alpha \to \beta$ and the corresponding argument type $\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 TypeSript 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 $\omega$ that can be assigned to any λ-term, thereby corresponding to the empty intersection. Using the universal type $\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.

Coppo–Dezani type assignment system

The Coppo–Dezani type assignment system $(\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 $(\vdash _{\text{CD}})$ is given by λ-terms (or, lambda expressions):

${\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ where }}x{\text{ ranges over term variables}}\\\end{aligned}}$

Type language

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

${\begin{aligned}\varphi &::=\alpha \mid \sigma \to \varphi &&{\text{ where }}\alpha {\text{ ranges over type variables}}\\\sigma &::=\varphi _{1}\cap \cdots \cap \varphi _{n}&&{\text{ where }}n\geq 1\end{aligned}}$

The intersection type constructor ($\cap$) is taken modulo associativity, commutativity and idempotence.

Typing rules

The typing rules $(\to \!\!{\text{I}})$, $(\to \!\!{\text{E}})$, $(\cap {\text{I}})$, and $(\cap {\text{E}})$ of $(\vdash _{\text{CD}})$ are

${\begin{array}{cc}{\dfrac {\Gamma ,x:\sigma \vdash _{\text{CD}}M:\varphi }{\Gamma \vdash _{\text{CD}}\lambda x.\!M:\sigma \to \varphi }}(\to \!\!{\text{I}})&{\dfrac {\Gamma \vdash _{\text{CD}}M:\sigma \to \varphi \quad \Gamma \vdash _{\text{CD}}N:\sigma }{\Gamma \vdash _{\text{CD}}M\;N:\varphi }}(\to \!\!{\text{E}})\\\\{\dfrac {\Gamma \vdash _{\text{CD}}M:\varphi _{1}\quad \ldots \quad \Gamma \vdash _{\text{CD}}M:\varphi _{n}}{\Gamma \vdash _{\text{CD}}M:\varphi _{1}\cap \cdots \cap \varphi _{n}}}(\cap {\text{I}})&{\dfrac {(1\leq i\leq n)}{\Gamma ,x:\varphi _{1}\cap \cdots \cap \varphi _{n}\vdash _{\text{CD}}x:\varphi _{i}}}(\cap {\text{E}})\end{array}}$

Properties

Typability and normalization are closely related in $(\vdash _{\text{CD}})$ by the following properties:

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

If the type language is extended to contain the empty intersection, i.e. $\sigma =\varphi _{1}\cap \cdots \cap \varphi _{n}{\text{ where }}n=0$, then $(\vdash _{\text{CD}})$ 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 $(\vdash _{\text{BCD}})$ extends the Coppo–Dezani type assignment system in the following three aspects:

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

Term language

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

${\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ where }}x{\text{ ranges over term variables}}\\\end{aligned}}$

Type language

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

${\begin{aligned}\sigma ,\tau &::=\alpha \mid \omega \mid \sigma \to \tau \mid \sigma \cap \tau &&{\text{ where }}\alpha {\text{ ranges over type variables}}\end{aligned}}$

Intersection type subtyping

Intersection type subtyping $(\leq )$ is defined as the smallest preorder (reflexive and transitive relation) over intersection types satisfying the following properties:

${\begin{aligned}&\sigma \leq \omega ,\quad \omega \leq \omega \to \omega ,\quad \sigma \cap \tau \leq \sigma ,\quad \sigma \cap \tau \leq \tau ,\\&(\sigma \to \tau _{1})\cap (\sigma \to \tau _{2})\leq \sigma \to \tau _{1}\cap \tau _{2},\\&{\text{if }}\sigma \leq \tau _{1}{\text{ and }}\sigma \leq \tau _{2}{\text{, then }}\sigma \leq \tau _{1}\cap \tau _{2},\\&{\text{if }}\sigma _{2}\leq \sigma _{1}{\text{ and }}\tau _{1}\leq \tau _{2}{\text{, then }}\sigma _{1}\to \tau _{1}\leq \sigma _{2}\to \tau _{2}\end{aligned}}$

Intersection type subtyping is decidable in quadratic time.

Typing rules

The typing rules $(\to \!\!{\text{I}})$, $(\to \!\!{\text{E}})$, $(\cap {\text{I}})$, $(\leq )$, $({\text{A}})$, and $(\omega )$ of $(\vdash _{\text{BCD}})$ are:

${\begin{array}{cc}{\dfrac {\Gamma ,x:\sigma \vdash _{\text{BCD}}M:\tau }{\Gamma \vdash _{\text{BCD}}\lambda x.\!M:\sigma \to \tau }}(\to \!\!{\text{I}})&{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \to \tau \quad \Gamma \vdash _{\text{BCD}}N:\sigma }{\Gamma \vdash _{\text{BCD}}M\;N:\tau }}(\to \!\!{\text{E}})\\\\{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \quad \Gamma \vdash _{\text{BCD}}M:\tau }{\Gamma \vdash _{\text{BCD}}M:\sigma \cap \tau }}(\cap {\text{I}})&{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \quad (\sigma \leq \tau )}{\Gamma \vdash _{\text{BCD}}M:\tau }}(\leq )\\\\{\dfrac {}{\Gamma ,x:\sigma \vdash _{\text{BCD}}x:\sigma }}({\text{A}})&{\dfrac {}{\Gamma \vdash _{\text{BCD}}M:\omega }}(\omega )\end{array}}$

Properties

• Semantics: $(\vdash _{\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.
• Subject reduction: If $\Gamma \vdash _{\text{BCD}}M:\sigma$ and $M\to _{\beta }N$, then $\Gamma \vdash _{\text{BCD}}N:\sigma$.
• Subject expansion: If $\Gamma \vdash _{\text{BCD}}N:\sigma$ and $M\to _{\beta }N$, then $\Gamma \vdash _{\text{BCD}}M:\sigma$.
• Characterization of strong normalization: $M$ is strongly normalizing wrt. β-reduction, if and only if $\Gamma \vdash _{\text{BCD}}M:\sigma$ is derivable without rule $(\omega )$ for some $\Gamma$ and $\sigma$.
• Principal pairs: If $M$ is strongly normalizing, then there exists a principal pair $(\Gamma ,\sigma )$ such that for any typing $\Gamma '\vdash _{\text{BCD}}M:\sigma '$ the pair $(\Gamma ',\sigma ')$ can be obtained from the principal pair $(\Gamma ,\sigma )$ by means of type expansions, liftings, and substitutions.