{-# 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 (..))
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 :: 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 => r) -> r
withArr Unit a b
Unit HasArrow Unit a b => r
r = r
HasArrow Unit 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