[Agda] Agda's syntax declaration

[Andreas Abel]

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".

On 04.11.2017 10:29, Ulf Norell wrote:
> Ok, let me try to be more precise. In your example you are defining a 
> single thing (id)
> with multiple properties. You can read it as something like this:
> 
> ```
> 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
> 
> 
> On Sat, Nov 4, 2017 at 8:44 AM, Martin Escardo <m.escardo at cs.bham.ac.uk 
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
> 
>     Thanks for you answer, Ulf.
> 
>     On 04/11/17 06:33, ulf.norell at gmail.com
>     <mailto:ulf.norell at gmail.com> wrote:
> 
> 
>         On Fri, Nov 3, 2017 at 11:37 PM, Martin Escardo
>         <m.escardo at cs.bham.ac.uk <mailto:m.escardo at cs.bham.ac.uk>
>         <mailto:m.escardo at cs.bham.ac.uk
>         <mailto:m.escardo at cs.bham.ac.uk>>> wrote:
> 
>              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
> Agda at lists.chalmers.se
> 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

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/