module Proarrow.Object.Terminal where

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

import Proarrow.Category.Instance.Free (Elem, FREE (..), Free (..), HasStructure (..), IsFreeOb (..), Ok, emb)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Profunctor.Terminal (TerminalProfunctor (..))
import Proarrow.Tools.Laws (AssertEq (..), Laws (..), Var)

class (CategoryOf k, Ob (TerminalObject :: k)) => HasTerminalObject k where
  type TerminalObject :: k
  terminate :: (Ob (a :: k)) => a ~> TerminalObject

terminate' :: forall {k} a a'. (HasTerminalObject k) => (a :: k) ~> a' -> a ~> TerminalObject
terminate' :: forall {k} (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
terminate' a ~> a'
a = forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @k @a' (a' ~> TerminalObject) -> (a ~> a') -> a ~> TerminalObject
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 ~> a'
a ((Ob a, Ob a') => a ~> TerminalObject)
-> (a ~> a') -> a ~> TerminalObject
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

-- | The type of elements of `a`.
type El a = TerminalObject ~> a

instance HasTerminalObject Type where
  type TerminalObject = ()
  terminate :: forall a. Ob a => a ~> TerminalObject
terminate a
_ = ()

instance (HasTerminalObject j, HasTerminalObject k) => HasTerminalObject (j, k) where
  type TerminalObject = '(TerminalObject, TerminalObject)
  terminate :: forall (a :: (j, k)). Ob a => a ~> TerminalObject
terminate = Fst a ~> TerminalObject
forall (a :: j). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate (Fst a ~> TerminalObject)
-> (Snd a ~> TerminalObject)
-> (:**:)
     (~>) (~>) '(Fst a, Snd a) '(TerminalObject, TerminalObject)
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)
:**: Snd a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

instance (CategoryOf j, CategoryOf k) => HasTerminalObject (j +-> k) where
  type TerminalObject = TerminalProfunctor
  terminate :: forall (a :: j +-> k). Ob a => a ~> TerminalObject
terminate = (a :~> TerminalProfunctor) -> Prof a TerminalProfunctor
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
a -> TerminalProfunctor a b
(Ob a, Ob b) => TerminalProfunctor a b
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor ((Ob a, Ob b) => TerminalProfunctor a b)
-> a a b -> TerminalProfunctor a b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> a 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 b
a

class ((Unit :: k) ~ TerminalObject, HasTerminalObject k, Monoidal k) => Semicartesian k
instance ((Unit :: k) ~ TerminalObject, HasTerminalObject k, Monoidal k) => Semicartesian k

data family TermF :: k
instance (HasTerminalObject `Elem` cs) => IsFreeOb (TermF :: FREE cs p) where
  type Lower f TermF = TerminalObject
  withLowerOb :: forall {k} (f :: j +-> k) r.
(Representable f, All cs k) =>
(Ob (Lower f TermF) => r) -> r
withLowerOb Ob (Lower f TermF) => r
r = r
Ob (Lower f TermF) => r
r
instance (HasTerminalObject `Elem` cs) => HasStructure cs p HasTerminalObject where
  data Struct HasTerminalObject a b where
    Terminal :: (Ob a) => Struct HasTerminalObject a TermF
  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 HasTerminalObject 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
_ (Terminal @a) = 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 @a @f (Lower f a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate)
deriving instance Eq (Struct HasTerminalObject a b)
deriving instance Show (Struct HasTerminalObject a b)
instance (Ok cs p, HasTerminalObject `Elem` cs) => HasTerminalObject (FREE cs p) where
  type TerminalObject = TermF
  terminate :: forall (a :: FREE cs p). Ob a => a ~> TerminalObject
terminate = Struct HasTerminalObject a TermF -> Free a a -> Free a TermF
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 HasTerminalObject a TermF
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct HasTerminalObject a TermF
Terminal Free a a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id

data instance Var '[HasTerminalObject] a b where
  T :: Var '[HasTerminalObject] "A" "B"
deriving instance Show (Var '[HasTerminalObject] a b)
instance Laws '[HasTerminalObject] where
  type EqTypes '[HasTerminalObject] = '[EMB "A", TermF]
  laws :: [AssertEq '[HasTerminalObject]]
laws = ['EMB "B" ~> TerminalObject
Free ('EMB "B") TermF
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FREE '[HasTerminalObject] (Var '[HasTerminalObject])).
Ob a =>
a ~> TerminalObject
terminate Free ('EMB "B") TermF
-> Free ('EMB "A") ('EMB "B") -> Free ('EMB "A") TermF
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE '[HasTerminalObject] (Var '[HasTerminalObject]))
       (c :: FREE '[HasTerminalObject] (Var '[HasTerminalObject]))
       (a :: FREE '[HasTerminalObject] (Var '[HasTerminalObject])).
Free b c -> Free a b -> Free a c
. Var '[HasTerminalObject] "A" "B" %1 -> Free ('EMB "A") ('EMB "B")
forall {j} (a :: j) (b :: j) (cs :: [Type -> Constraint])
       (p :: CAT j).
(Ob a, Ob b, Typeable a, Typeable b, Ok cs p) =>
p a b %1 -> Free ('EMB a) ('EMB b)
emb Var '[HasTerminalObject] "A" "B"
T Free ('EMB "A") TermF
-> Free ('EMB "A") TermF -> AssertEq '[HasTerminalObject]
forall {cs :: [Type -> Constraint]} (a :: FREE cs (Var cs))
       (b :: FREE cs (Var cs)).
(Elem a (EqTypes cs), Elem b (EqTypes cs)) =>
Free a b -> Free a b -> AssertEq cs
:=: 'EMB "A" ~> TerminalObject
Free ('EMB "A") TermF
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FREE '[HasTerminalObject] (Var '[HasTerminalObject])).
Ob a =>
a ~> TerminalObject
terminate]