Add new module `Effect.Functor.Naperian` #2004

Sofia-Insa · 2023-06-22T16:48:42Z

New module Effect.Functor.Naperian added to stdlib.
With two records defining Naperian functors:

record RawNaperian
record Naperian.

with two records : `RawNaperian` and `Naperian`

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

…tdlib into task2-Naperian

jamesmckinna

A very nice initial go at a contribution in this area, and hopefully one which can be taken further as suggested, without too much difficulty.

CHANGELOG.md

src/Effect/Functor/Naperian.agda

jamesmckinna · 2024-01-19T13:57:19Z

src/Effect/Functor/Naperian.agda

+
+-- " Functor f is Naperian if there is a type p of ‘positions’ such that fa≃p→a;
+-- then p behaves a little like a logarithm of f
+-- in particular, if f and g are both Naperian, then Log(f×g)≃Logf+Logg and Log(f.g) ≃ Log f × Log g"


So it would be great if your PR could come good on this promise by exhibiting the constructions?

src/Effect/Functor/Naperian.agda

jamesmckinna · 2024-01-19T14:10:40Z

src/Effect/Functor/Naperian.agda

+    rawNaperian : RawNaperian d RF
+  open RawNaperian rawNaperian public
+  field
+    tabulate-index : ∀ {A} → (fa : F A) → tabulate (index fa) ≡ fa


So: here the induced Setoid relation on F A?

src/Effect/Functor/Naperian.agda

JacquesCarette · 2024-01-19T21:56:50Z

I should take this PR over. I'm not entirely sure I know how?

MatthewDaggitt · 2024-03-17T12:34:04Z

Given the comment of @JacquesCarette above, @jamesmckinna would you be willing to take over this? Otherwise, I'll close it.

jamesmckinna · 2024-03-17T13:33:03Z

@MatthewDaggitt @JacquesCarette happy to take over on this one, but it'll be a while before I return proper attention to it, if that's OK?

jamesmckinna · 2024-03-17T15:36:10Z

Minimal cleanup for the time being.

JacquesCarette · 2024-03-17T15:38:00Z

Thanks a lot! I've been wanting to come back to these, but I've barely found enough time to do a few reviews.

JacquesCarette · 2024-05-06T01:24:34Z

This is now back onto my plate to finish. And I even know how to do so!

jamesmckinna · 2024-05-06T07:08:43Z

This is now back onto my plate to finish. And I even know how to do so!

Fantastic! I'm happy to hand the baton back. But sign me up as a reviewer come the right time...

jamesmckinna

Besides the notational nitpicking (which I think important, but advisory here), I think the design needs some more thinking as to the dependency/parametrisation in the Setoid case.

jamesmckinna · 2024-05-07T07:51:49Z

src/Effect/Functor/Naperian.agda

+-- Definitions of Naperian Functors, as named by Hancock and McBride,
+-- and subsequently documented by Jeremy Gibbons
+-- in the article "APLicative Programming with Naperian Functors"
+-- which appeared at ESOP 2017.


Suggested change

-- Definitions of Naperian Functors, as named by Hancock and McBride,

-- and subsequently documented by Jeremy Gibbons

-- in the article "APLicative Programming with Naperian Functors"

-- which appeared at ESOP 2017.

-- Naperian Functors, as defined by Hancock and McBride, and

-- subsequently documented by Jeremy Gibbons in the paper

-- "APLicative Programming with Naperian Functors" (ESOP 2017).

jamesmckinna · 2024-05-07T08:33:22Z

src/Effect/Functor/Naperian.agda

+-- Full Naperian has the coherence conditions too.
+-- Propositional version (hard to work with).
+
+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)


Is Propositional.Naperian definable directly from Naperian (≡.setoid A) below?

jamesmckinna · 2024-05-07T08:52:30Z

src/Effect/Functor/Naperian.agda

+    FA : (AS : Setoid a e) → (rn : RawNaperian c RF) → Setoid b (c ⊔ e)
+    FA AS rn = record
+      { Carrier = F X
+      ; _≈_ = λ fx fy → (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 AS renaming (Carrier to X)


Conventionally, in the stdlib

S is the generic Setoid; AS seems weird here

open Setoid S renaming (Carrier to A), ditto.

the Carrier field is (usually) not mentioned; I might be tempted just to write

record { _≈_ = λ (fx fy : F A) → (l : Log) → index fx l ≈ index fy l ...

but YMMV

jamesmckinna · 2024-05-07T08:53:38Z

src/Effect/Functor/Naperian.agda

+      module FS = Setoid (FA AS rawNaperian)
+      module A = Setoid AS


Similar comments to the above about 'conventional' naming?

jamesmckinna · 2024-05-07T08:56:01Z

src/Effect/Functor/Naperian.agda

+  record Naperian (AS : Setoid a e) : Set (suc a ⊔ b ⊔ suc c ⊔ e) where
+    field
+      rawNaperian : RawNaperian c RF
+    open RawNaperian rawNaperian public


This is the one area of the design with which I strongly diverge from your choices: this definition makes the RawNaperian structure potentially depend(ent) on the argument index AS, and that for me is a deal-breaker...

... so I'd be interested to learn the rationale for this choice!

jamesmckinna · 2024-05-07T08:58:55Z

src/Effect/Functor/Naperian.agda

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


If this choice causes ambiguity problems with opening Setoid etc. below, then suggest removing it in favour of ∀ {A} → ... in the types of index and tabulate below...

jamesmckinna · 2024-05-07T09:12:09Z

The PR is still DRAFT, so I'll revisit/re-review when it's 'ready', but at that point I'll also revisit the early comment above about proving the 'logarithm' properties.

Sofia-Insa and others added 4 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

jamesmckinna added addition paper-based labels Jun 27, 2023

jamesmckinna requested changes Jan 19, 2024

View reviewed changes

jamesmckinna and others added 6 commits March 17, 2024 13:45

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

jamesmckinna marked this pull request as draft March 17, 2024 15:36

jamesmckinna changed the title ~~Upload new file Effect.Functor.Naperian to stdlib~~ Add new module Effect.Functor.Naperian Mar 17, 2024

Merge branch 'master' into task2-Naperian

775560f

JacquesCarette added 2 commits May 6, 2024 20:03

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

6804ecd

whitespace

a1de89f

jamesmckinna requested changes May 7, 2024

View reviewed changes

jamesmckinna mentioned this pull request Oct 4, 2024

Problem with DISPLAY pragma for ⊥ in Data.Empty #2493

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add new module `Effect.Functor.Naperian` #2004

Add new module `Effect.Functor.Naperian` #2004

Sofia-Insa commented Jun 22, 2023 •

edited by jamesmckinna

Loading

jamesmckinna left a comment

jamesmckinna Jan 19, 2024

jamesmckinna Jan 19, 2024

JacquesCarette commented Jan 19, 2024

MatthewDaggitt commented Mar 17, 2024 •

edited

Loading

jamesmckinna commented Mar 17, 2024 •

edited

Loading

jamesmckinna commented Mar 17, 2024

JacquesCarette commented Mar 17, 2024

JacquesCarette commented May 6, 2024

jamesmckinna commented May 6, 2024

jamesmckinna left a comment

jamesmckinna May 7, 2024

jamesmckinna May 7, 2024

jamesmckinna May 7, 2024

jamesmckinna May 7, 2024

jamesmckinna May 7, 2024

jamesmckinna May 7, 2024

jamesmckinna commented May 7, 2024

Add new module Effect.Functor.Naperian #2004

Are you sure you want to change the base?

Add new module Effect.Functor.Naperian #2004

Conversation

Sofia-Insa commented Jun 22, 2023 • edited by jamesmckinna Loading

jamesmckinna left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

JacquesCarette commented Jan 19, 2024

MatthewDaggitt commented Mar 17, 2024 • edited Loading

jamesmckinna commented Mar 17, 2024 • edited Loading

jamesmckinna commented Mar 17, 2024

JacquesCarette commented Mar 17, 2024

JacquesCarette commented May 6, 2024

jamesmckinna commented May 6, 2024

jamesmckinna left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jamesmckinna commented May 7, 2024

Add new module `Effect.Functor.Naperian` #2004

Add new module `Effect.Functor.Naperian` #2004

Sofia-Insa commented Jun 22, 2023 •

edited by jamesmckinna

Loading

MatthewDaggitt commented Mar 17, 2024 •

edited

Loading

jamesmckinna commented Mar 17, 2024 •

edited

Loading