[Agda] Syntax declarations

[Ulf Norell]

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/48cb2b8c/attachment.html>