I was reading a paper on the GHC compiler's inliner, which they call The Rapier, and found a follow up paper ("The Foil: Capture-Avoiding Substitution With No Sharp Edges" https://arxiv.org/pdf/2210.04729.pdf) which tries to statically enforce the invariants needed to avoid name capture during substitutions etc.
The Foil typing in that paper is really convoluted, since Haskell's type system can't really cope well. Having dependent types available makes things a lot easier.
I took a crack at something similar (with stronger requirements) in Shen: https://github.com/NHALX/shen-misc/blob/master/foil.shen
The intent is to prevent shadowed name bindings and statically prove all bindings in the expression have unique names, as well as forbidding free variables.
Some notes:
- Names and Foil expressions are annotated with a list describing the expanding scope, which gets set in order from outer expression to inner.
- New names are generated with their scope variable unbound, waiting for let and lambda to fix them with a unique id.
- The substitution lists are able to statically grow their domain due to scope expansion.
There's some annoying flaws at the moment:
- If the unbound scope variable isn't bound to [] or something else at the top level, then it won't detect some invalid expressions.
- Scope shrinking with foil-dissolve doesn't seem like it has proper justification.
- T* needs to be patched.