module Proarrow.Promonad.State where

import Prelude (($))

import Proarrow.Adjunction qualified as Adj
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), swap', leftUnitorWith)
import Proarrow.Category.Monoidal.Action (SelfAction, Strong (..))
import Proarrow.Category.Opposite (OPPOSITE (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), arr, obj, type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Object (ObjDict (..), objDicts)
import Proarrow.Object.Dual (CompactClosed)
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable)
import Proarrow.Profunctor.Representable (Representable (..))
import Proarrow.Promonad.Reader (Reader (..))
import Proarrow.Promonad.Writer (Writer (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Object.BinaryProduct ((&&&))
import Proarrow.Monoid (Comonoid (..))

type State s = StateT s Id
pattern State :: forall {k} a b s. (Monoidal k, Ob (s :: k)) => (Ob a, Ob b) => (s ** a) ~> (s ** b) -> State s a b
pattern $bState :: forall {k :: Kind} (a :: k) (b :: k) (s :: k).
(Monoidal k, Ob s, Ob a, Ob b) =>
((s ** a) ~> (s ** b)) -> State s a b
$mState :: forall {r} {k :: Kind} {a :: k} {b :: k} {s :: k}.
(Monoidal k, Ob s) =>
State s a b
-> ((Ob a, Ob b) => ((s ** a) ~> (s ** b)) -> r)
-> ((# #) -> r)
-> r
State f <- (runStateT &&& objDicts -> (Id f, (ObjDict, ObjDict)))
  where
    State (s ** a) ~> (s ** b)
f = (:.:) (Reader ('OP s) :.: Id) (Writer s) a b -> StateT s Id a b
forall {i :: Kind} (s :: i) (p :: i +-> i) (a :: i) (b :: i).
(:.:) (Reader ('OP s) :.: p) (Writer s) a b -> StateT s p a b
StateT (((s ** a) ~> (s ** a)) -> Reader ('OP s) a (s ** a)
forall {k :: Kind} (a :: k) (b :: k) (r1 :: k).
Ob a =>
((r1 ** a) ~> b) -> Reader ('OP r1) a b
Reader (s ** a) ~> (s ** a)
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id Reader ('OP s) a (s ** a)
-> Id (s ** a) (s ** b) -> (:.:) (Reader ('OP s)) Id a (s ** b)
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((s ** a) ~> (s ** b)) -> Id (s ** a) (s ** b)
forall (k :: Kind) (a :: k) (b :: k). (a ~> b) -> Id a b
Id (s ** a) ~> (s ** b)
f (:.:) (Reader ('OP s)) Id a (s ** b)
-> Writer s (s ** b) b
-> (:.:) (Reader ('OP s) :.: Id) (Writer s) a b
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((s ** b) ~> (s ** b)) -> Writer s (s ** b) b
forall {k :: Kind} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (s ** b) ~> (s ** b)
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id) ((Ob (s ** a), Ob (s ** b)) => StateT s Id a b)
-> ((s ** a) ~> (s ** b)) -> StateT s Id a b
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (s ** a) ~> (s ** b)
f
{-# COMPLETE State #-}

-- | Note: This is only premonoidal, not monoidal.
instance (SymMonoidal k, Ob s) => MonoidalProfunctor (State (s :: k)) where
  par0 :: State s Unit Unit
par0 = ((s ** Unit) ~> (s ** Unit)) -> State s Unit Unit
forall {k :: Kind} (a :: k) (b :: k) (s :: k).
(Monoidal k, Ob s, Ob a, Ob b) =>
((s ** a) ~> (s ** b)) -> State s a b
State (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s Obj s -> (Unit ~> Unit) -> (s ** Unit) ~> (s ** Unit)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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` Unit ~> Unit
forall {j :: Kind} {k :: Kind} (p :: j +-> k).
MonoidalProfunctor p =>
p Unit Unit
par0) ((Ob Unit, Ob Unit) => State s Unit Unit)
-> (Unit ~> Unit) -> State s Unit Unit
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Unit ~> Unit
forall {j :: Kind} {k :: Kind} (p :: j +-> k).
MonoidalProfunctor p =>
p Unit Unit
par0 :: (Unit :: k) ~> Unit)
  par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
State s x1 x2 -> State s y1 y2 -> State s (x1 ** y1) (x2 ** y2)
par (State @a1 @b1 (s ** x1) ~> (s ** x2)
f) (State @a2 @b2 (s ** y1) ~> (s ** y2)
g) =
    let s :: Obj s
s = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s; a1 :: Obj x1
a1 = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a1; b1 :: Obj x2
b1 = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b1; a2 :: Obj y1
a2 = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a2; b2 :: Obj y2
b2 = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b2
    in ((s ** (x1 ** y1)) ~> (s ** (x2 ** y2)))
-> State s (x1 ** y1) (x2 ** y2)
forall {k :: Kind} (a :: k) (b :: k) (s :: k).
(Monoidal k, Ob s, Ob a, Ob b) =>
((s ** a) ~> (s ** b)) -> State s a b
State
         ( (Obj s
s Obj s
-> ((y2 ** x2) ~> (x2 ** y2))
-> (s ** (y2 ** x2)) ~> (s ** (x2 ** y2))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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` Obj y2 -> Obj x2 -> (y2 ** x2) ~> (x2 ** y2)
forall {k :: Kind} (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' Obj y2
b2 Obj x2
b1)
             ((s ** (y2 ** x2)) ~> (s ** (x2 ** y2)))
-> ((s ** (x1 ** y1)) ~> (s ** (y2 ** x2)))
-> (s ** (x1 ** y1)) ~> (s ** (x2 ** y2))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @s @b2 @b1
             (((s ** y2) ** x2) ~> (s ** (y2 ** x2)))
-> ((s ** (x1 ** y1)) ~> ((s ** y2) ** x2))
-> (s ** (x1 ** y1)) ~> (s ** (y2 ** x2))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((s ** y1) ~> (s ** y2)
g ((s ** y1) ~> (s ** y2))
-> Obj x2 -> ((s ** y1) ** x2) ~> ((s ** y2) ** x2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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` Obj x2
b1)
             (((s ** y1) ** x2) ~> ((s ** y2) ** x2))
-> ((s ** (x1 ** y1)) ~> ((s ** y1) ** x2))
-> (s ** (x1 ** y1)) ~> ((s ** y2) ** x2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @s @a2 @b1
             ((s ** (y1 ** x2)) ~> ((s ** y1) ** x2))
-> ((s ** (x1 ** y1)) ~> (s ** (y1 ** x2)))
-> (s ** (x1 ** y1)) ~> ((s ** y1) ** x2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj s
s Obj s
-> ((x2 ** y1) ~> (y1 ** x2))
-> (s ** (x2 ** y1)) ~> (s ** (y1 ** x2))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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` Obj x2 -> Obj y1 -> (x2 ** y1) ~> (y1 ** x2)
forall {k :: Kind} (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' Obj x2
b1 Obj y1
a2)
             ((s ** (x2 ** y1)) ~> (s ** (y1 ** x2)))
-> ((s ** (x1 ** y1)) ~> (s ** (x2 ** y1)))
-> (s ** (x1 ** y1)) ~> (s ** (y1 ** x2))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @s @b1 @a2
             (((s ** x2) ** y1) ~> (s ** (x2 ** y1)))
-> ((s ** (x1 ** y1)) ~> ((s ** x2) ** y1))
-> (s ** (x1 ** y1)) ~> (s ** (x2 ** y1))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((s ** x1) ~> (s ** x2)
f ((s ** x1) ~> (s ** x2))
-> Obj y1 -> ((s ** x1) ** y1) ~> ((s ** x2) ** y1)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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` Obj y1
a2)
             (((s ** x1) ** y1) ~> ((s ** x2) ** y1))
-> ((s ** (x1 ** y1)) ~> ((s ** x1) ** y1))
-> (s ** (x1 ** y1)) ~> ((s ** x2) ** y1)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @s @a1 @a2
         )
         ((Ob (x1 ** y1), Ob (x1 ** y1)) => State s (x1 ** y1) (x2 ** y2))
-> ((x1 ** y1) ~> (x1 ** y1)) -> State s (x1 ** y1) (x2 ** y2)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj x1
a1 Obj x1 -> Obj y1 -> (x1 ** y1) ~> (x1 ** y1)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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` Obj y1
a2)
         ((Ob (x2 ** y2), Ob (x2 ** y2)) => State s (x1 ** y1) (x2 ** y2))
-> ((x2 ** y2) ~> (x2 ** y2)) -> State s (x1 ** y1) (x2 ** y2)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj x2
b1 Obj x2 -> Obj y2 -> (x2 ** y2) ~> (x2 ** y2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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` Obj y2
b2)

type StateT :: k -> k +-> k -> k +-> k
newtype StateT s p a b where
  StateT :: (Reader (OP s) :.: p :.: Writer s) a b -> StateT s p a b

runStateT :: (Profunctor p) => StateT s p a b -> p (s ** a) (s ** b)
runStateT :: forall {k :: Kind} (p :: k +-> k) (s :: k) (a :: k) (b :: k).
Profunctor p =>
StateT s p a b -> p (s ** a) (s ** b)
runStateT (StateT (Reader (r1 ** a) ~> b
f :.: p b b
p :.: Writer b ~> (s ** b)
g)) = ((s ** a) ~> b) -> (b ~> (s ** b)) -> p b b -> p (s ** a) (s ** b)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (c :: k) (a :: k)
       (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (s ** a) ~> b
(r1 ** a) ~> b
f b ~> (s ** b)
g p b b
p

get :: forall {k} p s. (Promonad p, Monoidal k, Comonoid (s :: k)) => StateT s p Unit s
get :: forall {k :: Kind} (p :: k +-> k) (s :: k).
(Promonad p, Monoidal k, Comonoid s) =>
StateT s p Unit s
get = (:.:) (Reader ('OP s) :.: p) (Writer s) Unit s -> StateT s p Unit s
forall {i :: Kind} (s :: i) (p :: i +-> i) (a :: i) (b :: i).
(:.:) (Reader ('OP s) :.: p) (Writer s) a b -> StateT s p a b
StateT (((s ** Unit) ~> s) -> Reader ('OP s) Unit s
forall {k :: Kind} (a :: k) (b :: k) (r1 :: k).
Ob a =>
((r1 ** a) ~> b) -> Reader ('OP r1) a b
Reader (forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @s) Reader ('OP s) Unit s -> p s s -> (:.:) (Reader ('OP s)) p Unit s
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p s s
forall (a :: k). Ob a => p a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id (:.:) (Reader ('OP s)) p Unit s
-> Writer s s s -> (:.:) (Reader ('OP s) :.: p) (Writer s) Unit s
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (s ~> (s ** s)) -> Writer s s s
forall {k :: Kind} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k :: Kind} (c :: k). Comonoid c => c ~> (c ** c)
comult @s))

put :: forall {k} p s. (Promonad p, Monoidal k, Comonoid (s :: k)) => StateT s p s Unit
put :: forall {k :: Kind} (p :: k +-> k) (s :: k).
(Promonad p, Monoidal k, Comonoid s) =>
StateT s p s Unit
put = (:.:) (Reader ('OP s) :.: p) (Writer s) s Unit -> StateT s p s Unit
forall {i :: Kind} (s :: i) (p :: i +-> i) (a :: i) (b :: i).
(:.:) (Reader ('OP s) :.: p) (Writer s) a b -> StateT s p a b
StateT (((s ** s) ~> s) -> Reader ('OP s) s s
forall {k :: Kind} (a :: k) (b :: k) (r1 :: k).
Ob a =>
((r1 ** a) ~> b) -> Reader ('OP r1) a b
Reader ((s ~> Unit) -> (s ** s) ~> s
forall {k :: Kind} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (c :: k). Comonoid c => c ~> Unit
forall {k :: Kind} (c :: k). Comonoid c => c ~> Unit
counit @s)) Reader ('OP s) s s -> p s s -> (:.:) (Reader ('OP s)) p s s
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p s s
forall (a :: k). Ob a => p a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id (:.:) (Reader ('OP s)) p s s
-> Writer s s Unit
-> (:.:) (Reader ('OP s) :.: p) (Writer s) s Unit
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (s ~> (s ** Unit)) -> Writer s s Unit
forall {k :: Kind} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @k @s))

deriving newtype instance (Profunctor p, Monoidal k, Ob (s :: k)) => Profunctor (StateT s p)
deriving newtype instance (Representable p, Ob (s :: k), SymMonoidal k, Closed k) => Representable (StateT s p)
deriving newtype instance
  (Corepresentable p, Ob (s :: k), SelfAction k, CompactClosed k) => Corepresentable (StateT s p)
deriving newtype instance (Strong k p, Ob (s :: k), SelfAction k) => Strong k (StateT s p)

instance (Ob (s :: k), SelfAction k, Strong k p, Promonad p) => Promonad (StateT s p) where
  id :: forall (a :: k). Ob a => StateT s p a a
id @a = forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @s @a ((Ob (s ** a) => StateT s p a a) -> StateT s p a a)
-> (Ob (s ** a) => StateT s p a a) -> StateT s p a a
forall a b. (a -> b) -> a -> b
$ (:.:) (Reader ('OP s) :.: p) (Writer s) a a -> StateT s p a a
forall {i :: Kind} (s :: i) (p :: i +-> i) (a :: i) (b :: i).
(:.:) (Reader ('OP s) :.: p) (Writer s) a b -> StateT s p a b
StateT (((s ** a) ~> (s ** a)) -> Reader ('OP s) a (s ** a)
forall {k :: Kind} (a :: k) (b :: k) (r1 :: k).
Ob a =>
((r1 ** a) ~> b) -> Reader ('OP r1) a b
Reader (s ** a) ~> (s ** a)
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id Reader ('OP s) a (s ** a)
-> p (s ** a) (Act s a) -> (:.:) (Reader ('OP s)) p a (Act s a)
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (s ~> s) -> p a a -> p (Act s a) (Act s a)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c :: Kind} {d :: Kind} (m :: Kind) (p :: c +-> d) (a :: m)
       (b :: m) (x :: d) (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s) (forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
forall (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id @p @a) (:.:) (Reader ('OP s)) p a (Act s a)
-> Writer s (Act s a) a
-> (:.:) (Reader ('OP s) :.: p) (Writer s) a a
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (Act s a ~> (s ** a)) -> Writer s (Act s a) a
forall {k :: Kind} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (s ** a) ~> (s ** a)
Act s a ~> (s ** a)
forall (a :: k). Ob a => a ~> a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id)
  StateT (Reader ('OP s) b b
r1 :.: p b b
p1 :.: Writer s b c
w1) . :: forall (b :: k) (c :: k) (a :: k).
StateT s p b c -> StateT s p a b -> StateT s p a c
. StateT (Reader ('OP s) a b
r2 :.: p b b
p2 :.: Writer s b b
w2) = (:.:) (Reader ('OP s) :.: p) (Writer s) a c -> StateT s p a c
forall {i :: Kind} (s :: i) (p :: i +-> i) (a :: i) (b :: i).
(:.:) (Reader ('OP s) :.: p) (Writer s) a b -> StateT s p a b
StateT (Reader ('OP s) a b
r2 Reader ('OP s) a b -> p b b -> (:.:) (Reader ('OP s)) p a b
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (p b b
p1 p b b -> p b b -> p b b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (b ~> b) -> p b b
forall {k :: Kind} (p :: k +-> k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr ((:.:) (Writer s) (Reader ('OP s)) b b -> b ~> b
(Writer s :.: Reader ('OP s)) :~> (~>)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
Adj.counit (Writer s b b
w2 Writer s b b
-> Reader ('OP s) b b -> (:.:) (Writer s) (Reader ('OP s)) b b
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Reader ('OP s) b b
r1)) p b b -> p b b -> p b b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p b b
p2) (:.:) (Reader ('OP s)) p a b
-> Writer s b c -> (:.:) (Reader ('OP s) :.: p) (Writer s) a c
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Writer s b c
w1)

instance (Monoidal k, Ob s) => Functor (StateT s :: k +-> k -> k +-> k) where
  map :: forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> StateT s a ~> StateT s b
map (Prof a :~> b
n) = (StateT s a :~> StateT s b) -> Prof (StateT s a) (StateT s b)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(StateT (Reader ('OP s) a b
r :.: a b b
p :.: Writer s b b
w)) -> (:.:) (Reader ('OP s) :.: b) (Writer s) a b -> StateT s b a b
forall {i :: Kind} (s :: i) (p :: i +-> i) (a :: i) (b :: i).
(:.:) (Reader ('OP s) :.: p) (Writer s) a b -> StateT s p a b
StateT (Reader ('OP s) a b
r Reader ('OP s) a b -> b b b -> (:.:) (Reader ('OP s)) b a b
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: a b b -> b b b
a :~> b
n a b b
p (:.:) (Reader ('OP s)) b a b
-> Writer s b b -> (:.:) (Reader ('OP s) :.: b) (Writer s) a b
forall {j :: Kind} {k :: Kind} {i :: Kind} (p :: j +-> k) (a :: k)
       (b :: j) (q :: i +-> j) (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Writer s b b
w)