[ add ] Pointwise lifting of algebra to Data.Vec.Functional (Functional vector module #1945 redux)

[e-mniang]

This PR updates #1945 by bringing the functional vector and module structures/bundles in line with current stdlib conventions and removing nested submodules.

Next, I’ll add the necessary entry to the CHANGELOG.

Reviews and comments are welcome.

[jamesmckinna]

No review as such, but an observation about a global problem with both Base and Properties, echoing @JacquesCarette 's 'style' comment: in many/most/all(?) of the definitions, there is a need to standardise apart the name of a derived construction from that of its 'base' counterpart, and this PR adopts three distinct strategies to achieve this

• superscript ̌
• vec-/Vec prefixing
• base as a generic name for the 'base' notion (eg IsCommutativeMonoid), and the 'usual' isCamelCase : IsCamelCase idiom for naming the derived notion

Some of this seems to come about because of name clashes, either directly, or as a result of local opening of a base record. It would be great if, even at the cost of some slightly more involved qualified imports/private module declarations, that such things could be avoided, moreover in such a way as to make the above '(in)elegant variation' go away...

Suggest also that, for all these update/'redux' PRs:

• the title of the PR be a copy/tidying up of the original, but with the additional pointer to the original as you have it, eg here "[ add ] Pointwise lifting of algebra to Data.Vec.Functional (#1945 redux)", rather than the more gnomic "Update of...", which requires the reader to follow one level of indirection in order to know what's going on...

[jamesmckinna]

Thanks for the updates @e-mniang ! My recent round of nitpicks really home in on wanting to avoid the superscripts altogether:

• for the function/relation names on Vectors, the existing infrastructure suffices?
• for your additions of structure/bundle inheritance, with careful choice of parameter names, there's no need either!

Hope this

• is clear
• helps!

[JacquesCarette]

FYI: @e-mniang says she'll finish this once she's established a proper rhythm with this term's courses, back in France.

[jamesmckinna]

FYI: @e-mniang says she'll finish this once she's established a proper rhythm with this term's courses, back in France.

Safe journeys back!

Given the current merge hiatus thanks to GitHub, it seems fine to also have a hiatus in fretting too much about when updates get pushed...

... while commentary remains the stream that can never be shut off!

[e-mniang]

Hi! Thanks for the comments. I’ve made changes to address each point; I hope it’s in good shape now.

[jamesmckinna]

fix-whitespace src/Data/Vec/Functional/Algebra/Base.agda (DONE)

[jamesmckinna]

@JacquesCarette I've fixed the whitespace and CHANGELOG issues; can you re-review ahead of merging?

[jamesmckinna]

While merging is blocked, can we (re)consider where all this material belongs?

• currently, under Data.Vec.Functional.Algebra.*
• but should it, in fact, belong better under Algebra.Construct.FunctionalVector.*

The latter emphasises that we have constructions on algebras, rather than being 'accidental' algebraic consequences for functional vectors... but I confess I find the question hard to resolve, and its taken this long even for it to crystallise...

[JacquesCarette]

I like the current location. Because, to me Algebra.Construct is where constructions belong. What you do here is "the algebra (and properties) of functional vectors", so Data.Vec.Functional.Algebra seems like a great home (to me).