[Agda] Agda's syntax declaration

[Martin Escardo]

Sorry, Type was Set, I copied frin a development with adapting to this
context.

Type = Set.

M.

On 03/11/17 23:02, Martin Escardo wrote:
> 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