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

CHANGELOG.md

@@ -48,6 +48,15 @@ New modules
 
 * `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 (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
 -----------------------------
 

src/Data/Vec/Effectful.agda

@@ -14,14 +14,17 @@ open import Data.Vec.Base as Vec hiding (_⊛_)
 open import Data.Vec.Properties
 open import Effect.Applicative as App using (RawApplicative)
 open import Effect.Functor as Fun using (RawFunctor)
+open import Effect.Functor.Naperian as Nap using (RawNaperian; PropositionalNaperian)
 open import Effect.Monad using (RawMonad; module Join; RawMonadT; mkRawMonad)
 import Function.Identity.Effectful as Id
 open import Function.Base using (flip; _∘_)
-open import Level using (Level)
+open import Level using (Level; 0ℓ)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.PropositionalEquality
 
 private
   variable
-    a : Level
+    a b : Level
     A : Set a
     n : ℕ
 
@@ -33,6 +36,22 @@ functor = record
   { _<$>_ = map
   }
 
+naperian : RawNaperian (λ (A : Set a) → Vec A n) 0ℓ
+naperian {n = n} = record
+  { rawFunctor = functor
+  ; Log = Fin n
+  ; index = lookup
+  ; tabulate = tabulate
+  }
+
+fullNaperian : PropositionalNaperian (λ (A : Set a) → Vec A n) 0ℓ
+fullNaperian A = record
+  { rawNaperian = naperian
+  ; index-tabulate = λ f l → lookup∘tabulate f l
+  ; natural-tabulate = λ f k l → cong (λ fx → lookup fx l) (tabulate-∘ f k)
+  ; natural-index = λ f as l → lookup-map l f as
+  }
+
 applicative : RawApplicative (λ (A : Set a) → Vec A n)
 applicative {n = n} = record
   { rawFunctor = functor

src/Effect/Functor/Naperian.agda

@@ -0,0 +1,82 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Naperian functor
+--
+-- 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.
+-- https://link.springer.com/chapter/10.1007/978-3-662-54434-1_21
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Functor.Naperian where
+
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
+open import Function.Base using (_∘_; const)
+
+private
+  variable
+    a b c ℓ : Level
+    A : Set a
+
+-- From the paper:
+-- "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"
+
+-- RawNaperian contains just the functions, not the proofs
+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
+
+  -- 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
+      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)
+
+    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)
+
+  Naperian-Applicative : RawNaperian → RawApplicative F
+  Naperian-Applicative rn =
+    record
+      { rawFunctor = rawFunctor
+      ; pure = tabulate ∘ const 
+      ; _<*>_ = λ a b → tabulate (λ i → (index a i) (index b i))
+      }
+      where
+        open RawNaperian rn