{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Star where

import Data.Functor.Compose (Compose (..))
import Data.Kind (Type)
import Prelude qualified as P

import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Sub (SUBCAT, Sub (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..), Monoidal (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Category.Monoidal.Applicative (Alternative (..), Applicative (..))
import Proarrow.Category.Monoidal.Distributive (Traversable (..), Distributive)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, obj, (:~>), type (+->))
import Proarrow.Functor (Functor (..), Prelude (..))
import Proarrow.Object.BinaryCoproduct (COPROD (..), Coprod (..), HasBinaryCoproducts (..), copar)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep)
import Proarrow.Object.Initial (initiate)
import Proarrow.Profunctor.Identity (Id(..))

type Star :: (k1 -> k2) -> k1 +-> k2
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
unStar :: 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 :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
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 :: k) (b :: j). 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
unStar
  tabulate :: forall (b :: j) (a :: k). 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 :: j) (b :: j). (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 :: 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

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
unPrelude (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
unPrelude (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)

instance (Applicative f, Monoidal j, Monoidal k) => MonoidalProfunctor (Star (f :: j -> k)) where
  par0 :: Star f Unit Unit
par0 = (Unit ~> f Unit) -> Star f Unit Unit
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((Unit ~> Unit) -> Unit ~> f Unit
forall (a :: j). (Unit ~> a) -> Unit ~> f a
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
(Unit ~> a) -> Unit ~> f a
pure Unit ~> Unit
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Star @a x1 ~> f x2
f par :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
Star f x1 x2 -> Star f y1 y2 -> Star f (x1 ** y1) (x2 ** y2)
`par` Star @b y1 ~> f y2
g = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b (((x1 ** y1) ~> f (x2 ** y2)) -> Star f (x1 ** y1) (x2 ** y2)
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
forall (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 @f @a @b (x2 ** y2) ~> (x2 ** y2)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((f x2 ** f y2) ~> f (x2 ** y2))
-> ((x1 ** y1) ~> (f x2 ** f y2)) -> (x1 ** y1) ~> f (x2 ** y2)
forall (b :: k) (c :: k) (a :: k). (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
. (x1 ~> f x2
f (x1 ~> f x2) -> (y1 ~> f y2) -> (x1 ** y1) ~> (f x2 ** f y2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` y1 ~> f y2
g)))

instance (Functor f, Distributive j, Distributive k) => MonoidalProfunctor (Coprod (Star (f :: j -> k))) where
  par0 :: Coprod (Star f) Unit Unit
par0 = Star f InitialObject InitialObject
-> Coprod (Star f) ('COPR InitialObject) ('COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((InitialObject ~> f InitialObject)
-> Star f InitialObject InitialObject
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star InitialObject ~> f InitialObject
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate)
  Coprod (Star @a a1 ~> f b1
f) par :: forall (x1 :: COPROD k) (x2 :: COPROD j) (y1 :: COPROD k)
       (y2 :: COPROD j).
Coprod (Star f) x1 x2
-> Coprod (Star f) y1 y2 -> Coprod (Star f) (x1 ** y1) (x2 ** y2)
`par` Coprod (Star @b a1 ~> f b1
g) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @a @b (Star f (a1 || a1) (b1 || b1)
-> Coprod (Star f) ('COPR (a1 || a1)) ('COPR (b1 || b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (((a1 || a1) ~> f (b1 || b1)) -> Star f (a1 || a1) (b1 || b1)
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (((b1 ~> (b1 || b1)) -> f b1 ~> f (b1 || b1)
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 (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b) (f b1 ~> f (b1 || b1)) -> (a1 ~> f b1) -> a1 ~> f (b1 || b1)
forall (b :: k) (c :: k) (a :: k). (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
. a1 ~> f b1
f (a1 ~> f (b1 || b1))
-> (a1 ~> f (b1 || b1)) -> (a1 || a1) ~> f (b1 || b1)
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| (b1 ~> (b1 || b1)) -> f b1 ~> f (b1 || b1)
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 (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b) (f b1 ~> f (b1 || b1)) -> (a1 ~> f b1) -> a1 ~> f (b1 || b1)
forall (b :: k) (c :: k) (a :: k). (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
. a1 ~> f b1
g))))

-- Hmm, another wrapper required...
type CoprodDom :: j +-> k -> COPROD j +-> k
data CoprodDom p a b where
  Co :: {forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
CoprodDom p a ('COPR b) -> p a b
unCo :: p a b} -> CoprodDom p a (COPR b)
instance (Profunctor p) => Profunctor (CoprodDom p) where
  dimap :: forall (c :: j) (a :: j) (b :: COPROD j) (d :: COPROD j).
(c ~> a) -> (b ~> d) -> CoprodDom p a b -> CoprodDom p c d
dimap c ~> a
l (Coprod (Id a1 ~> b1
r)) (Co p a b
p) = p c b1 -> CoprodDom p c ('COPR b1)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> CoprodDom p a ('COPR b)
Co ((c ~> a) -> (b ~> b1) -> p a b -> p c b1
forall (c :: j) (a :: j) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l a1 ~> b1
b ~> b1
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: COPROD j) r.
((Ob a, Ob b) => r) -> CoprodDom p a b -> r
\\ Co p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

instance (Alternative f, Monoidal k, Distributive j) => MonoidalProfunctor (CoprodDom (Star (f :: j -> k))) where
  par0 :: CoprodDom (Star f) Unit Unit
par0 = Star f Unit InitialObject
-> CoprodDom (Star f) Unit ('COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> CoprodDom p a ('COPR b)
Co ((Unit ~> f InitialObject) -> Star f Unit InitialObject
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star Unit ~> f InitialObject
forall (a :: j). Ob a => Unit ~> f a
forall {j} {k} (f :: j -> k) (a :: j).
(Alternative f, Ob a) =>
Unit ~> f a
empty)
  Co (Star @a x1 ~> f b
f) par :: forall (x1 :: k) (x2 :: COPROD j) (y1 :: k) (y2 :: COPROD j).
CoprodDom (Star f) x1 x2
-> CoprodDom (Star f) y1 y2
-> CoprodDom (Star f) (x1 ** y1) (x2 ** y2)
`par` Co (Star @b y1 ~> f b
g) = let ab :: (b || b) ~> (b || b)
ab = forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj b -> (b ~> b) -> (b || b) ~> (b || b)
forall (a :: j) (b :: j) (x :: j) (y :: j).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b in Star f (x1 ** y1) (b || b)
-> CoprodDom (Star f) (x1 ** y1) ('COPR (b || b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> CoprodDom p a ('COPR b)
Co (((x1 ** y1) ~> f (b || b)) -> Star f (x1 ** y1) (b || b)
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Alternative f, Ob a, Ob b) =>
((a || b) ~> c) -> (f a ** f b) ~> f c
forall (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Alternative f, Ob a, Ob b) =>
((a || b) ~> c) -> (f a ** f b) ~> f c
alt @f @a @b (b || b) ~> (b || b)
ab ((f b ** f b) ~> f (b || b))
-> ((x1 ** y1) ~> (f b ** f b)) -> (x1 ** y1) ~> f (b || b)
forall (b :: k) (c :: k) (a :: k). (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
. (x1 ~> f b
f (x1 ~> f b) -> (y1 ~> f b) -> (x1 ** y1) ~> (f b ** f b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` y1 ~> f b
g))) ((Ob (b || b), Ob (b || b)) =>
 CoprodDom (Star f) (x1 ** y1) ('COPR (b || b)))
-> ((b || b) ~> (b || b))
-> CoprodDom (Star f) (x1 ** y1) ('COPR (b || b))
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
\\ (b || b) ~> (b || b)
ab

instance (Functor (f :: Type -> Type)) => Strong Type (Star f) where
  act :: forall a b x y.
(a ~> b) -> Star f x y -> Star f (Act a x) (Act b y)
act a ~> b
f (Star x ~> f y
k) = ((a, x) ~> f (b, y)) -> Star f (a, x) (b, y)
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (\(a
a, x
x) -> (y ~> (b, y)) -> f y ~> f (b, y)
forall a b. (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 (a ~> b
a -> b
f a
a,) (x ~> f y
x -> f y
k x
x))

instance (Functor f, P.Applicative f) => Strong (SUBCAT P.Traversable) (Star (Prelude f)) where
  act :: forall (a :: SUBCAT Traversable) (b :: SUBCAT Traversable) x y.
(a ~> b)
-> Star (Prelude f) x y -> Star (Prelude f) (Act a x) (Act b y)
act (Sub (Nat a1 .~> b1
n)) (Star x ~> Prelude f y
f) = (a1 x ~> Prelude f (b1 y)) -> Star (Prelude f) (a1 x) (b1 y)
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (\a1 x
t -> f (b1 y) -> Prelude f (b1 y)
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude ((x -> f y) -> b1 x -> f (b1 y)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> b1 a -> f (b1 b)
P.traverse (Prelude f y -> f y
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
unPrelude (Prelude f y -> f y) -> (x -> Prelude f y) -> x -> f y
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
. x ~> Prelude f y
x -> Prelude f y
f) (a1 x ~> b1 x
a1 x -> b1 x
a1 .~> b1
n a1 x
t)))

instance Traversable (Star P.Maybe) where
  traverse :: forall (p :: Type +-> Type).
(DistributiveProfunctor p, Strong Type p, SelfAction Type) =>
(Star Maybe :.: p) :~> (p :.: Star Maybe)
traverse (Star a ~> Maybe b
a2mb :.: p b b
p) = (a ~> Maybe b) -> p (Maybe b) (Maybe b) -> p a (Maybe b)
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> Maybe b
a2mb p (Maybe b) (Maybe b)
go p a (Maybe b) -> Star Maybe (Maybe b) b -> (:.:) p (Star Maybe) 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
:.: (Maybe b ~> Maybe b) -> Star Maybe (Maybe b) b
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star Maybe b ~> Maybe b
Maybe b -> Maybe b
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
    where
      go :: p (Maybe b) (Maybe b)
go =
        (Maybe b ~> Either () b)
-> (Either () b ~> Maybe b)
-> p (Either () b) (Either () b)
-> p (Maybe b) (Maybe b)
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap
          (Either () b -> (b -> Either () b) -> Maybe b -> Either () b
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe (() -> Either () b
forall a b. a -> Either a b
P.Left ()) b -> Either () b
forall a b. b -> Either a b
P.Right)
          (Maybe b -> () -> Maybe b
forall a b. a -> b -> a
P.const Maybe b
forall a. Maybe a
P.Nothing (() ~> Maybe b) -> (b ~> Maybe b) -> (() || b) ~> Maybe b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall x a y. (x ~> a) -> (y ~> a) -> (x || y) ~> a
||| b ~> Maybe b
b -> Maybe b
forall a. a -> Maybe a
P.Just)
          (p () ()
p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 p () () -> p b b -> p (() || b) (() || b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
`copar` p b b
p)

instance Traversable (Star []) where
  traverse :: forall (p :: Type +-> Type).
(DistributiveProfunctor p, Strong Type p, SelfAction Type) =>
(Star [] :.: p) :~> (p :.: Star [])
traverse (Star a ~> [b]
a2bs :.: p b b
p) = (a ~> [b]) -> p [b] [b] -> p a [b]
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> [b]
a2bs p [b] [b]
go p a [b] -> Star [] [b] b -> (:.:) p (Star []) 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
:.: ([b] ~> [b]) -> Star [] [b] b
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star [b] ~> [b]
[b] -> [b]
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
    where
      go :: p [b] [b]
go =
        ([b] ~> Either () (b, [b]))
-> (Either () (b, [b]) ~> [b])
-> p (Either () (b, [b])) (Either () (b, [b]))
-> p [b] [b]
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap
          (\[b]
l -> case [b]
l of [] -> () -> Either () (b, [b])
forall a b. a -> Either a b
P.Left (); (b
x : [b]
xs) -> (b, [b]) -> Either () (b, [b])
forall a b. b -> Either a b
P.Right (b
x, [b]
xs))
          ([b] -> () -> [b]
forall a b. a -> b -> a
P.const [] (() ~> [b]) -> ((b, [b]) ~> [b]) -> (() || (b, [b])) ~> [b]
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall x a y. (x ~> a) -> (y ~> a) -> (x || y) ~> a
||| \(b
x, [b]
xs) -> b
x b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
xs)
          (p () ()
p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 p () ()
-> p (b, [b]) (b, [b]) -> p (() || (b, [b])) (() || (b, [b]))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
`copar` (p b b
p p b b -> p [b] [b] -> p (b ** [b]) (b ** [b])
forall x1 x2 y1 y2. p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` p [b] [b]
go))

strength :: forall {m} f a b. (Functor f, Strong m (Star f), Ob (a :: m), Ob b) => Act a (f b) ~> f (Act a b)
strength :: forall {k} {k} {m} (f :: k -> k) (a :: m) (b :: k).
(Functor f, Strong m (Star f), Ob a, Ob b) =>
Act a (f b) ~> f (Act a b)
strength = Star f (Act a (f b)) (Act a b) -> Act a (f b) ~> f (Act a b)
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Star f a b -> a ~> f b
unStar ((a ~> a) -> Star f (f b) b -> Star f (Act a (f b)) (Act a b)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> Star f x y -> Star f (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) ((f b ~> f b) -> Star f (f b) b
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(f b))))