intersection types

I sketch the argument that pure lambda terms in normal form are typable using intersection types.  This completes the argument started in the previous episode, that intersection types are complete for normalizing terms: normal forms are typable, and typing is preserved by beta-expansion.  Hence any normalizing term is typable (since it reduces to a normal form by definition, and from this normal form we can walk typing back to the term).

Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable.  So typing is closed under beta-reduction.  With intersection typing, typing is also closed under beta-expansion, which is a critical step in showing that intersection typing is complete for normalizing terms: any normalizing term can be typed with intersection types (and simple function types).  

In a type system with intersection types, a term t that has type A and also has type B can be assigned the type 'A intersect B'.   This episode begins Chapter 12 of the podcast on intersection types.

Intersection types internalize the idea that a term has two types.  Curry-style typing is generally needed for this to be nontrivial.