{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Star where

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

import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (Strong (..))
import Proarrow.Category.Monoidal.Applicative (Alternative (..), Applicative (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (:~>), type (+->))
import Proarrow.Functor (Functor (..), Prelude (..))
import Proarrow.Object.BinaryCoproduct (COPROD (..), Cocartesian, Coprod (..), HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..), StrongProd)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep)
import Proarrow.Category.Instance.Sub (SUBCAT, Sub (..))
import Proarrow.Category.Instance.Nat (Nat(..))

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, Cartesian j, Cartesian k) => MonoidalProfunctor (Star (f :: j -> k)) where
  par0 :: Star f Unit Unit
par0 = (TerminalObject ~> f TerminalObject)
-> Star f TerminalObject TerminalObject
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (El TerminalObject -> TerminalObject ~> f TerminalObject
forall (a :: j). El a -> El (f a)
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
El a -> El (f a)
pure El TerminalObject
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 = let ab :: (x2 ** y2) ~> (x2 ** y2)
ab = forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj x2 -> (y2 ~> y2) -> (x2 ** y2) ~> (x2 ** y2)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b in ((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)
(x2 && y2) ~> (x2 ** y2)
ab ((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)) ((Ob (x2 ** y2), Ob (x2 ** y2)) => Star f (x1 ** y1) (x2 ** y2))
-> ((x2 ** y2) ~> (x2 ** y2)) -> Star f (x1 ** y1) (x2 ** y2)
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
\\ (x2 ** y2) ~> (x2 ** y2)
ab

-- 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 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, Cartesian k, Cocartesian j) => MonoidalProfunctor (CoprodDom (Star (f :: j -> k))) where
  par0 :: CoprodDom (Star f) Unit Unit
par0 = Star f TerminalObject InitialObject
-> CoprodDom (Star f) TerminalObject ('COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> CoprodDom p a ('COPR b)
Co ((TerminalObject ~> f InitialObject)
-> Star f TerminalObject InitialObject
forall {k1} {k} (b :: k1) (a :: k) (f :: k1 -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star TerminalObject ~> f InitialObject
forall (a :: j). Ob a => El (f a)
forall {j} {k} (f :: j -> k) (a :: j).
(Alternative f, Ob a) =>
El (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)))

strength :: forall f a b. (Functor f, StrongProd (Star f), Ob a, Ob b) => a && f b ~> f (a && b)
strength :: forall {k} (f :: k -> k) (a :: k) (b :: k).
(Functor f, StrongProd (Star f), Ob a, Ob b) =>
(a && f b) ~> f (a && b)
strength = Star f (a && f b) (a && b) -> (a && f b) ~> f (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 :: k) (b :: k) (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 :: k). (CategoryOf k, 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))))