Skip to content

Add new module Effect.Functor.Naperian - Continuation of #2004 #2815

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 20 commits into
base: master
Choose a base branch
from
Open

Add new module Effect.Functor.Naperian - Continuation of #2004 #2815

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
1a86ef4
Upload new file Effect.Functor.Naperian to stdlib
Sofia-Insa Jun 21, 2023
0dd5051
Update CHANGELOG.md
Sofia-Insa Jun 21, 2023
af6d2dc
Merge branch 'task2-Naperian' of https://github.com/Sofia-Insa/agda-s…
Sofia-Insa Jun 22, 2023
eba481c
Update CHANGELOG.md
Sofia-Insa Jun 22, 2023
603483f
updated `CHANGELOG`
jamesmckinna Mar 17, 2024
7dcb115
added note
jamesmckinna Mar 17, 2024
d76c8df
Merge branch 'master' into task2-Naperian
jamesmckinna Mar 17, 2024
73bd5bd
hopefully now fixed merge conflict with up-to-date `CHANGELOG`
jamesmckinna Mar 17, 2024
e233f0e
restored original details to `CHANGELOG`
jamesmckinna Mar 17, 2024
ad30c67
review comments from me
jamesmckinna Mar 17, 2024
775560f
Merge branch 'master' into task2-Naperian
JacquesCarette May 6, 2024
6804ecd
Setoid version of Naperian -- needs another pair of eyes.
JacquesCarette May 7, 2024
a1de89f
whitespace
JacquesCarette May 7, 2024
527e4d7
[FIX]: Naming + Propositional Naperian
gabriellisboaconegero Aug 21, 2025
3c478d3
[REFAC]: RawFunctor as part of RawNaperian + james revision
gabriellisboaconegero Aug 27, 2025
d697f2c
Merge branch 'master' into functor_naperian
gabriellisboaconegero Aug 27, 2025
0741736
[DOC]: Update CHANGELOG
gabriellisboaconegero Aug 27, 2025
5216bbb
[ADD]: Vec n is Naperian; rawNaperian to rawApplicative
gabriellisboaconegero Aug 29, 2025
ffda892
[NAMING]: Correct naming in Vec.Effectful and Naperian
gabriellisboaconegero Sep 2, 2025
6ad71f0
[NAMING]: ETA contract
gabriellisboaconegero Sep 2, 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
264 changes: 13 additions & 251 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,123 +46,17 @@ New modules

* `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.

* Nagata's construction of the "idealization of a module":
```agda
Algebra.Module.Construct.Idealization
```

* The unique morphism from the initial, resp. terminal, algebra:
```agda
Algebra.Morphism.Construct.Initial
Algebra.Morphism.Construct.Terminal
```

* Pointwise and equality relations over indexed containers:
```agda
Data.Container.Indexed.Relation.Binary.Pointwise
Data.Container.Indexed.Relation.Binary.Pointwise.Properties
Data.Container.Indexed.Relation.Binary.Equality.Setoid
```

* Prime factorisation of natural numbers.
```
Data.Nat.Primality.Factorisation
```

* Permutation relation for functional vectors:
```agda
Data.Vec.Functional.Relation.Binary.Permutation
```
defining `_↭_ : IRel (Vector A) _`

* Properties of `Data.Vec.Functional.Relation.Binary.Permutation`:
```agda
Data.Vec.Functional.Relation.Binary.Permutation.Properties
```
defining
```agda
↭-refl : Reflexive (Vector A) _↭_
↭-reflexive : xs ≡ ys → xs ↭ ys
↭-sym : Symmetric (Vector A) _↭_
↭-trans : Transitive (Vector A) _↭_
```
* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.

* New module defining Naperian functors, 'logarithms of containers' (Hancock/McBride)
```
Effect.Functor.Naperian
```
defining
```agda
record RawNaperian (RF : RawFunctor F) : Set _
record Naperian (RF : RawFunctor F) : Set _
```

* `Data.List.Relation.Binary.Sublist.Propositional.Slice`
replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*)
and adding new functions:
- `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*)
- `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*)

* `Data.Vec.Functional.Relation.Binary.Permutation`, defining:
```agda
_↭_ : IRel (Vector A) _
```

* `Data.Vec.Functional.Relation.Binary.Permutation.Properties` of the above:
```agda
↭-refl : Reflexive (Vector A) _↭_
↭-reflexive : xs ≡ ys → xs ↭ ys
↭-sym : Symmetric (Vector A) _↭_
↭-trans : Transitive (Vector A) _↭_
isIndexedEquivalence : {A : Set a} → IsIndexedEquivalence (Vector A) _↭_
indexedSetoid : {A : Set a} → IndexedSetoid ℕ a _
```

* `Function.Relation.Binary.Equality`
```agda
setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
```
and a convenient infix version
```agda
_⇨_ = setoid
```

* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
```agda
Induction.InfiniteDescent
```

* Symmetric interior of a binary relation
```
Relation.Binary.Construct.Interior.Symmetric
```

* Pointwise and equality relations over indexed containers:
```agda
Data.Container.Indexed.Relation.Binary.Pointwise
Data.Container.Indexed.Relation.Binary.Pointwise.Properties
Data.Container.Indexed.Relation.Binary.Equality.Setoid
```

* New IO primitives to handle buffering
```agda
IO.Primitive.Handle
IO.Handle
```

* `System.Random` bindings:
```agda
System.Random.Primitive
System.Random
```

* Show modules:
```agda
Data.List.Show
Data.Vec.Show
Data.Vec.Bounded.Show
```

```
Effect.Functor.Naperian
```
defining
```agda
record RawNaperian (F : Set a → Set b) (c : Level) : Set _
record Naperian (F : Set a → Set b) (c : Level) (S : Setoid a ℓ) : Set _
```
Additions to existing modules
-----------------------------

Expand All @@ -173,142 +67,10 @@ Additions to existing modules

* In `Data.Fin.Permutation.Components`:
```agda
record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
```

* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`:
```agda
rawNearSemiring : RawNearSemiring _ _
rawRingWithoutOne : RawRingWithoutOne _ _
+-rawGroup : RawGroup _ _
```

* In `Algebra.Construct.Terminal`:
```agda
rawNearSemiring : RawNearSemiring c ℓ
nearSemiring : NearSemiring c ℓ
```

* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.

* In `Algebra.Module.Construct.DirectProduct`:
```agda
rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
```

* In `Algebra.Module.Construct.TensorUnit`:
```agda
rawLeftSemimodule : RawLeftSemimodule _ c ℓ
rawLeftModule : RawLeftModule _ c ℓ
rawRightSemimodule : RawRightSemimodule _ c ℓ
rawRightModule : RawRightModule _ c ℓ
rawBisemimodule : RawBisemimodule _ _ c ℓ
rawBimodule : RawBimodule _ _ c ℓ
rawSemimodule : RawSemimodule _ c ℓ
rawModule : RawModule _ c ℓ
```

* In `Algebra.Construct.Terminal`:
```agda
rawNearSemiring : RawNearSemiring c ℓ
nearSemiring : NearSemiring c ℓ
```

* In `Algebra.Module.Construct.Zero`:
```agda
rawLeftSemimodule : RawLeftSemimodule R c ℓ
rawLeftModule : RawLeftModule R c ℓ
rawRightSemimodule : RawRightSemimodule R c ℓ
rawRightModule : RawRightModule R c ℓ
rawBisemimodule : RawBisemimodule R c ℓ
rawBimodule : RawBimodule R c ℓ
rawSemimodule : RawSemimodule R c ℓ
rawModule : RawModule R c ℓ
```

* In `Algebra.Morphism.Structures`
```agda
module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where
record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _

* In `Algebra.Properties.AbelianGroup`:
```
⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
```

* In `Algebra.Properties.Group`:
```agda
isQuasigroup : IsQuasigroup _∙_ _\\_ _//_
quasigroup : Quasigroup _ _
isLoop : IsLoop _∙_ _\\_ _//_ ε
loop : Loop _ _

\\-leftDividesˡ : LeftDividesˡ _∙_ _\\_
\\-leftDividesʳ : LeftDividesʳ _∙_ _\\_
\\-leftDivides : LeftDivides _∙_ _\\_
//-rightDividesˡ : RightDividesˡ _∙_ _//_
//-rightDividesʳ : RightDividesʳ _∙_ _//_
//-rightDivides : RightDivides _∙_ _//_

⁻¹-selfInverse : SelfInverse _⁻¹
\\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x
⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x
```

* In `Algebra.Properties.Loop`:
```agda
identityˡ-unique : x ∙ y ≈ y → x ≈ ε
identityʳ-unique : x ∙ y ≈ x → y ≈ ε
identity-unique : Identity x _∙_ → x ≈ ε
```

* In `Algebra.Properties.Monoid.Mult`:
```agda
×-homo-0 : ∀ x → 0 × x ≈ 0#
×-homo-1 : ∀ x → 1 × x ≈ x
```

* In `Algebra.Properties.Semiring.Mult`:
```agda
×-homo-0# : ∀ x → 0 × x ≈ 0# * x
×-homo-1# : ∀ x → 1 × x ≈ 1# * x
idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
```

* In `Algebra.Structures`
```agda
record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _

* In `Algebra.Structures.IsGroup`:
```agda
infixl 6 _//_
_//_ : Op₂ A
x // y = x ∙ (y ⁻¹)
infixr 6 _\\_
_\\_ : Op₂ A
x \\ y = (x ⁻¹) ∙ y
```

* In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the
extra property as an exposed definition:
```agda
*-cancelʳ-nonZero : AlmostRightCancellative 0# *
```

* In `Data.Container.Indexed.Core`:
```agda
Subtrees o c = (r : Response c) → X (next c r)
transpose[i,i,j]≡j : (i j : Fin n) → transpose i i j ≡ j
transpose[i,j,j]≡i : (i j : Fin n) → transpose i j j ≡ i
transpose[i,j,i]≡j : (i j : Fin n) → transpose i j i ≡ j
transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k
```

* In `Data.Fin.Properties`:
Expand Down
76 changes: 33 additions & 43 deletions src/Effect/Functor/Naperian.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,14 @@
module Effect.Functor.Naperian where

open import Effect.Functor using (RawFunctor)
open import Function.Bundles using (_⟶ₛ_; _⟨$⟩_; Func)
open import Level using (Level; suc; _⊔_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
open import Relation.Binary.PropositionalEquality.Properties as ≡
open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
open import Function.Base using (_∘_)

private
variable
a b c e f : Level
a b c ℓ : Level
A : Set a

-- From the paper:
Expand All @@ -33,49 +32,40 @@ private
-- then Log(f×g)≃Logf+Logg and Log(f.g) ≃ Log f × Log g"

-- RawNaperian contains just the functions, not the proofs
record RawNaperian {F : Set a → Set b} c (RF : RawFunctor F) : Set (suc (a ⊔ c) ⊔ b) where
field
Log : Set c
index : F A → (Log → A)
tabulate : (Log → A) → F A

-- Full Naperian has the coherence conditions too.
-- Propositional version (hard to work with).
module _ (F : Set a → Set b) c where
record RawNaperian : Set (suc (a ⊔ c) ⊔ b) where
field
rawFunctor : RawFunctor F
Log : Set c
index : F A → (Log → A)
tabulate : (Log → A) → F A
open RawFunctor rawFunctor public

-- module Propositional where
-- record Naperian {F : Set a → Set b} c (RF : RawFunctor F) : Set (suc (a ⊔ c) ⊔ b) where
-- field
-- rawNaperian : RawNaperian c RF
-- open RawNaperian rawNaperian public
-- field
-- tabulate-index : (fa : F A) → tabulate (index fa) ≡ fa
-- index-tabulate : (f : Log → A) → ((l : Log) → index (tabulate f) l ≡ f l)
-- Full Naperian has the coherence conditions too.

module _ {F : Set a → Set b} c (RF : RawFunctor F) where
private
FA : (S : Setoid a e) → (rn : RawNaperian c RF) → Setoid b (c ⊔ e)
FA S rn = record
{ _≈_ = λ (fx fy : F Carrier) → (l : Log) → index fx l ≈ index fy l
; isEquivalence = record
{ refl = λ _ → refl
; sym = λ eq l → sym (eq l)
; trans = λ i≈j j≈k l → trans (i≈j l) (j≈k l)
}
}
where
open Setoid S
open RawNaperian rn

record Naperian (S : Setoid a e) : Set (suc a ⊔ b ⊔ suc c ⊔ e) where
record Naperian (S : Setoid a ℓ) : Set (suc (a ⊔ c) ⊔ b ⊔ ℓ) where
field
rawNaperian : RawNaperian c RF
rawNaperian : RawNaperian
open RawNaperian rawNaperian public
open module S = Setoid S
private
module FS = Setoid (FA S rawNaperian)
module A = Setoid S
FS : Setoid b (c ⊔ ℓ)
FS = record
{ _≈_ = λ (fx fy : F Carrier) → ∀ (l : Log) → index fx l ≈ index fy l
; isEquivalence = record
{ refl = λ _ → refl
; sym = λ eq l → sym (eq l)
; trans = λ i≈j j≈k l → trans (i≈j l) (j≈k l)
}
}
module FS = Setoid FS
field
tabulate-index : (fx : F A.Carrier) → tabulate (index fx) FS.≈ fx
index-tabulate : (f : Log → A.Carrier) → ((l : Log) → index (tabulate f) l A.≈ f l)

index-tabulate : (f : Log → Carrier) → ((l : Log) → index (tabulate f) l ≈ f l)
natural-tabulate : (f : Carrier → Carrier) (k : Log → Carrier) → (tabulate (f ∘ k)) FS.≈ (f <$> (tabulate k))
natural-index : (f : Carrier → Carrier) (as : F Carrier) (l : Log) → (index (f <$> as) l) ≈ f (index as l)
Copy link
Contributor

Choose a reason for hiding this comment

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

Nice!
Can natural-tabulate also be eliminated by defining it in terms of index-tabulate, natural-index, and tabulate-index?

Copy link
Author

Choose a reason for hiding this comment

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

I don't think it can without assuming congruence on the setoid. I was trying to do so, but I was stuck and needed to prove the function congruence on the setoid S. I could figure out that

natural-index f (tabulate k) l -> index (f <$> tabulate k) l ≈ f (index (tabulate k) l)
index-tabulate k l                    -> index (tabulate k) l ≈ k l
index-tabulate (f ∘ k) l            -> index (tabulate (λ x → f (k x))) l ≈ f (k l)

If I assume ≈ congruence, then I could prove tabulate-index.

I don't think we can find a proof for tabulate-index without congruence, but I am not sure. I base my argument on the fact that tabulate-∘ needs cong to be proved.


tabulate-index : (fx : F Carrier) → tabulate (index fx) FS.≈ fx
tabulate-index = index-tabulate ∘ index

PropositionalNaperian : Set (suc (a ⊔ c) ⊔ b)
PropositionalNaperian = ∀ {A} → Naperian (≡.setoid A)
PropositionalNaperian = ∀ A → Naperian (≡.setoid A)