Love this post by about free variable traversals:
haskell.org/ghc/blog/20190
It’s a beautiful look at abstraction, code reuse, and efficiency <3
Conversation
nice! the approach of the bound library is also not bad
1
FWIW- I've mostly moved to using De Bruijn indices in terms and De Bruijn levels in the semantic domain, only plumbing names through in binders at all for pretty printing. Bound is nice, but paying no cost for name manipulation is better.
3
7
I use a sized env and De Bruijn indices/levels. It forces me to act when I walk under a λ or Π and I use HOAS for closures in my semantic domain, just because it is fast. I might turn to 's tricks to replace HOAS w/ an EDSL suited to closure compilation.
2
5
If I ever have to apply an explicit substitution I think of it as a personal failing, which keeps me on the straight and narrow performant path. The only real remaining culprit that feels like substitution for me is pruning meta variables during higher order pattern unification.
1
5
Yeah construct it in the syntax using de bruijn indices, then evaluate to a closure with the current environment + the original body. When you enter the body during readback, increment the size of current environment.
You can see it used in a dependent type system in “A simple type-theoretic language: Mini-TT”: cse.chalmers.se/~bengt/papers/
Might also be worth checking out 's post on it at colimit.net/posts/normalis
1
1
3
You can also see the approach used in 's github.com/jozefg/nbe-for, which was eventually extended to github.com/jozefg/blott for the paper “Implementing a Modal Dependent Type Theory”:
1