module Proarrow.Promonad.State where

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj)

data State s a b where
  State :: (Ob a, Ob b) => (s ** a) ~> (s ** b) -> State s a b

instance (Monoidal k, Ob s) => Profunctor (State (s :: k)) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> State s a b -> State s c d
dimap c ~> a
l b ~> d
r (State (s ** a) ~> (s ** b)
f) = ((s ** c) ~> (s ** d)) -> State s c d
forall {k} (a :: k) (b :: k) (s :: k).
(Ob a, Ob b) =>
((s ** a) ~> (s ** b)) -> State s a b
State ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s Obj s -> (b ~> d) -> (s ** b) ~> (s ** d)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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` b ~> d
r) ((s ** b) ~> (s ** d))
-> ((s ** c) ~> (s ** b)) -> (s ** c) ~> (s ** 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
. (s ** a) ~> (s ** b)
f ((s ** a) ~> (s ** b))
-> ((s ** c) ~> (s ** a)) -> (s ** c) ~> (s ** 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 @s Obj s -> (c ~> a) -> (s ** c) ~> (s ** a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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` c ~> a
l)) ((Ob c, Ob a) => State s c d) -> (c ~> a) -> State s 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 b, Ob d) => State s c d) -> (b ~> d) -> State s 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 a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> State s a b -> r
\\ State (s ** a) ~> (s ** b)
f = r
(Ob a, Ob b) => r
(Ob (s ** a), Ob (s ** b)) => r
r ((Ob (s ** a), Ob (s ** b)) => r) -> ((s ** a) ~> (s ** 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
\\ (s ** a) ~> (s ** b)
f

instance (Monoidal k, Ob s) => Promonad (State (s :: k)) where
  id :: forall a. (Ob a) => State s a a
  id :: forall (a :: k). Ob a => State s a a
id = ((s ** a) ~> (s ** a)) -> State s a a
forall {k} (a :: k) (b :: k) (s :: k).
(Ob a, Ob b) =>
((s ** a) ~> (s ** b)) -> State s a b
State (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s Obj s -> (a ~> a) -> (s ** a) ~> (s ** a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)
  State (s ** b) ~> (s ** c)
f . :: forall (b :: k) (c :: k) (a :: k).
State s b c -> State s a b -> State s a c
. State (s ** a) ~> (s ** b)
g = ((s ** a) ~> (s ** c)) -> State s a c
forall {k} (a :: k) (b :: k) (s :: k).
(Ob a, Ob b) =>
((s ** a) ~> (s ** b)) -> State s a b
State ((s ** b) ~> (s ** c)
f ((s ** b) ~> (s ** c))
-> ((s ** a) ~> (s ** b)) -> (s ** a) ~> (s ** c)
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
. (s ** a) ~> (s ** b)
g)

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} (a :: k) (b :: k) (s :: k).
(Ob a, Ob b) =>
((s ** a) ~> (s ** b)) -> State s a b
State (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (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} {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` Unit ~> Unit
forall {j} {k} (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. ((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
\\ (Unit ~> Unit
forall {j} {k} (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} (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} (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} (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} (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} (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} (a :: k) (b :: k) (s :: k).
(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} {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` Obj y2 -> Obj x2 -> (y2 ** x2) ~> (x2 ** y2)
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (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} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (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} (p :: PRO 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} {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` 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} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (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} (p :: PRO 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} {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` Obj x2 -> Obj y1 -> (x2 ** y1) ~> (y1 ** x2)
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (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} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (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} (p :: PRO 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} {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` 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} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (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. ((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
\\ (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} {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` 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. ((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
\\ (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} {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` Obj y2
b2)