Another variation on De Bruijn indices, which I’m particularly fond of, uses normal, unnamespaced indices, and stores the preferred name of the variable only at the abstraction. This also removes the disadvantage of De Bruijn indices that the names get lost, while preserving the two advantages they have:
alpha-equivalence is still easy to test for — just compare the trees recursively while ignoring the name fields of the lambdas
you can’t make a subtle substitution mistake, as long as you follow the rule that the only thing allowed to handle the stored variable names is the pretty printer
Granted, instead of capture bugs you now get shifting bugs, but these have the advantage that they affect all terms equally, and not only those with shadowing, and are thus much easier to notice.
Beautiful work, as can be expected from this author.
Another variation on De Bruijn indices, which I’m particularly fond of, uses normal, unnamespaced indices, and stores the preferred name of the variable only at the abstraction. This also removes the disadvantage of De Bruijn indices that the names get lost, while preserving the two advantages they have:
Granted, instead of capture bugs you now get shifting bugs, but these have the advantage that they affect all terms equally, and not only those with shadowing, and are thus much easier to notice.