module Proarrow.Profunctor.Wrapped where import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..)) import Proarrow.Category.Instance.Prof (Prof (..)) import Proarrow.Category.Monoidal (MonoidalProfunctor (..)) import Proarrow.Core (Iso, Profunctor (..), Promonad (..), iso) import Proarrow.Monoid (Comonoid (..), Monoid (..)) import Proarrow.Profunctor.Corepresentable (Corepresentable (..)) import Proarrow.Profunctor.Day (Day (..), DayUnit (..)) import Proarrow.Profunctor.Representable (Representable (..)) newtype Wrapped p a b = Wrapped {forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k). Wrapped p a b -> p a b unWrapped :: p a b} deriving newtype (CategoryOf k CategoryOf j (CategoryOf j, CategoryOf k) => (forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> Wrapped p a b -> Wrapped p c d) -> (forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Wrapped p a b -> r) -> Profunctor (Wrapped p) forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> Wrapped p a b -> Wrapped p c d forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Wrapped p a b -> r forall k j (p :: k -> j -> Type). Profunctor p => CategoryOf k forall k j (p :: k -> j -> Type). Profunctor p => CategoryOf j forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j) (d :: j). Profunctor p => (c ~> a) -> (b ~> d) -> Wrapped p a b -> Wrapped p c d forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r. Profunctor p => ((Ob a, Ob b) => r) -> Wrapped p a b -> r forall {j} {k} (p :: j +-> k). (CategoryOf j, CategoryOf k) => (forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> p a b -> p c d) -> (forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r) -> Profunctor p $cdimap :: forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j) (d :: j). Profunctor p => (c ~> a) -> (b ~> d) -> Wrapped p a b -> Wrapped p c d dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> Wrapped p a b -> Wrapped p c d $c\\ :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r. Profunctor p => ((Ob a, Ob b) => r) -> Wrapped p a b -> r \\ :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Wrapped p a b -> r Profunctor, Profunctor (Wrapped p) Profunctor (Wrapped p) => (forall (a :: k). Ob a => Wrapped p a a) -> (forall (b :: k) (c :: k) (a :: k). Wrapped p b c -> Wrapped p a b -> Wrapped p a c) -> Promonad (Wrapped p) forall (a :: k). Ob a => Wrapped p a a forall (b :: k) (c :: k) (a :: k). Wrapped p b c -> Wrapped p a b -> Wrapped p a c forall {k} (p :: k +-> k). Profunctor p => (forall (a :: k). Ob a => p a a) -> (forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c) -> Promonad p forall k (p :: k -> k -> Type). Promonad p => Profunctor (Wrapped p) forall k (p :: k -> k -> Type) (a :: k). (Promonad p, Ob a) => Wrapped p a a forall k (p :: k -> k -> Type) (b :: k) (c :: k) (a :: k). Promonad p => Wrapped p b c -> Wrapped p a b -> Wrapped p a c $cid :: forall k (p :: k -> k -> Type) (a :: k). (Promonad p, Ob a) => Wrapped p a a id :: forall (a :: k). Ob a => Wrapped p a a $c. :: forall k (p :: k -> k -> Type) (b :: k) (c :: k) (a :: k). Promonad p => Wrapped p b c -> Wrapped p a b -> Wrapped p a c . :: forall (b :: k) (c :: k) (a :: k). Wrapped p b c -> Wrapped p a b -> Wrapped p a c Promonad, Profunctor (Wrapped p) Monoidal k Monoidal j Wrapped p Unit Unit (Monoidal j, Monoidal k, Profunctor (Wrapped p)) => Wrapped p Unit Unit -> (forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). Wrapped p x1 x2 -> Wrapped p y1 y2 -> Wrapped p (x1 ** y1) (x2 ** y2)) -> MonoidalProfunctor (Wrapped p) forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). Wrapped p x1 x2 -> Wrapped p y1 y2 -> Wrapped p (x1 ** y1) (x2 ** y2) forall k j (p :: k -> j -> Type). MonoidalProfunctor p => Profunctor (Wrapped p) forall k j (p :: k -> j -> Type). MonoidalProfunctor p => Monoidal k forall k j (p :: k -> j -> Type). MonoidalProfunctor p => Monoidal j forall k j (p :: k -> j -> Type). MonoidalProfunctor p => Wrapped p Unit Unit forall k j (p :: k -> j -> Type) (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). MonoidalProfunctor p => Wrapped p x1 x2 -> Wrapped p y1 y2 -> Wrapped p (x1 ** y1) (x2 ** y2) forall {j} {k} (p :: j +-> k). (Monoidal j, Monoidal k, Profunctor p) => p Unit Unit -> (forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)) -> MonoidalProfunctor p $cpar0 :: forall k j (p :: k -> j -> Type). MonoidalProfunctor p => Wrapped p Unit Unit par0 :: Wrapped p Unit Unit $cpar :: forall k j (p :: k -> j -> Type) (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). MonoidalProfunctor p => Wrapped p x1 x2 -> Wrapped p y1 y2 -> Wrapped p (x1 ** y1) (x2 ** y2) par :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). Wrapped p x1 x2 -> Wrapped p y1 y2 -> Wrapped p (x1 ** y1) (x2 ** y2) MonoidalProfunctor, Profunctor (Wrapped p) Dagger k (Dagger k, Profunctor (Wrapped p)) => (forall (a :: k) (b :: k). Wrapped p a b -> Wrapped p b a) -> DaggerProfunctor (Wrapped p) forall (a :: k) (b :: k). Wrapped p a b -> Wrapped p b a forall k (p :: k +-> k). (Dagger k, Profunctor p) => (forall (a :: k) (b :: k). p a b -> p b a) -> DaggerProfunctor p forall k (p :: k -> k -> Type). DaggerProfunctor p => Profunctor (Wrapped p) forall k (p :: k -> k -> Type). DaggerProfunctor p => Dagger k forall k (p :: k -> k -> Type) (a :: k) (b :: k). DaggerProfunctor p => Wrapped p a b -> Wrapped p b a $cdagger :: forall k (p :: k -> k -> Type) (a :: k) (b :: k). DaggerProfunctor p => Wrapped p a b -> Wrapped p b a dagger :: forall (a :: k) (b :: k). Wrapped p a b -> Wrapped p b a DaggerProfunctor, Profunctor (Wrapped p) Profunctor (Wrapped p) => (forall (a :: k) (b :: j). Wrapped p a b -> a ~> (Wrapped p % b)) -> (forall (b :: j) (a :: k). Ob b => (a ~> (Wrapped p % b)) -> Wrapped p a b) -> (forall (a :: j) (b :: j). (a ~> b) -> (Wrapped p % a) ~> (Wrapped p % b)) -> Representable (Wrapped p) forall (a :: k) (b :: j). Wrapped p a b -> a ~> (Wrapped p % b) forall (b :: j) (a :: k). Ob b => (a ~> (Wrapped p % b)) -> Wrapped p a b forall (a :: j) (b :: j). (a ~> b) -> (Wrapped p % a) ~> (Wrapped p % b) forall k j (p :: k -> j -> Type). Representable p => Profunctor (Wrapped p) forall k j (p :: k -> j -> Type) (a :: k) (b :: j). Representable p => Wrapped p a b -> a ~> (Wrapped p % b) forall k j (p :: k -> j -> Type) (b :: j) (a :: k). (Representable p, Ob b) => (a ~> (Wrapped p % b)) -> Wrapped p a b forall k j (p :: k -> j -> Type) (a :: j) (b :: j). Representable p => (a ~> b) -> (Wrapped p % a) ~> (Wrapped p % b) forall {j} {k} (p :: j +-> k). Profunctor p => (forall (a :: k) (b :: j). p a b -> a ~> (p % b)) -> (forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b) -> (forall (a :: j) (b :: j). (a ~> b) -> (p % a) ~> (p % b)) -> Representable p $cindex :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j). Representable p => Wrapped p a b -> a ~> (Wrapped p % b) index :: forall (a :: k) (b :: j). Wrapped p a b -> a ~> (Wrapped p % b) $ctabulate :: forall k j (p :: k -> j -> Type) (b :: j) (a :: k). (Representable p, Ob b) => (a ~> (Wrapped p % b)) -> Wrapped p a b tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (Wrapped p % b)) -> Wrapped p a b $crepMap :: forall k j (p :: k -> j -> Type) (a :: j) (b :: j). Representable p => (a ~> b) -> (Wrapped p % a) ~> (Wrapped p % b) repMap :: forall (a :: j) (b :: j). (a ~> b) -> (Wrapped p % a) ~> (Wrapped p % b) Representable, Profunctor (Wrapped p) Profunctor (Wrapped p) => (forall (a :: k) (b :: j). Wrapped p a b -> (Wrapped p %% a) ~> b) -> (forall (a :: k) (b :: j). Ob a => ((Wrapped p %% a) ~> b) -> Wrapped p a b) -> (forall (a :: k) (b :: k). (a ~> b) -> (Wrapped p %% a) ~> (Wrapped p %% b)) -> Corepresentable (Wrapped p) forall (a :: k) (b :: k). (a ~> b) -> (Wrapped p %% a) ~> (Wrapped p %% b) forall (a :: k) (b :: j). Ob a => ((Wrapped p %% a) ~> b) -> Wrapped p a b forall (a :: k) (b :: j). Wrapped p a b -> (Wrapped p %% a) ~> b forall k j (p :: k -> j -> Type). Corepresentable p => Profunctor (Wrapped p) forall k j (p :: k -> j -> Type) (a :: k) (b :: k). Corepresentable p => (a ~> b) -> (Wrapped p %% a) ~> (Wrapped p %% b) forall k j (p :: k -> j -> Type) (a :: k) (b :: j). (Corepresentable p, Ob a) => ((Wrapped p %% a) ~> b) -> Wrapped p a b forall k j (p :: k -> j -> Type) (a :: k) (b :: j). Corepresentable p => Wrapped p a b -> (Wrapped p %% a) ~> b forall {j} {k} (p :: j +-> k). Profunctor p => (forall (a :: k) (b :: j). p a b -> (p %% a) ~> b) -> (forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b) -> (forall (a :: k) (b :: k). (a ~> b) -> (p %% a) ~> (p %% b)) -> Corepresentable p $ccoindex :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j). Corepresentable p => Wrapped p a b -> (Wrapped p %% a) ~> b coindex :: forall (a :: k) (b :: j). Wrapped p a b -> (Wrapped p %% a) ~> b $ccotabulate :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j). (Corepresentable p, Ob a) => ((Wrapped p %% a) ~> b) -> Wrapped p a b cotabulate :: forall (a :: k) (b :: j). Ob a => ((Wrapped p %% a) ~> b) -> Wrapped p a b $ccorepMap :: forall k j (p :: k -> j -> Type) (a :: k) (b :: k). Corepresentable p => (a ~> b) -> (Wrapped p %% a) ~> (Wrapped p %% b) corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Wrapped p %% a) ~> (Wrapped p %% b) Corepresentable) instance (Comonoid c, Monoid m, MonoidalProfunctor p) => Monoid (Wrapped p c m) where mempty :: Unit ~> Wrapped p c m mempty () = (c ~> Unit) -> (Unit ~> m) -> Wrapped p Unit Unit -> Wrapped p c m forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> Wrapped p a b -> Wrapped p c d forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap c ~> Unit forall {k} (c :: k). Comonoid c => c ~> Unit counit Unit ~> m forall {k} (m :: k). Monoid m => Unit ~> m mempty Wrapped p Unit Unit forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit par0 mappend :: (Wrapped p c m ** Wrapped p c m) ~> Wrapped p c m mappend (Wrapped p c m l, Wrapped p c m r) = (c ~> (c ** c)) -> ((m ** m) ~> m) -> Wrapped p (c ** c) (m ** m) -> Wrapped p c m forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> Wrapped p a b -> Wrapped p c d forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap c ~> (c ** c) forall {k} (c :: k). Comonoid c => c ~> (c ** c) comult (m ** m) ~> m forall {k} (m :: k). Monoid m => (m ** m) ~> m mappend (Wrapped p c m l Wrapped p c m -> Wrapped p c m -> Wrapped p (c ** c) (m ** m) forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k). Wrapped p x1 x2 -> Wrapped p y1 y2 -> Wrapped p (x1 ** y1) (x2 ** y2) forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). MonoidalProfunctor p => p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2) `par` Wrapped p c m r) instance (MonoidalProfunctor p) => Monoid (Wrapped p) where mempty :: Unit ~> Wrapped p mempty = (DayUnit :~> Wrapped p) -> Prof DayUnit (Wrapped p) forall {j} {k} (p :: j +-> k) (q :: j +-> k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(DayUnit a ~> Unit f Unit ~> b g) -> p a b -> Wrapped p a b forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k). p a b -> Wrapped p a b Wrapped ((a ~> Unit) -> (Unit ~> b) -> p Unit Unit -> p a b forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> p a b -> p c d forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap a ~> Unit f Unit ~> b g p Unit Unit forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit par0) mappend :: (Wrapped p ** Wrapped p) ~> Wrapped p mappend = (Day (Wrapped p) (Wrapped p) :~> Wrapped p) -> Prof (Day (Wrapped p) (Wrapped p)) (Wrapped p) forall {j} {k} (p :: j +-> k) (q :: j +-> k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day a ~> (c ** e) f (Wrapped p c d p) (Wrapped p e f q) (d ** f) ~> b g) -> p a b -> Wrapped p a b forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k). p a b -> Wrapped p a b Wrapped ((a ~> (c ** e)) -> ((d ** f) ~> b) -> p (c ** e) (d ** f) -> p a b forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> p a b -> p c d forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap a ~> (c ** e) f (d ** f) ~> b g (p c d p p c d -> p e f -> p (c ** e) (d ** f) forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k). p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2) forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j). MonoidalProfunctor p => p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2) `par` p e f q)) wrapped :: Iso (p a b) (p a' b') (Wrapped p a b) (Wrapped p a' b') wrapped :: forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k) (a' :: k) (b' :: k) (p :: Type -> Type -> Type). Profunctor p => p (Wrapped p a b) (Wrapped p a' b') -> p (p a b) (p a' b') wrapped = (p a b ~> Wrapped p a b) -> (Wrapped p a' b' ~> p a' b') -> Iso (p a b) (p a' b') (Wrapped p a b) (Wrapped p a' b') forall {k1} {k2} (s :: k1) (a :: k1) (b :: k2) (t :: k2). (s ~> a) -> (b ~> t) -> Iso s t a b iso p a b ~> Wrapped p a b p a b -> Wrapped p a b forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k). p a b -> Wrapped p a b Wrapped Wrapped p a' b' ~> p a' b' Wrapped p a' b' -> p a' b' forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k). Wrapped p a b -> p a b unWrapped