<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:Consolas;
panose-1:2 11 6 9 2 2 4 3 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;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:"Consolas",serif;}
span.EmailStyle20
{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">Ah thank you. I see actually I can use let arbitrary deep in an expression while where is only allowed on the top level, right?<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">Yes, building pattern matching into the syntax would make sense. I also like to use local case expressions, where the definitional equality is extended when checking the right hand side of a case
expression (we called this the “smart case”.<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>
<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">Jesper Cockx <Jesper@sikanda.be><br>
<b>Date: </b>Saturday, 29 February 2020 at 14:09<br>
<b>To: </b>Thorsten Altenkirch <psztxa@exmail.nottingham.ac.uk><br>
<b>Cc: </b>agda list <agda@lists.chalmers.se><br>
<b>Subject: </b>Re: [Agda] let vs where<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">Hi Thorsten,<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">'Let' statements are part of the term syntax of Agda and are desugared during typechecking (by inlining). In contrast, 'where' statements are part of the syntax for
<i>declarations</i> so they cannot appear inside terms directly. Pattern matching is not part of the term syntax of Agda (unlike Coq where eliminators can appear in terms), so in general pattern matching can only happen at the declaration level.
<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">The exception to this rule are pattern matching lambdas, which are actually implemented internally by lifting the whole expression to an (anonymous) top-level definition. It should probably be possible to extend
let-expressions with the same trick. However, this would mean pattern-matching let's would be generative, i.e. two syntactically equal let-expressions might not be definitionally equal since they are desugared to two separate anonymous definitions internally.<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">Another more drastic solution would be to extend Agda's internal syntax with some kind of pattern-matching construct, e.g. eliminators or case trees. But this would basically require a complete overhaul of Agda's
internals, so I do not expect this will happen in the forseeable future (perhaps it could be part of the mythical Agda 3.0).<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">-- Jesper<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">On Sat, Feb 29, 2020 at 2:13 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
Hi,<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
Can somebody remind me for what (historical ?) reasons “where” allows pattern matching but not “let”? What are the obstacles to fixing this?<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
Thanks,<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
Thorsten<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<o:p></o:p></p>
</div>
<pre style="margin-left:36.0pt">This message and any attachment are intended solely for the addressee<o:p></o:p></pre>
<pre style="margin-left:36.0pt">and may contain confidential information. If you have received this<o:p></o:p></pre>
<pre style="margin-left:36.0pt">message in error, please contact the sender and delete the email and<o:p></o:p></pre>
<pre style="margin-left:36.0pt">attachment. <o:p></o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt">Any views or opinions expressed by the author of this email do not<o:p></o:p></pre>
<pre style="margin-left:36.0pt">necessarily reflect the views of the University of Nottingham. Email<o:p></o:p></pre>
<pre style="margin-left:36.0pt">communications with the University of Nottingham may be monitored <o:p></o:p></pre>
<pre style="margin-left:36.0pt">where permitted by law.<o:p></o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
</div>
<p class="MsoNormal" style="margin-left:36.0pt">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>
</blockquote>
</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>