-- | A 'Cocone' is a list of arrows sharing a single target (the coapex), as a profunctor from lists of
-- objects to objects; a 'Sink' is a cocone with the coapex hidden existentially.
module Proarrow.Profunctor.Instance.Cocone where

import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Colimit.BinaryCoproduct (COPROD (..), Coprod (..), HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), UN, rmap, type (+->))
import Proarrow.Profunctor.Instance.List (LIST (..), List (..))

-- | A cocone is a bunch of arrows with a shared target.
data Cocone (bs :: LIST k) (a :: COPROD k) where
  Coapex :: (Ob a) => Cocone (L '[]) (COPR a)
  Coleg :: b ~> a -> Cocone (L bs) (COPR a) -> Cocone (L (b : bs)) (COPR a)

instance (CategoryOf k) => Profunctor (Cocone :: COPROD k +-> LIST k) where
  dimap :: forall (c :: LIST k) (a :: LIST k) (b :: COPROD k) (d :: COPROD k).
(c ~> a) -> (b ~> d) -> Cocone a b -> Cocone c d
dimap c ~> a
List (~>) c a
Nil b ~> d
r Cocone a b
Coapex = Cocone c d
Cocone (L '[]) (COPR (UN COPR d))
(Ob (COPR a), Ob d) => Cocone c d
forall {k} (b :: k). Ob b => Cocone (L '[]) (COPR b)
Coapex ((Ob (COPR a), Ob d) => Cocone c d)
-> Coprod (~>) (COPR a) d -> Cocone c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: COPROD k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Coprod (~>) a b -> r
\\ b ~> d
Coprod (~>) (COPR a) d
r
  dimap (Cons a ~> b
l List (~>) (L as1) (L bs1)
ls) r :: b ~> d
r@(Coprod a1 ~> b1
r') (Coleg b ~> a
f Cocone (L bs) (COPR a)
fs) = (a ~> b1)
-> Cocone (L as1) (COPR b1) -> Cocone (L (a : as1)) (COPR b1)
forall {k} (b :: k) (a :: k) (bs :: [k]).
(b ~> a) -> Cocone (L bs) (COPR a) -> Cocone (L (b : bs)) (COPR a)
Coleg (a1 ~> b1
r' (a1 ~> b1) -> (a ~> a1) -> a ~> b1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> a1
b ~> a
f (b ~> a1) -> (a ~> b) -> a ~> a1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
l) ((L as1 ~> L bs)
-> (COPR a ~> COPR b1)
-> Cocone (L bs) (COPR a)
-> Cocone (L as1) (COPR b1)
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: LIST k) (a :: LIST k) (b :: COPROD k) (d :: COPROD k).
(c ~> a) -> (b ~> d) -> Cocone a b -> Cocone c d
dimap L as1 ~> L bs
List (~>) (L as1) (L bs1)
ls b ~> d
COPR a ~> COPR b1
r Cocone (L bs) (COPR a)
fs)
  (Ob a, Ob b) => r
r \\ :: forall (a :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone a b
Coapex = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Coleg b ~> a
l Cocone (L bs) (COPR a)
Coapex = r
(Ob b, Ob a) => r
(Ob a, Ob b) => r
r ((Ob b, Ob a) => r) -> (b ~> a) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> a
l
  (Ob a, Ob b) => r
r \\ Coleg b ~> a
l c :: Cocone (L bs) (COPR a)
c@(Coleg b ~> a
_ Cocone (L bs) (COPR a)
c1) = r
(Ob b, Ob a) => r
(Ob a, Ob b) => r
r ((Ob b, Ob a) => r) -> (b ~> a) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> a
l ((Ob (L bs), Ob (COPR a)) => r) -> Cocone (L bs) (COPR a) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone (L bs) (COPR a)
c ((Ob (L bs), Ob (COPR a)) => r) -> Cocone (L bs) (COPR a) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone (L bs) (COPR a)
c1

instance (HasCoproducts k) => MonoidalProfunctor (Cocone :: COPROD k +-> LIST k) where
  one :: Cocone Unit Unit
one = Cocone Unit Unit
Cocone (L '[]) (COPR InitialObject)
forall {k} (b :: k). Ob b => Cocone (L '[]) (COPR b)
Coapex
  Coapex @l ** :: forall (x1 :: LIST k) (x2 :: COPROD k) (y1 :: LIST k)
       (y2 :: COPROD k).
Cocone x1 x2 -> Cocone y1 y2 -> Cocone (x1 ** y1) (x2 ** y2)
** Cocone y1 y2
rs = (y2 ~> COPR (a || UN COPR y2))
-> Cocone y1 y2 -> Cocone y1 (COPR (a || UN COPR y2))
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
forall (b :: COPROD k) (d :: COPROD k) (a :: LIST k).
(b ~> d) -> Cocone a b -> Cocone a d
rmap ((UN COPR y2 ~> (a || UN COPR y2))
-> Coprod (~>) (COPR (UN COPR y2)) (COPR (a || UN COPR y2))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p (COPR a1) (COPR b1)
Coprod (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @l)) Cocone y1 y2
rs ((Ob y1, Ob y2) => Cocone (L (UN L y1)) (COPR (a || UN COPR y2)))
-> Cocone y1 y2 -> Cocone (L (UN L y1)) (COPR (a || UN COPR y2))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone y1 y2
rs
  Coleg b ~> a
l Cocone (L bs) (COPR a)
ls ** (Cocone y1 y2
rs :: Cocone rs r) = (b ~> (a || UN COPR y2))
-> Cocone (L (bs ++ UN L y1)) (COPR (a || UN COPR y2))
-> Cocone (L (b : (bs ++ UN L y1))) (COPR (a || UN COPR y2))
forall {k} (b :: k) (a :: k) (bs :: [k]).
(b ~> a) -> Cocone (L bs) (COPR a) -> Cocone (L (b : bs)) (COPR a)
Coleg (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @_ @(UN COPR r) (a ~> (a || UN COPR y2)) -> (b ~> a) -> b ~> (a || UN COPR y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> a
l) (Cocone (L bs) (COPR a)
ls Cocone (L bs) (COPR a)
-> Cocone y1 y2 -> Cocone (L bs ** y1) (COPR a ** 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)
forall (x1 :: LIST k) (x2 :: COPROD k) (y1 :: LIST k)
       (y2 :: COPROD k).
Cocone x1 x2 -> Cocone y1 y2 -> Cocone (x1 ** y1) (x2 ** y2)
** Cocone y1 y2
rs) ((Ob b, Ob a) =>
 Cocone (L (b : (bs ++ UN L y1))) (COPR (a || UN COPR y2)))
-> (b ~> a)
-> Cocone (L (b : (bs ++ UN L y1))) (COPR (a || UN COPR y2))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> a
l ((Ob y1, Ob y2) =>
 Cocone (L (b : (bs ++ UN L y1))) (COPR (a || UN COPR y2)))
-> Cocone y1 y2
-> Cocone (L (b : (bs ++ UN L y1))) (COPR (a || UN COPR y2))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: LIST k) (b :: COPROD k) r.
((Ob a, Ob b) => r) -> Cocone a b -> r
\\ Cocone y1 y2
rs

-- | A sink is a cocone, but with the apex type hidden by an existential.
data Sink (as :: [k]) where
  Cocone :: Cocone (L as) (COPR a) -> Sink as