Coyoneda.hs

{-# OPTIONS_GHC -Wno-orphans #-}

-- | The coyoneda construction: @'Coyoneda' p@ pairs a value of @p c d@ with reindexing arrows, making it
-- the free profunctor on an arbitrary type of kind @j +-> k@ (the 'HasFree' instance for 'Profunctor'). By
-- the coyoneda lemma it is equivalent to @p@ when @p@ is already a profunctor ('coyoneda'\/'unCoyoneda').
module Proarrow.Profunctor.Instance.Coyoneda where

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (:~>), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Free (HasFree (..))
import Proarrow.Profunctor.Instance.Costar (Costar, pattern Costar)
import Proarrow.Profunctor.Instance.Star (Star, pattern Star)

-- | The free profunctor on @p@ (the 'HasFree' instance for 'Profunctor'): a @p c d@ together with
-- reindexing arrows on both sides. Equivalent to @p@ when @p@ is already a profunctor
-- ('coyoneda'\/'unCoyoneda').
type Coyoneda :: (j +-> k) -> j +-> k
data Coyoneda p a b where
  Coyoneda :: (a ~> c) -> (d ~> b) -> p c d -> Coyoneda p a b

instance (CategoryOf j, CategoryOf k) => Profunctor (Coyoneda (p :: j +-> k)) where
  dimap l r (Coyoneda f g p) = Coyoneda (f . l) (r . g) p
  r \\ Coyoneda f g _ = r \\ f \\ g

instance (Functor Coyoneda) where
  map (Prof n) = Prof \(Coyoneda g h p) -> Coyoneda g h (n p)

instance Promonad (Star Coyoneda) where
  id = Star (Prof \p -> coyoneda p \\ p)
  Star (Prof l) . Star (Prof r) = Star (Prof (l . unCoyoneda . r))

instance Promonad (Costar Coyoneda) where
  id = Costar (Prof unCoyoneda)
  Costar (Prof l) . Costar (Prof r) = Costar (Prof (\p -> (l . (coyoneda \\ p) . r) p))

instance HasFree Profunctor where
  type Free Profunctor p = Coyoneda p
  lift = Prof \p -> coyoneda p \\ p
  foldMap (Prof f) = Prof (f . unCoyoneda)

coyoneda :: (CategoryOf j, CategoryOf k, Ob a, Ob b) => p a b -> Coyoneda (p :: j +-> k) a b
coyoneda = Coyoneda id id

unCoyoneda :: (Profunctor p) => Coyoneda p :~> p
unCoyoneda (Coyoneda f g p) = dimap f g p