agda
[ design ] Re-exports from `Algebra.Properties.X`
Reading over #2695 and its antecedent PRs #2688 and #2692 , I have the feeling that we still haven't quite got the API right for Properties modules:
- it's not obvious that we do, but I think we should, reexport the axioms from the underlying
isX : IsX ...substructure, otherwise we are left in the (slightly?) uneasy position of having to make multiple re-imports to get the 'widest possible' API (so perhaps the design question is more: "how wide should the API be?") - we certainly don't consistently re-export
Algebra.Properties.Y yfor each sub-bundley :Ywhich is re-exported publicly by bundleX, but again, I think that we should (which, if nothing else, would encourage us to improve consistency in naming such properties)
Group is the first really intricate version of the phenomenon, where some recent retrofitting #2251 manages to re-export the underlying Loop and Quasigroup properties, but we still don't re-export the Monoid (and hence Semigroup) properties for the underlying monoid object.
We should improve our documentation of what we (think that we should) do, and try to ensure that we do, indeed, do it!
I agree with both of those suggestions. The only question is whether this is a breaking change because if people have opened both IsX and Properties.X will they get clashes if Properties.X also exports IsX fields? I suspect we probably will...
Happy to badge this as v3.0, not least because that would give us longer to discuss/reflect.
I think my instincts in this context are to make the API as wide as possible cf. #2762 but perhaps there are possibilities to offer users 'narrow' and 'wide' versions (for Structures), and to refactor Properties in similar fashion?
But yes, I think you're right that trying to amalgamate Properties 'in one place' will end up being breaking...
I am definitely a big fan of offering both narrow and wide versions of APIs.
Library developers are going to want to be as precise as possible, with as few dependencies as possible. Users who are merely looking to "get things done" generally want a wide version. It's the difference between "the theory (presentation) of a group" (something rather small) and "Group Theory" (a book's worth of stuff).
@JacquesCarette I take your point, and am conscious of it as a theme running through many (design) issues and PRs over the years, but I think that here my focus is on a more fine-grained choice than simply 'wide' vs. 'narrow': whichever point on the spectrum you choose, there should be some kind of 'hereditary' exposure of the corresponding substructure, up to and including the actual base axiomatisation of the algebraic structure at hand.
We observe that 'hereditary' principle at the level of Structures/Bundles (mostly; though from time to time we find 'holes' that need filling), but apparently not (so much; so systematically) at the level of Properties. Moreover, Properties modules don't reiterate the hereditary re-export of the IsX/IsY base axiomatisation, and I wondered if we could/should. (Mindful of @MatthewDaggitt 's criticism of this as a potentially breaking chnage)
Of course, following through will make the Properties APIs get 'wider', but only to the extent that we design in... and indeed, the underlying drift of this proposal would make IsX the 'narrow' API, and Properties the 'wide' one. It just seems perverse (to me, at least) for a given Properties.X to be more selective about what it exports than those properties already available as Properties.Y for IsY substructures of IsX... but perhaps we *also* need a Properties.NarrowandProperties.Widerefactorisation ofProperties`...?
I personally expect Properties to be 'wide'. I would prefer IsX to be fairly narrow.
In both cases, if a structure X includes a particular property already, then any structure Y that we can retract to an X structure should also have that property available. This exact expectation is why I want to be quite conservative in IsX !