Reconciling `Data.Nat.Divisibility.Core._∣_` and `Algebra.Definitions.RawMagma._∣_`

[jamesmckinna]

The substance of the issue (for the additive fragment of Nat) is already discussed in #1919, but that issue can (should!) be closed by merging #1948. So this is a placeholder to work on this specific problem in the multiplicative fragment of Nat.

Carrying over the summary from #2013:
Two Three parts to this:

• low-hanging fruit: added pattern synonym and consequences/uses of it to Data.Nat.* (merged in Reconciling Data.Nat.Divisibility.Core._∣_ and Algebra.Definitions.RawMagma._∣_ #2013)
• higher-hanging fruit: reconcile the two definitions of _∣_ for the Data.Nat.Base.*-rawMagma instance
• knock-on changes for Data.Integer.Divisibility.* and Data.Rational.* only if the preceding step succeeds

cf. #679

[jamesmckinna]

Picking this up again on the back of #2604.

There seem to be two directions to go in (once again: flip symmetry!)

• redefine Data.Nat.Divisibility.Core._∣_ in terms of Algebra.Definitions.RawMagma *-rawMagma, renaming _,_ to divides, and then having to fix up all the uses in Data.Nat/Data.Integer/Data.Rational uses with appropriate sprinkles of symmetry
• redefine Algebra.Definitions.RawMagma._∣_ to flip the direction of the equality fields, etc.

Personally, I think that the latter is the better course of action, but may cause problems for external clients of stdlib such as @mechvel 's libraries.

TL;DR: heuristic should read

complicated/unknown = simpler/known

However, I think it is the better choice, because of the following refinement of the complicated = simple heuristic which has emerged in writing equations in the library, as discussed elsewhere (I can't remember off the top of my head, but I was the one making the point, about mode of an equation... how do we search GitHub comments for these things?) namely:

• complicated might only appear as a variable name in the stated equation, but it will be used in a context where that variable sis instantiated with an arbitrarily complicated expression... whereas
• simple might be a superficially more complicated RHS expression than the LHS, but is appearing in a 'standard' form. moreover one which instantiates its sub-terms upon application of the relevant lemma.

For divisibility, I'm imagining that we want equality to accept an arbitrary LHS, and then to re-express it on the RHS as a known product of factors. Currently the definitions in Algebra.Definitions.RawMagma._∣_ are the 'wrong way round' for that reading... with a lot of bogus/redundant appeals to sym as a consequence.

[jamesmckinna]

Suggest also, for technical reasons, that we do not export _∣_ as a definition in its own right when observing the convention that, for commutative monoid operations, it be 'taken as read' that it refers to right-divisibility. Rather, in the spirit of reducing module-local cognitive load, that the user should make that choice clear when importing divisibility via a renaming declaration... which makes explicit what is going on 'in place'. cf. some of @JacquesCarette 's and @MatthewDaggitt 's recent comments.

Or else that if we do want to retain the existing convention, that we make it a module definition, rather than a flat type definition, because that plays better with open/renaming etc. of the fields of the associated record on subsequent (possibly qualified) import. Or at least, that how it seems for me when experimenting with these choices... shout-out to @gallais for comment on this in the context of #2604 (it would, of course, be a breaking change, so maybe belongs in a separate PR.

[mechvel]

Please, remain the general _∣_ definition untouched.
My library uses the general _∣_ widely. Its definition has been changed once, respectively this required an effort of me to change much of code. Now you go with the next round. I disliked the first change, and do not understand the reasons for the future one.

[MatthewDaggitt]

I don't have much to add except that, for different reasons, both seem bad...

[mechvel]

I recall the story. Initially it was

_∣_ :   Rel A _
x ∣ y = ∃ \ q → q ∙ x ≈ y

(transpositions possible).
It was the best and the most mathematically natural : "x divides y iff there exists a quotient element".

Then it was changed and put to the official version without asking people.
I complained, and still have spent effort to change my large application.
Now you start the next round.
Please, either remain with existing version or return to the initial definition of ∃ \ q → q ∙ x ≈ y.

[jamesmckinna]

I don't have much to add except that, for different reasons, both seem bad...

'both' meaning each of the two suggestions as to how to solve the DRY problem?

I'm not sure whether you're really saying that abstract and concrete divisibility should remain apart... which doesn't seem right/desirable (to me, at least)

[jamesmckinna]

@mechvel i shouldn't relitigate the earlier breaking change, except to say:

• (pragmatic) the type checker performs better when not overloading the 'standard' existential quantified in the old way to which you would have us return; custom records ensure things are 'standardised apart'
• (type-theoretic) records in (Agda's) dependent type theory are conceptually prior to their use in representing the orthodox first-order existential quantified. They are moreover extensible with additional manifest fields, and thus more flexible as a representation mechanism than the fixed (closed) definition you advocate.

For better or worse, we are now in a phase of library development which goes beyond v2.0: v2.3 involving non-breaking, 'conservative' changed, and v3.0 as the opportunity to clean up a lot of suboptimal legacy design decisions, many of which have emerged over the course of the sustained scrutiny to which the library has been subjected since v1.*

I'm sorry to hear that the v2.0 changes are still causing you problems, especially given that the v2.0 change to divisibility retained the shared constructor name_,_ in the interests of backwards compatibility.

[mechvel]

I'm sorry to hear that the v2.0 changes are still causing you problems

a) I thought that ∃ \ q → q ∙ x ≈ y was the best definition.
b) v2.0 changes forced my considerable effort to make changes in my program. But it does not cause further problems for me.
c) As you are going to do further changes in the divisibility definition, I expect the next round with problems.

[jamesmckinna]

@mechvel , regarding:

c) do you mean problems with abstract divisibility, or concrete? I have already indicated above that while I may regard changing the latter in favour of the definition of the former as potentially less desirable than the other way round, if it minimises the knock-on consequences of this change, then fine by me. If both are affected, then it would be helpful to get an estimate of who much is affected in each direction, since the purpose of any PR fixing this issue would be to have a single, unitary definition applicable across both situations, and for historical/legacy reasons, this has sadly not been the case.

b) it would be useful to understand how, and the extent, of the changes you had to make after the v2.0 change, either in terms of lines of code, or in terms of typechecking time, or in terms of the abstractions used in your library. One reason the previous change retained the _,_ for both products/existentials and divisibility, was to permit pattern-matching definitions to remain unchanged. But obviously the record field/projection names changed, so if you used those heavily, I can see that there might have been problems (developing strategies for mitigating those problems is a separate question). It would be useful for further development of the field of dependently-typed programming in general to understand the tensions/trade-offs between conventional software engineering practices in terms of abstraction, programming to an interface, etc. stand up against the opportunities/temptations afforded by a programming style (incl. the use of pattern-matching) which encourages abstractions to be exposed, perhaps harmfully. In this regard, a link to the 'before-v2.0' and 'after-v2.0' versions of your library would be helpful, for the sake of comparison, if you are willing/able to share those.

a) this issue seems intractable unless we can agree sensible measures against which to judge 'best'. At the moment there is simply an impasse between conflicting views.

Currently, this is (only) an open issue, without any accompanying PR on which to discuss details of the design decisions involved. But I think that in the long term, the standard library should aim to resolve this issue positively rather than maintain what are in effect two distinct codebases for the same concept, with all that that entails in terms of code duplication, maintenance overhead, etc.