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

[James Wood]

Hi Joey,

Note that the AACMM (Universes of Syntax with Binding) paper now has a
journal version living at https://arxiv.org/abs/2001.11001v1. I'd take
the journal version to be the definitive source for this approach.

As for understanding it, it might be instructive to focus on and
reproduce section 3 first, and then worry about the later sections
later. In short: section 3 moves us from having multiple traversals of
the syntax (notably renaming and substitution) to having just one:
`semantics`. This already has a big payoff. The approach is finished off
in sections 5 and 6, where rules are given for producing typing rules
which always support a `semantics`.

Another useful reference for the section 3 material is Conor McBride's
note living at http://strictlypositive.org/ren-sub.pdf, which is a more
first-principles exposition.

Alternatively, I think it's also quite possible to not fully understand
what's going on, and work off of the examples in the repository and in
the paper. The syntax for creating a type system is very different from
standard Agda, but it should be clear roughly what's doing what.

Regards,
James

On 22/04/2020 05: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
> <https://eur02.safelinks.protection.outlook.com/?url=http%3A%2F%2Ftydeworkshop.org%2F2019-abstracts%2Fpaper16.pdf&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C50713c043e464b79282008d7e672c7e5%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637231253744934329&sdata=DKPJOMPezopdby5AwTVlVS1LDc60S8O4u2JbTU0XJSU%3D&reserved=0>
> * 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
> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2F10.1145%2F3236785&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C50713c043e464b79282008d7e672c7e5%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637231253744934329&sdata=xAROgarNzIlPDMPWidXOXUSgMplYhbrPoYC27jWha40%3D&reserved=0>
> 
> What do you use? What do you like? What has tutorials / code examples /
> libraries?
> 
> Thanks!
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C50713c043e464b79282008d7e672c7e5%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637231253744964311&sdata=m4Ub1bL51mkUuwYZw34omWWvhmRWiHcv9PfmXxc3kV8%3D&reserved=0
>