Many textbooks cover intersection types in the lambda-calculus. The typing rules for intersection can be defined as follows (on top of the simply typed lambda-calculus with subtyping):

$$ \dfrac{\Gamma \vdash M : T_1 \quad \Gamma \vdash M : T_2} {\Gamma \vdash M : T_1 \wedge T_2} (\wedge I) \qquad\qquad \dfrac{} {\Gamma \vdash M : \top} (\top I) $$

Intersection types have interesting properties with respect to normalization:

  • A lambda-term can be typed without using the $\top I$ rule iff it is strongly normalizing.
  • A lambda-term admits a type not containing $\top$ iff it has a normal form.

What if instead of adding intersections, we add unions?

$$ \dfrac{\Gamma \vdash M : T_1} {\Gamma \vdash M : T_1 \vee T_2} (\vee I_1) \qquad\qquad \dfrac{\Gamma \vdash M : T_2} {\Gamma \vdash M : T_1 \vee T_2} (\vee I_2) $$

Does the lambda-calculus with simple types, subtyping and unions have any interesting similar property? How can the terms typable with union be characterized?


3 Answers 3


In the first system what you call subtyping are these two rules:

$$\dfrac{Γ, x:T_1 \vdash M:S}{Γ, x:T_1 ∧ T_2 \vdash M:S}(∧E_1)\quad\dfrac{Γ, x:T_2 \vdash M:S}{Γ, x:T_1 ∧ T_2 \vdash M:S}(∧E_2)$$

They correspond to elimination rules for $∧$; without them the connective $∧$ is more or less useless.

In the second system (with connectives $∨$ and $→$, to which we could also add a $⊥$), the above subtyping rules are irrelevant, and I think the accompanying rules you had in mind are the following:

$$\dfrac{Γ, x: T_1 \vdash M:S\quad Γ, x:T_2 \vdash M:S}{Γ, x:T_1 ∨ T_2 \vdash M:S}(∨E)\quad\dfrac{}{Γ, x: {⊥} \vdash M:S}({⊥}E)$$

For what it's worth, this system allows to type $(λx. I)Ω:A→A$ (using the ${⊥}E$ rule), which cannot be typed with just simple types, which has a normal form, but is not strongly normalizing.

Random thoughts: (maybe this is worth asking on TCS)

This leads me to conjecture that the related properties are something like:

  • a λ-term $M$ admits a type not containing $⊥$ iff $MN$ has a normal form for all $N$ which has a normal form. ($δ$ fails both tests, but the above λ-term pass them)
  • a λ-term $M$ can be typed without using the ${⊥}E$ rule iff $MN$ is strongly normalizing for all strongly normalizing $N$.

Exercise: prove me wrong.

Also it seems to be a degenerated case, maybe we should consider adding this guy into the picture. As far as I remember, it would allow to obtain $A ∨ (A → {⊥})$?

  • $\begingroup$ Good point about the subtyping rules, they show that union types aren't nearly as natural as intersections (which get typed orthogonally to arrows). About the second part I need to think some more. $\endgroup$ Commented Mar 7, 2012 at 23:27
  • 1
    $\begingroup$ I think $M=(\lambda x.xx)(\lambda y.y)$ answers the exercise, if you are talking about union types. $\endgroup$
    – jmad
    Commented Mar 8, 2012 at 0:16
  • $\begingroup$ About call/cc: it needs more than just lambda-terms (like lambda-mu-terms or another framework) but type systems are more complex, logic systems, in which union types may be irrelevant. $\endgroup$
    – jmad
    Commented Mar 8, 2012 at 1:23
  • $\begingroup$ @jmad: Indeed, intersection types are needed to type this term :-( Maybe considering unions and intersections together would be interesting? $\endgroup$ Commented Mar 8, 2012 at 10:15
  • $\begingroup$ I would be interested in a λ-term one can type with union types (rs. with intersection types) but not with simple types (rs. with intersection types). $\endgroup$
    – jmad
    Commented Mar 8, 2012 at 19:51

I just want to explain why intersection types are well-suited to characterize classes of normalization (strong, head or weak), whereas other type systems can not. (simply-typed or system F).

The key difference is that you have to say: "if I can type $M_2$ and $M_1→M_2$ then I can type $M_1$". This is often not true in non-intersection types because a term can be duplicated:

$$ (\lambda x.Mxx)N → MNN$$

and then typing $MNN$ means that you can type both occurrences of $N$ but not with the same type, for example $$M:T_1→T_2→T_3 \qquad N:T_1 \qquad N:T_2$$ With intersection types you can transform this into: $$M:T_1\wedge T_2→T_1\wedge T_2→T_3 \qquad N:T_1\wedge T_2$$ and then the crucial step is now really easy: $$(\lambda x.Mxx):T_1\wedge T_2→T_3 \qquad N:T_1\wedge T_2$$ so $(\lambda x.Mxx)N$ can by typed with intersection types.

Now about union types: suppose you can type $(\lambda x.xx)(\lambda y.y)$ with some union type, then you can also type $\lambda x.xx$ and then get for some types $S, T_1, \dots$ $$x : T_1\vee T_2 \vee \dots \vee T_n ⊢xx:S$$ But you still have to prove that for every $i$, $x:T_i⊢xx:S$ which seems impossible even is $S$ is an union type.

This is why I don't think there is an easy characterization about normalization for union types.


The standard approach is to expand the Curry-Howard Correspondence to cover disjunctions by providing cover for the tautologies: $$ O: (a ⊃ c) ⊃ (b ⊃ c) ⊃ a ∨ b ⊃ c,\quad 𝐝: a ⊃ a ∨ b,\quad 𝐪: b ⊃ a ∨ b,$$ and define $[f,g] = Ofg$, where $f: a ⊃ c$ and $g: b ⊃ c$, with $[f,g](𝐝x) = fx$, where $x: a$, and $[f,g](𝐪y) = gy$, where $y: b$, and also postulate (as an expansion of the η-rule) that each $h: a ∨ b ⊃ c$ can be expressed as $h = [h ∘ 𝐝, h ∘ 𝐪]$.

For something that's purely internal and self-contained as a language, just to improvise a possible solution: you'd have to expand the language to include the notion of partially defined terms, of disjoint union $f + g$ for partial functions $f$ and $g$ that have non-intersecting domains, and for the undefined function $0$. Then, we include the partial functions $𝐛: a ⊃ a ∨ b$ and $𝐩: b ⊃ a ∨ b$, such that $𝐛(𝐝x) = x$, for $x: a$, $𝐩(𝐪y) = y$, for $y: b$, with $𝐛(𝐪y)$ and $𝐩(𝐝x)$ both being undefined; i.e. $$ 𝐛 ∘ 𝐝 = I: a ⊃ a,\quad 𝐛 ∘ 𝐪 = 0: b ⊃ a,\quad 𝐩 ∘ 𝐝 = 0: a ⊃ b,\quad 𝐩 ∘ 𝐪 = I: b ⊃ b,\\ 𝐝 ∘ 𝐛 + 𝐪 ∘ 𝐩 = I: a ∨ b ⊃ a ∨ b,$$ with $$[f,g] = f ∘ 𝐛 + g ∘ 𝐩.$$

This is similar to the upsampling and downsampling functions used in wavelet analysis.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.