{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Pullback where

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, type (+->), lmap, UN)
import Proarrow.Object (pattern Objs)
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..), HasProducts, PROD (..), Prod (..))
import Proarrow.Object.Initial (HasZeroObject (..))
import Proarrow.Profunctor.List (LIST (..), List (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))

-- | 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
  par0 :: Cone Unit Unit
par0 = Cone Unit Unit
Cone ('PR TerminalObject) (L '[])
forall {k} (a :: k). Ob a => Cone ('PR a) (L '[])
Apex
  Apex @a par :: forall (x1 :: PROD k) (x2 :: LIST k) (y1 :: PROD k) (y2 :: LIST k).
Cone x1 x2 -> Cone y1 y2 -> Cone (x1 ** y1) (x2 ** y2)
`par` 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
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 `par` (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)
`par` 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

-- | Pullbacks are an inherently dependently typed concept:
-- The type of the apex object depends on the values of the given arrows.
-- But at runtime we can still calculate the arrows and the type, which we hide behind an existential.
class (HasProducts k) => HasPullbacks k where
  pullback :: forall (o :: k) a b. a ~> o -> b ~> o -> Cosink [a, b]

equalizer :: forall {k} (a :: k) b. (HasPullbacks k) => a ~> b -> a ~> b -> Cosink '[a]
equalizer :: forall {k} (a :: k) (b :: k).
HasPullbacks k =>
(a ~> b) -> (a ~> b) -> Cosink '[a]
equalizer f :: a ~> b
f@a ~> b
Objs a ~> b
g = case (a ~> (a && b)) -> (a ~> (a && b)) -> Cosink '[a, a]
forall (o :: k) (a :: k) (b :: k).
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
forall k (o :: k) (a :: k) (b :: k).
HasPullbacks k =>
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
pullback (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> b) -> a ~> (a && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> b
f) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> b) -> a ~> (a && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> b
g) of
  Cone (Leg a ~> b
_ Cone ('PR a) (L bs)
cone) -> Cone ('PR a) (L '[a]) -> Cosink '[a]
forall {k} (a :: k) (as :: [k]). Cone ('PR a) (L as) -> Cosink as
Cone Cone ('PR a) (L '[a])
Cone ('PR a) (L bs)
cone

kernel :: (HasPullbacks k, HasZeroObject k) => (a :: k) ~> b -> Cosink '[a]
kernel :: forall k (a :: k) (b :: k).
(HasPullbacks k, HasZeroObject k) =>
(a ~> b) -> Cosink '[a]
kernel f :: a ~> b
f@a ~> b
Objs = (a ~> b) -> (a ~> b) -> Cosink '[a]
forall {k} (a :: k) (b :: k).
HasPullbacks k =>
(a ~> b) -> (a ~> b) -> Cosink '[a]
equalizer a ~> b
forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b
forall k (a :: k) (b :: k). (HasZeroObject k, Ob a, Ob b) => a ~> b
zero a ~> b
f

class ik `InternalIn` k where
  type C0 ik :: k
  type C1 ik :: k
  source :: C1 ik ~> (C0 ik :: k)
  target :: C1 ik ~> (C0 ik :: k)
  identity :: C0 ik ~> (C1 ik :: k)
  compose :: Cosink [C1 ik, C1 ik, C1 ik :: k] -- first arrow projection, second arrow projection, composite