<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:-webkit-standard;
panose-1:2 11 6 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">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<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span>
<span lang="SV" style="mso-fareast-language:EN-US">var : Fin n -> Lam n<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="SV" style="mso-fareast-language:EN-US"> lam : Lam (suc n) -> Lam n<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="SV" style="mso-fareast-language:EN-US"> app : Lam n -> Lam n -> Lam n<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="SV" style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">but actually we want to model typed terms, that is Lam : Con -> Ty -> Set with<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span>
<span lang="SV" style="mso-fareast-language:EN-US">var : Var G A -> Lam G A<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="SV" style="mso-fareast-language:EN-US">
</span><span lang="PL" style="mso-fareast-language:EN-US">lam : Lam G.A B -> Lam G (A => B)<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="PL" style="mso-fareast-language:EN-US"> app : Lam G (A => B) -> Lam G A -> Lam G B<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="PL" style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">where we used typed de Bruijn indizes: Var : Con -> Ty -> Set with<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span>
<span lang="PL" style="mso-fareast-language:EN-US">zero : Var G.A A<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="PL" style="mso-fareast-language:EN-US">
</span><span lang="SV" style="mso-fareast-language:EN-US">suc : Var G A -> Var G.B A<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="SV" style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">the story continues when you want to model dependent types. We, Ambrus and I have written a paper about this:<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black"><a href="http://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf">Type Theory in Type Theory using Quotient Inductive Types</a><o:p></o:p></span></p>
<p class="MsoNormal"><i><span style="mso-fareast-language:EN-US">@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} }</span></i><span style="mso-fareast-language:EN-US"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-left:36.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black">Agda <agda-bounces@lists.chalmers.se> on behalf of Joey Eremondi <joey.eremondi@gmail.com><br>
<b>Date: </b>Wednesday, 22 April 2020 at 05:13<br>
<b>To: </b>Agda mailing list <agda@lists.chalmers.se><br>
<b>Subject: </b>[Agda] What do you use for variable binding in 2020?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">I'm modelling a programming language/core-calculus in Agda, and I'm wondering what people use to model binding and name capture?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">I'm aware of:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* De Bruijn/ Locally Nameless: seems pretty solid, but requires implementing substitution and other traversals myself, possibly twice.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* 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<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* Shifted Names: looks promising, but I'm not sure how mature this idea is
<a href="http://tydeworkshop.org/2019-abstracts/paper16.pdf">http://tydeworkshop.org/2019-abstracts/paper16.pdf</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* Type/scope safe universes: I haven't fully grokked this one, but it's got a lot of smart people behind it.
<a href="https://dl.acm.org/doi/10.1145/3236785">https://dl.acm.org/doi/10.1145/3236785</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">What do you use? What do you like? What has tutorials / code examples / libraries?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Thanks!<o:p></o:p></p>
</div>
</div>
</div>
<PRE>
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.
</PRE></body>
</html>