Closed dvanhorn closed 7 years ago
Having slept on this, I now realize what I said about de-Bruijn indices is nonsense. The key here is that variable allocation happens for binding sites, not occurrences. De-Bruijn is a strategy for representing occurrences as a path to the binder. There's no information at the binding site, AFAICT. So I'm not sure how you could make an allocation strategy based on de-Bruijn indices.
But the point stands: no strategy is incorrect.
Yeah I agree with this.
This comment is wrong but in an interesting way. The point did not come across that any allocation strategy is fine and no matter what, it cannot mess up soundness. De-Bruijn would be a funny strategy: everything at lexical depth n would be joined; totally weird, but not wrong. And they're right that source location is what you actually want for the most precise monomorphic strategy.
Worth checking if we should add something hear to avoid this confusion.