[Agda] Agda's syntax declaration

[Martin Escardo]

Here is a particular (useful) concrete instance of the phenomenon I
discussed in the previous message:

```
id : {A : Type} → A → A
id {A} x = x

syntax id {A} x = x ∶ A

infixl 0 id
```

Here the symbol "∶" is the unicode one, not the Ascii one that is
built-in in Agda for type declarations.

This allows you to

  * Say "x" with an explicit description of its type, by writing "x ∶ A"
(like in Haskell)

  * This can be for clarity (the human reader of your Agda proof).

  * For disambiguation (the computer reader of your Agda proof).

This also allows, with the associativity for id (!), to write things such as

   * x ∶ A
       ∶ A'

to emphasize that the defined type of x is A, but is definitionally
equal to A' in a complex proof that we want not only Agda to approve of,
but also people to understand and appreciate.

Anyway, this was just a successful example of a use of "syntax", by
guesswork

Please, Agda developers, tell us the precise syntax of syntax.

Best,
Martin


On 03/11/17 22:37, Martin Escardo 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)?
> 
> * There isn't any precise definition, as far as I know, of the syntax of
> syntax.
> 
> * And there isn't much documentation, as discussed.
> 
> * And it is impossible to google search for "Agda syntax" (say) because
> this gives answers about Agda's syntax, and not about the "syntax"
> keyword. (And it doesn't help to search for "Agda syntax" or "Agda
> syntax keyword" or "Agda syntax declaration".)
> 
> Anyway, after heroic guesswork, I managed to make some useful things to
> work nicely using "syntax". (So thanks for implementing this feature!)
> 
> Definitely the most mysterious thing, to make such things work, was to
> declare the (polymorphic) identity function as an infix left-associative
> operator with priority 0:
> 
> infixl 0 id
> 
> This does work (for some things I've done), but I am not sure how I
> figured it out (it is not documented), and I still don't know what
> making the identity into an infix left-associative operator means.
> 
> :-)
> 
> Enjoy the weekend.
> 
> Best,
> Martin
> 
> On 03/11/17 21:51, nad at cse.gu.se wrote:
>> On 2017-11-03 16:58, Andrea Vezzosi wrote:
>>> About the list syntax, I was able to find this gist, not sure how well
>>> it works in practice though.
>>>
>>> https://gist.github.com/bishboria/8568581
>>
>> Note that regular list literals have the advantage that there is no need
>> to give parentheses around list elements, or around list literals.
>>
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe