{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Profunctor.Costar where

import Control.Monad qualified as P
import Data.Functor.Compose (Compose (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (:~>), type (+->), (//), rmap, obj)
import Proarrow.Functor (Functor (..), Prelude (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), dimapCorep)
import Proarrow.Promonad (Procomonad (..))
import Prelude qualified as P
import Proarrow.Category.Monoidal (MonoidalProfunctor (..), withOb2)
import Proarrow.Object.Terminal (HasTerminalObject(..))
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..))
import Proarrow.Category.Monoidal.Distributive (Traversable (..), Cotraversable (..))
import Proarrow.Profunctor.Star (Star (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))

type Costar :: (j -> k) -> k +-> j
data Costar f a b where
  Costar :: (Ob a) => {forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Costar f a b -> f a ~> b
unCostar :: f a ~> b} -> Costar f a b

instance (Functor f) => Profunctor (Costar f) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Costar f a b -> Costar f c d
dimap = (c ~> a) -> (b ~> d) -> Costar f a b -> Costar f c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Corepresentable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Costar f a b -> r
\\ Costar f a ~> b
f = r
(Ob a, Ob b) => r
(Ob (f a), Ob b) => r
r ((Ob (f a), Ob b) => r) -> (f a ~> b) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ f a ~> b
f

instance (Functor f) => Corepresentable (Costar f) where
  type Costar f %% a = f a
  coindex :: forall (a :: k) (b :: j). Costar f a b -> (Costar f %% a) ~> b
coindex = Costar f a b -> f a ~> b
Costar f a b -> (Costar f %% a) ~> b
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Costar f a b -> f a ~> b
unCostar
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((Costar f %% a) ~> b) -> Costar f a b
cotabulate = (f a ~> b) -> Costar f a b
((Costar f %% a) ~> b) -> Costar f a b
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Costar f %% a) ~> (Costar f %% b)
corepMap = (a ~> b) -> f a ~> f b
(a ~> b) -> (Costar f %% a) ~> (Costar f %% b)
forall (a :: k) (b :: k). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map

instance (P.Monad m) => Procomonad (Costar (Prelude m)) where
  extract :: Costar (Prelude m) :~> (~>)
extract (Costar Prelude m a ~> b
f) = Prelude m a ~> b
Prelude m a -> b
f (Prelude m a -> b) -> (a -> Prelude m a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m a -> Prelude m a
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (m a -> Prelude m a) -> (a -> m a) -> a -> Prelude m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a -> m a
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure
  duplicate :: Costar (Prelude m) :~> (Costar (Prelude m) :.: Costar (Prelude m))
duplicate (Costar Prelude m a ~> b
f) = (Prelude m a ~> m a) -> Costar (Prelude m) a (m a)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar Prelude m a ~> m a
Prelude m a -> m a
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
unPrelude Costar (Prelude m) a (m a)
-> Costar (Prelude m) (m a) b
-> (:.:) (Costar (Prelude m)) (Costar (Prelude m)) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (Prelude m (m a) ~> b) -> Costar (Prelude m) (m a) b
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (Prelude m a ~> b
Prelude m a -> b
f (Prelude m a -> b)
-> (Prelude m (m a) -> Prelude m a) -> Prelude m (m a) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m a -> Prelude m a
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (m a -> Prelude m a)
-> (Prelude m (m a) -> m a) -> Prelude m (m a) -> Prelude m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m (m a) -> m a
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
P.join (m (m a) -> m a)
-> (Prelude m (m a) -> m (m a)) -> Prelude m (m a) -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Prelude m (m a) -> m (m a)
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
unPrelude)

composeCostar :: (Functor g) => Costar f :.: Costar g :~> Costar (Compose g f)
composeCostar :: forall {k} {j} (g :: k -> Type) (f :: j -> k).
Functor g =>
(Costar f :.: Costar g) :~> Costar (Compose g f)
composeCostar (Costar f a ~> b
f :.: Costar g b ~> b
g) = (Compose g f a ~> b) -> Costar (Compose g f) a b
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (g b ~> b
g b -> b
g (g b -> b) -> (Compose g f a -> g b) -> Compose g f a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (f a ~> b) -> g (f a) ~> g b
forall (a :: k) (b :: k). (a ~> b) -> g a ~> g b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map f a ~> b
f (g (f a) -> g b)
-> (Compose g f a -> g (f a)) -> Compose g f a -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Compose g f a -> g (f a)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)

-- | Every functor between cartesian categories is a colax monoidal functor.
instance (Cartesian j, Cartesian k, Functor (f :: j -> k)) => MonoidalProfunctor (Costar f) where
  par0 :: Costar f Unit Unit
par0 = (f TerminalObject ~> TerminalObject)
-> Costar f TerminalObject TerminalObject
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar f TerminalObject ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  Costar @a f x1 ~> x2
f par :: forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
Costar f x1 x2 -> Costar f y1 y2 -> Costar f (x1 ** y1) (x2 ** y2)
`par` Costar @b f y1 ~> y2
g = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @j @a @b ((f (x1 ** y1) ~> (x2 ** y2)) -> Costar f (x1 ** y1) (x2 ** y2)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (f x1 ~> x2
f (f x1 ~> x2) -> (f (x1 ** y1) ~> f x1) -> f (x1 ** y1) ~> x2
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((x1 ** y1) ~> x1) -> f (x1 ** y1) ~> f x1
forall (a :: j) (b :: j). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @j @a @b) (f (x1 ** y1) ~> x2)
-> (f (x1 ** y1) ~> y2) -> f (x1 ** y1) ~> (x2 && y2)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& f y1 ~> y2
g (f y1 ~> y2) -> (f (x1 ** y1) ~> f y1) -> f (x1 ** y1) ~> y2
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((x1 ** y1) ~> y1) -> f (x1 ** y1) ~> f y1
forall (a :: j) (b :: j). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @j @a @b)))

instance (Functor t, Traversable (Star t)) => Cotraversable (Costar t) where
  cotraverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: Costar t) :~> (Costar t :.: p)
cotraverse (p a b
p :.: Costar t b ~> b
f) = p a b
p p a b
-> ((Ob a, Ob b) => (:.:) (Costar t) p a b)
-> (:.:) (Costar t) p a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (t a ~> t a) -> Costar t a (t a)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar t a ~> t a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Costar t a (t a) -> p (t a) b -> (:.:) (Costar t) p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: case (:.:) (Star t) p (t a) b -> (:.:) p (Star t) (t a) b
(Star t :.: p) :~> (p :.: Star t)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, DistributiveProfunctor p, Strong k p,
 SelfAction k) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(Star t :.: p) :~> (p :.: Star t)
traverse ((t a ~> t a) -> Star t (t a) a
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star t a ~> t a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Star t (t a) a -> p a b -> (:.:) (Star t) p (t a) b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p a b
p) of p (t a) b
p' :.: Star b ~> t b
g -> (b ~> b) -> p (t a) b -> p (t a) b
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (t b ~> b
f (t b ~> b) -> (b ~> t b) -> b ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> t b
g) p (t a) b
p'

costrength :: forall {m} f a b. (Functor f, Strong m (Costar f), Ob (a :: m), Ob b) => f (Act a b) ~> Act a (f b)
costrength :: forall {d} {k} {m} (f :: d -> k) (a :: m) (b :: d).
(Functor f, Strong m (Costar f), Ob a, Ob b) =>
f (Act a b) ~> Act a (f b)
costrength = Costar f (Act a b) (Act a (f b)) -> f (Act a b) ~> Act a (f b)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Costar f a b -> f a ~> b
unCostar ((a ~> a) -> Costar f b (f b) -> Costar f (Act a b) (Act a (f b))
forall (a :: m) (b :: m) (x :: d) (y :: k).
(a ~> b) -> Costar f x y -> Costar f (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) ((f b ~> f b) -> Costar f b (f b)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(f b))))