Here's my take: with de Bruijn indices, variables need to be incremented when you put them under a new binder. They refer to binding sites relative to their occurrence. Levels refer to them absolutely and thus don't need incrementing under a new binder.
Conversation
My (probably bad) understanding is that the nifty thing about indices is that you can avoid having to rename things. The nifty thing about levels is that you can move around terms without having to shift indices. Combining them together with NbE gets you the best of both somehow?
1
1
Indices are nicer for writing evaluators (they basically say how far up the stack to look for the value). The way I see it, levels are nice for free variables, and indices for bound variables. Boundness vs freeness depends on your perspective :-)
1
1
2
The thing that kind of makes me unhappy about the approach is the fact that you have to copy around the entire environment all the time, regardless of if any of it is used. Seems a tad wasteful, but I dunno.
4
1
What is fast is not always elegant, and what is elegant is not always fast. Ideally we wouldn't need interpreters at all - see e.g. Grégoir and Leroy's paper on Coq's vm_compute, or Dirk Kleeblatt's thesis. Also ongoing work on Lean 4.
3
7
Yeah, big fan of the compilation to byte-code stuff! More just lamenting about how nested lambdas/currying seems very ordered/listy when what I really want is to be able to build up graphs of dependencies between things. Still trying to articulate what I mean though.
1
1
1
Like the level/index stuff doesn't it seem to help when comparing two things that might be out of order, but equivalent if you consider the way they are structured dependency-wise, and seems like it could make this harder.
1
1
Yeah, I've not run into it yet, more just anticipating it. And the dependency information is going to be handy for other stuff too, like multistage programming - I think? It also seems handy for low level processors ultimately (if we could sidestep machine code somehow).
2
1
Adam Chipala mentioned something similar in his talk at POPL, but it's been something on my mind for some time - very much inspired by discussions I've had with .