Splitting files in Algebra

[thomas-lamiaux]

We were talking about the files organization inside of Algebra. The question being when should we split files ? For instance, there is the Group folder where everything are separated VS the AbGroup folder where a lot of things are in the base. There is also the question of more specific constructions like the polynomials ?

What would be your opinion about this question ?

[felixwellen]

I agree that there is some inconsistency among Group and AbGroup. I would be more for moving things away from Base in AbGroup. According to my personal taste Polynomials should be either in CommRing or in CommAlgebra, but this is not a strong opinion. There are a couple of other things that might better be somewhere else (like Matrix) - but this is another issue (#814 )

[thomas-lamiaux]

I was thinking that it is important to have specific files rather than modules (also in more general case). This way it is easier to find something in the library as the names give a good description of the content. It also avoid code duplication as it is easier to say what as been done or not.

For instance in general case I would be for something that looks more like the groups. But then maybe with an import file a bit bigger that would also contains morphisms.

[mortberg]

For each algebraic structure S I would suggest the following organization:

• Base.agda : definition and basic operation of S
• SIP.agda: all the SIP stuff
• Properties.agda : basic algebraic properties of S
• Foo.agda : various things for S can be put in separate files at the top-level in the S folder, e.g. S/Morphisms.agda, etc.
• Instances/ : concrete instances of the structure, e.g. integers, polynomials, etc.

For an type T which comes up in algebra (e.g. Polynomials, Matrix, etc.) I would have a separate folder for each T in the Cubical.Algebra folder containing:

• Base.agda : definition of the default/best implementation with operations
• Properties.agda : basic properties
• Foo.agda : specific results/operations on T, e.g. universal properties, efficient algorithms (like Karatsuba), etc.
• MoreTs/ : alternative representations, preferably with equivalences proved to the Base definition

For each of these there should the be a S.agda/T.agda file at the top-level in Cubical.Algebra which exports the Base and Properties files

[thomas-lamiaux]

For the case of polynomial or direct sum I think there is two issues.

1. Splitting files I think it is important to have files that specify what has been proven on the structure. For instance for polynomials something like :

   • Base
   • Rename Properties to things like CommRingProperties
   • Universal Property (still missing)
   • ...

2. Then there is the issue of what to do when there is several possible definition. This is the case in Polynomials but also #798 or #811 and in probably other files.

I think that the best would be something like in Int. Having the "good definition" on top. Then folders for each alternative definition containing the usual things like Base etc... + a file named EquivDefinition or something like that the proves that the equivalence with the "good definition"

[thomas-lamiaux]

@mortberg I would agree on the general organization you are offering. The question to me now is would be how much do you split foo

[felixwellen]

For each algebraic structure S I would suggest the following organization:

* `Base.agda` : definition and basic operation of `S`, maybe some basic equivalence (like SIP instance which is automatically derived)

* `Properties.agda` : basic algebraic properties of `S`

* `Foo.agda` : various things for `S` can be put in separate files at the top-level in the `S` folder, e.g. `S/Morphisms.agda`, etc.

* `Instances/` : concrete instances of the structure, e.g. integers, polynomials, etc.

* `Constructions/` : constructions on the structure, e.g. direct sum, tensor product, etc.

For an type T which comes up in algebra (e.g. Polynomials, Matrix, etc.) I would have a separate folder for each T in the Cubical.Algebra folder containing:

* `Base.agda` : definition of the default/best implementation with operations

* `Properties.agda` : basic properties

* `Foo.agda` : specific results/operations on T, e.g. universal properties, efficient algorithms (like Karatsuba), etc.

* `MoreTs/` : alternative representations, preferably with equivalences proved to the Base definition

For each of these there should the be a S.agda/T.agda file at the top-level in Cubical.Algebra which exports the Base and Properties files

Sounds all reasonable to me. I would however find it a bit weird to strongly enforce the structure for Ss which don't have much files yet. E.g. I would leave it up to judgement, if the folder Cubical.Algebra.S needs to have subfolders.

[mortberg]

@mortberg I would agree on the general organization you are offering. The question to me now is would be how much do you split foo

I think it's impossible to give a general rule that applies to all structures and types, but a rule of thumb can be that each Foo should contain one main result (e.g. correctness of some algorithm or proof of some universal property) or gather all results related to a specific thing (e.g. various notions of morphisms of groups and their equivalence as well as properties can all be in the same file)

[mortberg]

For each algebraic structure S I would suggest the following organization:

* `Base.agda` : definition and basic operation of `S`, maybe some basic equivalence (like SIP instance which is automatically derived)

* `Properties.agda` : basic algebraic properties of `S`

* `Foo.agda` : various things for `S` can be put in separate files at the top-level in the `S` folder, e.g. `S/Morphisms.agda`, etc.

* `Instances/` : concrete instances of the structure, e.g. integers, polynomials, etc.

* `Constructions/` : constructions on the structure, e.g. direct sum, tensor product, etc.

For an type T which comes up in algebra (e.g. Polynomials, Matrix, etc.) I would have a separate folder for each T in the Cubical.Algebra folder containing:

* `Base.agda` : definition of the default/best implementation with operations

* `Properties.agda` : basic properties

* `Foo.agda` : specific results/operations on T, e.g. universal properties, efficient algorithms (like Karatsuba), etc.

* `MoreTs/` : alternative representations, preferably with equivalences proved to the Base definition

For each of these there should the be a S.agda/T.agda file at the top-level in Cubical.Algebra which exports the Base and Properties files

Sounds all reasonable to me. I would however find it a bit weird to strongly enforce the structure for Ss which don't have much files yet. E.g. I would leave it up to judgement, if the folder Cubical.Algebra.S needs to have subfolders.

What do you have in mind more concretely? An S with few files would probably just be the Base and Properties file, no?

[thomas-lamiaux]

I think it's impossible to give a general rule that applies to all structures and types, but a rule of thumb can be that each Foo should contain one main result (e.g. correctness of some algorithm or proof of some universal property) or gather all results related to a specific thing (e.g. various notions of morphisms of groups and their equivalence as well as properties can all be in the same file) I agree on this

[thomas-lamiaux]

In the folder Construction, I think we should also put things like FreeMonoid, FreeGroup that are currently in HIT

Also in vo construction should the result be an AbGroup or the input. I think the latter. For instance Abelianization is currently in Group but it should be in AbGroup in my opinion.

[felixwellen]

What do you have in mind more concretely? An S with few files would probably just be the Base and Properties file, no?

But if there is Base and one Construction C would you really insist on moving that to Construction/C? We could also say just something like: "Split up folders Cubical/Algebra/S with lot's of content according to the following scheme: ...".

[thomas-lamiaux]

Fixing the convention, I have stumbled on https://github.com/agda/cubical/blob/master/Cubical/Algebra/CommRingSolver/RawRing.agda. I was wondering if this is something that we should put in Ring ?

[mortberg]

For each algebraic structure S I would suggest the following organization:

* `Base.agda` : definition and basic operation of `S`

* `SIP.agda`: all the SIP stuff

* `Properties.agda` : basic algebraic properties of `S`

* `Foo.agda` : various things for `S` can be put in separate files at the top-level in the `S` folder, e.g. `S/Morphisms.agda`, etc.

* `Instances/` : concrete instances of the structure, e.g. integers, polynomials, etc.

For an type T which comes up in algebra (e.g. Polynomials, Matrix, etc.) I would have a separate folder for each T in the Cubical.Algebra folder containing:

* `Base.agda` : definition of the default/best implementation with operations

* `Properties.agda` : basic properties

* `Foo.agda` : specific results/operations on T, e.g. universal properties, efficient algorithms (like Karatsuba), etc.

* `MoreTs/` : alternative representations, preferably with equivalences proved to the Base definition

For each of these there should the be a S.agda/T.agda file at the top-level in Cubical.Algebra which exports the Base and Properties files

We decided to implement this in a separate PR