Conversation

David Thrane Christiansen
@d_christiansen
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.
1
2
Brendan Zabarauskas
@brendanzab
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
David Thrane Christiansen
@d_christiansen
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
2
Brendan Zabarauskas
@brendanzab
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
Rob Rix‎
@rob_rix
it’s really *very* expensive traversing trees and substituting a lot too, tho. (in the context of a dependently-typed lang where you’ve probably got higher-order unification, anyway)
2
2
@edwinb@types.pl
@edwinbrady
Haven't read the OP properly yet (I will!), but I just want to add that it looks very much like how Idris 2 evaluates, and that basically never substitutes during unification. Because, as you say, it hurts...
1
5