Representable.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Representable profunctors: profunctors of the shape /functor followed by hom/, identifying @p a b@
-- with @a ~> p % b@. Since a functor between different kinds cannot be written directly as a Haskell data
-- type, representable profunctors (with their functorial action '%') are how this library encodes such
-- functors; 'Rep' packages any 'Proarrow.Functor.FunctorForRep' as its representable profunctor.
module Proarrow.Profunctor.Representable where

import Data.Kind (Constraint)

import Proarrow.Category.Enriched.Thin (DecidableProfunctor (..), Thin, ThinProfunctor (..), mapDecision)
import Proarrow.Category.Instance.Bool (Booleans (..))
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit ()
import Proarrow.Core (CategoryOf (..), Hom, Profunctor (..), Promonad (..), lmap, rmap, (:~>), type (+->))
import Proarrow.Functor (FunctorForRep (..), Presheaf, withMappedOb)
import Proarrow.Object (Obj, obj, src, tgt)
import Proarrow.Optic (PIso, iso)
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..), corepUniv, dimapCorep, withObCorep)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))

infixl 8 %

-- | A profunctor is representable if @p ? a@ as a presheaf is representable in a functorial way over @a@.
type Representable :: forall {j} {k}. j +-> k -> Constraint
class (Profunctor p) => Representable (p :: j +-> k) where
  type p % (a :: j) :: k
  index :: p a b -> a ~> p % b
  tabulate :: (Ob b) => (a ~> p % b) -> p a b
  tabulate f = lmap f repUniv
  repMap :: (a ~> b) -> p % a ~> p % b
  repMap @a f = index @p (rmap f (repUniv @p @a)) \\ f
  repUniv :: (Ob a) => p (p % a) a
  repUniv @a = tabulate (repObj @p @a)
  {-# MINIMAL index, ((tabulate, repMap) | repUniv) #-}

instance Representable (->) where
  type (->) % a = a
  index f = f
  tabulate f = f
  repMap f = f
  repUniv = id

instance Representable Booleans where
  type Booleans % x = x
  index = id
  tabulate = id
  repMap = id

instance (Representable p, Representable q) => Representable (p :**: q) where
  type (p :**: q) % '(a, b) = '(p % a, q % b)
  index (p :**: q) = index p :**: index q
  tabulate (f :**: g) = tabulate f :**: tabulate g
  repMap (f :**: g) = repMap @p f :**: repMap @q g
  repUniv = repUniv :**: repUniv

instance (CategoryOf k) => Representable (Id :: k +-> k) where
  type Id % a = a
  index = unId
  tabulate = Id
  repMap = id

instance (Representable p, Representable q) => Representable (p :.: q) where
  type (p :.: q) % a = p % (q % a)
  index (p :.: q) = repMap @p (index q) . index p
  tabulate :: forall a b. (Ob b) => (a ~> ((p :.: q) % b)) -> (:.:) p q a b
  tabulate f = withObRep @q @b (tabulate f :.: tabulate id)
  repMap f = repMap @p (repMap @q f)

repObj :: forall p a. (Representable p, Ob a) => Obj (p % a)
repObj = repMap @p (obj @a)

withObRep :: forall p a r. (Representable p, Ob a) => ((Ob (p % a)) => r) -> r
withObRep r = r \\ repObj @p @a

dimapRep :: forall p a b c d. (Representable p) => (c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep l r = tabulate @p . dimap l (repMap @p r) . index \\ r

tabulated :: forall p a a' b b'. (Representable p, Ob b) => PIso (a ~> p % b) (a' ~> p % b') (p a b) (p a' b')
tabulated = iso tabulate index

-- | A representable presheaf is a contravariant representable functor in the Haskell sense.
type RepresentablePresheaf (f :: Presheaf k) = Representable f

type Key (f :: Presheaf k) = f % '()
tabulatedPresheaf :: (RepresentablePresheaf f, Ob a) => PIso (a ~> Key f) (a' ~> Key f) (f a '()) (f a' '())
tabulatedPresheaf = tabulated

instance (Representable p) => Corepresentable (Op p) where
  type Op p %% OP a = OP (p % a)
  coindex (Op f) = Op (index f)
  cotabulate (Op f) = Op (tabulate f)
  corepMap (Op f) = Op (repMap @p f)
  corepUniv = Op repUniv

instance (Corepresentable p) => Representable (Op p) where
  type Op p % OP a = OP (p %% a)
  index (Op f) = Op (coindex f)
  tabulate (Op f) = Op (cotabulate f)
  repMap (Op f) = Op (corepMap @p f)
  repUniv = Op corepUniv

-- | The corepresenting functor of @p@ repackaged with the opposite variance: a value is an arrow
-- @a '~>' p '%%' b@, making @'CorepStar' p@ 'Representable'.
type CorepStar :: (k +-> j) -> (j +-> k)
data CorepStar p a b where
  CorepStar :: (Ob b) => {unCorepStar :: a ~> p %% b} -> CorepStar p a b

instance (Corepresentable p) => Profunctor (CorepStar p) where
  dimap = dimapRep
  r \\ CorepStar f = r \\ f
instance (Corepresentable p) => Representable (CorepStar p) where
  type CorepStar p % a = p %% a
  index (CorepStar f) = f
  tabulate = CorepStar
  repMap = corepMap @p

mapCorepStar :: (Corepresentable p, Corepresentable q) => p ~> q -> CorepStar q ~> CorepStar p
mapCorepStar (Prof n) = Prof \(CorepStar @a f) -> CorepStar (coindex (n (corepUniv @_ @a)) . f)

-- | The representing functor of @p@ repackaged with the opposite variance: a value is an arrow
-- @p '%' a '~>' b@, making @'RepCostar' p@ 'Corepresentable'.
type RepCostar :: (k +-> j) -> (j +-> k)
data RepCostar p a b where
  RepCostar :: (Ob a) => {unRepCostar :: p % a ~> b} -> RepCostar p a b

instance (Representable p) => Profunctor (RepCostar p) where
  dimap = dimapCorep
  r \\ RepCostar f = r \\ f
instance (Representable p) => Corepresentable (RepCostar p) where
  type RepCostar p %% a = p % a
  coindex (RepCostar f) = f
  cotabulate = RepCostar
  corepMap = repMap @p
instance (Representable p, Thin j) => ThinProfunctor (RepCostar p :: j +-> k) where
  type HasArrow (RepCostar p :: j +-> k) a b = HasArrow (Hom j) (p % a) b
  arr @a = withObRep @p @a (RepCostar arr)
  withArr (RepCostar f) r = withArr f r

instance (Representable p, DecidableProfunctor (Hom j)) => DecidableProfunctor (RepCostar p :: j +-> k) where
  type Holds (RepCostar p :: j +-> k) a b = Holds (Hom j) (p % a) b
  decide @a @b = withObRep @p @a (mapDecision RepCostar (decide @(Hom j) @(p % a) @b))
  toHolds (RepCostar f) r = toHolds f r

-- | @'CorepStar' p a b@ holds in a thin category exactly when @a ≤ p %% b@.
instance (Corepresentable p, Thin k) => ThinProfunctor (CorepStar p :: j +-> k) where
  type HasArrow (CorepStar p :: j +-> k) a b = HasArrow (Hom k) a (p %% b)
  arr @_ @b = withObCorep @p @b (CorepStar arr)
  withArr (CorepStar f) r = withArr f r

instance (Corepresentable p, DecidableProfunctor (Hom k)) => DecidableProfunctor (CorepStar p :: j +-> k) where
  type Holds (CorepStar p :: j +-> k) a b = Holds (Hom k) a (p %% b)
  decide @a @b = withObCorep @p @b (mapDecision CorepStar (decide @(Hom k) @a @(p %% b)))
  toHolds (CorepStar f) r = toHolds f r

mapRepCostar :: (Representable p, Representable q) => p ~> q -> RepCostar q ~> RepCostar p
mapRepCostar (Prof n) = Prof \(RepCostar @a f) -> RepCostar (f . index (n (repUniv @_ @a)))

flipRep :: forall p. (Representable p) => (~>) :~> p -> RepCostar p :~> (~>)
flipRep n p = coindex p . index (n (src p))

unflipRep :: forall p. (Representable p) => RepCostar p :~> (~>) -> (~>) :~> p
unflipRep n f = tabulate (n (RepCostar (repMap @p f))) \\ f

flipCorep :: forall p. (Corepresentable p) => (~>) :~> p -> CorepStar p :~> (~>)
flipCorep n p = coindex (n (tgt p)) . index p

unflipCorep :: forall p. (Corepresentable p) => CorepStar p :~> (~>) -> (~>) :~> p
unflipCorep n f = cotabulate (n (CorepStar (corepMap @p f))) \\ f

-- | The representable profunctor of a functor-for-representation @f@ ('FunctorForRep'): a value
-- @'Rep' f a b@ is an arrow @a '~>' f \@ b@. This is the profunctor encoding of
-- functors used throughout the library.
type Rep :: (j +-> k) -> j +-> k
data Rep f a b where
  Rep :: forall b f a. (Ob b) => {unRep :: a ~> f @ b} -> Rep f a b

instance (FunctorForRep f) => Profunctor (Rep f) where
  dimap = dimapRep
  r \\ Rep f = r \\ f
instance (FunctorForRep f) => Representable (Rep f) where
  type Rep f % a = f @ a
  index (Rep f) = f
  tabulate = Rep
  repMap = fmap @f
instance (FunctorForRep f, Thin k) => ThinProfunctor (Rep f :: j +-> k) where
  type HasArrow (Rep f :: j +-> k) a b = HasArrow (Hom k) a (f @ b)
  arr @_ @b = withMappedOb @f @b (Rep arr)
  withArr (Rep f) r = withArr f r

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

rep :: forall f a b a' b'. (FunctorForRep f, Ob b) => PIso (a ~> f @ b) (a' ~> f @ b') (Rep f a b) (Rep f a' b')
rep = tabulated

instance (FunctorForRep f, Promonad (Corep f)) => Promonad (RepCostar (Rep f)) where
  id @b = RepCostar (unCorep (id @(Corep f) @b))
  RepCostar @a l . RepCostar @b r = RepCostar (unCorep (Corep @a @f l . Corep @b @f r))