module Proarrow.Profunctor.Instance.Cone where

import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), UN, lmap, type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), HasProducts, PROD (..), Prod (..))
import Proarrow.Profunctor.Instance.List (LIST (..), List (..))

-- | A cone is a bunch of arrows with a shared source.
data Cone (a :: PROD k) (bs :: LIST k) where
  Apex :: (Ob a) => Cone (PR a) (L '[])
  Leg :: a ~> b -> Cone (PR a) (L bs) -> Cone (PR a) (L (b : bs))

instance (CategoryOf k) => Profunctor (Cone :: LIST k +-> PROD k) where
  dimap :: forall (c :: PROD k) (a :: PROD k) (b :: LIST k) (d :: LIST k).
(c ~> a) -> (b ~> d) -> Cone a b -> Cone c d
dimap c ~> a
l b ~> d
List (~>) b d
Nil Cone a b
Apex = Cone c d
Cone ('PR (UN 'PR c)) (L '[])
(Ob c, Ob ('PR a)) => Cone c d
forall {k} (a :: k). Ob a => Cone ('PR a) (L '[])
Apex ((Ob c, Ob ('PR a)) => Cone c d) -> Prod (~>) c ('PR a) -> Cone 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 :: PROD k) (b :: PROD k) r.
((Ob a, Ob b) => r) -> Prod (~>) a b -> r
\\ c ~> a
Prod (~>) c ('PR a)
l
  dimap (Prod a1 ~> b1
l) (Cons a ~> b
r List (~>) (L as1) (L bs1)
rs) (Leg a ~> b
f Cone ('PR a) (L bs)
fs) = (a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
forall {k} (a :: k) (b :: k) (bs :: [k]).
(a ~> b) -> Cone ('PR a) (L bs) -> Cone ('PR a) (L (b : bs))
Leg (a ~> b
r (a ~> b) -> (a1 ~> a) -> a1 ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b1 ~> a
a ~> b
f (b1 ~> a) -> (a1 ~> b1) -> a1 ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> b1
l) (('PR a1 ~> 'PR a)
-> (L bs ~> L bs1) -> Cone ('PR a) (L bs) -> Cone ('PR a1) (L bs1)
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 :: PROD k) (a :: PROD k) (b :: LIST k) (d :: LIST k).
(c ~> a) -> (b ~> d) -> Cone a b -> Cone c d
dimap ((a1 ~> b1) -> Prod (~>) ('PR a1) ('PR b1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod a1 ~> b1
l) L bs ~> L bs1
List (~>) (L as1) (L bs1)
rs Cone ('PR a) (L bs)
fs)
  (Ob a, Ob b) => r
r \\ :: forall (a :: PROD k) (b :: LIST k) r.
((Ob a, Ob b) => r) -> Cone a b -> r
\\ Cone a b
Apex = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Leg a ~> b
l Cone ('PR a) (L bs)
Apex = 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
l
  (Ob a, Ob b) => r
r \\ Leg a ~> b
l c :: Cone ('PR a) (L bs)
c@(Leg a ~> b
_ Cone ('PR a) (L bs)
c1) = 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
l ((Ob ('PR a), Ob (L bs)) => r) -> Cone ('PR a) (L bs) -> 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 :: PROD k) (b :: LIST k) r.
((Ob a, Ob b) => r) -> Cone a b -> r
\\ Cone ('PR a) (L bs)
c ((Ob ('PR a), Ob (L bs)) => r) -> Cone ('PR a) (L bs) -> 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 :: PROD k) (b :: LIST k) r.
((Ob a, Ob b) => r) -> Cone a b -> r
\\ Cone ('PR a) (L bs)
c1

instance (HasProducts k) => MonoidalProfunctor (Cone :: LIST k +-> PROD k) where
  one :: Cone Unit Unit
one = Cone Unit Unit
Cone ('PR TerminalObject) (L '[])
forall {k} (a :: k). Ob a => Cone ('PR a) (L '[])
Apex
  Apex @a ** :: forall (x1 :: PROD k) (x2 :: LIST k) (y1 :: PROD k) (y2 :: LIST k).
Cone x1 x2 -> Cone y1 y2 -> Cone (x1 ** y1) (x2 ** y2)
** Cone y1 y2
rs = ('PR (a && UN 'PR y1) ~> y1)
-> Cone y1 y2 -> Cone ('PR (a && UN 'PR y1)) y2
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
forall (c :: PROD k) (a :: PROD k) (b :: LIST k).
(c ~> a) -> Cone a b -> Cone c b
lmap (((a && UN 'PR y1) ~> UN 'PR y1)
-> Prod (~>) ('PR (a && UN 'PR y1)) ('PR (UN 'PR y1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a)) Cone y1 y2
rs ((Ob y1, Ob y2) => Cone ('PR (a && UN 'PR y1)) (L (UN L y2)))
-> Cone y1 y2 -> Cone ('PR (a && UN 'PR y1)) (L (UN L 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 :: PROD k) (b :: LIST k) r.
((Ob a, Ob b) => r) -> Cone a b -> r
\\ Cone y1 y2
rs
  Leg a ~> b
l Cone ('PR a) (L bs)
ls ** (Cone y1 y2
rs :: Cone r rs) = ((a && UN 'PR y1) ~> b)
-> Cone ('PR (a && UN 'PR y1)) (L (bs ++ UN L y2))
-> Cone ('PR (a && UN 'PR y1)) (L (b : (bs ++ UN L y2)))
forall {k} (a :: k) (b :: k) (bs :: [k]).
(a ~> b) -> Cone ('PR a) (L bs) -> Cone ('PR a) (L (b : bs))
Leg (a ~> b
l (a ~> b) -> ((a && UN 'PR y1) ~> a) -> (a && UN 'PR y1) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: 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).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @_ @(UN PR r)) (Cone ('PR a) (L bs)
ls Cone ('PR a) (L bs)
-> Cone y1 y2 -> Cone ('PR a ** y1) (L bs ** 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 :: PROD k) (x2 :: LIST k) (y1 :: PROD k) (y2 :: LIST k).
Cone x1 x2 -> Cone y1 y2 -> Cone (x1 ** y1) (x2 ** y2)
** Cone y1 y2
rs) ((Ob a, Ob b) =>
 Cone ('PR (a && UN 'PR y1)) (L (b : (bs ++ UN L y2))))
-> (a ~> b)
-> Cone ('PR (a && UN 'PR y1)) (L (b : (bs ++ UN L 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
\\ a ~> b
l ((Ob y1, Ob y2) =>
 Cone ('PR (a && UN 'PR y1)) (L (b : (bs ++ UN L y2))))
-> Cone y1 y2
-> Cone ('PR (a && UN 'PR y1)) (L (b : (bs ++ UN L 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 :: PROD k) (b :: LIST k) r.
((Ob a, Ob b) => r) -> Cone a b -> r
\\ Cone y1 y2
rs

-- | A cosink (a.k.a a source) is a cone, but with the apex type hidden by an existential.
data Cosink (as :: [k]) where
  Cone :: Cone (PR a) (L as) -> Cosink as