module Proarrow.Profunctor.Costar where

import Control.Monad qualified as P
import Data.Functor.Compose (Compose (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (:~>), type (+->))
import Proarrow.Functor (Functor (..), Prelude (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), dimapCorep)
import Proarrow.Promonad (Procomonad (..))
import Prelude qualified as P

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 :: j) (a :: j) (b :: k) (d :: k).
(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 :: j) (b :: k) 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 :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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)