Agda-stdlib: operator precedents are too tight

[HuStmpHrrr]

I once a while find that the precedent settings are probably suboptimal.

In particular, I find the precedents have the following problems.

1. the range of usage is too short. the default precedent is 20, but stdlib clusters most of the operators (0, 10). therefore, a new operator is very hard to get an appropriate precedent
2. the precedent settings are too localized. namely, the settings only consider the precedents of the operators that are immediately related. however, this in general does not serve well when the program gets larger.

to give concrete example, in https://github.com/agda/agda-stdlib/blob/master/src/Data/Product.agda

infixr 4 _,′_
infix 4 -,_

while https://agda.readthedocs.io/en/v2.5.4.2/language/built-ins.html#equality

infix 4 _≡_

that is, product constructor has the same precedent has propositional equality. this is quite inconvenient as product constructor should have higher precedent as it's very often considered as data constructor.

on the other hand, for some reason, monad operators have very low precedents:

https://github.com/agda/agda-stdlib/blob/master/src/Category/Monad/Indexed.agda

  infixl 1 _>>=_ _>>_ _>=>_
  infixr 1 _=<<_ _<=<_

[MatthewDaggitt]

It's a good point. I guess as a starting point we could multiply everything by something? 2? 3? The only problem is this might cause quite a lot of problems with people's existing code...

If we're going to do this we should do it before v1.0 releases (hopefully next month).

[HuStmpHrrr]

yes. it's a breaking change, but i hope it's going to generate more benefit. otherwise i am not sure what can be a better fix.

not having enough choice of precedent is an unnecessary pain, especially when agda users like notations.

[HuStmpHrrr]

i'd suggest to make x5, so that the precedent of equality can match up with the default precedent. or x4 to make it a bit lower than default so that when people define data, equality can behavior less annoying.

[MatthewDaggitt]

Sounds reasonable. Let's leave it a few days and see if anyone else has anything to chip in? After that feel free to open a PR.

[JacquesCarette]

I agree, x5 sounds good.

[HuStmpHrrr]

I pulled some stats:

$ find . -type f -name '*.agda' -exec grep infix {} + | sed -E -n 's/.*infix.? ([0-9]+) .*/\1/p' | sort -n | uniq -c
     11 0
     40 1
     23 2
     27 3
    172 4
     71 5
     44 6
     52 7
     25 8
     21 9
     12 10

in fact, I just realized that the precedents are involved by the upstream builtin library: https://github.com/agda/agda/blob/26a26b4fe9f3909cf62e4150f20eab17959c27aa/src/data/lib/prim/Agda/Builtin/Equality.agda, which makes me think that it's probably better if agda allows rebind precedents.

[andreasabel]

Alternatively, we should investigate whether we introduce rational precedences into Agda, to get rid of problems like that once and for all.

[HuStmpHrrr]

I like how the syntax looks like in your reply in the other issue:

open Product using (_×_) renaming (_,_ to infixr 5 _∷_)

but I don't think it's rewarding to spend time on investigating reasonability of precedence of every symbol. the central issue is that the usage of range is so much clustered than what the parser supports, so the limited resources must induce limited choice. the stats shows that when people choose a precedence, the common choice must lie in the middle part of the distribution and the chances descend if deviate from that, which follows the nature of statistics, and therefore the solution is to provide larger range for the middle part, instead of trying to reason about every combination of usage of all notations.

[MatthewDaggitt]

Removing this from v1.0 release as hopefully the discussion in https://github.com/agda/agda/issues/3574 will come up with a backwards compatible way of doing this.

[nad]

Alternatively, we should investigate whether we introduce rational precedences into Agda, to get rid of problems like that once and for all.

I'm not sure that a total ordering of precedences is the best possible design.

[MatthewDaggitt]

Addressed by agda/agda#3992 which added fractional precedents, yay!

[HuStmpHrrr]

yaaaaaay!