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:

• [x] low-hanging fruit: added pattern synonym and consequences/uses of it to Data.Nat.* (merged in #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.

[mechvel]

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.

About `best': \ because ∃ \ q → q ∙ x ≈ y is a mathematically clear definition. When you define it as a record, you force a user to think about a programming language specifics, about record etc, instead of thinking about divisibility.

But I do not know about the implementation possibilities. So, let the team decide, as always, you know better..
If a record for divisibility in v2.2 (v2.0 ?) is much better for implementation, all right.
I only complained on a sudden change in the official version, without asking users.

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.

Nothing particular. Just many places have become errors, and I needed to import the divisibility items somewhat in a different way. I do not recall now, why. Maybe importing from Data.Product using (_,_) to be changed with something, I do not recall.

import Algebra.Properties.Magma.Divisibility as DivPropMagma                    
...                                                                             
open DivPropMagma M public                                                      
                                                                                
∣resp :  _∣_ Respects2 _≈_                                                      
∣resp {x} {x'} {y} {y'} x≈x' y≈y' (q , qx≈y) =  (q , qx'≈y')                    
      where                                                                     
      ...                                                                       

May be, the necessity to write open _∣ʳ_, how does it correlate with the parts of _×_ ...

module OfCommutativeSemigroup {α α≈} (S : CommutativeSemigroup α α≈)            
  where                                                                         
  open CommutativeSemigroup S                                                   
                                                                                
  open OfSemigroup            semigroup  public hiding (_≉_; x∙yz≈xy∙z)         
  open OfComSemigroupStandard S          public                                 
  open OfComSemigroupDiv S public using (xy≈z⇒x∣z; ∣-factors; ∣-factors-≈)      
                                                                                
  open _∣ʳ_                                                                     
                                                                                
  ∣x⇒∣xy :  ∀ {z} x y → z ∣ x → z ∣ x ∙ y                                       
  ∣x⇒∣xy {z} x y z∣x =  ∣-respʳ (comm y x) (∣x⇒∣yx y z∣x)                       
                                                                                
  ∣⇒quot∣ :  ∀ {x y} (div : x ∣ y) → (quotient div) ∣ y                         
  ∣⇒quot∣ {x} {y} (q , qx≈y) =  x , xq≈y                                        
                                where ...                                       

Earlier I wrote f (q , qx≈y) = ...
And now I write open _∣ʳ_ using (quotient; equality) ...

I do not recall, no real problems, just many places to fix in a simple way, and - without understanding, why, with a feeling of unnecessary complication.
The main matter was that this was done without asking users.

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.

How it was in lib-1.7.1 it can be seen in
http://www.botik.ru/pub/local/Mechveliani/inAgda/admissiblePPO-wellFounded.zip

This small library must be type-checked - under the system required in readme.txt.
See readme.txt,
sourse/GenAlgebra-I.agda, Nat/*.agda, everywhere where _∣_ occurs.

How it is currently in my general library for computer algebra under lib-2.2, see in the attached archive
onDivisibility.zip.

This is not self-contained.
These are the three modules from the library which is under preparation.

onDivisibility.zip

c) do you mean problems with abstract divisibility, or concrete?

I pay attention only to abstract divisibility --- for Magma in general.

As to Nat, Integer, Binary, they have the instances of multiplicative Magma and additive Magma. So each of them has two instances of the divisibility, and they do not need any special divisibility as open.

Personally I do not use special divisibility on Nat, Integer, Binary.
For example, my application declares in certain modules for ℕ:

open import Data.Nat.Divisibility using ()                                      
                               renaming (_∣_ to _∣adHoc_; divides to dividesℕ)  
                                                -- to fix _∣_ for ℕ in lib-2.0  
                                                                                
open Divisibility ℕ-props.*-magma using (_∣_; _∤_; _,_)                         
                                  -- use general divisibility from Standard     
                                                                                
-- This is a fix _∣_ for ℕ in standard lib-2.0                                  
∣adHoc⇒∣ :  _∣adHoc_ ⇒  _∣_                                                     
∣adHoc⇒∣ (dividesℕ q y≡qx) =  q , (sym y≡qx)                                    
                                                                                
∣⇒∣adHoc :  _∣_ ⇒  _∣adHoc_                                                     
∣⇒∣adHoc (q , qx≡y) =  dividesℕ q (sym qx≡y)                                    
...                                                                             
                                                                                

This is annoying to write and read such pieces of code.

Now you are going to do further changes. This is a certain danger.

[mechvel]

I am trying to understand what promises your phrase

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.*

"legacy -- A gift of property by will, ...".
legacy decisions -- I guess these are decisions inherited from past (?).

suboptimal -- close to optimal or in-optimal?
sustained scrutiny -- durable study?

Finally I applied the program translator to Russian, and now translate its result myself to English.
Probably your phrase is more of English, but I provide my translation in order to know of whether I understand the meaning:

"and v3.0 as a possibility to fix many in-optimal out of date design decisions, many of which have emerged over the course of the durable study to which the library has been subjected since v1.*"
?

[mechvel]

I wrote

How it was in lib-1.7.1 it can be seen in http://www.botik.ru/pub/local/Mechveliani/inAgda/admissiblePPO-wellFounded.zip

As you are going to look into this source, your comments are welcome in general.

[jamesmckinna]

Re: hard to understand English... Apologies for this! Hopefully the following is better (but it's hard for me to judge)

• re: "legacy"/"suboptimal" the library has accumulated lots of modules, contributed developed at different times, and not always either in the 'best' way, or in ways consistent with existing other modules. v2.0 represented a lot of work to tackle this problem, and we hope in v3.0 to have another iteration of this process. The drive to streamline various definitions (here: the distinct versions of abstract and concrete divisibility) is part of that process.

[jamesmckinna]

Re: v2.0 changes We precisely retained the _,_ constructor for the definition of divisibility so that definitions previously of the form

Earlier I wrote f (q , qx≈y) = ...

should still have typechecked correctly. If they did not, then I am sorry, not least for only learning about this now.

[jamesmckinna]

Re: the proposed changes here The minimal change would indeed be to find a way to avoid the annoyance of having to write

-- This is a fix _∣_ for ℕ in standard lib-2.0                                  
∣adHoc⇒∣ :  _∣adHoc_ ⇒  _∣_                                                     
∣adHoc⇒∣ (dividesℕ q y≡qx) =  q , (sym y≡qx)                                    
                                                                                
∣⇒∣adHoc :  _∣_ ⇒  _∣adHoc_                                                     
∣⇒∣adHoc (q , qx≡y) =  dividesℕ q (sym qx≡y)                                    

The larger scale proposal at the top considered also:

• changing the orientation of the equation (I could imagine this might be a big pain to change, so is not 'essential', although I have argued above for how/why it might be desirable)
• changing the definition not of divisibility, but of mutual divisibility in order to profit from the recent addition of Relation.Binary.Construct.Interior.Symmetric to the library, but again this is not essential (although again in the spirit of making things 'less ad hoc')

So it is useful to have your feedback on each of those.

As to the issues regarding ongoing changes to the library, I regard this as inevitable given the continued growth and evolution of the library. What is harder to achieve in a volunteer, distributed effort such as stdlib, is that we somehow are able to arrive at 'perfect' decisions that are correct first time, for all time. Hence the periodic phases of large-scale 'breaking' changes.

[mechvel]

I do not believe that the above two possible changes have sense. And even if they do, they do not worth the dispenses they would cause for users.

[mechvel]

I keep on asking the team to return to the definition

∃ \ q → q ∙ x ≈ y                                                               

For example, I have in the name space

1. divisibility _∣_ in ℕ with respect to its *-magma,

2. divisibility _∣⁺_ in ℕ with respect to +-magma,
   (where m ∣⁼ n means m + d ≡ n for some d).

3. divisibility _∣⁺ₗ_ in List ℕ with respect to +ₗmagma
   fot the pointwise summing of lists over _+_.

4. divisibility _∣ₑ_ in PP = Σ (List ℕ) NoLast0)
   with respect to +ₑmagma, defined as e ∣ₑ e' = (proj₁ e) ∣⁺ₗ (proj₁ e')

Now, under lib-2.2,
a proof for _∣_ is denoted (q , q*m≡n) is the code,
a proof for _|⁼_ is denoted (q ,+ q+m≡n),
a proof for _|⁺ₗ_ is denoted (qs ,+l qs+ₗxs≋ys).
a proof for _|ₑ_ is denoted (q ,ₑ q+ₑe=ₑe').

And it is needed (for operations over List ℕ, over PP ) an import like

open Dec2CommutativeMonoid ∙ₗDec2CommutativeMonoid public using (...)           
  renaming                                                                      
    (_∙_ to _+ₗ_; ... _∣_ to _∣⁺ₗ_; _,_ to _,l+_; _∣?_ to _∣⁺ₗ?_)               
                                                                                
open OfMagma-I +ₑMagma using() renaming (_∣_ to _∣ₑ_; _,_ to _,ₑ_)              

And in old library, all these divisibilty proofs where constructed with the same _,_ pair constructor; much of import renaming is saved, the code is easier to write and read.

Another reason is that it follows clearly the algebra notion of divisibility.