<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Tue, Mar 20, 2018 at 5:47 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">OK, thanks for the clarification. I assume, though, that somewhere there is a table that records <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">_←_,_ </span>as syntax to parse with precedence 40? Cheers, -- P</div></blockquote><span class="gmail-"><br></span></div><div class="gmail_quote"><span class="gmail-">Of course. There's a field for syntax associated with each name.<br><br>If you're curious it's here:<br><br><a href="https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87ac0f01d5c8/src/full/Agda/Syntax/Abstract/Name.hs#L48">https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87ac0f01d5c8/src/full/Agda/Syntax/Abstract/Name.hs#L48</a><br><br></span></div><div class="gmail_quote"><span class="gmail-">and the definition of Fixity' here:<br><br><a href="https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87ac0f01d5c8/src/full/Agda/Syntax/Fixity.hs#L39">https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87ac0f01d5c8/src/full/Agda/Syntax/Fixity.hs#L39</a><br></span></div><div class="gmail_quote"><span class="gmail-"><br></span></div><div class="gmail_quote"><span class="gmail-">/ Ulf<br></span></div><div class="gmail_quote"><span class="gmail-"><br></span><span class="gmail-"></span><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail_extra"><div><div class="gmail-h5"><div class="gmail_quote">On 20 March 2018 at 12:34, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote"><span>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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);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><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="gmail-m_2801356315573441506m_137507260583459382m_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_2801356315573441506m_137507260583459382m_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="gmail-m_2801356315573441506m_137507260583459382m_7935836703162483873gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-kr" style="box-sizing:border-box;font-weight:bold">infixr</span> <span class="gmail-m_2801356315573441506m_137507260583459382m_7935836703162483873gmail-m_-5169221102346419984gmail-m_8494344911004524403gmail-mi" style="box-sizing:border-box;color:rgb(0,153,153)">40</span> bind<img class="gmail-m_2801356315573441506m_137507260583459382m_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: rgba(0, 0, 0, 0) url("") no-repeat scroll 0% 0%; height: 8px; opacity: 0.3; width: 20px;"></pre></div>?</div></div></blockquote><div><br></div></span><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_2801356315573441506m_137507260583459382gmail-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_2801356315573441506m_137507260583459382gmail-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.<span class="gmail-m_2801356315573441506HOEnZb"><font color="#888888"><br></font></span></span></font></span></div><span class="gmail-m_2801356315573441506HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf<br></div><div> </div></font></span><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div class="gmail-m_2801356315573441506h5"><div dir="ltr"><div class="gmail_extra"><span></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></span><div><div class="gmail-m_2801356315573441506m_137507260583459382h5"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);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="gmail-m_2801356315573441506m_137507260583459382m_7935836703162483873HOEnZb"><div class="gmail-m_2801356315573441506m_137507260583459382m_7935836703162483873h5"><br>
<br>
On 18.03.2018 14:22, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);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="gmail-m_2801356315573441506m_137507260583459382m_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></div></div><span>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" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></span></blockquote></div><br></div></div>
</blockquote></div><br></div></div></div>
<br>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br></blockquote></div><br></div></div>