module Proarrow.Profunctor.Star where

import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..), (:~>))
import Proarrow.Functor (Functor(..), Prelude(..))
import Proarrow.Profunctor.Representable (Representable(..), dimapRep)
import Proarrow.Profunctor.Composition ((:.:)(..))
import Data.Functor.Compose (Compose(..))
import qualified Prelude as P

type Star :: (k1 -> k2) -> PRO k2 k1
data Star f a b where
  Star :: Ob b => { forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Star f a b -> a ~> f b
getStar :: a ~> f b } -> Star f a b

instance Functor f => Profunctor (Star f) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Star f a b -> Star f c d
dimap = (c ~> a) -> (b ~> d) -> Star f a b -> Star f c d
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> Star f a b -> r
\\ Star a ~> f b
f = r
(Ob a, Ob b) => r
(Ob a, Ob (f b)) => r
r ((Ob a, Ob (f b)) => r) -> (a ~> f b) -> r
forall (a :: j) (b :: j) 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
\\ a ~> f b
f

instance Functor f => Representable (Star f) where
  type Star f % a = f a
  index :: forall (a :: j) (b :: k). Star f a b -> a ~> (Star f % b)
index = Star f a b -> a ~> f b
Star f a b -> a ~> (Star f % b)
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Star f a b -> a ~> f b
getStar
  tabulate :: forall (b :: k) (a :: j). Ob b => (a ~> (Star f % b)) -> Star f a b
tabulate = (a ~> f b) -> Star f a b
(a ~> (Star f % b)) -> Star f a b
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star
  repMap :: forall (a :: k) (b :: k). (a ~> b) -> (Star f % a) ~> (Star f % b)
repMap = (a ~> b) -> f a ~> f b
(a ~> b) -> (Star f % a) ~> (Star 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 => Promonad (Star (Prelude m)) where
  id :: forall a. Ob a => Star (Prelude m) a a
id = (a ~> Prelude m a) -> Star (Prelude m) a a
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (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)
  Star b ~> Prelude m c
g . :: forall b c a.
Star (Prelude m) b c
-> Star (Prelude m) a b -> Star (Prelude m) a c
. Star a ~> Prelude m b
f = (a ~> Prelude m c) -> Star (Prelude m) a c
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star \a
a -> m c -> Prelude m c
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (Prelude m b -> m b
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
getPrelude (a ~> Prelude m b
a -> Prelude m b
f a
a) m b -> (b -> m c) -> m c
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
P.>>= (Prelude m c -> m c
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
getPrelude (Prelude m c -> m c) -> (b -> Prelude m c) -> b -> m c
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
. b ~> Prelude m c
b -> Prelude m c
g))

composeStar :: Functor f => Star f :.: Star g :~> Star (Compose f g)
composeStar :: forall {k} {k1} (f :: k -> Type) (g :: k1 -> k).
Functor f =>
(Star f :.: Star g) :~> Star (Compose f g)
composeStar (Star a ~> f b
f :.: Star b ~> g b
g) = (a ~> Compose f g b) -> Star (Compose f g) a b
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (f (g b) -> Compose f g b
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g b) -> Compose f g b) -> (a -> f (g b)) -> a -> Compose f 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
. (b ~> g b) -> f b ~> f (g 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 b ~> g b
g (f b -> f (g b)) -> (a -> f b) -> a -> f (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
. a ~> f b
a -> f b
f)