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

[Thorsten Altenkirch]

There are several levels of abstraction when describing a language. We start with strings but soon realize that trees work better (actually many programmers never reach this point). But then to capture binding we can use scoped terms, that is we define Lam : Nat -> Set as

                var : Fin n -> Lam n
                lam : Lam (suc n) -> Lam n
                app : Lam n -> Lam n -> Lam n

but actually we want to model typed terms, that is Lam : Con -> Ty -> Set with

                var : Var G A -> Lam G A
                lam : Lam G.A B -> Lam G (A => B)
                app : Lam G (A => B) -> Lam G A -> Lam G B

where we used typed de Bruijn indizes: Var : Con -> Ty -> Set with

                zero : Var G.A A
                suc : Var G A -> Var G.B A

the story continues when you want to model dependent types. We, Ambrus and I have written a paper about this:

Type Theory in Type Theory using Quotient Inductive Types<http://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf>
@inproceedings{10.1145/2837614.2837638, author = {Altenkirch, Thorsten and Kaposi, Ambrus}, title = {Type Theory in Type Theory Using Quotient Inductive Types}, year = {2016}, isbn = {9781450335492}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/2837614.2837638}, doi = {10.1145/2837614.2837638}, booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, pages = {18–29}, numpages = {12}, keywords = {Higher Inductive Types, Metaprogramming, Agda, Logical Relations, Homotopy Type Theory}, location = {St. Petersburg, FL, USA}, series = {POPL ’16} }


Thorsten


From: Agda <agda-bounces at lists.chalmers.se> on behalf of Joey Eremondi <joey.eremondi at gmail.com>
Date: Wednesday, 22 April 2020 at 05:13
To: Agda mailing list <agda at lists.chalmers.se>
Subject: [Agda] What do you use for variable binding in 2020?

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!



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




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