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

gabriellisboaconegero · 2025-08-22T19:11:01Z

This pull request aims to continue and complete the work started in #2004

The first version already includes changes requested by @jamesmckinna, such as correct stdlib naming variables and redefinition of PropositionalNaperian.

with two records : `RawNaperian` and `Naperian`

Added new file `Effect.Functor.Naperian` and two records to it

…tdlib into task2-Naperian

jamesmckinna · 2025-08-27T08:10:05Z

Thanks very much for continuing to work on this, and for responding to the earlier review comments.

I refactored the current version, as a way of trying to isolate the details of the contribtion; I'm happy to make local suggestions in a review, but I still think a global change is needed, as follows:

simplified the imports
lifted out the parametrisation, via an anonymous module, to expose the common elements between the private definition of FA, and that of Naperian itself
folded that definition into Naperian as a private manifest field
renamed the constructions so that each local module definition corresponding to a given record is given the same name (Agda's namespace control allows this, and, I think, is that rare case where a pun on names aids comprehension)
then I realised that the (extensional/observational) definition of equality in the setoid FS, in terms of change-of-base along index, precisely permits one of the 'axiom' fields to be expressed in terms of the other, so lifted that out as a manifest field.

Accordingly:

module _ {F : Set a → Set b} c (RF : RawFunctor F) where

-- RawNaperian contains just the functions, not the proofs

  record RawNaperian : 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.

  record Naperian (S : Setoid a ℓ) : Set (suc (a ⊔ c) ⊔ b ⊔ ℓ) where
    field
      rawNaperian : RawNaperian
    open RawNaperian rawNaperian public
    open module S = Setoid S
    private
      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 Carrier) → tabulate (index fx) FS.≈ fx
      index-tabulate : (f : Log → Carrier) (l : Log) → index (tabulate f) l ≈ f l
  
    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)

jamesmckinna · 2025-08-27T08:20:10Z

Now, after such (I think: semantics-preserving!) rearrangement, we can observe that the parametrisation on S : Setoid is still external to the definition of Naperian, whereas the parametrisation on A : Set a in the definition of RawNaperian is internal, ie., at least if I understand things correctly, that index and tabulate are insufficiently generalised: their types should, I think, depend on the underlying Carrier of a given Setoid argument, rather than being free-standing fields of a RawNaperian which are then applied to such a Carrier...

As things stand, Naperian doesn't define 'functorial' behaviour; rather it collects properties that for a given S : Setoid, says that some underlying RawNaperian raw functor is extensional on F S, rather than specifying such behaviour parametrically. In formalistic terms, it also permits a given Naperian to choose a different underlying RawNaperian for each choice of S, which is surely not what we want for a given Functor?

Hope that the suggested refactoring make sit easier to see a possible way forward, but as I've critiqued the previous design in this style, a shout-out to @JacquesCarette for comment on this latest iteration.

jamesmckinna · 2025-08-27T08:22:34Z

Re: CHANGELOG
This is a horrible mess caused by this PR basing off the old, pre-v2.3 version, so perhaps the best thing to do is to push a 'fresh' copy of CHANGELOG on master to his branch, and then add the small patch needed to record the addition of this one new module? But others with superior git-fu (mine is still very rudimentary) may have a better suggestion!

jamesmckinna

Lots that can be (further) simplified, but I still think that the parametrisation on Setoid needs fixing!

jamesmckinna · 2025-08-27T08:25:57Z

src/Effect/Functor/Naperian.agda

+module Effect.Functor.Naperian where
+
+open import Effect.Functor using (RawFunctor)
+open import Function.Bundles using (_⟶ₛ_; _⟨$⟩_; Func)


Suggested change

open import Function.Bundles using (_⟶ₛ_; _⟨$⟩_; Func)

open import Function.Base using (_∘_)

jamesmckinna · 2025-08-27T08:27:00Z

src/Effect/Functor/Naperian.agda

+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 (_≡_)


The relation itself is now never used, only its property of admitting a Setoid bundle, so this can be deleted

Suggested change

open import Relation.Binary.PropositionalEquality.Core using (_≡_)

jamesmckinna · 2025-08-27T08:27:30Z

src/Effect/Functor/Naperian.agda

+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 ≡


Can simplify this to:

Suggested change

open import Relation.Binary.PropositionalEquality.Properties as ≡

import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)

jamesmckinna · 2025-08-27T08:28:49Z

src/Effect/Functor/Naperian.agda

+
+private
+  variable
+    a b c e f : Level


Standardise, based on parametrisation on S : Setoid a ℓ, itself a lexical convention:

Suggested change

a b c e f : Level

a b c ℓ : Level

jamesmckinna · 2025-08-27T08:29:22Z

src/Effect/Functor/Naperian.agda

+-- 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)


jamesmckinna · 2025-08-27T08:30:27Z

src/Effect/Functor/Naperian.agda

+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
+    field
+      rawNaperian : RawNaperian c RF
+    open RawNaperian rawNaperian public
+    private
+      module FS = Setoid (FA S rawNaperian)
+      module A = Setoid S
+    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)
+


See the revised version in my extended comment.

jamesmckinna · 2025-08-27T08:31:17Z

src/Effect/Functor/Naperian.agda

+      index-tabulate : (f : Log → A.Carrier) → ((l : Log) → index (tabulate f) l A.≈ f l)
+
+  PropositionalNaperian : Set (suc (a ⊔ c) ⊔ b)
+  PropositionalNaperian = ∀ {A} → Naperian (≡.setoid A)


On the current design wrt parametrisation, I think that A should be explicit:

Suggested change

PropositionalNaperian = ∀ {A} → Naperian (≡.setoid A)

PropositionalNaperian = ∀ A → Naperian (≡.setoid A)

JacquesCarette · 2025-08-27T15:21:24Z

Yes, it would make sense to 'restart' the work on CHANGELOG from a recent version, as the merge is otherwise going to be hell.

JacquesCarette · 2025-08-27T15:25:09Z

Thanks for the review @jamesmckinna . All the explicit suggestions should go in - please do so @gabriellisboaconegero .

jamesmckinna · 2025-08-29T05:14:42Z

src/Effect/Functor/Naperian.agda

+      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)


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

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.

JacquesCarette · 2025-08-30T19:26:34Z

src/Data/Vec/Effectful.agda

  { _<$>_ = map
  }

+naperian : RawNaperian (λ (A : Set a) → Vec A n) 0ℓ


I think I would name this rawNaperian and the one below naperian.

Similarly: rawApplicative below... etc.

Changing the naming of naperian was easy. However, changing applicative to rawApplicative caused problems with the module TraversableM, as it attempts to open the rawApplicative inside the RawMonad, which can conflict with the naming.

The way I found was to explicitly extract the rawApplicative from RawMonad with open TraversableA (RawMonad.rawApplicative Mon) public

JacquesCarette · 2025-08-30T19:27:05Z

src/Data/Vec/Effectful.agda

+fullNaperian : PropositionalNaperian (λ (A : Set a) → Vec A n) 0ℓ
+fullNaperian A = record
+  { rawNaperian = naperian
+  ; index-tabulate = λ f l → lookup∘tabulate f l


eta contract?

jamesmckinna · 2025-08-31T08:19:11Z

src/Effect/Functor/Naperian.agda

+  Naperian-Applicative : RawNaperian → RawApplicative F
+  Naperian-Applicative rn =


Suggested change

Naperian-Applicative : RawNaperian → RawApplicative F

Naperian-Applicative rn =

rawApplicative : RawNaperian → RawApplicative F

rawApplicative rn =

on our 'usual' naming model?

jamesmckinna · 2025-08-31T08:24:39Z

Nice to see the Vec example, but before adding any more (const functors have Log the empty type; Id the unit type, etc.) can we agree on how to resolve the dependency question I keep hammering on about?

JacquesCarette · 2025-08-31T15:54:11Z

but before adding any more [...] resolve the dependency question I keep hammering on about?

Is this the 'parametrisation' comment above, or something else? I did discuss changing some of that with @gabriellisboaconegero last week so that RawNaperian would explicit depend on a Set while Naperian on a Setoid.

jamesmckinna · 2025-09-02T12:54:35Z

but before adding any more [...] resolve the dependency question I keep hammering on about?

Is this the 'parametrisation' comment above, or something else? I did discuss changing some of that with @gabriellisboaconegero last week so that RawNaperian would explicit depend on a Set while Naperian on a Setoid.

yes, this is the parametrisation comment, but I don't think it is solved by changing the parametrisation(s) of RawNaperian and Naperian, but I look forward to seeing the emerging design along the lines you sketch above. My concern is that each notion should somehow be a property of a single underlying (Raw)Functor, whereas what we have at the moment seems simply to allow that underlying object to vary with the external parameter!?

But it's entirely possible that I have misunderstood something fundamental, so I'll wait and see! It (perhaps) doesn't help that #496 is still open, and that we haven't (really) resolved how a RawFunctor should behave/be constrained when its underlying Sets carry a Setoid structure, etc. although it's perhaps 'obvious' that the 'object' part should respect such structure... (premature adoption of concepts from haskell considered harmful?)

JacquesCarette

Hopefully this is what @jamesmckinna meant!

jamesmckinna · 2025-09-20T08:57:06Z

Hopefully this is what @jamesmckinna meant!

I'll try to look at this over the w/e, but I wonder if it's also worth soliciting a review from @gallais who did a lot of the early work on (Raw)Functor etc.

Meanwhile, I from time to time meet up with Hancock himself, so I'll also try to discuss this with him!

Sofia-Insa and others added 14 commits June 21, 2023 16:52

Upload new file Effect.Functor.Naperian to stdlib

1a86ef4

with two records : `RawNaperian` and `Naperian`

Update CHANGELOG.md

0dd5051

Added new file `Effect.Functor.Naperian` and two records to it

Merge branch 'task2-Naperian' of https://github.com/Sofia-Insa/agda-s…

af6d2dc

…tdlib into task2-Naperian

Update CHANGELOG.md

eba481c

updated CHANGELOG

603483f

added note

7dcb115

Merge branch 'master' into task2-Naperian

d76c8df

hopefully now fixed merge conflict with up-to-date CHANGELOG

73bd5bd

restored original details to CHANGELOG

e233f0e

review comments from me

ad30c67

Merge branch 'master' into task2-Naperian

775560f

Setoid version of Naperian -- needs another pair of eyes.

6804ecd

whitespace

a1de89f

[FIX]: Naming + Propositional Naperian

527e4d7

jamesmckinna requested changes Aug 27, 2025

View reviewed changes

gabriellisboaconegero added 3 commits August 27, 2025 14:43

[REFAC]: RawFunctor as part of RawNaperian + james revision

3c478d3

Merge branch 'master' into functor_naperian

d697f2c

[DOC]: Update CHANGELOG

0741736

jamesmckinna reviewed Aug 29, 2025

View reviewed changes

[ADD]: Vec n is Naperian; rawNaperian to rawApplicative

5216bbb

JacquesCarette requested changes Aug 30, 2025

View reviewed changes

jamesmckinna reviewed Aug 31, 2025

View reviewed changes

gabriellisboaconegero added 2 commits September 2, 2025 14:37

[NAMING]: Correct naming in Vec.Effectful and Naperian

ffda892

[NAMING]: ETA contract

6ad71f0

JacquesCarette approved these changes Sep 19, 2025

View reviewed changes

	open import Function.Bundles using (_⟶ₛ_; _⟨$⟩_; Func)
	open import Function.Base using (_∘_)

	open import Relation.Binary.PropositionalEquality.Properties as ≡
	import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)

	PropositionalNaperian = ∀ {A} → Naperian (≡.setoid A)
	PropositionalNaperian = ∀ A → Naperian (≡.setoid A)

		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)

		Naperian-Applicative : RawNaperian → RawApplicative F
		Naperian-Applicative rn =

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

Are you sure you want to change the base?

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

Uh oh!

Conversation

gabriellisboaconegero commented Aug 22, 2025

Uh oh!

jamesmckinna commented Aug 27, 2025

Uh oh!

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

Uh oh!

Uh oh!

jamesmckinna commented Aug 27, 2025

Uh oh!

jamesmckinna left a comment

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!

Choose a reason for hiding this comment

Uh oh!

JacquesCarette commented Aug 27, 2025

Uh oh!

JacquesCarette commented Aug 27, 2025

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 commented Aug 31, 2025

Uh oh!

JacquesCarette commented Aug 31, 2025

Uh oh!

jamesmckinna commented Sep 2, 2025

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Sep 20, 2025

Uh oh!

Uh oh!

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

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

jamesmckinna commented Aug 27, 2025 •

edited

Loading