Conversation

You've got a "TODO how?" in there :-)

swann

@evertedsphere

David Thrane Christiansen

I think I'll leave that in until I understand that part to my satisfaction haha

@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.

David Thrane Christiansen

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?

@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 :-)

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.

András Kovács

@andrasKovacs6

In a naive Haskell/ML implementation, env copying is just copying a single pointer, which is pretty fast. The drawback though is some space leak, but for reasonable examples it's not an issue.

Yeah, I'll believe you - it's a mild annoyance. I think I'm going to have to use immutable data structures for environments (in my Rust implementation). I think my struggle is more to do with how to then progress from there to doing more interesting stuff with dependency graphs.

Replying to

See this sibling thread:

Quote Tweet