[Agda] Syntax declarations

[Philip Wadler]

Thank you! 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/

On 21 March 2018 at 02:42, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/b9461927b33d4b93005e723033be87
> ac0f01d5c8/src/full/Agda/Syntax/Abstract/Name.hs#L48
>
> and the definition of Fixity' here:
>
> https://github.com/agda/agda/blob/b9461927b33d4b93005e723033be87
> ac0f01d5c8/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/69b68f4d/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180321/69b68f4d/attachment.ksh>