Characterization of lambda-terms that have union types

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?

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.

StackExchange Computer Science Q#62, answer score: 17