search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
583 stars 236 forks source link

Get rid of inconsistent `homo` name in algebra hierarchy? #2458

Open jamesmckinna opened 2 months ago

jamesmckinna commented 2 months ago

Revisiting #1544, I am (now) conscious that the opposite choice is already made regarding the name of the homomorphism property in Algebra.Morphism.Structures.IsMagmaHomomorphism, which for whatever reason, is called homo, whereas all the subsequent field names for such properties are tagged by the associated piece of syntax, viz. ε-homo for IsMonoidHomomorphism, etc.

Correspondingly, congruence for ⁻¹_ is ⁻¹-cong in the definition of Algebra.Structures.IsGroup... etc.

So I'm tempted to conclude that we should, in fact, retain the name ∙-cong, and moreover rename Algebra.Morphism.Structures.IsMagmaHomomorphism.homo to ∙-homo...?

This seems to arise from the v1.5 deprecations in Algebra.Morphism, some of whose definitions (moreover of syntax!) nevertheless still appear in eg Data.Nat.Properties (thanks to suppression of the deprecation warnings... sigh)

UPDATED: seemingly only 15 uses of such homo in the library needing to be updated?

Originally posted by @jamesmckinna in https://github.com/agda/agda-stdlib/issues/1544#issuecomment-2258438936

This is the 'complementary'/'counter' issue to #1544 , again in pursuit of consistency/uniformity, but in the 'opposite' direction to that issue. In such a narrow sense, we should agree to solve only one of these, and not the other, but in the interests of a 'balanced' discussion, worth separating out, I think!?

UPDATED: looking at #2464 it seems that there are in fact 21 bindings of the field name, and a further 23 uses of it... assuming that I have caught them all!

JacquesCarette commented 2 months ago

The data, at the time, didn't support my 'hunch' that ∙-cong was the better way to go.

Really, cong for an n-ary operator should take that operator symbol as input, rather than as a baked-in name. But I don't think Agda is ready for that, so ∙-cong is the current best that can be done?

jamesmckinna commented 2 months ago

While I agree with the general principle that cong (and homo!) should key off the (arity of the) symbol being characterised... if we attempted that we'd get so much ambiguity in the field names as the record hierarchy builds up that I just don't think Agda could cope...

... so the conclusion I drew as regards ∙-cong was, as here, to stick with status quo (contra @MatthewDaggitt ) for that name, and hence for consistency's sake to emulate that here for homo...

JacquesCarette commented 2 months ago

Right - I did want to abstractly discuss hypothetical-rewrite, and agree that the current best solution is to embed the name of the operation in the name, consistently.

MatthewDaggitt commented 2 months ago

Okay, happy to go with embedding the name as part of the operator as standard!

jamesmckinna commented 2 months ago

@JacquesCarette comments as to whether this would be a breaking change? On that basis, so too should this issue be!