A simpler and more extendable implementation for binders.
Context
I've been trying to make locally nameless-like to work for a while and while in principle it provides major advantages, in practice it is hard to make it behave nicely with unification and simple terms are not meaningfully faster.
In fact after thinking for a while, for simple terms where binders are expanded only a few times and with lazy rename, alpha-renaming should be faster as it will rarely happens, additionally alpha-renaming may produce a de-bruijin term which makes it faster for compute-intensive terms.
There are a couple lessons learned here that needs to be documented in the future, but for now, optimizing alpha-renaming will be the goal.
Goals
A simpler and more extendable implementation for binders.
Context
I've been trying to make locally nameless-like to work for a while and while in principle it provides major advantages, in practice it is hard to make it behave nicely with unification and simple terms are not meaningfully faster.
In fact after thinking for a while, for simple terms where binders are expanded only a few times and with lazy rename, alpha-renaming should be faster as it will rarely happens, additionally alpha-renaming may produce a de-bruijin term which makes it faster for compute-intensive terms.
There are a couple lessons learned here that needs to be documented in the future, but for now, optimizing alpha-renaming will be the goal.
Related
165