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)