{-# OPTIONS_GHC -Wno-orphans #-}

-- | The __terminal category__: the unit kind @()@ with its single object @'()@ and only the
-- identity arrow 'Unit'.
module Proarrow.Category.Instance.Unit where

import Data.Type.Nat (SNat (..), snat)
import Prelude (type (~))

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Enriched.Thin
  ( DecidableProfunctor (..)
  , Decision (..)
  , Enumerable (..)
  , Finite (..)
  , Indexed (..)
  , IndexedList (..)
  , ThinProfunctor (..)
  )
import Proarrow.Category.Instance.Bool (BOOL (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault)

type Unit :: CAT ()
data Unit a b where
  Unit :: Unit '() '()

-- | The category with one object, the terminal category.
instance CategoryOf () where
  type (~>) = Unit
  type Ob a = a ~ '()

instance Promonad Unit where
  id :: forall (a :: ()). Ob a => Unit a a
id = Unit a a
Unit '() '()
Unit
  Unit b c
Unit . :: forall (b :: ()) (c :: ()) (a :: ()).
Unit b c -> Unit a b -> Unit a c
. Unit a b
Unit = Unit a c
Unit '() '()
Unit

instance Profunctor Unit where
  dimap :: forall (c :: ()) (a :: ()) (b :: ()) (d :: ()).
(c ~> a) -> (b ~> d) -> Unit a b -> Unit c d
dimap = (c ~> a) -> (b ~> d) -> Unit a b -> Unit c d
Unit c a -> Unit b d -> Unit a b -> Unit c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: ()) (b :: ()) r. ((Ob a, Ob b) => r) -> Unit a b -> r
\\ Unit a b
Unit = r
(Ob a, Ob b) => r
r

instance DaggerProfunctor Unit where
  dagger :: forall (a :: ()) (b :: ()). Unit a b -> Unit b a
dagger Unit a b
Unit = Unit b a
Unit '() '()
Unit

instance ThinProfunctor Unit where
  type HasArrow Unit a b = (a ~ b)
  arr :: forall (a :: ()) (b :: ()).
(Ob a, Ob b, HasArrow Unit a b) =>
Unit a b
arr = Unit a b
Unit '() '()
Unit
  withArr :: forall (a :: ()) (b :: ()) r.
Unit a b -> ((HasArrow Unit a b, Ob a, Ob b) => r) -> r
withArr Unit a b
Unit (HasArrow Unit a b, Ob a, Ob b) => r
r = r
(HasArrow Unit a b, Ob a, Ob b) => r
r

instance DecidableProfunctor Unit where
  type Holds Unit a b = TRU
  decide :: forall (a :: ()) (b :: ()).
(Ob a, Ob b) =>
Decision Unit a b (Holds Unit a b)
decide = Unit a b -> Decision Unit a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes Unit a b
Unit '() '()
Unit
  toHolds :: forall (a :: ()) (b :: ()) r.
Unit a b -> ((Holds Unit a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds Unit a b
Unit (Holds Unit a b ~ 'TRU, Ob a, Ob b) => r
r = r
(Holds Unit a b ~ 'TRU, Ob a, Ob b) => r
r

instance Indexed ()

instance Finite () where
  type Objects () = '[ '()]
  finite :: IndexedList (Objects ())
finite = IndexedList '[] -> IndexedList '[ '()]
forall {k} (a :: k) (as1 :: [k]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
FCons IndexedList '[]
forall {k}. IndexedList '[]
FNil

instance Enumerable () where
  withIndex :: forall (a :: ()) r. Ob a => (KnownIndex a => r) -> r
withIndex KnownIndex a => r
r = r
KnownIndex a => r
r
  withOb :: forall (a :: ()) r. KnownIndex a => (Ob a => r) -> r
withOb @a Ob a => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @(Index a) of SNat (Index a)
SZ -> r
Ob a => r
r