What is the need for InsertedMeta?
atennapel opened this issue · 7 comments
I saw you updated the code for implicit arguments, it's very clean now. The only thing that I don't understand is the need for InsertedMeta. This was not in the code before, just Meta is enough, you can create spine (filter out non-bound variables) in freshMeta. With InsertedMeta the creation of the spine is delayed a little bit because it's done in evaluation. Is the reason for InsertedMeta efficiency/performance, because it seems redundant in the presence of Meta.
Relatedly, I wondered if you could just have let-defined indices and a defined context so the bound variable spine only needs the depth to do the correct binding.
Efficiency, and when we get to more advanced/typed unification, simplicity as well. Without InsertedMeta, fresh meta creation is linear in local scope and evaluating an inserted meta is quadratic. With InsertedMeta, it's constant time and linear respectively, and also simpler.
Relatedly, I wondered if you could just have let-defined indices and a defined context so the bound variable spine only needs the depth to do the correct binding.
I don't really understand, can you explain?
I may be way off since I only glanced through the code yesterday, but I had in mind that you use different indices for let bindings than for lambdas and Pis and you store the defined let bound variables in their own context and with their own binding level. I may be missing something but this would mean that you don't need the bitmask and you could use the variables Bound 0, ..., Bound (level - 1) when doing meta insertion. Is there something obviously deficient about that idea?
That doesn't work, because bound variables can become defined during evaluation. For example, take
let f = \x. t in
f u
In the scope of t, x is bound, but when we actually evaluate t, x is defined as u. So it's not possible to separate bound and defined contexts.
Ah I see, that makes perfect sense.
Could Meta be removed then?
Could Meta be removed then?
No, only Meta can be returned from quoting.