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.

Answer 3

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.