[Agda] Syntax declarations

[Philip Wadler]

Adam, Thanks for the pointer. I admit to still being confused. Let me
explain why. If syntax declarations were written as follows

infixr 40 _←_,_
syntax x ← e₁ , e₂ = bind e₁ (λ x → e₂)

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

infixr 30 _:=_,_
syntax x := e₁ , e₂ = bind e₁ (λ x → e₂)

Instead we write

infixr 40 bindsyntax bind e₁ (λ x → e₂) = x ← e₁ , e₂

Now the parser has to look for  _←_,_  but give it the precedence of bind,
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

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 18 March 2018 at 10:27, Adam Sandberg Eriksson <adam at sandbergericsson.se>
wrote:

> Ulf gave a rationale last year on this list: https://lists.chalmers.se/
> pipermail/agda/2017/009810.html
>
> —Adam
>
> > On 18 Mar 2018, at 13:22, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> >
> > It's great that Agda now has syntax declarations!
> >
> > I'm confused by the design. What is implemented is:
> > infixr 40
> >  bind
> >
> > syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂
> > Whereas what I would have expected is:
> > infixr 40 _←_,_
> > syntax x ← e₁ , e₂ = bind e₁ (λ x → e₂)
> > Can someone please enlighten me as to the rationale behind the current
> design? Cheers, -- P
> >
> >
> > .   \ Philip Wadler, Professor of Theoretical Computer Science,
> > .   /\ School of Informatics, University of Edinburgh
> > .  /  \ and Senior Research Fellow, IOHK
> > . http://homepages.inf.ed.ac.uk/wadler/
> > The University of Edinburgh is a charitable body, registered in
> > Scotland, with registration number SC005336.
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180318/01d0a54a/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180318/01d0a54a/attachment.ksh>