[PRL] Type question...

[Felix S Klock II]

On Oct 5, 2007, at 8:24 AM, Mitchell Wand wrote:

> Just back from ICFP, so I'm only getting to this now.
>
> Of course Y (and its friends) have no simple type, because the  
> simply-typed lambda calculus is strongly normalizing, and Y has no  
> normal form.
>
> Every pure lambda term is typable with recursive types, since you  
> can give any pure lambda term the type  (mu t)(t -> t).  If you add  
> constants, of course, all bets are off.
>
> I believe there is a theorem that says that all pure lambda terms  
> are typable using intersection types, but I don't know the details.

Mmm, I think the theorem is that a term is strongly normalizing if  
and only if it is typable using intersection types.

-Felix