Taking some time playing with 's codebruijn approach to names. It seems to have some benefits when working with normalization by evaluation. You can identify when your expressions become closed very easily and it allows for very nice hash-consing as a result.
Conversation
Is this an alternative to or orthogonal to the initial encodings vs tagless-final encodings argument Oleg makes about writing interpreters for an expression language? [your mention of hash-consing made me think of that work]
1
1
The question comes down to "how do you deal with names?" Do you use weak or strong HOAS, deBruijn, naive substitution, work with separate values that you can compute with fast, then map back. codebruijn inverts deBruijn. the binders effectively tells you the path to all the uses.
1
4
Oooh, thanks for this explanation! I've tried to figure out what was going on with codebruijn and had a bit of trouble. This helps a bunch! So far I've been using the 'fast value + NbE method' (not sure if there is a better name). How does it compare with codebruijn for NbE?