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)