module Proarrow.Profunctor.Wrapped where

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Core (Profunctor (..), Promonad (..))
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Profunctor.Day (Day (..), DayUnit (..))
import Proarrow.Category.Dagger (DaggerProfunctor (..))

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}

instance (Profunctor p) => Profunctor (Wrapped p) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Wrapped p a b -> Wrapped p c d
dimap c ~> a
f b ~> d
g = p c d -> Wrapped p c d
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Wrapped p a b
Wrapped (p c d -> Wrapped p c d)
-> (Wrapped p a b -> p c d) -> Wrapped p a b -> Wrapped p c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
f b ~> d
g (p a b -> p c d)
-> (Wrapped p a b -> p a b) -> Wrapped p a b -> p c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> Wrapped p a b -> r
\\ Wrapped p a b
p = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Promonad p) => Promonad (Wrapped p) where
  id :: forall (a :: k). Ob a => Wrapped p a a
id = p a a -> Wrapped p a a
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Wrapped p a b
Wrapped p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Wrapped p b c
f . :: forall (b :: k) (c :: k) (a :: k).
Wrapped p b c -> Wrapped p a b -> Wrapped p a c
. Wrapped p a b
g = p a c -> Wrapped p a c
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Wrapped p a b
Wrapped (p b c
f p b c -> p a b -> p a c
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b
g)

instance (MonoidalProfunctor p) => MonoidalProfunctor (Wrapped p) where
  par0 :: Wrapped p Unit Unit
par0 = p Unit Unit -> Wrapped p Unit Unit
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Wrapped p a b
Wrapped p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Wrapped p x1 x2
l par :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
Wrapped p x1 x2
-> Wrapped p y1 y2 -> Wrapped p (x1 ** y1) (x2 ** y2)
`par` Wrapped p y1 y2
r = p (x1 ** y1) (x2 ** y2) -> Wrapped p (x1 ** y1) (x2 ** y2)
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Wrapped p a b
Wrapped (p x1 x2
l p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
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 y1 y2
r)

instance (DaggerProfunctor p) => DaggerProfunctor (Wrapped p) where
  dagger :: forall (a :: j) (b :: j). Wrapped p a b -> Wrapped p b a
dagger = p b a -> Wrapped p b a
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Wrapped p a b
Wrapped (p b a -> Wrapped p b a)
-> (Wrapped p a b -> p b a) -> Wrapped p a b -> Wrapped p b a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> p b a
forall (a :: j) (b :: j). p a b -> p b a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger (p a b -> p b a)
-> (Wrapped p a b -> p a b) -> Wrapped p a b -> p b a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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

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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
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 {k} {j} (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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
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 {k} {j} (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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
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))