From 7ff2746ab4f574439f71273bc31e80baeab9ab2b Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Wed, 8 Mar 2023 15:05:07 -0500
Subject: [PATCH] Define new profunctors Forget and Coforget

---
 Data/Profunctor/Costrong.idr      | 10 ++++
 Data/Profunctor/Representable.idr |  9 ++++
 Data/Profunctor/Sieve.idr         |  9 ++++
 Data/Profunctor/Strong.idr        | 15 ++++++
 Data/Profunctor/Traversing.idr    |  6 +++
 Data/Profunctor/Types.idr         | 78 +++++++++++++++++++++++++++++++
 6 files changed, 127 insertions(+)

diff --git a/Data/Profunctor/Costrong.idr b/Data/Profunctor/Costrong.idr
index 8b25bcf..1a19bfd 100644
--- a/Data/Profunctor/Costrong.idr
+++ b/Data/Profunctor/Costrong.idr
@@ -89,6 +89,16 @@ GenCostrong Pair Tagged where
   costrongl (Tag (x,_)) = Tag x
   costrongr (Tag (_,x)) = Tag x
 
+export
+GenCostrong Either (Forget r) where
+  costrongl (MkForget k) = MkForget (k . Left)
+  costrongr (MkForget k) = MkForget (k . Right)
+
+export
+GenCostrong Pair (Coforget r) where
+  costrongl (MkCoforget k) = MkCoforget (fst . k)
+  costrongr (MkCoforget k) = MkCoforget (snd . k)
+
 
 ------------------------------------------------------------------------------
 -- Cotambara
diff --git a/Data/Profunctor/Representable.idr b/Data/Profunctor/Representable.idr
index 63059aa..fdf23c3 100644
--- a/Data/Profunctor/Representable.idr
+++ b/Data/Profunctor/Representable.idr
@@ -1,5 +1,6 @@
 module Data.Profunctor.Representable
 
+import Control.Applicative.Const
 import Control.Monad.Identity
 import Data.Morphisms
 import Data.Profunctor
@@ -61,6 +62,10 @@ export
 Functor f => Representable (Star f) f where
   tabulate = MkStar
 
+export
+Representable (Forget r) (Const r) where
+  tabulate = MkForget . (runConst .)
+
 export
 Corepresentable Morphism Identity where
   cotabulate f = Mor (f . Id)
@@ -75,3 +80,7 @@ namespace Corepresentable
 export
 Functor f => Corepresentable (Costar f) f where
   cotabulate = MkCostar
+
+export
+Corepresentable (Coforget r) (Const r) where
+  cotabulate = MkCoforget . (. MkConst)
diff --git a/Data/Profunctor/Sieve.idr b/Data/Profunctor/Sieve.idr
index 693646b..d04eed9 100644
--- a/Data/Profunctor/Sieve.idr
+++ b/Data/Profunctor/Sieve.idr
@@ -1,5 +1,6 @@
 module Data.Profunctor.Sieve
 
+import Control.Applicative.Const
 import Control.Monad.Identity
 import Data.Morphisms
 import Data.Profunctor
@@ -47,6 +48,10 @@ export
 Functor f => Sieve (Star f) f where
   sieve = applyStar
 
+export
+Sieve (Forget r) (Const r) where
+  sieve (MkForget k) = MkConst . k
+
 
 export
 Cosieve Morphism Identity where
@@ -62,3 +67,7 @@ namespace Cosieve
 export
 Functor f => Cosieve (Costar f) f where
   cosieve = applyCostar
+
+export
+Cosieve (Coforget r) (Const r) where
+  cosieve (MkCoforget k) = k . runConst
diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr
index d7729f1..c74b3c3 100644
--- a/Data/Profunctor/Strong.idr
+++ b/Data/Profunctor/Strong.idr
@@ -132,6 +132,21 @@ GenStrong Either Tagged where
   strongl (Tag x) = Tag (Left x)
   strongr (Tag x) = Tag (Right x)
 
+export
+GenStrong Pair (Forget r) where
+  strongl (MkForget k) = MkForget (k . fst)
+  strongr (MkForget k) = MkForget (k . snd)
+
+export
+Monoid r => GenStrong Either (Forget r) where
+  strongl (MkForget k) = MkForget (either k (const neutral))
+  strongr (MkForget k) = MkForget (either (const neutral) k)
+
+export
+GenStrong Either (Coforget r) where
+  strongl (MkCoforget k) = MkCoforget (Left . k)
+  strongr (MkCoforget k) = MkCoforget (Right . k)
+
 
 ------------------------------------------------------------------------------
 -- Tambara
diff --git a/Data/Profunctor/Traversing.idr b/Data/Profunctor/Traversing.idr
index 200d678..e1aa5ab 100644
--- a/Data/Profunctor/Traversing.idr
+++ b/Data/Profunctor/Traversing.idr
@@ -1,5 +1,6 @@
 module Data.Profunctor.Traversing
 
+import Control.Applicative.Const
 import Control.Monad.Identity
 import Data.Morphisms
 import Data.Tensor
@@ -106,6 +107,11 @@ Applicative f => Traversing (Star f) where
   traverse' (MkStar p) = MkStar (traverse p)
   wander f (MkStar p) = MkStar (f p)
 
+export
+Monoid r => Traversing (Forget r) where
+  traverse' (MkForget k) = MkForget (foldMap k)
+  wander f (MkForget k) = MkForget (runConst . f (MkConst . k))
+
 
 ------------------------------------------------------------------------------
 -- CofreeTraversing
diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr
index 8648e23..8c17445 100644
--- a/Data/Profunctor/Types.idr
+++ b/Data/Profunctor/Types.idr
@@ -192,3 +192,81 @@ Profunctor Tagged where
   dimap _ f (Tag x) = Tag (f x)
   lmap = const retag
   rmap f (Tag x) = Tag (f x)
+
+
+||| `Forget r` is equivalent to `Star (Const r)`.
+public export
+record Forget {0 k : Type} r a (b : k) where
+  constructor MkForget
+  runForget : a -> r
+
+public export
+reforget : Forget r a b -> Forget r a c
+reforget (MkForget k) = MkForget k
+
+export
+Functor (Forget r a) where
+  map _ = reforget
+
+export
+Contravariant (Forget {k=Type} r a) where
+  contramap _ = reforget
+
+export
+Monoid r => Applicative (Forget r a) where
+  pure _ = MkForget (const neutral)
+  MkForget f <*> MkForget g = MkForget (f <+> g)
+
+export
+Monoid r => Monad (Forget {k=Type} r a) where
+  join = reforget
+  (>>=) = reforget .: const
+
+export
+Foldable (Forget r a) where
+  foldr _ x _ = x
+  foldl _ x _ = x
+  null = const True
+  foldlM _ x _ = pure x
+  toList _ = []
+  foldMap _ _ = neutral
+
+export
+Traversable (Forget r a) where
+  traverse _ = pure . reforget
+
+export
+Profunctor (Forget r) where
+  dimap f _ (MkForget k) = MkForget (k . f)
+  lmap f (MkForget k) = MkForget (k . f)
+  rmap = map
+
+
+||| `Coforget r` is equivalent to `Costar (Const r)`.
+public export
+record Coforget {0 k : Type} r (a : k) b where
+  constructor MkCoforget
+  runCoforget : r -> b
+
+public export
+recoforget : Coforget r a c -> Coforget r b c
+recoforget (MkCoforget k) = MkCoforget k
+
+export
+Functor (Coforget r a) where
+  map f (MkCoforget k) = MkCoforget (f . k)
+
+export
+Applicative (Coforget r a) where
+  pure = MkCoforget . const
+  MkCoforget f <*> MkCoforget g = MkCoforget (\r => f r (g r))
+
+export
+Monad (Coforget r a) where
+  MkCoforget k >>= f = MkCoforget (\r => runCoforget (f $ k r) r)
+
+export
+Profunctor (Coforget f) where
+  dimap _ f (MkCoforget k) = MkCoforget (f . k)
+  lmap _ = recoforget
+  rmap = map