<div dir="ltr">Adam, Thanks for the pointer. I admit to still being confused. Let me explain why. If syntax declarations were written as follows<div><br></div><div><span class="gmail-m_8494344911004524403gmail-kr" style="box-sizing:border-box"></span><span class="gmail-m_8494344911004524403gmail-kr" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">  infixr</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap"> </span><span class="gmail-m_8494344911004524403gmail-mi" style="font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;color:rgb(0,153,153)">40</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap"> _←_,_</span></div><div><span class="gmail-m_8494344911004524403gmail-kr" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box">  </span><span class="gmail-m_8494344911004524403gmail-kr" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">syntax</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap"> x ← e₁ , e₂ = bind e₁ </span><span class="gmail-m_8494344911004524403gmail-o" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">(</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap">λ x </span><span class="gmail-m_8494344911004524403gmail-ow" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">→</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap"> e₂</span><span class="gmail-m_8494344911004524403gmail-o" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">)</span></div><div><span class="gmail-m_8494344911004524403gmail-o" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold"><br></span></div>Then the parser could look for _←_,_ with precedence 40 (and right associative), exactly the same way it parses everything else. Further, it would be fine to provide alternate syntaxes for the same thing<div><br></div><div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><span class="gmail-m_8494344911004524403gmail-kr" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">  infixr</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap"> 3</span><span class="gmail-m_8494344911004524403gmail-mi" style="font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;color:rgb(0,153,153)">0</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap"> _:=_,_</span></div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><span class="gmail-m_8494344911004524403gmail-kr" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box">  </span><span class="gmail-m_8494344911004524403gmail-kr" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">syntax</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap"> x := e₁ , e₂ = bind e₁ </span><span class="gmail-m_8494344911004524403gmail-o" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">(</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap">λ x </span><span class="gmail-m_8494344911004524403gmail-ow" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">→</span><span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap"> e₂</span><span class="gmail-m_8494344911004524403gmail-o" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold">)</span></div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><span class="gmail-m_8494344911004524403gmail-o" style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre-wrap;box-sizing:border-box;font-weight:bold"><br></span></div>Instead we write</div><div><pre style="white-space:pre-wrap;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial;box-sizing:border-box;font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;margin:0px;padding:12px;line-height:normal;display:block;overflow:auto;color:rgb(64,64,64);background-color:rgb(255,255,255)"><span class="gmail-m_8494344911004524403gmail-kr" style="box-sizing:border-box;font-weight:bold">infixr</span> <span class="gmail-m_8494344911004524403gmail-mi" style="box-sizing:border-box;color:rgb(0,153,153)">40</span> bind
<span class="gmail-m_8494344911004524403gmail-kr" style="box-sizing:border-box;font-weight:bold">syntax</span> bind e₁ <span class="gmail-m_8494344911004524403gmail-o" style="box-sizing:border-box;font-weight:bold">(</span>λ x <span class="gmail-m_8494344911004524403gmail-ow" style="box-sizing:border-box;font-weight:bold">→</span> e₂<span class="gmail-m_8494344911004524403gmail-o" style="box-sizing:border-box;font-weight:bold">)</span> <span class="gmail-m_8494344911004524403gmail-ow" style="box-sizing:border-box;font-weight:bold">=</span> x ← e₁ , e₂</pre></div><div>Now the parser has to look for <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span> </span>_←_,_<span>  but give it the precedence of <span style="color:rgb(64,64,64);font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:pre-wrap;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">bind</span></span></span>, and it is harder to provide alternative syntaxes. The design seems backward to me, but I suspect there are good reasons why it is the way it is. It would help me to understand syntax declarations if I knew what they are, but the note cited doesn't explain. Cheers, -- P</div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 18 March 2018 at 10:27, Adam Sandberg Eriksson <span dir="ltr"><<a href="mailto:adam@sandbergericsson.se" target="_blank">adam@sandbergericsson.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Ulf gave a rationale last year on this list: <a href="https://lists.chalmers.se/pipermail/agda/2017/009810.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>pipermail/agda/2017/009810.<wbr>html</a><br>
<br>
—Adam<br>
<div><div class="h5"><br>
> On 18 Mar 2018, at 13:22, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a>> wrote:<br>
><br>
> It's great that Agda now has syntax declarations!<br>
><br>
> I'm confused by the design. What is implemented is:<br>
> infixr 40<br>
>  bind<br>
><br>
> syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂<br>
> Whereas what I would have expected is:<br>
> infixr 40 _←_,_<br>
> syntax x ← e₁ , e₂ = bind e₁ (λ x → e₂)<br>
> Can someone please enlighten me as to the rationale behind the current design? Cheers, -- P<br>
><br>
><br>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
> .   /\ School of Informatics, University of Edinburgh<br>
> .  /  \ and Senior Research Fellow, IOHK<br>
> . <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a><br>
</div></div>> The University of Edinburgh is a charitable body, registered in<br>
> Scotland, with registration number SC005336.<br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br>
<br>
</blockquote></div><br></div>