[cvoss]

What happens in the evaluator when you have

(\ a . a a) (\ x . \ y . x y)

Variables are uniquely named at parse time, but after one beta step, you have two distinct instances each of x and y, albeit in different scopes, and after a second beta step, you have two distinct variables named y in the same scope.

[kccqzy]

Interesting example! I think at that time I was either working with simply typed lambda calculus or something slightly better (maybe Hindley-Milner based system) where the omega combinator isn't allowed. Do you know what sort of type system restriction would make the above idea sound?

[cvoss]

If you'll permit me to tweak the example, I'll now instead choose

(\ a . a a) (\ x . \y . y x) => \ y . y (\ x . \ y' . y' x)

which still exhibits the variable shadowing problem.

In a good language (where "good" means the type system lets you do as much as you want to do while still being sound) you should be able to find some type for omega. The question is whether you can find the right type for omega to let us do what we want for this example.

Try the simple thing first:

w := (\ a : * -> * . a a) : (* -> *) -> * // works because (* -> *) is a subtype of *

Here is a bad thing you shouldn't be able to do with omega:

w w : untypable // thankfully, because (* -> *) -> * is not a subtype of * -> *

And here is a perfectly safe thing to do, which is exactly our example:

f := (\ x : * . \ y : * -> T . y x) : * -> (* -> T) -> T

w f : *

Unhappily such a weak type makes it pretty unusable within larger terms... So alternatively, we can try harder to find a good type for omega

w := (\ a : * -> (* -> T) -> T . a a) : (* -> (* -> T) -> T) -> (* -> T) -> T

w f : (* -> T) -> T // better!

Something similar would happen with the Y combinator. In a good language, there ought to be many valid types you can find for `\ f . (\ x . f x x) (\ x . f x x)` but not any that would permit you to construct a diverging computation with it.