[Agda-dev] 2.4.4 roadmap

[Andreas Abel]

On 08.10.2015 15:09, Nils Anders Danielsson wrote:
 > ...
> I looked at an operator-heavy Agda development that can be found online,
> and noted why parsing failed. I could find four different reasons:
>
> (1) The default precedence of syntax declarations has changed from -666
>      to 20.
>
> (2) An operator was in scope with multiple, inconsistent fixities (and
>      not disambiguated by the context).
>
> (3) Code of the form TERM INFIX TERM INFIX TERM, PREFIX TERM INFIX TERM
>      or TERM INFIX TERM POSTFIX (with matching precedences).
>
> (4) Code of the form TERM INFIX PREFIX TERM or TERM POSTFIX INFIX TERM
>      (with matching precedences).
>
> I think code falling under (2) and (3) should be rejected, and I don't
> think we should have multiple default fixities.

For (2), we should have add away to change fixities during import.  See 
issue 1346.

Agreed, (3) should be rejected.

> The only remaining case is (4). In some cases I could fix both (3) and
> (4) at the same time, by introducing a fixity declaration. The
> number of remaining cases was small. If people have to update their code
> anyway, due to (1)-(3), then the additional cost of (4) might be
> negligible.

(4) not working is counterintuitive.  Although the additional cost in 
loc may be low, the psychological barrier ("but this SHOULD work") might 
be high.

> As we have discussed before it is probably possible to handle (4).
> However, this would make the grammar more complicated, so I would prefer
> not to do this.
>
>> I am for postponing the release of the new operator parsing.  Sections
>> depend on it, but are they already stable?
>
> I'm using sections frequently, and don't currently see a need for
> changing anything.
>
>> (There are issues with bloated error messages.)
>
> I tried to fix this during the last Agda meeting. Is this still an
> issue?

I don't know, I missed the meeting.
(I had put that in parentheses as I was not sure).

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/