Idea: Syntax for specifying binding rules

[pdubroy]

It might be nice to have a syntax for specifying lexical binding rules for languages. Currently, the best way to do name resolution is inside an attribute/operation, but this makes it more difficult to reuse the results. A declarative syntax could be useful for (say) an IDE that wants support renaming variables, without having to rely on language- and implementation-specific attributes/operations.

One idea I had is a syntax to embed the binding rules in the grammar itself: https://gist.github.com/pdubroy/984ad6e3ecf181b1c15c#file-gistfile1-txt. However, this would complicate the grammars somewhat, and would likely only be able to handle simple cases.

Another option would be some sort of supplemental syntax -- maybe separate rules in the grammar that define how names are resolved. E.g.:

ML {
  Expr = ...
  LetExpr = ...

  @LetExpr = /* binding syntax goes here */
}

Some relevant papers:

• A Theory of Name Resolution with Extended Coverage and Proofs
• Romeo: a System For More Flexible Binding-Safe Programming

[pdubroy]

Also: Toward a General Theory of Names, Binding and Scope

[pdubroy]

If we implement this, it would require a lot of thought and careful design, and we should start by implementing it as a library feature first.

[alexwarth]

Eelco Visser and co. seem to have a nice way to specify this kind of thing. We should study their approach carefully. Here are some links:

• http://researchr.org/publication/NeronTVW15
• http://researchr.org/publication/VanAntwerpenNTVWPEPM2016
• http://conf.researchr.org/event/POPL-2016/popl-2016-tutorials-t2-part-2-declare-your-language-name-binding-with-scope-graphs