Support other styles of name binding
Opened this issue · 1 comments
brendanzab commented
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.
- 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.
brendanzab commented
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).