Costar.hs

{-# LANGUAGE AllowAmbiguousTypes #-}

-- | 'Costar' embeds a functor @f@ as a profunctor with the functor on the source side:
-- @Costar f a b = f a ~> b@. It is the corepresentable profunctor of @f@, dual to
-- 'Proarrow.Profunctor.Instance.Star.Star'.
module Proarrow.Profunctor.Instance.Costar where

import Control.Monad qualified as P
import Data.Functor.Compose (Compose (..))
import Prelude qualified as P

import Proarrow.Category.Enriched.Thin (DecidableProfunctor (..), Thin, ThinProfunctor (..), mapDecision)
import Proarrow.Category.Instance.Nat (Nat' (..), type (.->) (..))
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), withOb2)
import Proarrow.Category.Monoidal.Cartesian (Cartesian)
import Proarrow.Category.Monoidal.Distributive (Cotraversable (..), Traversable (..))
import Proarrow.Core (CategoryOf (..), Hom, Profunctor (..), Promonad (..), rmap, (//), (:~>), type (+->))
import Proarrow.Functor (Functor (..), Prelude (..), withObF)
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), dimapCorep)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Product ((:*:) (..))
import Proarrow.Profunctor.Instance.Star (Star, pattern Star)
import Proarrow.Promonad (Procomonad (..))

type Costar' :: OPPOSITE (j .-> k) -> k +-> j
data Costar' f a b where
  Costar' :: (Ob a) => f a ~> b -> Costar' (OP (NT f)) a b

type Costar f = Costar' (OP (NT f))
pattern Costar :: () => (Ob a) => (f a ~> b) -> Costar f a b
pattern Costar f = Costar' f
{-# COMPLETE Costar #-}
unCostar :: Costar f a b -> f a ~> b
unCostar (Costar f) = f

instance (Functor f) => Profunctor (Costar f) where
  dimap = dimapCorep
  r \\ Costar f = r \\ f

instance Functor Costar' where
  map (Op (Nat' n)) = Prof \(Costar f) -> Costar (f . n)

instance (Functor f) => Corepresentable (Costar f) where
  type Costar f %% a = f a
  coindex = unCostar
  cotabulate = Costar
  corepMap = map

instance (Profunctor p) => Promonad (Costar ((:*:) p)) where
  id = Costar (Prof \(_ :*: q) -> q)
  Costar (Prof l) . Costar (Prof r) = Costar (Prof \(p :*: a) -> l (p :*: r (p :*: a)))

instance (P.Monad m) => Procomonad (Costar (Prelude m)) where
  proextract (Costar f) = f . Prelude . P.pure
  produplicate (Costar f) = Costar unPrelude :.: Costar (f . Prelude . P.join . unPrelude)

composeCostar :: (Functor g) => Costar f :.: Costar g :~> Costar (Compose g f)
composeCostar (Costar f :.: Costar g) = Costar (g . map f . getCompose)

-- | Every functor between cartesian categories is a colax monoidal functor.
instance (Cartesian j, Cartesian k, Functor (f :: j -> k)) => MonoidalProfunctor (Costar f) where
  one = withObF @f @(Unit :: j) (Costar terminate)
  Costar @a f ** Costar @b g = withOb2 @j @a @b (Costar (f . map (fst @j @a @b) &&& g . map (snd @j @a @b)))

instance (Functor t, Traversable (Star t)) => Cotraversable (Costar t) where
  cotraverse (p :.: Costar f) = p // Costar id :.: case traverse (Star id :.: p) of p' :.: Star g -> rmap (f . g) p'

instance (Functor f, Thin j) => ThinProfunctor (Costar f :: j +-> k) where
  type HasArrow (Costar f :: j +-> k) a b = HasArrow (Hom j) (f a) b
  arr = Costar arr
  withArr (Costar f) r = withArr f r

instance (Functor f, DecidableProfunctor (Hom j)) => DecidableProfunctor (Costar f :: j +-> k) where
  type Holds (Costar f :: j +-> k) a b = Holds (Hom j) (f a) b
  decide @a @b = withObF @f @a (mapDecision Costar (decide @(Hom j) @(f a) @b))
  toHolds (Costar f) r = toHolds f r