Functional vector module #1945
Functional vector module #1945
Conversation
Taneb
left a comment
Taneb
left a comment
There was a problem hiding this comment.
I like this addition. There's a lot of algebraic structures that you could define but don't, especially:
IsCommutativeMagmaIsCommutativeSemigroupIsGroupIsAbelianGroupIsPrerightSemimoduleIsRightSemimoduleIsBisemimoduleIsRightModuleIsBimoduleIsModule
And with element-wise multiplication:
IsNearSemiringIsSemiringWithoutOneIsCommutativeSemiringWithoutOneIsSemiringWithoutAnnihilatingZeroIsSemiringIsCommutativeSemiringIsRingWithoutOneIsRingIsCommutativeRing
Plus the corresponding bundles.
|
I added all of them. |
| ```agda | ||
| <-weakInduction-startingFrom : P i → (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j | ||
| ``` | ||
|
|
There was a problem hiding this comment.
In these cases we typically only mention we have added entirely new modules rather than listing their content.
Cf. https://github.com/agda/agda-stdlib/blob/master/CHANGELOG.md#new-modules
| import Algebra.Structures as AS | ||
|
|
||
| module Data.Vec.Functional.Algebra.Base | ||
| {c ℓ} (cring : CommutativeRing c ℓ) where |
There was a problem hiding this comment.
I'm not happy about this whole module being parameterized on CommutativeRing, as many of the definitions work with smaller algebraic structures, but I'm not sure what to do about it. Maybe other people have some ideas?
There was a problem hiding this comment.
I haven't (yet) looked at this too closely, but it seems as though we might more generally want d isX implies (Vector n d) isX and then if d is suitable as X scalars for the right notion of IsYModule over X then (Vector n d) isYModule over d...?
|
I have changed most of my code and it is not done yet. It is still with a lot of comments. I tried to make the code work with more cases, but I don't know if it is helpful in that way. |
|
I can remove the code that is commented on if they are not necessary. I also would like some suggestions if something is not in the right way. |
|
Sorry not to have had time for a thorough review of this draft PR yet! |
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
This seems like good additions to stdlib, if it were made to fit the style more. Can anyone jump in and do so? (i.e. I'm asking permission)
| A : Set ℓ | ||
| n : ℕ | ||
|
|
||
| module EqualityVecFunc (_≈_ : Rel A ℓ) where |
There was a problem hiding this comment.
Is there a reason everything in here is in sub-modules? That is not a common stdlib pattern.
| _≈ᴹ_ = Pointwise _≈_ | ||
|
|
||
| module VecAddition (_∙_ : Op₂ A) where | ||
| _∙ᴹ_ : Op₂ $ Vector A n |
There was a problem hiding this comment.
Why not call this _+ᴹ_ ?
| _∙ᴹ_ : Op₂ $ Vector A n | ||
| _∙ᴹ_ = zipWith _∙_ | ||
|
|
||
| module VecMagma (rawMagma : RawMagma a ℓ) where |
There was a problem hiding this comment.
I expected the 'result' here to define an instance the structure Magma instead of all the exploded pieces of one.
(Same for Monoid, Group, etc)
| ∙ᴹ-comm ∙-comm xs ys i = ∙-comm (xs i) (ys i) | ||
|
|
||
|
|
||
| -- isMagma : IsMagma _≈_ _∙_ → IsMagma _≈ᴹ_ (_∙ᴹ_ {n}) |
There was a problem hiding this comment.
This commented out code is good code! It fits the rest of the stdlib style.
Yes, anyone can do it. |
5 participants
Added structures and bundles about functional vectors and modules.