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

[gabriellisboaconegero]

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.

[jamesmckinna]

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]

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]

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!

[JacquesCarette]

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]

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

[jamesmckinna]

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]

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]

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

[jamesmckinna]

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!