module Proarrow.Promonad.State where

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


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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`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
  lift0 :: State s Unit Unit
lift0 = State s Unit Unit
forall (a :: k). Ob a => State s a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  lift2 :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
State s x1 x2 -> State s y1 y2 -> State s (x1 ** y1) (x2 ** y2)
lift2 (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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj y2 -> Obj x2 -> (y2 ** x2) ~> (x2 ** y2)
forall (a :: k) (b :: k). Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall k (a :: k) (b :: k).
SymMonoidal k =>
Obj a -> Obj 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
. Obj s -> Obj y2 -> Obj x2 -> ((s ** y2) ** x2) ~> (s ** (y2 ** x2))
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj s
s Obj y2
b2 Obj x2
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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`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
. Obj s -> Obj y1 -> Obj x2 -> (s ** (y1 ** x2)) ~> ((s ** y1) ** x2)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj s
s Obj y1
a2 Obj x2
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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj x2 -> Obj y1 -> (x2 ** y1) ~> (y1 ** x2)
forall (a :: k) (b :: k). Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall k (a :: k) (b :: k).
SymMonoidal k =>
Obj a -> Obj 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
. Obj s -> Obj x2 -> Obj y1 -> ((s ** x2) ** y1) ~> (s ** (x2 ** y1))
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj s
s Obj x2
b1 Obj y1
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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`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
. Obj s -> Obj x1 -> Obj y1 -> (s ** (x1 ** y1)) ~> ((s ** x1) ** y1)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj s
s Obj x1
a1 Obj y1
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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`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 (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj y2
b2)