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

e-mniang · 2025-08-28T17:47:04Z

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.

JacquesCarette

A few minor style things, but this looks quite good.

JacquesCarette · 2025-08-28T20:03:27Z

src/Data/Vec/Functional/Algebra/Base.agda

+lift₁ᴹ f = map f
+
+-- Vector RawMagma construction
+VecRawMagma : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ


I would use (say) Data.Sum.Algebra as a guide for naming conventions of these.

src/Data/Vec/Functional/Algebra/Base.agda

JacquesCarette · 2025-08-28T20:05:17Z

src/Data/Vec/Functional/Algebra/Base.agda

+
+-- Left scalar action obtained from the ring/semiring multiplication
+_*ₗ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n)
+_*ₗ_ _*_ r xs = map (λ x → _*_ r x) xs


Suggested change

_*ₗ_ _*_ r xs = map (λ x → _*_ r x) xs

_*ₗ_ _*_ r xs = map (r *_) xs

Also, worth adding some global variable declarations to avoid having to mention {S : Set a} prefixes in types at all?

JacquesCarette · 2025-08-28T20:05:49Z

src/Data/Vec/Functional/Algebra/Base.agda

+
+-- Right scalar action (same underlying Op₂, but as a right action)
+_*ᵣ_ : {S : Set a} → Op₂ S → Opᵣ S (Vector S n)
+_*ᵣ_ _*_ xs r = map (λ x → _*_ x r) xs


Suggested change

_*ᵣ_ _*_ xs r = map (λ x → _*_ x r) xs

_*ᵣ_ _*_ xs r = map (_* r) xs

JacquesCarette · 2025-08-28T20:09:31Z

src/Data/Vec/Functional/Algebra/Properties.agda

+  isSemiringVec = record {
+    isSemiringWithoutAnnihilatingZero = record
+      { +-isCommutativeMonoid = isCommutativeMonoid n +-isCommutativeMonoid
+      ; *-cong    = λ x≈y u≈v i → *-cong (x≈y i) (u≈v i)


there are many combinators in Function.Base that could be used here.

src/Data/Vec/Functional/Algebra/Properties.agda

jamesmckinna · 2025-08-29T03:54:36Z

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 (Functional vector module #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...

src/Data/Vec/Functional/Algebra/Base.agda

src/Data/Vec/Functional/Algebra/Properties.agda

jamesmckinna · 2025-09-02T12:01:17Z

src/Data/Vec/Functional/Algebra/Base.agda

+pointwiseᵛ : ( _≈_ : Rel A ℓ ) → Rel (Vector A n) ℓ
+pointwiseᵛ _≈_ = Pointwise _≈_


Is this (redundant) repetition worth the gain (eg in uniformity of naming?)
I'd be tempted to do two things here:

make the import on L20 qualified, as Pointwise

inline all uses of pointwiseᵛ in favour simply of Pointwise as it stands...

jamesmckinna · 2025-09-02T12:02:33Z

src/Data/Vec/Functional/Algebra/Base.agda

+zipWithᵛ : Op₂ A → Op₂ (Vector A n)
+zipWithᵛ _∙_ = zipWith _∙_
+
+mapᵛ : Op₁ A → Op₁ (Vector A n)
+mapᵛ f = map f


Ditto. (and all the more so, now that 3 imported definitions are being subject to the same treatment...)

jamesmckinna · 2025-09-02T12:03:40Z

src/Data/Vec/Functional/Algebra/Base.agda

+rawMagmaᵛ : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ
+rawMagmaᵛ M n =


Now that M is being referenced only locally via the where clause, again... I'd drop the superscript.

jamesmckinna · 2025-09-02T12:06:16Z

src/Data/Vec/Functional/Algebra/Base.agda

+_*ₗᵛ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n)
+_*ₗᵛ_ _*_ r xs = map (r *_) xs


Two suggestions:

eta-contract (no need to mention xs on either LHS or RHS)

now you've used map, rather than mapᵛ, its alias...

... so I'd go all the way now:

Suggested change

_*ₗᵛ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n)

_*ₗᵛ_ _*_ r xs = map (r *_) xs

_*ₗ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n)

_*ₗ_ _*_ r = map (r *_)

jamesmckinna · 2025-09-02T12:06:41Z

src/Data/Vec/Functional/Algebra/Base.agda

+_*ᵣᵛ_ : {S : Set a} → Op₂ S → Opᵣ S (Vector S n)
+_*ᵣᵛ_ _*_ xs r = map (_* r) xs


jamesmckinna · 2025-09-02T12:12:27Z

src/Data/Vec/Functional/Algebra/Properties.agda

+    module VM = RawMagma magmaᵛ
+    module M = RawMagma rawMagma
+
+  open IsEquivalence


Is this needed?

jamesmckinna · 2025-09-02T12:17:43Z

src/Data/Vec/Functional/Algebra/Properties.agda

+  isMagmaᵛ : IsMagma M._≈_ M._∙_ → IsMagma VM._≈_ VM._∙_
+  isMagmaᵛ base = record
+    { isEquivalence = flip Pointwise.isEquivalence _ B.isEquivalence
+    ; ∙-cong        = λ x≈y u≈v i → B.∙-cong (x≈y i) (u≈v i)
+    }
+    where module B = IsMagma base


Now you've chosen base for the 'base' argument, you won't need the superscript...?

As for module B = IsMagma base why change the names module CM = ..., module SG = ... of the subsequent locally-bound modules... when B would suffice in those instances as well?

jamesmckinna · 2025-09-02T12:19:28Z

src/Data/Vec/Functional/Algebra/Properties.agda

+    monoidᵛ = rawMonoidᵛ rawMonoid n
+    module VM = RawMonoid monoidᵛ
+    module RM = RawMonoid rawMonoid


Again, I see no use of monoidᵛ besides the definition of module VM, so consider inlining it:

Suggested change

monoidᵛ = rawMonoidᵛ rawMonoid n

module VM = RawMonoid monoidᵛ

module RM = RawMonoid rawMonoid

module VM = RawMonoid (rawMonoid M n)

module M = RawMonoid M

etc. No need for RM here?

jamesmckinna · 2025-09-02T12:25:05Z

src/Data/Vec/Functional/Algebra/Properties.agda

+  module' : Module _ _ _
+  module' = record { isModule = isModule }


For the underlying name of the bundle, stdlib uses in eg. Algebra.Module.Construct.TensorUnit the name ⟨module⟩, and I would follow suit here, for the sake of consistency.

jamesmckinna · 2025-09-02T12:27:58Z

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 · 2025-09-19T14:43:37Z

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

jamesmckinna · 2025-09-20T08:53:41Z

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!

update of pr 1945

3cf9d5a

JacquesCarette requested changes Aug 28, 2025

View reviewed changes

changes after review

c36797b

jamesmckinna reviewed Aug 29, 2025

View reviewed changes

src/Data/Vec/Functional/Algebra/Properties.agda Outdated Show resolved Hide resolved

jamesmckinna reviewed Aug 29, 2025

View reviewed changes

src/Data/Vec/Functional/Algebra/Base.agda Outdated Show resolved Hide resolved

jamesmckinna reviewed Aug 29, 2025

View reviewed changes

src/Data/Vec/Functional/Algebra/Base.agda Outdated Show resolved Hide resolved

jamesmckinna reviewed Aug 29, 2025

View reviewed changes

src/Data/Vec/Functional/Algebra/Properties.agda Outdated Show resolved Hide resolved

e-mniang changed the title ~~Update of pr 1945~~ [ add ] Pointwise lifting of algebra to Data.Vec.Functional (Functional vector module #1945 redux) Aug 29, 2025

names changes

e67c13e

jamesmckinna reviewed Sep 2, 2025

View reviewed changes

	_ₗ_ __ r xs = map (λ x → _*_ r x) xs
	_ₗ_ __ r xs = map (r *_) xs

	_ᵣ_ __ xs r = map (λ x → _*_ x r) xs
	_ᵣ_ __ xs r = map (_* r) xs

		pointwiseᵛ : ( _≈_ : Rel A ℓ ) → Rel (Vector A n) ℓ
		pointwiseᵛ _≈_ = Pointwise _≈_

		rawMagmaᵛ : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ
		rawMagmaᵛ M n =

		_*ₗᵛ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n)
		_ₗᵛ_ __ r xs = map (r *_) xs

		_*ᵣᵛ_ : {S : Set a} → Op₂ S → Opᵣ S (Vector S n)
		_ᵣᵛ_ __ xs r = map (_* r) xs

		module' : Module _ _ _
		module' = record { isModule = isModule } No newline at end of file

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

Are you sure you want to change the base?

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

Uh oh!

Conversation

e-mniang commented Aug 28, 2025

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jamesmckinna commented Aug 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Sep 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Sep 2, 2025

Uh oh!

JacquesCarette commented Sep 19, 2025

Uh oh!

jamesmckinna commented Sep 20, 2025

Uh oh!

Uh oh!

jamesmckinna commented Aug 29, 2025 •

edited

Loading

jamesmckinna Sep 2, 2025 •

edited

Loading