<div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote">On Tue, Mar 20, 2018 at 3:02 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks, Ulf and Andreas. Thinking of it in terms of printing an internal tree, rather than parsing to create an internal tree, explains a lot.<div><br></div><div class="gmail_extra"><span class=""><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;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">It also (sort of) matches the way mixfix operators work: the fact that you can write `x + y` for `_+_ x y` is a property of the name `_+_` and not a separate entity that may or may not be in scope.</span></blockquote><div><br></div></span><div>I'm still confused by this. Wouldn't</div><div><br></div><div><span class="m_7935836703162483873gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-kr" style="font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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="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;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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="m_7935836703162483873gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-mi" style="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;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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="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;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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><br></div><div><br></div><div>fit the pattern you describe better than</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="m_7935836703162483873gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-kr" style="box-sizing:border-box;font-weight:bold">infixr</span> <span class="m_7935836703162483873gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-mi" style="box-sizing:border-box;color:rgb(0,153,153)">40</span> bind<img class="m_7935836703162483873gmail-ajT" src="https://ssl.gstatic.com/ui/v1/icons/mail/images/cleardot.gif" style="font-size:12.8px;color:rgb(34,34,34);font-family:arial,sans-serif;white-space:normal;background:url("") no-repeat;height:8px;opacity:0.3;width:20px"></pre></div>?</div></div></blockquote><div><br></div><div>I simply meant that the infix notation of _+_ isn't something separate from the function _+_.<br><br>Writing <br><br><div><span class="gmail-m_7935836703162483873gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-kr" style="font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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="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;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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_7935836703162483873gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-mi" style="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;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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="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;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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><br></div><div><br></div>would require <span style="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;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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">_←_,_ <font size="2"><span style="font-family:arial,helvetica,sans-serif">to be a thing that you could talk about, which (for better or for worse) is not how<br></span></font></span></div><div><span style="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;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;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"><font size="2"><span style="font-family:arial,helvetica,sans-serif">syntax declarations were designed.<br></span></font></span></div><div><br></div><div>/ Ulf<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><span class=""></span>On 19 March 2018 at 06:54, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><span class=""></span><div><div class="h5"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Phil, rest assured that you are not the only one stumbling over this design choice.<br>
<br>
My explanation attempt:<span><br>
<br>
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂<br>
<br></span>
can be read as<br>
<br>
print "bind e₁(λ x→ e₂)" as "x ← e₁ , e₂".<br>
<br>
This reading emphasizes the uniqueness condition for syntax-attachments to a identifier ("bind").<br>
<br>
And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and treat it as "bind e₁(λ x→ e₂)".<br>
<br>
Best,<br>
Andreas<div class="m_7935836703162483873HOEnZb"><div class="m_7935836703162483873h5"><br>
<br>
On 18.03.2018 14:22, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
It's great that Agda now has syntax declarations!<br>
<br>
I'm confused by the design. What is implemented is:<br>
<br>
infixr 40 bind<br>
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂<br>
<br>
Whereas what I would have expected is:<br>
<br>
infixr 40 _←_,_<br>
syntax x ← e₁ , e₂ = bind e₁(λ x→ e₂)<br>
<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>
</blockquote>
<br>
<br></div></div><span class="m_7935836703162483873HOEnZb"><font color="#888888">
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~ab<wbr>ela/</a><br>
<br>
</font></span></blockquote></div><br></div></div></div></div>
<br>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<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></blockquote></div><br></div></div>