Terminal.hs

-- | The terminal profunctor, with exactly one value between any two objects: the terminal object of the
-- category of profunctors @j +-> k@.
module Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (.., TerminalProfunctor)) where

import Proarrow.Category.Enriched.Dagger (Dagger, DaggerProfunctor (..))
import Proarrow.Category.Enriched.Thin (DecidableProfunctor (..), Decision (..), ThinProfunctor (..))
import Proarrow.Category.Instance.Bool (BOOL (..))
import Proarrow.Category.Monoidal (Monoidal, MonoidalProfunctor (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Object (pattern Obj, type Obj)

-- | The profunctor with exactly one value between any two objects: the terminal object of the
-- category of profunctors @j +-> k@.
type TerminalProfunctor :: j +-> k
data TerminalProfunctor a b where
  TerminalProfunctor' :: Obj a -> Obj b -> TerminalProfunctor (a :: j) (b :: k)

instance (CategoryOf j, CategoryOf k) => Profunctor (TerminalProfunctor :: j +-> k) where
  dimap l r TerminalProfunctor = TerminalProfunctor \\ l \\ r
  r \\ TerminalProfunctor = r

instance (CategoryOf k) => Promonad (TerminalProfunctor :: k +-> k) where
  id = TerminalProfunctor
  TerminalProfunctor . TerminalProfunctor = TerminalProfunctor

instance (Monoidal j, Monoidal k) => MonoidalProfunctor (TerminalProfunctor :: j +-> k) where
  one = TerminalProfunctor' one one
  TerminalProfunctor' a1 b1 ** TerminalProfunctor' a2 b2 = TerminalProfunctor' (a1 ** a2) (b1 ** b2)

instance (Dagger k) => DaggerProfunctor (TerminalProfunctor :: k +-> k) where
  dagger TerminalProfunctor = TerminalProfunctor

pattern TerminalProfunctor
  :: forall {j} {k} a b. (CategoryOf j, CategoryOf k) => (Ob (a :: j), Ob (b :: k)) => TerminalProfunctor a b
pattern TerminalProfunctor = TerminalProfunctor' Obj Obj

{-# COMPLETE TerminalProfunctor #-}

instance (CategoryOf j, CategoryOf k) => ThinProfunctor (TerminalProfunctor :: j +-> k)

instance (CategoryOf j, CategoryOf k) => DecidableProfunctor (TerminalProfunctor :: j +-> k) where
  type Holds TerminalProfunctor a b = TRU
  decide = Yes TerminalProfunctor
  toHolds TerminalProfunctor r = r