[Agda] Syntax declarations

[Ulf Norell]

On Tue, Mar 20, 2018 at 5:47 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> OK, thanks for the clarification. I assume, though, that somewhere there
> is a table that records _←_,_ as syntax to parse with precedence 40?
> Cheers, -- P
>

Of course. There's a field for syntax associated with each name.

If you're curious it's here:

https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87ac0f01d5c8/src/full/Agda/Syntax/Abstract/Name.hs#L48

and the definition of Fixity' here:

https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87ac0f01d5c8/src/full/Agda/Syntax/Fixity.hs#L39

/ Ulf

On 20 March 2018 at 12:34, Ulf Norell <ulf.norell at gmail.com> wrote:
>
>>
>> On Tue, Mar 20, 2018 at 3:02 PM, Philip Wadler <wadler at inf.ed.ac.uk>
>> wrote:
>>
>>> Thanks, Ulf and Andreas. Thinking of it in terms of printing an internal
>>> tree, rather than parsing to create an internal tree, explains a lot.
>>>
>>> It also (sort of) matches the way mixfix operators work: the fact that
>>>> you can write `x + y` for `_+_ x y` is a property of the name `_+_` and not
>>>> a separate entity that may or may not be in scope.
>>>
>>>
>>> I'm still confused by this. Wouldn't
>>>
>>> infixr 40 _←_,_
>>>
>>> fit the pattern you describe better than
>>>
>>> infixr 40 bind
>>>
>>> ?
>>>
>>
>> I simply meant that the infix notation of _+_ isn't something separate
>> from the function _+_.
>>
>> Writing
>>
>> infixr 40 _←_,_
>>
>> would require _←_,_ to be a thing that you could talk about, which (for
>> better or for worse) is not how
>> syntax declarations were designed.
>>
>> / Ulf
>>
>>
>>> On 19 March 2018 at 06:54, Andreas Abel <abela at chalmers.se> wrote:
>>>
>>>> Phil, rest assured that you are not the only one stumbling over this
>>>> design choice.
>>>>
>>>> My explanation attempt:
>>>>
>>>>   syntax  bind e₁(λ x→  e₂)  =  x ← e₁ , e₂
>>>>
>>>> can be read as
>>>>
>>>>   print "bind e₁(λ x→  e₂)" as "x ← e₁ , e₂".
>>>>
>>>> This reading emphasizes the uniqueness condition for syntax-attachments
>>>> to a identifier ("bind").
>>>>
>>>> And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and
>>>> treat it as "bind e₁(λ x→  e₂)".
>>>>
>>>> Best,
>>>> Andreas
>>>>
>>>>
>>>> On 18.03.2018 14:22, Philip Wadler wrote:
>>>>
>>>>> It's great that Agda now has syntax declarations!
>>>>>
>>>>> I'm confused by the design. What is implemented is:
>>>>>
>>>>> infixr  40  bind
>>>>> syntax  bind e₁(λ x→  e₂)  =  x ← e₁ , e₂
>>>>>
>>>>> Whereas what I would have expected is:
>>>>>
>>>>> infixr  40  _←_,_
>>>>> syntax  x ← e₁ , e₂ = bind e₁(λ x→  e₂)
>>>>>
>>>>> Can someone please enlighten me as to the rationale behind the current
>>>>> design? Cheers, -- P
>>>>>
>>>>>
>>>>> .   \ Philip Wadler, Professor of Theoretical Computer Science,
>>>>> .   /\ School of Informatics, University of Edinburgh
>>>>> .  /  \ and Senior Research Fellow, IOHK
>>>>> . http://homepages.inf.ed.ac.uk/wadler/
>>>>>
>>>>
>>>>
>>>> --
>>>> 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/
>>>>
>>>>
>>>
>>> The University of Edinburgh is a charitable body, registered in
>>> Scotland, with registration number SC005336.
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180321/8d79781c/attachment.html>