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

[Andreas Abel]

De Bruijn indices.

 > * Type/scope safe universes: I haven't fully grokked this one, but it's
 > got a lot of smart people behind it.

This paper is a systematization of de Bruijn indices.  (If I understand 
it correctly.)

On 2020-04-22 06:07, Joey Eremondi 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
> https://lists.chalmers.se/mailman/listinfo/agda
>