module Proarrow.Promonad.Reader where

import Proarrow.Adjunction (Adjunction (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), leftUnitorInvWith, obj2)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, type (+->))
import Proarrow.Helper.CCC
  ( FK (F)
  , lam
  , lift
  , toCCC
  , pattern (:&)
  , type (*)
  )
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..), associatorProdInv)
import Proarrow.Object.Exponential (BiCCC)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Promonad (Procomonad (..))
import Proarrow.Promonad.Writer (Writer (..))

data Reader r a b where
  Reader :: (Ob a, Ob b) => (r && a) ~> b -> Reader r a b

instance (BiCCC k, Ob r) => Profunctor (Reader r :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Reader r a b -> Reader r c d
dimap c ~> a
l b ~> d
r (Reader (r && a) ~> b
f) = ((r && c) ~> d) -> Reader r c d
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((r && a) ~> b) -> Reader r a b
Reader (b ~> d
r (b ~> d) -> ((r && c) ~> b) -> (r && c) ~> d
forall (b :: k) (c :: k) (a :: k). (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
. (r && a) ~> b
f ((r && a) ~> b) -> ((r && c) ~> (r && a)) -> (r && c) ~> b
forall (b :: k) (c :: k) (a :: k). (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
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r Obj r -> (c ~> a) -> (r && c) ~> (r && a)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** c ~> a
l)) ((Ob b, Ob d) => Reader r c d) -> (b ~> d) -> Reader r c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ b ~> d
r ((Ob c, Ob a) => Reader r c d) -> (c ~> a) -> Reader r c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ c ~> a
l
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Reader r a b -> r
\\ Reader (r && a) ~> b
f = r
(Ob a, Ob b) => r
(Ob (r && a), Ob b) => r
r ((Ob (r && a), Ob b) => r) -> ((r && a) ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ (r && a) ~> b
f

instance (BiCCC k, Ob r) => Promonad (Reader r :: k +-> k) where
  id :: forall (a :: k). Ob a => Reader r a a
id = ((r && a) ~> a) -> Reader r a a
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((r && a) ~> b) -> Reader r a b
Reader (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @r)
  Reader @b @c (r && b) ~> c
g . :: forall (b :: k) (c :: k) (a :: k).
Reader r b c -> Reader r a b -> Reader r a c
. Reader @a (r && a) ~> b
f = ((r && a) ~> c) -> Reader r a c
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((r && a) ~> b) -> Reader r a b
Reader (forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(F r * F a) @(F c) (((forall (x :: FK k).
  Cast x (TermF && ('F r * 'F a)) =>
  x ~> ('F r * 'F a))
 -> (TermF && ('F r * 'F a)) ~> 'F c)
-> TermF ~> (('F r * 'F a) ~~> 'F c)
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * ('F r * 'F a)) ~> 'F r
r :& (TermF * ('F r * 'F a)) ~> 'F a
a) -> forall {k} (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
forall (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
lift @(F r * F b) (r && b) ~> c
FromFree ('F r * 'F b) ~> FromFree ('F c)
g ((TermF * ('F r * 'F a)) ~> 'F r
r ((TermF * ('F r * 'F a)) ~> 'F r)
-> ((TermF * ('F r * 'F a)) ~> 'F b)
-> (TermF * ('F r * 'F a)) ~> ('F r && 'F b)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (FromFree ('F r * 'F a) ~> FromFree ('F b))
-> ((TermF * ('F r * 'F a)) ~> ('F r * 'F a))
-> (TermF * ('F r * 'F a)) ~> 'F b
forall {k} (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
lift (r && a) ~> b
FromFree ('F r * 'F a) ~> FromFree ('F b)
f ((TermF * ('F r * 'F a)) ~> 'F r
r ((TermF * ('F r * 'F a)) ~> 'F r)
-> ((TermF * ('F r * 'F a)) ~> 'F a)
-> (TermF * ('F r * 'F a)) ~> ('F r && 'F a)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (TermF * ('F r * 'F a)) ~> 'F a
a))))

instance (Monoid m, BiCCC k) => Procomonad (Reader m :: k +-> k) where
  extract :: Reader m :~> (~>)
extract (Reader (m && a) ~> b
f) = (m && a) ~> b
f ((m && a) ~> b) -> (a ~> (m && a)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (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
. (Unit ~> m) -> a ~> (m ** a)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith (forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @m)
  duplicate :: Reader m :~> (Reader m :.: Reader m)
duplicate (Reader @a (m && a) ~> b
f) = ((m && a) ~> (m && a)) -> Reader m a (m && a)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((r && a) ~> b) -> Reader r a b
Reader (m && a) ~> (m && a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Reader m a (m && a)
-> Reader m (m && a) b -> (:.:) (Reader m) (Reader m) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((m && (m && a)) ~> b) -> Reader m (m && a) b
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((r && a) ~> b) -> Reader r a b
Reader ((m && a) ~> b
f ((m && a) ~> b)
-> ((m && (m && a)) ~> (m && a)) -> (m && (m && a)) ~> b
forall (b :: k) (c :: k) (a :: k). (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
. (((m ** m) ~> m
(m && m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend :: m && m ~> m) ((m && m) ~> m) -> (a ~> a) -> ((m && m) && a) ~> (m && a)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (((m && m) && a) ~> (m && a))
-> ((m && (m && a)) ~> ((m && m) && a))
-> (m && (m && a)) ~> (m && a)
forall (b :: k) (c :: k) (a :: k). (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
. forall (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @m @m @a) ((Ob (m && a), Ob b) => (:.:) (Reader m) (Reader m) a b)
-> ((m && a) ~> b) -> (:.:) (Reader m) (Reader m) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ (m && a) ~> b
f

instance (BiCCC k, Ob r) => MonoidalProfunctor (Reader r :: k +-> k) where
  par0 :: Reader r Unit Unit
par0 = Reader r Unit Unit
Reader r TerminalObject TerminalObject
forall (a :: k). Ob a => Reader r a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Reader @x1 @x2 (r && x1) ~> x2
f par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Reader r x1 x2 -> Reader r y1 y2 -> Reader r (x1 ** y1) (x2 ** y2)
`par` Reader @y1 @y2 (r && y1) ~> y2
g =
    ((r && (x1 ** y1)) ~> (x2 ** y2)) -> Reader r (x1 ** y1) (x2 ** y2)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((r && a) ~> b) -> Reader r a b
Reader
      ( ( forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(F r * (F x1 * F y1)) @(F x2 * F y2)
            ( ((forall (x :: FK k).
  Cast x (TermF && ('F r * ('F x1 * 'F y1))) =>
  x ~> ('F r * ('F x1 * 'F y1)))
 -> (TermF && ('F r * ('F x1 * 'F y1))) ~> ('F x2 * 'F y2))
-> TermF ~> (('F r * ('F x1 * 'F y1)) ~~> ('F x2 * 'F y2))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F r
r :& ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F x1
x :& (TermF * ('F r * ('F x1 * 'F y1))) ~> 'F y1
y)) ->
                let f' :: ((TermF * ('F r * ('F x1 * 'F y1))) ~> ('F r * 'F x1))
-> (TermF * ('F r * ('F x1 * 'F y1))) ~> 'F x2
f' = forall {k} (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
forall (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
lift @(F r * F x1) (r && x1) ~> x2
FromFree ('F r * 'F x1) ~> FromFree ('F x2)
f
                    g' :: ((TermF * ('F r * ('F x1 * 'F y1))) ~> ('F r * 'F y1))
-> (TermF * ('F r * ('F x1 * 'F y1))) ~> 'F y2
g' = forall {k} (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
forall (a :: FK k) (b :: FK k) (i :: FK k).
(BiCCC k, Ob a, Ob b) =>
(FromFree a ~> FromFree b) -> (i ~> a) -> i ~> b
lift @(F r * F y1) (r && y1) ~> y2
FromFree ('F r * 'F y1) ~> FromFree ('F y2)
g
                in ((TermF * ('F r * ('F x1 * 'F y1))) ~> ('F r * 'F x1))
-> (TermF * ('F r * ('F x1 * 'F y1))) ~> 'F x2
f' ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F r
r ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F r)
-> ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F x1)
-> (TermF * ('F r * ('F x1 * 'F y1))) ~> ('F r && 'F x1)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (TermF * ('F r * ('F x1 * 'F y1))) ~> 'F x1
x) ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F x2)
-> ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F y2)
-> (TermF * ('F r * ('F x1 * 'F y1))) ~> ('F x2 && 'F y2)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& ((TermF * ('F r * ('F x1 * 'F y1))) ~> ('F r * 'F y1))
-> (TermF * ('F r * ('F x1 * 'F y1))) ~> 'F y2
g' ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F r
r ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F r)
-> ((TermF * ('F r * ('F x1 * 'F y1))) ~> 'F y1)
-> (TermF * ('F r * ('F x1 * 'F y1))) ~> ('F r && 'F y1)
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (TermF * ('F r * ('F x1 * 'F y1))) ~> 'F y1
y)
            )
        )
          ((r && (x1 && y1)) ~> (x2 ** y2))
-> ((r && (x1 ** y1)) ~> (r && (x1 && y1)))
-> (r && (x1 ** y1)) ~> (x2 ** y2)
forall (b :: k) (c :: k) (a :: k). (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
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r Obj r
-> ((x1 ** y1) ~> (x1 && y1))
-> (r && (x1 ** y1)) ~> (r && (x1 && y1))
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** (forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @x1 @y1 :: x1 ** y1 ~> x1 && y1))
      )
      ((Ob (x1 ** y1), Ob (x1 ** y1)) => Reader r (x1 ** y1) (x2 ** y2))
-> Obj (x1 ** y1) -> Reader r (x1 ** y1) (x2 ** y2)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @x1 @y1
      ((Ob (x2 ** y2), Ob (x2 ** y2)) => Reader r (x1 ** y1) (x2 ** y2))
-> ((x2 ** y2) ~> (x2 ** y2)) -> Reader r (x1 ** y1) (x2 ** y2)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @x2 @y2

instance (BiCCC k, Ob r) => Adjunction (Writer r :: k +-> k) (Reader r) where
  unit :: forall (a :: k). Ob a => (:.:) (Reader r) (Writer r) a a
unit @a = ((r && a) ~> (r && a)) -> Reader r a (r && a)
forall {k} (a :: k) (b :: k) (r :: k).
(Ob a, Ob b) =>
((r && a) ~> b) -> Reader r a b
Reader (r && a) ~> (r && a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Reader r a (r && a)
-> Writer r (r && a) a -> (:.:) (Reader r) (Writer r) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((r && a) ~> (r && a)) -> Writer r (r && a) a
forall {k} (a :: k) (b :: k) (m :: k).
(Ob a, Ob b) =>
(a ~> (m && b)) -> Writer m a b
Writer (r && a) ~> (r && a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob (r && a), Ob (r && a)) => (:.:) (Reader r) (Writer r) a a)
-> ((r && a) ~> (r && a)) -> (:.:) (Reader r) (Writer r) a a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r Obj r -> (a ~> a) -> (r && a) ~> (r && a)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)
  counit :: (Writer r :.: Reader r) :~> (~>)
counit (Writer a ~> (r && b)
f :.: Reader (r && b) ~> b
g) = (r && b) ~> b
g ((r && b) ~> b) -> (a ~> (r && b)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (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
. a ~> (r && b)
f