search

AndrasKovacs / elaboration-zoo

Minimal implementations for dependent type checking and elaboration
BSD 3-Clause "New" or "Revised" License
600 stars 34 forks source link

What is the need for InsertedMeta? #28

Closed atennapel closed 3 years ago

atennapel commented 3 years ago

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.

Boarders commented 3 years ago

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.

AndrasKovacs commented 3 years ago

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?

Boarders commented 3 years ago

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?

AndrasKovacs commented 3 years ago

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.

Boarders commented 3 years ago

Ah I see, that makes perfect sense.

atennapel commented 3 years ago

Could Meta be removed then?

AndrasKovacs commented 3 years ago

Could Meta be removed then?

No, only Meta can be returned from quoting.