module Proarrow.Category.Instance.Zero where

import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault)
import Proarrow.Preorder.ThinCategory (ThinProfunctor (..))
import Proarrow.Category.Dagger (DaggerProfunctor (..))

type data VOID

type Zero :: CAT VOID
data Zero a b

-- Stolen from the constraints package
class Bottom where
  no :: a

-- | The category with no objects, the initial category.
instance CategoryOf VOID where
  type (~>) = Zero
  type Ob a = Bottom

instance Promonad Zero where
  id :: forall (a :: VOID). Ob a => Zero a a
id = Zero a a
forall a. Bottom => a
forall a. a
no
  . :: forall (b :: VOID) (c :: VOID) (a :: VOID).
Zero b c -> Zero a b -> Zero a c
(.) = \case {}

instance Profunctor Zero where
  dimap :: forall (c :: VOID) (a :: VOID) (b :: VOID) (d :: VOID).
(c ~> a) -> (b ~> d) -> Zero a b -> Zero c d
dimap = (c ~> a) -> (b ~> d) -> Zero a b -> Zero c d
Zero c a -> Zero b d -> Zero a b -> Zero 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
_ \\ :: forall (a :: VOID) (b :: VOID) r.
((Ob a, Ob b) => r) -> Zero a b -> r
\\ Zero a b
x = case Zero a b
x of {}

instance ThinProfunctor Zero where
  arr :: forall (a :: VOID) (b :: VOID).
(Ob a, Ob b, HasArrow Zero a b) =>
Zero a b
arr = Zero a b
forall a. Bottom => a
forall a. a
no
  withArr :: forall (a :: VOID) (b :: VOID) r.
Zero a b -> (HasArrow Zero a b => r) -> r
withArr = \case {}

instance DaggerProfunctor Zero where
  dagger :: forall (a :: VOID) (b :: VOID). Zero a b -> Zero b a
dagger = \case {}