module Proarrow.Object.Initial where

import Data.Kind (Type)
import Data.Void (Void, absurd)
import Prelude (Eq, Show, type (~))

import Proarrow.Category.Instance.Free (Elem, FREE (..), Free (..), HasStructure (..), IsFreeOb (..), Ok)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Initial (InitialProfunctor)

class (CategoryOf k, Ob (InitialObject :: k)) => HasInitialObject k where
  type InitialObject :: k
  initiate :: (Ob (a :: k)) => InitialObject ~> a

initiate' :: forall {k} a' a. (HasInitialObject k) => (a' :: k) ~> a -> InitialObject ~> a
initiate' :: forall {k} (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
initiate' a' ~> a
a = a' ~> a
a (a' ~> a) -> (InitialObject ~> a') -> InitialObject ~> 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
. forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @k @a' ((Ob a', Ob a) => InitialObject ~> a)
-> (a' ~> a) -> InitialObject ~> a
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' ~> a
a

instance HasInitialObject Type where
  type InitialObject = Void
  initiate :: forall a. Ob a => InitialObject ~> a
initiate = InitialObject ~> a
Void -> a
forall a. Void -> a
absurd

instance (HasInitialObject j, HasInitialObject k) => HasInitialObject (j, k) where
  type InitialObject = '(InitialObject, InitialObject)
  initiate :: forall (a :: (j, k)). Ob a => InitialObject ~> a
initiate = InitialObject ~> Fst a
forall (a :: j). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (InitialObject ~> Fst a)
-> (InitialObject ~> Snd a)
-> (:**:) (~>) (~>) '(InitialObject, InitialObject) '(Fst a, Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: InitialObject ~> Snd a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

instance (CategoryOf j, CategoryOf k) => HasInitialObject (j +-> k) where
  type InitialObject = InitialProfunctor
  initiate :: forall (a :: j +-> k). Ob a => InitialObject ~> a
initiate = (InitialProfunctor :~> a) -> Prof InitialProfunctor a
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case {}

class (HasInitialObject k, HasTerminalObject k, (InitialObject :: k) ~ TerminalObject) => HasZeroObject k where
  zero :: (Ob (a :: k), Ob b) => a ~> b
instance (HasInitialObject k, HasTerminalObject k, (InitialObject :: k) ~ TerminalObject) => HasZeroObject k where
  zero :: forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b
zero = TerminalObject ~> b
InitialObject ~> b
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (TerminalObject ~> b) -> (a ~> TerminalObject) -> a ~> 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
. a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

data family InitF :: k
instance (HasInitialObject `Elem` cs) => IsFreeOb (InitF :: FREE cs p) where
  type Lower f InitF = InitialObject
  withLowerOb :: forall {k} (f :: j +-> k) r.
(Representable f, All cs k) =>
(Ob (Lower f InitF) => r) -> r
withLowerOb Ob (Lower f InitF) => r
r = r
Ob (Lower f InitF) => r
r
instance (HasInitialObject `Elem` cs) => HasStructure cs p HasInitialObject where
  data Struct HasInitialObject a b where
    Initial :: (Ob b) => Struct HasInitialObject InitF b
  foldStructure :: forall {k} (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p).
(All cs k, Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct HasInitialObject a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Initial @b) = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f InitialObject ~> Lower f b
Ob (Lower f b) => InitialObject ~> Lower f b
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
deriving instance Eq (Struct HasInitialObject a b)
deriving instance Show (Struct HasInitialObject a b)
instance (Ok cs p, HasInitialObject `Elem` cs) => HasInitialObject (FREE cs p) where
  type InitialObject = InitF
  initiate :: forall (a :: FREE cs p). Ob a => InitialObject ~> a
initiate = Struct HasInitialObject InitF a -> Free InitF InitF -> Free InitF a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct HasInitialObject InitF a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (b :: FREE cs p).
Ob b =>
Struct HasInitialObject InitF b
Initial Free InitF InitF
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id