Discussion:
Syntax declarations
(too old to reply)
Philip Wadler
2018-03-18 13:22:24 UTC
Permalink
Raw Message
It's great that Agda now has syntax declarations!

I'm confused by the design. What is implemented is:

infixr 40 bindsyntax 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/
Adam Sandberg Eriksson
2018-03-18 13:27:07 UTC
Permalink
Raw Message
Ulf gave a rationale last year on this list: https://lists.chalmers.se/pipermail/agda/2017/009810.html

—Adam
Post by Philip Wadler
It's great that Agda now has syntax declarations!
infixr 40
bind
syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂
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
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-03-18 19:50:14 UTC
Permalink
Raw Message
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/
Post by Adam Sandberg Eriksson
Ulf gave a rationale last year on this list: https://lists.chalmers.se/
pipermail/agda/2017/009810.html
—Adam
Post by Philip Wadler
It's great that Agda now has syntax declarations!
infixr 40
bind
syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂
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
Post by Philip Wadler
. \ 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
https://lists.chalmers.se/mailman/listinfo/agda
Ulf Norell
2018-03-19 05:55:12 UTC
Permalink
Raw Message
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.
The main reason for it being this way around it that it means we don't need
a separate kind of entity of syntaxes for the scope checker to manage,
which simplified the implementation quite a lot.

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.

/ Ulf
Andreas Abel
2018-03-19 09:54:16 UTC
Permalink
Raw Message
Phil, rest assured that you are not the only one stumbling over this
design choice.

My explanation attempt:

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

can be read as

print "bind e₁(λ x→ e₂)" as "x ← e₁ , e₂".

This reading emphasizes the uniqueness condition for syntax-attachments
to a identifier ("bind").

And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and treat
it as "bind e₁(λ x→ e₂)".

Best,
Andreas
Post by Philip Wadler
It's great that Agda now has syntax declarations!
infixr 40 bind
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
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/
--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

***@gu.se
http://www.cse.chalmers.se/~abela/
Philip Wadler
2018-03-20 14:02:29 UTC
Permalink
Raw Message
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.

It also (sort of) matches the way mixfix operators work: the fact that you
Post by Ulf Norell
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.
I'm still confused by this. Wouldn't

infixr 40 _←_,_

fit the pattern you describe better than

infixr 40 bind

? 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/
Post by Ulf Norell
Phil, rest assured that you are not the only one stumbling over this
design choice.
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
can be read as
print "bind e₁(λ x→ e₂)" as "x ← e₁ , e₂".
This reading emphasizes the uniqueness condition for syntax-attachments to
a identifier ("bind").
And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and treat
it as "bind e₁(λ x→ e₂)".
Best,
Andreas
Post by Philip Wadler
It's great that Agda now has syntax declarations!
infixr 40 bind
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
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/
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
http://www.cse.chalmers.se/~abela/
Ulf Norell
2018-03-20 15:34:00 UTC
Permalink
Raw Message
Post by Philip Wadler
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.
It also (sort of) matches the way mixfix operators work: the fact that you
Post by Ulf Norell
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.
I'm still confused by this. Wouldn't
infixr 40 _←_,_
fit the pattern you describe better than
infixr 40 bind
?
I simply meant that the infix notation of _+_ isn't something separate from
the function _+_.

Writing

infixr 40 _←_,_

would require _←_,_ to be a thing that you could talk about, which (for
better or for worse) is not how
syntax declarations were designed.

/ Ulf
Post by Philip Wadler
Post by Ulf Norell
Phil, rest assured that you are not the only one stumbling over this
design choice.
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
can be read as
print "bind e₁(λ x→ e₂)" as "x ← e₁ , e₂".
This reading emphasizes the uniqueness condition for syntax-attachments
to a identifier ("bind").
And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and treat
it as "bind e₁(λ x→ e₂)".
Best,
Andreas
Post by Philip Wadler
It's great that Agda now has syntax declarations!
infixr 40 bind
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
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/
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
http://www.cse.chalmers.se/~abela/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-03-20 16:47:14 UTC
Permalink
Raw Message
OK, thanks for the clarification. I assume, though, that somewhere there is
a table that records _←_,_ as syntax to parse with precedence 40? 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/
Post by Ulf Norell
Post by Philip Wadler
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.
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.
I'm still confused by this. Wouldn't
infixr 40 _←_,_
fit the pattern you describe better than
infixr 40 bind
?
I simply meant that the infix notation of _+_ isn't something separate
from the function _+_.
Writing
infixr 40 _←_,_
would require _←_,_ to be a thing that you could talk about, which (for
better or for worse) is not how
syntax declarations were designed.
/ Ulf
Post by Philip Wadler
Phil, rest assured that you are not the only one stumbling over this
design choice.
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
can be read as
print "bind e₁(λ x→ e₂)" as "x ← e₁ , e₂".
This reading emphasizes the uniqueness condition for syntax-attachments
to a identifier ("bind").
And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and treat
it as "bind e₁(λ x→ e₂)".
Best,
Andreas
Post by Philip Wadler
It's great that Agda now has syntax declarations!
infixr 40 bind
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
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/
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
http://www.cse.chalmers.se/~abela/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Ulf Norell
2018-03-21 05:42:06 UTC
Permalink
Raw Message
Post by Philip Wadler
OK, thanks for the clarification. I assume, though, that somewhere there
is a table that records _←_,_ as syntax to parse with precedence 40?
Cheers, -- P
Of course. There's a field for syntax associated with each name.

If you're curious it's here:

https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87ac0f01d5c8/src/full/Agda/Syntax/Abstract/Name.hs#L48

and the definition of Fixity' here:

https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87ac0f01d5c8/src/full/Agda/Syntax/Fixity.hs#L39

/ Ulf
Post by Philip Wadler
Post by Ulf Norell
Post by Philip Wadler
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.
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.
I'm still confused by this. Wouldn't
infixr 40 _←_,_
fit the pattern you describe better than
infixr 40 bind
?
I simply meant that the infix notation of _+_ isn't something separate
from the function _+_.
Writing
infixr 40 _←_,_
would require _←_,_ to be a thing that you could talk about, which (for
better or for worse) is not how
syntax declarations were designed.
/ Ulf
Post by Philip Wadler
Phil, rest assured that you are not the only one stumbling over this
design choice.
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
can be read as
print "bind e₁(λ x→ e₂)" as "x ← e₁ , e₂".
This reading emphasizes the uniqueness condition for syntax-attachments
to a identifier ("bind").
And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and
treat it as "bind e₁(λ x→ e₂)".
Best,
Andreas
Post by Philip Wadler
It's great that Agda now has syntax declarations!
infixr 40 bind
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
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/
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
http://www.cse.chalmers.se/~abela/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Philip Wadler
2018-03-21 17:08:17 UTC
Permalink
Raw Message
Thank you! 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/
Post by Ulf Norell
Post by Philip Wadler
OK, thanks for the clarification. I assume, though, that somewhere there
is a table that records _←_,_ as syntax to parse with precedence 40?
Cheers, -- P
Of course. There's a field for syntax associated with each name.
https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87
ac0f01d5c8/src/full/Agda/Syntax/Abstract/Name.hs#L48
https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87
ac0f01d5c8/src/full/Agda/Syntax/Fixity.hs#L39
/ Ulf
Post by Philip Wadler
Post by Ulf Norell
Post by Philip Wadler
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.
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.
I'm still confused by this. Wouldn't
infixr 40 _←_,_
fit the pattern you describe better than
infixr 40 bind
?
I simply meant that the infix notation of _+_ isn't something separate
from the function _+_.
Writing
infixr 40 _←_,_
would require _←_,_ to be a thing that you could talk about, which (for
better or for worse) is not how
syntax declarations were designed.
/ Ulf
Post by Philip Wadler
Phil, rest assured that you are not the only one stumbling over this
design choice.
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
can be read as
print "bind e₁(λ x→ e₂)" as "x ← e₁ , e₂".
This reading emphasizes the uniqueness condition for
syntax-attachments to a identifier ("bind").
And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and
treat it as "bind e₁(λ x→ e₂)".
Best,
Andreas
Post by Philip Wadler
It's great that Agda now has syntax declarations!
infixr 40 bind
syntax bind e₁(λ x→ e₂) = x ← e₁ , e₂
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/
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
http://www.cse.chalmers.se/~abela/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Loading...