[Agda] Syntax declarations

[Philip Wadler]

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

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