Intersection type discipline

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

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

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

${\displaystyle {\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 (${\displaystyle \cap }$) is taken modulo associativity, commutativity and idempotence.

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

${\displaystyle {\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}}}$

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

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

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

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

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

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

${\displaystyle {\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 ${\displaystyle (\leq )}$ is defined as the smallest preorder (reflexive and transitive relation) over intersection types satisfying the following properties:

${\displaystyle {\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.[15]

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

${\displaystyle {\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}}}$

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