Having a bit of fun re-implementing a normalisation-by-evaluation base elaborator using arena allocation for terms. Seems to work well, and doesn't result in much weirdness with lifetimes! Only end up needing to use reference counting in values.
Conversation
Still not sure how best to implement my environments as I need them to be persistent. I've used `im::Vector` lib.rs/crates/im in the past, but it seems a tad chonky (size wise) to store in values… maybe I should just go with linked lists?
2
For now I'm just copying the environment every time I need to make a new closure an apply it, which is… not ideal. But yeah, not really something I want to spend too much time pondering right now.
1
Next I'm going to add error recovery with node poisoning, and figure out if I can add reasonably fine grained location tracking without making development a chore and losing sight of the core type theory. But so far I'm impressed!