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)