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