28
$\begingroup$

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?

$\endgroup$
11
$\begingroup$

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

$\endgroup$
  • $\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$ – Gilles Mar 7 '12 at 23:27
  • $\begingroup$ I think $M=(\lambda x.xx)(\lambda y.y)$ answers the exercise, if you are talking about union types. $\endgroup$ – jmad Mar 8 '12 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 Mar 8 '12 at 1:23
  • $\begingroup$ @jmad: Indeed, intersection types are needed to type this term :-( Maybe considering unions and intersections together would be interesting? $\endgroup$ – Stéphane Gimenez Mar 8 '12 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 Mar 8 '12 at 19:51
16
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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