Inconvenient precedences

[JacquesCarette]

As I was setting A3 for my course using PLFA, one of the exercise was:

Prove the following:

⊎-comm : ∀ {A B : Set} → (A ⊎ B) ↔ (B ⊎ A)

where _⊎_ is from Data.Sum.Base and declared infixr 1 _⊎_ and _↔_ is from Function.Bundles and declared infix 3 _↔_. The first is as per README.Design.Fixity but the second doesn't correspond to anything in there.

The problem, of course, is that this leads to needing parens where there really shouldn't be a need for them. The same holds for all the rest of the combinators in Function.Bundles.

Unsurprisingly, PLFA defines all of these combinators to be at level 0 instead.

We should change these. Level 0 seems right. Yes, strictly speaking, this would be a 'breaking' change. Except that I don't think it would break any existing code is current code would have had to put in parentheses (unless they were doing something extremely weird with unions or products of equivalences).

cc: @wenkokke @wadler .

[JacquesCarette]

To be clear: I regard this as a bug (a usability bug) that should be fixed, even though it might break some odd code.

[wadler]

Thanks for the CC on this message, Jacques.

PLFA defines all of these combinators to be at level 0 instead.

If so, that's an oversight. PLFA tries to align with the Standard Library almost everywhere. Go well, -- P

…

________________________________ From: Jacques Carette ***@***.***> Sent: 20 December 2024 16:41 To: agda/agda-stdlib ***@***.***> Cc: Philip Wadler ***@***.***>; Mention ***@***.***> Subject: [agda/agda-stdlib] Inconvenient precedences (Issue #2531) This email was sent to you by someone outside the University. You should only click on links or attachments if you are certain that the email is genuine and the content is safe. As I was setting A3 for my course using PLFA, one of the exercise was: Prove the following: ⊎-comm : ∀ {A B : Set} → (A ⊎ B) ↔ (B ⊎ A) where _⊎_ is from Data.Sum.Base and declared infixr 1 _⊎_ and _↔_ is from Function.Bundles and declared infix 3 _↔_. The first is as per README.Design.Fixity but the second doesn't correspond to anything in there. The problem, of course, is that this leads to needing parens where there really shouldn't be a need for them. The same holds for all the rest of the combinators in Function.Bundles. Unsurprisingly, PLFA defines all of these combinators to be at level 0 instead. We should change these. Level 0 seems right. Yes, strictly speaking, this would be a 'breaking' change. Except that I don't think it would break any existing code is current code would have had to put in parentheses (unless they were doing something extremely weird with unions or products of equivalences). cc: @wenkokke<https://github.com/wenkokke> @wadler<https://github.com/wadler> . — Reply to this email directly, view it on GitHub<#2531>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ABFJ7MWMLCDSVEI6BDHB4IL2GRCE3AVCNFSM6AAAAABT7O266GVHI2DSMVQWIX3LMV43ASLTON2WKOZSG42TGMBYGY3TSMI>. You are receiving this because you were mentioned.Message ID: ***@***.***> The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

[jamesmckinna]

'Obvious' question(s):

• what is the precedence of the function space arrow _->_? (Maybe it's too below the surface of syntax even to be exposed as such)
• Should we regard the proposal/usability argument essentially to amount to saying all such hom-objects should have the same precedence, not just those arising from Function.Bundles?

[JacquesCarette]

@wadler : I think PLFA got it right here. (It's not the only place - I've got more issues incoming, when I find the time.)

@jamesmckinna :

• I don't think it has a 'published' precedence? Reading things here and there, it behaves as if it has arbitrarily low (i.e. -infinity) precedence (and right-associative)
• I don't know about all 'hom-objects', but certainly all type-level binary relations should have the same precedence (likely 0).

[jamesmckinna]

@JacquesCarette I'm very much in sympathy with the spirit of the proposal, but find it isn't easy to find a consistent live once indexing plays a role: the various indexed analogues of Function.Bundles for eg unary predicates, are all declared at infix 4... (I haven't looked at dependent nodes of the Function hierarchy yet...)

[JacquesCarette]

Those were likely "just done", as there is nothing in our guidelines that would tell you what fixity these should have. More legacy.

[jamesmckinna]

From style-guide under Fixity:

• General operations and relations

* binary relations of all kinds are `infix 4`

• Type formers

* binary properties `infix 4 _Absorbs_`

So... we did have some sort of guideline in place...the solution would appear to be to add an additional item under Type formers, and to agree whether the 'arrows' under Unary etc. are 'binary properties' or 'type formers'...?

* function-space-like `infixr 0 _↔_`

[JacquesCarette]

Yes, I think adding a case under Type formers would make sense.

I definitely see the various kinds of equivalences (defined under Function.Bundles) as being "properties" (even though they, strictly speaking, are 'structure' - but I think the problem here is a confusion between 'property' a la HoTT and how it is used in stdlib).