While I have used de bruijn indices successfully in the past, a part of me wonders, why can't this problem be solved at the parser level before we even get a syntax tree? The parser knows when we are introducing a new variable in a lambda abstraction, and it can keep track of a stack of variables to be able to give them new fresh names so that in later passes we won't have to worry about name conflicts. I mean when writing a parser I basically already need to keep a stack of environments to resolve names. I sometimes keep variable names as simply a source code range where it is first introduced: so instead of dealing with the variable "f" I deal with (1,4)-(1,5) meaning the variable introduced in line 1 between columns 4 and 5; here I can still recover the string-based name but I also get to differentiate between identically named variables defined in different locations.
Is this a viable idea?
Take a look at The Rapier in GHC: https://www.researchgate.net/publication/220676611_Secrets_o...
It employs a similar idea. Track the set of in scope variables and use them to unique variables on collision.
Yeah, it's viable. I do this for my scheme implementation. Defining a new lexical variable generates a new globally unique identifier: https://github.com/maplant/scheme-rs/blob/fb89f6481443130399...
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.
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?
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.