moniker
moniker copied to clipboard
Support other styles of name binding
Initially we have support for locally nameless variable binding, but perhaps it would be handy to also support others, so users could compare them for performance. The original Unbound implementation also supports a nominal representation, for example.
- [x] locally nameless
- [ ] nominal
- [ ] ordered terms (see freebroccolo's ocaml-ordered-terms implementation)
- [ ] scope graphs (see A Theory of Name Resolution)
More variations can be found in steshaw/lennart-lambda.
Just added scope graphs to the list! This could ultimately be a more flexible approach to name binding that is more sympathetic to the actual shape of programs (ie. as graphs), as opposed to other systems that pretend programs are trees (like locally nameless).