Some sort of use-def/def-use pointers and stuff like in the imperative version of "Shrinking Lambda Expressions in Linear Time" and "Shrinking Reductions in SML.NET" would be convenient for optimization. Alphatization is not as convenient and mangles the names, which is bad for debugging and especially error messages.
E.g. ATM the well-foundedness analysis must construct scope trees to deal properly with scoping without mangling the names (to keep error messages intelligible).
Some sort of use-def/def-use pointers and stuff like in the imperative version of "Shrinking Lambda Expressions in Linear Time" and "Shrinking Reductions in SML.NET" would be convenient for optimization. Alphatization is not as convenient and mangles the names, which is bad for debugging and especially error messages.
E.g. ATM the well-foundedness analysis must construct scope trees to deal properly with scoping without mangling the names (to keep error messages intelligible).