{-# OPTIONS_GHC -Wno-orphans #-}

-- | Terminal objects: 'HasTerminalObject' with the unique arrow 'terminate', instances for the base
-- kinds, and global elements @'El' a = 'TerminalObject' '~>' a@.
module Proarrow.Limit.Terminal where

import Data.Kind (Type)
import Prelude (Show, type (~))
import Prelude qualified as P

import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Free
  ( Elem (..)
  , FREE (..)
  , Free (..)
  , HasStructure (..)
  , IsFreeOb (..)
  , Lower
  , withLowerOb
  )
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), obj, type (+->))
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Proarrow.Tools.Laws (Law (..), Laws (..), (===))

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 :: CAT 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

-- | The constant arrow at an element: 'terminate', then the element.
const :: forall {k} (a :: k) b. (HasTerminalObject k, Ob a) => El b -> a ~> b
const :: forall {k} (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
const El b
u = El b
u El b -> (a ~> TerminalObject) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @k @a

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

instance HasTerminalObject () where
  type TerminalObject = '()
  terminate :: forall (a :: ()). Ob a => a ~> TerminalObject
terminate = a ~> TerminalObject
Unit '() '()
U.Unit

instance HasTerminalObject BOOL where
  type TerminalObject = TRU
  terminate :: forall (a :: BOOL). Ob a => a ~> TerminalObject
terminate @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> a ~> TerminalObject
Booleans 'FLS 'TRU
F2T
    Obj a
Booleans a a
Tru -> a ~> TerminalObject
Booleans 'TRU 'TRU
Tru

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

instance (HasTerminalObject k, CategoryOf j) => Representable (TerminalProfunctor :: j +-> k) where
  type TerminalProfunctor % x = TerminalObject
  index :: forall (a :: k) (b :: j).
TerminalProfunctor a b -> a ~> (TerminalProfunctor % b)
index TerminalProfunctor a b
TerminalProfunctor = a ~> (TerminalProfunctor % b)
a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (TerminalProfunctor % b)) -> TerminalProfunctor a b
tabulate a ~> (TerminalProfunctor % b)
f = TerminalProfunctor a b
(Ob a, Ob TerminalObject) => 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 TerminalObject) => TerminalProfunctor a b)
-> (a ~> TerminalObject) -> TerminalProfunctor a b
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 ~> (TerminalProfunctor % b)
a ~> TerminalObject
f
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (TerminalProfunctor % a) ~> (TerminalProfunctor % b)
repMap a ~> b
_ = (TerminalProfunctor % a) ~> (TerminalProfunctor % b)
TerminalObject ~> TerminalObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

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
  lowerOb :: forall k' (f :: k +-> k') r.
(Representable f, All cs k') =>
(Ob (Lower f TermF) => r) -> r
lowerOb @k' @_ Ob (Lower f TermF) => r
r = forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k r.
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @HasTerminalObject @cs @k' r
Ob (Lower f TermF) => r
HasTerminalObject k' => r
r
instance (HasTerminalObject `Elem` cs) => HasStructure cs (p :: CAT k) HasTerminalObject where
  data Struct HasTerminalObject a b where
    Terminate :: (Ob a) => Struct HasTerminalObject a TermF
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(HasTerminalObject k', 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
_ (Terminate @a) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a Lower f a ~> TerminalObject
Ob (Lower f a) => Lower f a ~> TerminalObject
forall (a :: k'). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
instance Show (Struct HasTerminalObject a b) where
  showsPrec :: Int -> Struct HasTerminalObject a b -> ShowS
showsPrec Int
_ Struct HasTerminalObject a b
R:StructkcspHasTerminalObjectab k cs p a b
Terminate = String -> ShowS
P.showString String
"terminate"
instance (HasTerminalObject `Elem` cs) => HasTerminalObject (FREE cs (p :: CAT k)) 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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct HasTerminalObject a TermF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct HasTerminalObject a TermF
Terminate Free a a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil

-- | Every arrow into the terminal object is 'terminate'.
instance Laws '[HasTerminalObject] where
  laws :: [Law '[HasTerminalObject]]
laws =
    [ String -> LawBody '[HasTerminalObject] -> Law '[HasTerminalObject]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"uniqueness" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        g <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @TerminalObject String
"g"
        g === terminate
    ]