Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
3cf9d5a
update of pr 1945
e-mniang Aug 28, 2025
c36797b
changes after review
e-mniang Aug 28, 2025
e67c13e
names changes
e-mniang Aug 29, 2025
e8de375
applying the reviews
e-mniang Oct 5, 2025
743ae6b
Update Base.agda
jamesmckinna Oct 10, 2025
ee19d44
Merge branch 'master' into updating-pr-1945
jamesmckinna Oct 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
120 changes: 54 additions & 66 deletions src/Data/Vec/Functional/Algebra/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some Vector-related module Definitions
-- Some VecF.Vector-related module Definitions
Copy link
Contributor

@JacquesCarette JacquesCarette Oct 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While importing Data.Vec.Functional as VecF makes sense, VecF in the top-comment does not. I would expand this out to "Functional Vector-related"

------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}
Expand All @@ -12,128 +12,116 @@ open import Level using (Level; suc; _⊔_)
open import Function using (_$_)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Vec.Functional
import Data.Vec.Functional as VecF
open import Algebra.Core
open import Algebra.Bundles
open import Algebra.Module
open import Relation.Binary using (Rel)
open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
import Data.Vec.Functional.Relation.Binary.Pointwise as Pointwise

private variable
a ℓ : Level
A : Set a
n : ℕ

------------------------------------------------------------------------
-- Vector-lifted relations & operators
-- VecF.Vector-lifted raw structures
Copy link
Contributor

@JacquesCarette JacquesCarette Oct 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same comment. I would be tempted to go with just "Lifted raw structures" or if one wants more, "Raw structures lifted to Functional Vectors".


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

zipWithᵛ : Op₂ A → Op₂ (Vector A n)
zipWithᵛ _∙_ = zipWith _∙_

mapᵛ : Op₁ A → Op₁ (Vector A n)
mapᵛ f = map f

------------------------------------------------------------------------
-- Vector-lifted raw structures

rawMagmaᵛ : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ
rawMagmaᵛ M n =
rawMagma : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ
rawMagma M n =
record
{ Carrier = Vector M.Carrier n
; _≈_ = pointwiseᵛ M._≈_
; _∙_ = zipWithᵛ M._∙_
{ Carrier = VecF.Vector M.Carrier n
; _≈_ = Pointwise.Pointwise M._≈_
; _∙_ = VecF.zipWith M._∙_
}
where module M = RawMagma M

rawMonoidᵛ : RawMonoid a ℓ → (n : ℕ) → RawMonoid a ℓ
rawMonoidᵛ M n =
rawMonoid : RawMonoid a ℓ → (n : ℕ) → RawMonoid a ℓ
rawMonoid M n =
record
{ RawMagma (rawMagmaᵛ M.rawMagma n)
{ RawMagma (rawMagma M.rawMagma n)
; ε = λ _ → M.ε
}
where module M = RawMonoid M

rawGroupᵛ : RawGroup a ℓ → (n : ℕ) → RawGroup a ℓ
rawGroupᵛ G n =
rawGroup : RawGroup a ℓ → (n : ℕ) → RawGroup a ℓ
rawGroup G n =
record
{ RawMonoid (rawMonoidᵛ G.rawMonoid n)
; _⁻¹ = mapᵛ G._⁻¹
{ RawMonoid (rawMonoid G.rawMonoid n)
; _⁻¹ = VecF.map G._⁻¹
}
where module G = RawGroup G

rawNearSemiringᵛ : RawNearSemiring a ℓ → (n : ℕ) → RawNearSemiring a ℓ
rawNearSemiringᵛ NS n =
rawNearSemiring : RawNearSemiring a ℓ → (n : ℕ) → RawNearSemiring a ℓ
rawNearSemiring NS n =
record
{ Carrier = Vector NS.Carrier n
; _≈_ = pointwiseᵛ NS._≈_
; _+_ = zipWithᵛ NS._+_
; _*_ = zipWithᵛ NS._*_
{ Carrier = VecF.Vector NS.Carrier n
; _≈_ = Pointwise.Pointwise NS._≈_
; _+_ = VecF.zipWith NS._+_
; _*_ = VecF.zipWith NS._*_
; 0# = λ _ → NS.0#
}
where module NS = RawNearSemiring NS

rawSemiringᵛ : RawSemiring a ℓ → (n : ℕ) → RawSemiring a ℓ
rawSemiringᵛ S n =
rawSemiring : RawSemiring a ℓ → (n : ℕ) → RawSemiring a ℓ
rawSemiring S n =
record
{ RawNearSemiring (rawNearSemiringᵛ S.rawNearSemiring n)
{ RawNearSemiring (rawNearSemiring S.rawNearSemiring n)
; 1# = λ _ → S.1#
}
where module S = RawSemiring S

rawRingᵛ : RawRing a ℓ → (n : ℕ) → RawRing a ℓ
rawRingᵛ R n =
rawRing : RawRing a ℓ → (n : ℕ) → RawRing a ℓ
rawRing R n =
record
{ RawSemiring (rawSemiringᵛ R.rawSemiring n)
; -_ = mapᵛ R.-_
{ RawSemiring (rawSemiring R.rawSemiring n)
; -_ = VecF.map R.-_
}
where module R = RawRing R

------------------------------------------------------------------------
-- Vector actions (left/right scalar multiplication)
-- VecF.Vector actions (left/right scalar multiplication)

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

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

------------------------------------------------------------------------
-- Vector-lifted semimodule bundles
-- VecF.Vector-lifted semimodule bundles

rawLeftSemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawLeftSemimodule (RawNearSemiring.Carrier NS) a ℓ
rawLeftSemimoduleᵛ NS n =
rawLeftSemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawLeftSemimodule (RawNearSemiring.Carrier NS) a ℓ
rawLeftSemimodule NS n =
record
{ Carrierᴹ = Vector NS.Carrier n
; _≈ᴹ_ = pointwiseᵛ NS._≈_
; _+ᴹ_ = zipWithᵛ NS._+_
; _*ₗ_ = _*ₗᵛ_ NS._*_
{ Carrierᴹ = VecF.Vector NS.Carrier n
; _≈ᴹ_ = Pointwise.Pointwise NS._≈_
; _+ᴹ_ = VecF.zipWith NS._+_
; _*ₗ_ = _*ₗ_ NS._*_
; 0ᴹ = λ _ → NS.0#
}
where module NS = RawNearSemiring NS

rawRightSemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawRightSemimodule (RawNearSemiring.Carrier NS) a ℓ
rawRightSemimoduleᵛ NS n =
rawRightSemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawRightSemimodule (RawNearSemiring.Carrier NS) a ℓ
rawRightSemimodule NS n =
record
{ Carrierᴹ = Vector NS.Carrier n
; _≈ᴹ_ = pointwiseᵛ NS._≈_
; _+ᴹ_ = zipWithᵛ NS._+_
; _*ᵣ_ = _*ᵣᵛ_ NS._*_
{ Carrierᴹ = VecF.Vector NS.Carrier n
; _≈ᴹ_ = Pointwise.Pointwise NS._≈_
; _+ᴹ_ = VecF.zipWith NS._+_
; _*ᵣ_ = _*ᵣ_ NS._*_
; 0ᴹ = λ _ → NS.0#
}
where module NS = RawNearSemiring NS

rawBisemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawBisemimodule (RawNearSemiring.Carrier NS)
rawBisemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawBisemimodule (RawNearSemiring.Carrier NS)
(RawNearSemiring.Carrier NS) a ℓ
rawBisemimoduleᵛ NS n =
rawBisemimodule NS n =
record
{ Carrierᴹ = Vector NS.Carrier n
; _≈ᴹ_ = pointwiseᵛ NS._≈_
; _+ᴹ_ = zipWithᵛ NS._+_
; _*ₗ_ = _*ₗᵛ_ NS._*_
; _*ᵣ_ = _*ᵣᵛ_ NS._*_
{ Carrierᴹ = VecF.Vector NS.Carrier n
; _≈ᴹ_ = Pointwise.Pointwise NS._≈_
; _+ᴹ_ = VecF.zipWith NS._+_
; _*ₗ_ = _*ₗ_ NS._*_
; _*ᵣ_ = _*ᵣ_ NS._*_
; 0ᴹ = λ _ → NS.0#
}
where module NS = RawNearSemiring NS
Loading
Loading