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.

History

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 as normalization) of the λ-calculus by means of type 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 with Henk 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 prominent intersection type systems (excluding the universal type) is undecidable. Complementarily, undecidability of the dual problem of type inhabitation in prominent intersection type systems was proven by Paweł Urzyczyn.^[11] Later, this result was refined showing exponential space completeness of rank 2 intersection type inhabitation and undecidability of rank 3 intersection type inhabitation.^[12] Remarkably, principal type inhabitation is decidable in polynomial time.^[13]

Coppo–Dezani type assignment system

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

Term language

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}}}$

Type language

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.

Typing rules

The typing 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}}}$

Properties

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]

Barendregt–Coppo–Dezani type assignment system

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

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

Term language

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}}}$

Type language

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

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]

Typing rules

The typing 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}}}$

Properties

• 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]

References

1. Henk Barendregt; Wil Dekkers; Richard Statman (20 June 2013). Lambda Calculus with Types. Cambridge University Press. pp. 1–. ISBN 978-0-521-76614-2.
2. Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1980). "An extension of the basic functionality theory for the λ-calculus". Notre Dame Journal of Formal Logic. 21 (4): 685–693. doi:10.1305/ndjfl/1093883253. S2CID 29748788.
3. Barendregt, Henk; Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1983). "A filter lambda model and the completeness of type assignment". Journal of Symbolic Logic. 48 (4): 931–940. doi:10.2307/2273659. JSTOR 2273659. S2CID 45660117.
4. van Bakel, Steffen (2011). "Strict intersection types for the Lambda calculus". ACM Computing Surveys. 43 (3): 20:1–20:49. CiteSeerX 10.1.1.310.2166. doi:10.1145/1922649.1922657. S2CID 5537689.
5. "Intersection Types in TypeScript". Retrieved 2019-08-01.
6. "Compound Types in Scala". Retrieved 2019-08-01.
7. Pottinger, G. (1980). A type assignment for the strongly normalizable λ-terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism, 561-577.
8. Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Sallé, Patrick (1979). "Functional Characterization of Some Semantic Equalities inside Lambda-Calculus". In Hermann A. Maurer (ed.). Automata, Languages and Programming, 6th Colloquium, Graz, Austria, July 16-20, 1979, Proceedings. Vol. 71. Springer. pp. 133–146. doi:10.1007/3-540-09510-1_11. ISBN 3-540-09510-1.
9. Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1978). "A new type assignment for λ-terms". Archiv für mathematische Logik und Grundlagenforschung. 19 (1): 139–156. doi:10.1007/BF02011875. S2CID 206809924.
10. Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Venneri, Betti (1981). "Functional characters of solvable terms". Mathematical Logic Quarterly. 27 (2–6): 45–58. doi:10.1002/malq.19810270205.
11. Urzyczyn, Paweł (1999). "The emptiness problem for intersection types". Journal of Symbolic Logic. 64 (3): 1195–1215. doi:10.2307/2586625. JSTOR 2586625. S2CID 36979036.
12. Urzyczyn, Paweł (2009). "Inhabitation of low-rank intersection types". International Conference on Typed Lambda Calculi and Applications. TLCA 2009. Vol. 5608. Springer. pp. 356–370. doi:10.1007/978-3-642-02273-9_26. ISBN 978-3-642-02272-2.
13. Dudenhefner, Andrej; Rehof, Jakob (2019). "Principality and approximation under dimensional bound". Proceedings of the ACM on Programming Languages. POPL 2019. Vol. 3. ACM. pp. 8:1–8:29. doi:10.1145/3290321. ISSN 2475-1421.
14. Van Bakel, Steffen (1992). "Complete restrictions of the intersection type discipline". Theoretical Computer Science. 102 (1): 135–163. CiteSeerX 10.1.1.310.903. doi:10.1016/0304-3975(92)90297-S.
15. Dudenhefner, Andrej; Martens, Moritz; Rehof, Jakob (2017). "The algebraic intersection type unification problem". Logical Methods in Computer Science. 13 (3). arXiv:1611.05672. doi:10.23638/LMCS-13(3:9)2017. S2CID 31640337.
16. Ghilezan, Silvia (1996). "Strong normalization and typability with intersection types". Notre Dame Journal of Formal Logic. 37 (1): 44–52. doi:10.1305/ndjfl/1040067315.
17. Ronchi Della Rocca, Simona; Venneri, Betti (1983). "Principal type schemes for an extended type theory". Theoretical Computer Science. 28 ((1-2)): 151–169. doi:10.1016/0304-3975(83)90069-5.