From #49810:
The plan is to generalize the existing
CanonicalVarso that it represents a "bound" thing -- probably it just gets unified withDebruijnIndex.
General instructions:
The canonical var is a "new type index" declared here:
We would basically just want to remove it completely and replace uses of it with DebruijnIndex. There are a few complications to be overcome. One is that debruijn indices are currently 1-based (that is https://github.com/rust-lang/rust/issues/49813), so indexing with them will require some tweaks. Another related problem is that DebruijnIndex does not implement the Idx trait, so we can't presently have a IndexVec<DebruijnIndex>, as we do in the CanonicalVarValues struct:
This is not that big a deal -- we can just use a plain vector -- although if we make debruijn indices 0-based we could then generate it with the newtype_index! macro, which would be nice.
Can we pick some better names while we're at it?
Which names are you thinking we should change?
DebruijnIndex in particular is one I find extremely opaque. I get that it's a math term and there's a wikipedia article, but I don't think we should require that sort of reading to understand a term in a codebase (I argue for Mappable over Functor for the same reason). CanonicalVar is better in context, but I also think it's the sort of name that unless you see it specifically in the context of canonicalization there's no reason you'd know what it means.
Hmm. I suppose we could call it BinderIndex or something maybe? That said, I sort of like DebruijnIndex because it has a very unique, instant meaning, and I'm not sure that there exists a non-mathemetical term for this thing. Still, ordinarily I agree we should strive for "accessible and memorable" terminology.
If there is a very precise technical term for something, it's least ambiguous if you give that something the name. Giving something a more friendly, and less descriptive name, means that people who know the term _won't be_ immediately familiar with it, whereas people who aren't familiar with the concept still need to look it up anyway. Plus, technical terms are more memorable. I'd prefer to stick with DeBruijnIndex here.
Even though DeMorgan Machine is generally a more precise technical term for computers today, we use the term computer, since it had a more generally understandable meaning for those involved, even if that term was nonsense when applied to a machine at the time. I don't think "math calls it X" is a great argument in a code base meant to be read by programmers, who may or may not have a degree in mathematics.
This might be a reasonable argument about technical terms (e.g. Functor) in user-facing libraries, but I'd argue the internals of a compiler are technical enough that one should expect some compiler / programming language theory terminology (e.g. DeBruijnIndex).
(Although now that I've just noticed, I would be in favour of changing the capitalisation on the name ;) )
BinderDepth or BinderDistance might work out as alternatives?
Although I'm not sure I like Binder either, but there I have no suggestions.
(Using Binder and BinderSomething would make it easier to connect the two though)
Also, aren't many canonical vars bound at the same binder? How would that work?
This does seem like a case where a vague, non-"scary" term might be more obfuscating in practice than the technically correct, unambiguous term.
imo, if DeBruijnIndex usually appears in close proximity to a Binder, then renaming it to BinderIndex is probably a net win. But if DeBruijnIndex is mostly operated on/passed around independently of whatever type it is an index for, then it's probably better to keep it the way it is.
@Ixrec AIUI, it's specifically "how many Binders do I have to pass through to get to the Binder that introduces this parameter?" - "index" can be confusing because there is a separate notion of "which parameter" within a Binder - and the anonymous ones are distinguished by... an index.
I think I would like to give this a shot. But this is currently blocked by #49813, isn't it?
My opinion on the naming: I prefer the name DeBruijnIndex. A second name would surely make this matter more confusing since the programmer wouldn't then be aware of the literature name (and might therefore miss an important connection to sources of information via search engines). But for a first encounter with the term the reader should be provided with a link to a glossary which should contain a snappy definition and an example. (I started to make an effort to add a glossary for these terms inside the chalk crate. But it is not complete and will be moved to the rustc guide.)
@fabric-and-ink yeah this is sort of a "meta issue"
but I'll try to comment here or ping you once we get #49813 resolved
cc @fabric-and-ink — still interested in giving this a shot? #49813 is finally closed.
I guess a good first step would be to convert DebruijnIndex to support the Idx trait. The idea would be to declare it via the newtype_index! macro.
Ok! I will do my best.
The next step would be to replace CanonicalVar with DebruijnIndex, right?
@fabric-and-ink argh sorry for missing your update! probably yes! Let me give a look
Ok, let me know then :)
Most helpful comment
Hmm. I suppose we could call it
BinderIndexor something maybe? That said, I sort of likeDebruijnIndexbecause it has a very unique, instant meaning, and I'm not sure that there exists a non-mathemetical term for this thing. Still, ordinarily I agree we should strive for "accessible and memorable" terminology.