Conversation

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
David Thrane Christiansen
@d_christiansen
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
Brendan Zabarauskas
@brendanzab
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
Brendan Zabarauskas
@brendanzab
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
Rob Rix‎
@rob_rix
If I’m understanding you correctly, I think you’re bang on with this; e.g. in higher-order unification you can talk about terms being equal under some assumptions (= “a context”), but it’s tricky both because of this & because of dependencies between bindings.
1
1
Rob Rix‎
@rob_rix
e.g. you can’t reorder just *anything,* and what you *can* reorder depends on the types of the terms in a lang with “full-spectrum” dependent types (IIRC). I think you’ve run into this, if I recall old threads right? But just to echo that this jives with my experience as well.
1
1
Brendan Zabarauskas
@brendanzab
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
Rob Rix‎
@rob_rix
Reading some of
@kmett
’s examples of bound always makes me think about this stuff. E.g. simultaneous and mutually-recursive bindings admitted by tagging bound variables (de Bruijn indices, albeit cleverly-represented ones) with some extra data.
1
2
Rob Rix‎
@rob_rix
Like, I *want* to represent syntax as hypergraphs, and I want to preserve names, but I want alpha-equivalence, and I don’t want to substitute or walk under binders, but I do want scope-safety enforced by the types, and I usually end up crushed under the weight of my constraints.
2
3