[Agda] What do you use for variable binding in 2020?

[Siek, Jeremy]

Hi Joey,

These days I’m using de Bruijn but in the style of PLFA and I’m relatively happy with it.
However, if you need any non-trivial lemmas about substitution (such as commutativity
of substitution), then it might be worth your while to use my library to define your
abstract syntax trees and substitution functions:

https://github.com/jsiek/abstract-binding-trees

(I note that there are more sophisticated libraries for this kind of thing, but
I’ve found it difficult to understand the other ones.)

Cheers,
Jeremy

On Apr 22, 2020, at 12:07 AM, Joey Eremondi <joey.eremondi at gmail.com<mailto:joey.eremondi at gmail.com>> wrote:

I'm modelling a programming language/core-calculus in Agda, and I'm wondering what people use to model binding and name capture?
I'm familiar with a few techniques in general, but I'm wondering if specific ones works better in Agda, or have libraries to support them, or at least good examples of code using them.

My language has a lot of constructs, so the ideal for me is something that either doesn't require me to implement substitution myself, or where I can do it generically, so I'm not writing a ton of boiler plate.

I'm aware of:

* De Bruijn/ Locally Nameless: seems pretty solid, but requires implementing substitution and other traversals myself, possibly twice.
* PHOAS: handles capturing and shadowing easily, but seems to be more popular with Coq? Not sure how it scales modelling to things like type rules and small-step semantics
* Shifted Names: looks promising, but I'm not sure how mature this idea is http://tydeworkshop.org/2019-abstracts/paper16.pdf
* Type/scope safe universes: I haven't fully grokked this one, but it's got a lot of smart people behind it. https://dl.acm.org/doi/10.1145/3236785

What do you use? What do you like? What has tutorials / code examples / libraries?

Thanks!
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

__________________________________________
Jeremy G. Siek    <jsiek at indiana.edu<mailto:jsiek at indiana.edu>>
Professor
Luddy School of Informatics, Computing, and Engineering
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200424/c2c60221/attachment.html>