[Agda] Syntax declarations

[Philip Wadler]

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

.   \ 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 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
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180320/977ef6a1/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180320/977ef6a1/attachment.ksh>