module Proarrow.Promonad.Collage where import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..), lmap, rmap) import Proarrow.Category.Instance.Prof (Prof(..)) import Proarrow.Category.Instance.Coproduct (COPRODUCT(..), (:++:)(..), coproductId) import Proarrow.Functor (Functor(..)) type Collage :: PRO j k -> PRO (COPRODUCT j k) (COPRODUCT j k) data Collage p a b where InL :: (a ~> b) -> Collage p (L a) (L b) InR :: (a ~> b) -> Collage p (R a) (R b) L2R :: p a b -> Collage p (L a) (R b) instance Profunctor p => Profunctor (Collage p) where dimap :: forall (c :: COPRODUCT j k) (a :: COPRODUCT j k) (b :: COPRODUCT j k) (d :: COPRODUCT j k). (c ~> a) -> (b ~> d) -> Collage p a b -> Collage p c d dimap (InjL a1 ~> b1 l) (InjL a1 ~> b1 r) (InL a ~> b f) = (a1 ~> b1) -> Collage p ('L a1) ('L b1) forall {k} {k} (a :: k) (b :: k) (p :: PRO k k). (a ~> b) -> Collage p ('L a) ('L b) InL ((a1 ~> b1) -> (a1 ~> b1) -> (b1 ~> a1) -> a1 ~> b1 forall (c :: j) (a :: j) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap a1 ~> b1 l a1 ~> b1 r b1 ~> a1 a ~> b f) dimap (InjR a1 ~> b1 l) (InjR a1 ~> b1 r) (InR a ~> b f) = (a1 ~> b1) -> Collage p ('R a1) ('R b1) forall {k} {j} (a :: k) (b :: k) (p :: PRO j k). (a ~> b) -> Collage p ('R a) ('R b) InR ((a1 ~> b1) -> (a1 ~> b1) -> (b1 ~> a1) -> a1 ~> b1 forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap a1 ~> b1 l a1 ~> b1 r b1 ~> a1 a ~> b f) dimap (InjL a1 ~> b1 l) (InjR a1 ~> b1 r) (L2R p a b p) = p a1 b1 -> Collage p ('L a1) ('R b1) forall {j} {k} (p :: PRO j k) (a :: j) (b :: k). p a b -> Collage p ('L a) ('R b) L2R ((a1 ~> a) -> (b ~> b1) -> p a b -> p a1 b1 forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> p a b -> p c d forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap a1 ~> b1 a1 ~> a l a1 ~> b1 b ~> b1 r p a b p) dimap (InjR a1 ~> b1 _) (InjL a1 ~> b1 _) Collage p a b f = case Collage p a b f of (Ob a, Ob b) => r r \\ :: forall (a :: COPRODUCT j k) (b :: COPRODUCT j k) r. ((Ob a, Ob b) => r) -> Collage p a b -> r \\ InL a ~> b f = r (Ob a, Ob b) => r (Ob a, Ob b) => r r ((Ob a, Ob b) => r) -> (a ~> b) -> r forall (a :: j) (b :: j) 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 \\ a ~> b f (Ob a, Ob b) => r r \\ InR a ~> b f = r (Ob a, Ob b) => r (Ob a, Ob b) => r r ((Ob a, Ob b) => 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 \\ a ~> b f (Ob a, Ob b) => r r \\ L2R p a b p = r (Ob a, Ob b) => r (Ob a, Ob b) => r r ((Ob a, Ob b) => r) -> p a b -> r forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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 \\ p a b p instance Profunctor p => Promonad (Collage p) where id :: forall a. Ob a => Collage p a a id :: forall (a :: COPRODUCT j k). Ob a => Collage p a a id = case forall {j} {k} (a :: COPRODUCT j k). IsCoproduct a => (:++:) (~>) (~>) a a forall (a :: COPRODUCT j k). IsCoproduct a => (:++:) (~>) (~>) a a coproductId @a of InjL a1 ~> b1 f -> (b1 ~> b1) -> Collage p ('L b1) ('L b1) forall {k} {k} (a :: k) (b :: k) (p :: PRO k k). (a ~> b) -> Collage p ('L a) ('L b) InL a1 ~> b1 b1 ~> b1 f InjR a1 ~> b1 f -> (b1 ~> b1) -> Collage p ('R b1) ('R b1) forall {k} {j} (a :: k) (b :: k) (p :: PRO j k). (a ~> b) -> Collage p ('R a) ('R b) InR a1 ~> b1 b1 ~> b1 f InL a ~> b g . :: forall (b :: COPRODUCT j k) (c :: COPRODUCT j k) (a :: COPRODUCT j k). Collage p b c -> Collage p a b -> Collage p a c . InL a ~> b f = (a ~> b) -> Collage p ('L a) ('L b) forall {k} {k} (a :: k) (b :: k) (p :: PRO k k). (a ~> b) -> Collage p ('L a) ('L b) InL (a ~> b g (a ~> b) -> (a ~> a) -> a ~> b forall (b :: j) (c :: j) (a :: j). (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 ~> a a ~> b f) InR a ~> b g . L2R p a b p = p a b -> Collage p ('L a) ('R b) forall {j} {k} (p :: PRO j k) (a :: j) (b :: k). p a b -> Collage p ('L a) ('R b) L2R ((b ~> b) -> p a b -> p a b forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap a ~> b b ~> b g p a b p) L2R p a b p . InL a ~> b f = p a b -> Collage p ('L a) ('R b) forall {j} {k} (p :: PRO j k) (a :: j) (b :: k). p a b -> Collage p ('L a) ('R b) L2R ((a ~> a) -> p a b -> p a b forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k). Profunctor p => (c ~> a) -> p a b -> p c b lmap a ~> a a ~> b f p a b p) InR a ~> b g . InR a ~> b f = (a ~> b) -> Collage p ('R a) ('R b) forall {k} {j} (a :: k) (b :: k) (p :: PRO j k). (a ~> b) -> Collage p ('R a) ('R b) InR (a ~> b g (a ~> b) -> (a ~> 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 . a ~> a a ~> b f) instance Functor Collage where map :: forall (a :: PRO j k) (b :: PRO j k). (a ~> b) -> Collage a ~> Collage b map (Prof a :~> b n) = (Collage a :~> Collage b) -> Prof (Collage a) (Collage b) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \case InL a ~> b l -> (a ~> b) -> Collage b ('L a) ('L b) forall {k} {k} (a :: k) (b :: k) (p :: PRO k k). (a ~> b) -> Collage p ('L a) ('L b) InL a ~> b l InR a ~> b r -> (a ~> b) -> Collage b ('R a) ('R b) forall {k} {j} (a :: k) (b :: k) (p :: PRO j k). (a ~> b) -> Collage p ('R a) ('R b) InR a ~> b r L2R a a b p -> b a b -> Collage b ('L a) ('R b) forall {j} {k} (p :: PRO j k) (a :: j) (b :: k). p a b -> Collage p ('L a) ('R b) L2R (a a b -> b a b a :~> b n a a b p)