<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><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><div>I'm still confused by this. Wouldn't</div><div><br></div><div><span class="gmail-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_-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="gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-kr" style="box-sizing:border-box;font-weight:bold">infixr</span> <span class="gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-mi" style="box-sizing:border-box;color:rgb(0,153,153)">40</span> bind<img class="gmail-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("//ssl.gstatic.com/ui/v1/icons/mail/ellipsis.png") no-repeat; height: 8px; opacity: 0.3; width: 20px;"></pre></div>? 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 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><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 class=""><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="HOEnZb"><div class="h5"><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="HOEnZb"><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>