module Proarrow.Profunctor.Costar where

import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..), (:~>))
import Proarrow.Functor (Functor(..))
import Proarrow.Profunctor.Corepresentable (Corepresentable(..), dimapCorep)
import Proarrow.Profunctor.Composition ((:.:)(..))
import Data.Functor.Compose (Compose(..))

type Costar :: (j -> k) -> PRO j k
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
getCostar :: 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 :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
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 :: j) (b :: k). 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
getCostar
  cotabulate :: forall (a :: j) (b :: k).
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 :: j) (b :: j).
(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 :: 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

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)