{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.Unit where

import Prelude (type (~))

import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Preorder.ThinCategory (ThinProfunctor (..), Codiscrete, Discrete (..))
import Proarrow.Category.Dagger (DaggerProfunctor (..))

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 :: PRO 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 '() '() = ()
  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 => r) -> r
withArr Unit a b
Unit HasArrow Unit a b => r
r = r
HasArrow Unit a b => r
r

instance Codiscrete Unit
instance Discrete Unit where
  withEq :: forall (a :: ()) (b :: ()) r. Unit a b -> ((a ~ b) => r) -> r
withEq Unit a b
Unit (a ~ b) => r
r = r
(a ~ b) => r
r

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

instance HasInitialObject () where
  type InitialObject = '()
  initiate :: forall (a :: ()). Ob a => InitialObject ~> a
initiate = InitialObject ~> a
Unit '() '()
Unit