module Proarrow.Category.Instance.Zero where

import Proarrow.Core (CAT, CategoryOf(..), Promonad(..), Profunctor(..), dimapDefault)

data VOID

type Zero :: CAT VOID
data Zero a b

class IsVoid (a :: VOID) where
  voidId :: Zero a a

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

instance Promonad Zero where
  id :: forall (a :: VOID). Ob a => Zero a a
id = Zero a a
forall (a :: VOID). IsVoid a => Zero a a
voidId
  . :: forall (b :: VOID) (c :: VOID) (a :: VOID).
Zero b c -> Zero a b -> Zero a c
(.) = 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