From 14d392c021579db5f4e987781f8ba351dfc39eed Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 6 Mar 2023 21:39:24 -0500
Subject: [PATCH] Define free and cofree Mapping functors

This was an absolute mess to port from the Haskell version,
but it should be equivalent to the original code.
---
 Data/Profunctor/Mapping.idr | 109 ++++++++++++++++++++++++++++++++++++
 1 file changed, 109 insertions(+)

diff --git a/Data/Profunctor/Mapping.idr b/Data/Profunctor/Mapping.idr
index 56d3d67..fae756f 100644
--- a/Data/Profunctor/Mapping.idr
+++ b/Data/Profunctor/Mapping.idr
@@ -1,5 +1,8 @@
 module Data.Profunctor.Mapping
 
+import Control.Monad.Identity
+import Data.Morphisms
+import Data.Tensor
 import Data.Profunctor
 import Data.Profunctor.Traversing
 
@@ -28,3 +31,109 @@ export
     using Traversing.Function Closed.Function where
   map' = map
   roam = id
+
+
+public export
+record CofreeMapping p a b where
+  constructor MkCFM
+  runCFM : forall f. Functor f => p (f a) (f b)
+
+export
+Profunctor p => Profunctor (CofreeMapping p) where
+  lmap f (MkCFM p) = MkCFM (lmap (map f) p)
+  rmap f (MkCFM p) = MkCFM (rmap (map f) p)
+  dimap f g (MkCFM p) = MkCFM (dimap (map f) (map g) p)
+
+export
+Profunctor p => Functor (CofreeMapping p a) where
+  map = rmap
+
+export
+ProfunctorFunctor CofreeMapping where
+  promap f (MkCFM p) = MkCFM (f p)
+
+export
+ProfunctorComonad CofreeMapping where
+  proextract (MkCFM p) = dimap Id runIdentity p
+  produplicate (MkCFM p) = MkCFM $ MkCFM $ p @{Compose}
+
+export
+Symmetric ten => Profunctor p => GenStrong ten (CofreeMapping p) where
+  strongr (MkCFM p) = MkCFM (p @{Compose {g=ten c} @{%search} @{MkFunctor mapSnd}})
+  strongl (MkCFM p) = MkCFM (p @{Compose {g=(`ten` c)} @{%search} @{MkFunctor mapFst}})
+
+export
+Profunctor p => Closed (CofreeMapping p) where
+  closed (MkCFM p) = MkCFM (p @{Compose {g = \b => x -> b} @{%search} @{MkFunctor (.)}})
+
+roamCofree : Profunctor p => ((a -> b) -> s -> t) -> CofreeMapping p a b -> CofreeMapping p s t
+roamCofree f (MkCFM p) = MkCFM $ dimap (map (flip f)) (map ($ id)) $
+      p @{Compose @{%search} @{functor}}
+  where
+    functor : Functor (\a => (a -> b) -> t)
+    functor = MkFunctor (\f => (. (. f)))
+
+export
+Profunctor p => Traversing (CofreeMapping p) where
+  traverse' (MkCFM p) = MkCFM (p @{Compose})
+  wander f = roamCofree $ (runIdentity .) . f . (Id .)
+
+export
+Profunctor p => Mapping (CofreeMapping p) where
+  map' (MkCFM p) = MkCFM (p @{Compose})
+  roam = roamCofree
+
+
+
+public export
+data FreeMapping : (p : Type -> Type -> Type) -> Type -> Type -> Type where
+  MkFM : Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b
+
+export
+Profunctor (FreeMapping p) where
+  lmap f (MkFM l m r) = MkFM l m (r . f)
+  rmap f (MkFM l m r) = MkFM (f . l) m r
+  dimap f g (MkFM l m r) = MkFM (g . l) m (r . f)
+
+export
+ProfunctorFunctor FreeMapping where
+  promap f (MkFM l m r) = MkFM l (f m) r
+
+export
+ProfunctorMonad FreeMapping where
+  propure p = MkFM runIdentity p Id
+  projoin (MkFM l' (MkFM l m r) r') = MkFM @{Compose} (l' . map l) m (map r . r')
+
+export
+Functor (FreeMapping p a) where
+  map = rmap
+
+export
+GenStrong Pair (FreeMapping p) where
+  strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
+  strongl = dimap Builtin.swap Builtin.swap . strongr {p=FreeMapping p}
+
+export
+GenStrong Either (FreeMapping p) where
+  strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
+  strongl = dimap Tensor.swap Tensor.swap . strongr {p=FreeMapping p}
+
+export
+Closed (FreeMapping p) where
+  closed (MkFM l m r) = dimap Mor applyMor $ MkFM @{Compose} (map l) m (map r)
+
+roamFree : ((a -> b) -> s -> t) -> FreeMapping p a b -> FreeMapping p s t
+roamFree f (MkFM l m r) = MkFM @{Compose @{functor}} (($ id) . map @{functor} l) m (map @{functor} r . flip f)
+  where
+    functor : Functor (\a => (a -> b) -> t)
+    functor = MkFunctor (\f => (. (. f)))
+
+export
+Traversing (FreeMapping p) where
+  traverse' (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
+  wander f = roamFree $ (runIdentity .) . f . (Id .)
+
+export
+Mapping (FreeMapping p) where
+  map' (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
+  roam = roamFree