Characterization of lambda-terms that have union types

Question

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?

Answer 1

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 → {⊥})$?

Answer 2

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.