-- | The empty profunctor, with no values at all: the initial object of the category of profunctors
-- @j +-> k@.
module Proarrow.Profunctor.Instance.Initial where

import Prelude (Eq, Show)

import Proarrow.Category.Enriched.Dagger (Dagger, DaggerProfunctor (..))
import Proarrow.Category.Enriched.Thin (DecidableProfunctor (..), Decision (..), Thin, ThinProfunctor (..))
import Proarrow.Category.Instance.Bool (BOOL (..))
import Proarrow.Category.Instance.Zero (Bottom (..))
import Proarrow.Core (CategoryOf, Profunctor (..), type (+->))

-- | The profunctor with no values at all: the initial object of the category of profunctors
-- @j +-> k@.
type InitialProfunctor :: j +-> k
data InitialProfunctor a b
  deriving (Int -> InitialProfunctor a b -> ShowS
[InitialProfunctor a b] -> ShowS
InitialProfunctor a b -> String
(Int -> InitialProfunctor a b -> ShowS)
-> (InitialProfunctor a b -> String)
-> ([InitialProfunctor a b] -> ShowS)
-> Show (InitialProfunctor a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k) j (b :: j). Int -> InitialProfunctor a b -> ShowS
forall k (a :: k) j (b :: j). [InitialProfunctor a b] -> ShowS
forall k (a :: k) j (b :: j). InitialProfunctor a b -> String
$cshowsPrec :: forall k (a :: k) j (b :: j). Int -> InitialProfunctor a b -> ShowS
showsPrec :: Int -> InitialProfunctor a b -> ShowS
$cshow :: forall k (a :: k) j (b :: j). InitialProfunctor a b -> String
show :: InitialProfunctor a b -> String
$cshowList :: forall k (a :: k) j (b :: j). [InitialProfunctor a b] -> ShowS
showList :: [InitialProfunctor a b] -> ShowS
Show, InitialProfunctor a b -> InitialProfunctor a b -> Bool
(InitialProfunctor a b -> InitialProfunctor a b -> Bool)
-> (InitialProfunctor a b -> InitialProfunctor a b -> Bool)
-> Eq (InitialProfunctor a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k) j (b :: j).
InitialProfunctor a b -> InitialProfunctor a b -> Bool
$c== :: forall k (a :: k) j (b :: j).
InitialProfunctor a b -> InitialProfunctor a b -> Bool
== :: InitialProfunctor a b -> InitialProfunctor a b -> Bool
$c/= :: forall k (a :: k) j (b :: j).
InitialProfunctor a b -> InitialProfunctor a b -> Bool
/= :: InitialProfunctor a b -> InitialProfunctor a b -> Bool
Eq)

instance (CategoryOf j, CategoryOf k) => Profunctor (InitialProfunctor :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> InitialProfunctor a b -> InitialProfunctor c d
dimap c ~> a
_ b ~> d
_ = \case {}
  \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> InitialProfunctor a b -> r
(\\) (Ob a, Ob b) => r
_ = \case {}

instance (Dagger k) => DaggerProfunctor (InitialProfunctor :: k +-> k) where
  dagger :: forall (a :: k) (b :: k).
InitialProfunctor a b -> InitialProfunctor b a
dagger = \case {}

instance (Thin j, Thin k) => (ThinProfunctor (InitialProfunctor :: j +-> k)) where
  type HasArrow (InitialProfunctor :: j +-> k) a b = Bottom
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow InitialProfunctor a b) =>
InitialProfunctor a b
arr = InitialProfunctor a b
forall a. Bottom => a
forall a. a
no
  withArr :: forall (a :: k) (b :: j) r.
InitialProfunctor a b
-> ((HasArrow InitialProfunctor a b, Ob a, Ob b) => r) -> r
withArr = \case {}

instance (Thin j, Thin k) => DecidableProfunctor (InitialProfunctor :: j +-> k) where
  type Holds (InitialProfunctor :: j +-> k) a b = FLS
  decide :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Decision InitialProfunctor a b (Holds InitialProfunctor a b)
decide = Decision InitialProfunctor a b 'FLS
Decision InitialProfunctor a b (Holds InitialProfunctor a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
  toHolds :: forall (a :: k) (b :: j) r.
InitialProfunctor a b
-> ((Holds InitialProfunctor a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds = \case {}