I must say I am with Martin on this. I never understood why the syntax
declarations are backwards. The usual mathematical style is that you
introduce a notation and what it expands to. It is the notation which
is the new thing and whose meaning is defined in terms of things
understood before, and the defined thing is commonly on the left hand
side of the =.
And Ulf, your explanation is very implementation-centric.
I think it was easiest for the user, if declarations of the form
lhs = rhs
could be uniformly be understood as "rewrite lhs to rhs if you are stuck
on with something involving lhs".
If we take a step back, there is two things that we would want from a
notation introduced by a syntax declaration:
1. Have Agda parse it.
2. Have Agda use it when it prints stuff to us.
For 1. it is perfectly fine to have several notations that expand to the
same function symbol or function application.
For 2. having several notations for the same function symbol leads to
more ambiguity. (There is already some ambiguity, because Agda could
print the original function symbol or use the notation.)
As it stands, I deem goal 1. higher in practice, and also, it works
better. For 2. there is an overlapping feature, DISPLAY pragmas, which
can sometimes be used to fix up the printing. (Note that for the
display pragma, DISPLAY lhs = rhs, means "rewrite lhs to rhs for the
purpose of printing", which is the intuitive reading.)
Also, goal 2. does seem to be achieved in practice. For instance,
trying the notation for the Sigma type in Data.Product:
open import Data.Product
goal : ∀{A : Set}{B : A → Set} → Σ[ x ∈ A ] B x
goal = {!!}
Agda prints the goal as
Σ-syntax .A .B
In this case, DISPLAY does not help either,
{-# DISPLAY Σ-syntax A B = Σ[ x ∈ A ] B x #-}
as Agda reports
Not allowed in DISPLAY pragma right-hand side: lambdas
when checking the pragma
DISPLAY Σ-syntax A B = Σ-syntax A λ x → B x
Since the "syntax" facility does not work properly, I don't use it.
Well, the father of the syntax facility ran away soon after the conception.
Cheers,
Andreas
P.S.: Martin, for now you should just memorize to read
syntax lhs = rhs
as "a new syntax for lhs is rhs".
Post by Ulf NorellOk, let me try to be more precise. In your example you are defining a
single thing (id)
```
id.TYPE = {A : Type} → A → A
id.VALUE = {A} x ↦ x
id.SYNTAX = {A} x ↦ x "∶" A
id.FIXITY = infixl 0
```
Contrary to your intuition "∶" is not a thing in its own right, but
simply a terminal symbol in
the parsing rule for id.
/ Ulf
Thanks for you answer, Ulf.
On Fri, Nov 3, 2017 at 11:37 PM, Martin Escardo
Can I say some things about Agda's syntax declaration?
* Why are the definitions backwards (what you define is in the
right-hand side)?
They're not. You are defining the syntax for a particular name
in the same way that
you define the value of a particular name (`syntax f x = bla` vs
`f x = bla`). If syntax
declarations were the other way around you would be very
surprised to find that you
can't have multiple syntax declarations for the same name (which
you can't).
I don't understand this remark. Consider again
```
id : {A : Type} → A → A
id {A} x = x
syntax id {A} x = x ∶ A
infixl 0 id
```
In the syntax definition, I have *already* define id (occurring in
the left-hand side), and the new thing I am *defining* in the syntax
declaration is ":", which occurs in the *right*-hand side.
At first I tried to define ":" to be left-associative, but this
didn't work. Then cheating from other people's examples I realized
that one is expected to define `id` to be left-associative. I didn't
answer the question myself as you suggest: I still don't know what
it means for id to be left-associative. :-) The above works and is
useful, but I don't understand it.
Best,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
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/