[Agda] Agda's syntax declaration

[Martin Escardo]

I shoudn't type so fast without reading what I wrote.

I copied from a development without adapting to this context.

This is what I meant to write.

M,

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