nLab intersection type

Idea

Intersection types are a way to add finite polymorphism to the simply typed λ-calculus. For example, the judgment $\Gamma \vdash e \colon \tau \wedge \sigma$ means that $e$ has both types $\tau$ and $\sigma$.

Intersection types (without a universal type $\omega$) capture exactly the strongly-normalizing terms of the λ-calculus. For example the value $\lambda x. x \, x$ can be typed using the following judgment: $x : (\sigma \to \sigma) \wedge \sigma \vdash x\,x : \sigma$. However, type inference for intersection type systems is undecidable.

Typing rules

In most intersection type systems, we can derive a rule for function elimination similar to:

$$\frac{ \Gamma \vdash f \colon \bigwedge_{i \in I}(A_i \to B_i) \qquad \Gamma \vdash x : A }{ \Gamma \vdash f \, x \colon \bigwedge_{k \in I, A \leq A_k} B_k }$$

Non-idempotent intersection types

In the majority of intersection type systems, $\wedge$ is associative, commutative and idempotent. However, $\wedge$ can also be seen as the non-idempotent multiplicative conjunction from linear logic.

Related concepts

• polymorphism

• union types?

References

• M. Coppo, M. Dezani-Ciancaglini: A new type assignment for lambda-terms, Archive for Mathematical Logic 19 (1978) 139–156 [doi:10.1007/BF02011875]

• M. Coppo, M. Dezani-Ciancaglini: An extension of the basic functionality theory for the λ-calculus, Notre Dame Journal of Formal Logic 4 (1980) 685–693 [doi:10.1305/ndjfl/1093883253, pdf]