{-# LANGUAGE AllowAmbiguousTypes #-}

-- | A __power grate__ is a 'Proarrow.Optic.Grate.Grate' whose exponent is a fixed tensor /power/ of
-- the focus: the witness @'Pow' n@ presents @s@ as @a ** ... ** a@ (@n@ times), i.e. the exponential
-- by a finite arity, which is also the reader applicative for @n@ readers. That fixed, finite shape
-- is a genuine decomposition, so a power grate is also a __fixed-arity
-- 'Proarrow.Optic.Traversal.Traversal'__ (@'PowerGrateFl' <: 'GrateFl', 'KaleidoFl', 'MonTravFl'@):
-- it zips, aggregates, folds, sets and traverses like those do.
--
-- Its /distinctive/ power over a grate or kaleidoscope is the eliminator: 'powerGrateP' distributes
-- an arbitrary 'MonoidalProfunctor' -- the @Applicative@\/zip structure ('one' and '**') alone --
-- rather than the full 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor' a
-- traversal needs or the traversable carrier a kaleidoscope needs. With a fixed arity, /any/ functor
-- carrier @Costar f@ distributes, by unzipping @f (a ** ... ** a)@ into @f a ** ... ** f a@.
--
-- The aggregation is stated over an abstract @'MonoidalProfunctor' r@, /not/ the Hask-specific
-- @Costar f = f a -> b@: 'powerGrateOf' works at any monoidal profunctor carrier (the hom @('~>')@
-- gives 'Proarrow.Optic.Setter.over'; an applicative @'Proarrow.Profunctor.Instance.Star.Star' f@
-- combines the foci through @f@).
module Proarrow.Optic.PowerGrate
  ( PowerGrateFl (..)
  , PowerGrate
  , PowerGrate'
  , powerGrateOf
  , zipWithOf

    -- * @n@-ary aggregation
  , Nat (..)
  , Tensor
  , KnownNat (..)
  , Pow (..)
  , CoPow (..)
  , powerGrate
  ) where

import Data.Kind (Constraint)
import Proarrow.Adjunction (Proadjunction (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, swapInner, type (**))
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Monoidal.Action (CoprodAction)
import Proarrow.Category.Monoidal.Cartesian (Cartesian)
import Proarrow.Category.Monoidal.Closed (Closed (..), mkExponential)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..), fst, snd, (&&&))
import Proarrow.Category.Monoidal.Distributive (Traversable (..))
import Proarrow.Category.Monoidal.Strength (Strong (..))
import Proarrow.Colimit.BinaryCoproduct (COPROD (..), Coprod (..), HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (//), (\\), type (+->))
import Proarrow.Functor (Functor)
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( ExOptic
  , FLAVOR
  , Optic
  , Prostrong (..)
  , legs2prof
  , withLegs
  )
import Proarrow.Optic.Fold (FoldFl (..))
import Proarrow.Optic.Glass (GlassFl (..))
import Proarrow.Optic.Grate (GrateFl (..))
import Proarrow.Optic.Kaleidoscope (CotravFl, KaleidoFl (..), Kaleidoscopic (..), kaleidoscopeOf)
import Proarrow.Optic.Setter (SetterFl (..))
import Proarrow.Optic.Traversal (MonTravFl (..), TravFl (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Costar (Costar)
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (RepCostar (..), Representable (..))
import Prelude (type (~))

-- | The power-grate flavor: distribute any 'MonoidalProfunctor' @r@ through the witness
-- pair. 'Proarrow.Optic.Traversal.TravFl' is a superclass: every power-grate witness is a
-- traversal witness (instantiate @r@ at a 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor',
-- a special 'MonoidalProfunctor'), so it folds, sets, and traverses. The extra power is
-- distributing the /non/-SDP monoidal profunctors as well. 'Proarrow.Optic.Kaleidoscope.KaleidoFl'
-- is a superclass too: a tensor power is an applicative functor (the reader applicative).
type PowerGrateFl :: forall {k}. FLAVOR k k
class (MonTravFl p q, GrateFl p q) => PowerGrateFl (p :: k +-> k) (q :: k +-> k) where
  powerGrateP :: (MonoidalProfunctor r) => p s a -> q b t -> r a b -> r s t

instance (CategoryOf k) => PowerGrateFl (Id :: k +-> k) (Id :: k +-> k) where
  powerGrateP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
MonoidalProfunctor r =>
Id s a -> Id b t -> r a b -> r s t
powerGrateP (Id s ~> a
l) (Id b ~> t
r) = (s ~> a) -> (b ~> t) -> r a b -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> a
l b ~> t
r
instance (PowerGrateFl f g, PowerGrateFl f' g') => PowerGrateFl (f :.: f') (g' :.: g) where
  powerGrateP :: forall (r :: i +-> i) (s :: i) (a :: i) (b :: i) (t :: i).
MonoidalProfunctor r =>
(:.:) f f' s a -> (:.:) g' g b t -> r a b -> r s t
powerGrateP (f s b
f :.: f' b a
f') (g' b b
g' :.: g b t
g) = forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(PowerGrateFl p q, MonoidalProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: i +-> i) (q :: i +-> i) (r :: i +-> i) (s :: i)
       (a :: i) (b :: i) (t :: i).
(PowerGrateFl p q, MonoidalProfunctor r) =>
p s a -> q b t -> r a b -> r s t
powerGrateP @f @g f s b
f g b t
g (r b b -> r s t) -> (r a b -> r b b) -> r a b -> r s t
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(PowerGrateFl p q, MonoidalProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: i +-> i) (q :: i +-> i) (r :: i +-> i) (s :: i)
       (a :: i) (b :: i) (t :: i).
(PowerGrateFl p q, MonoidalProfunctor r) =>
p s a -> q b t -> r a b -> r s t
powerGrateP @f' @g' f' b a
f' g' b b
g'

-- | The carrier of the literature's kaleidoscope eliminator (@>-@): @'Costar' f@, i.e. @f a -> b@ for
-- any functor @f@ on a cartesian category. Power grates distribute any 'MonoidalProfunctor', and
-- @'Costar' f@ is one, so this is 'powerGrateP' at that carrier; it exists as an instance (rather than
-- only through 'powerGrateOf') so that a power grate composed with another flavor that also runs
-- at @Costar f@ -- an algebraic lens, say -- can be eliminated there directly.
instance (Cartesian k, Functor (f :: k -> k)) => Prostrong PowerGrateFl (Costar f :: k +-> k) where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(PowerGrateFl f g, Profunctor f, Profunctor g) =>
((f :.: Costar f) :.: g) :~> Costar f
proact (f a b
f :.: Costar f b b
c :.: g b b
g) = f a b -> g b b -> Costar f b b -> Costar' ('OP ('NT f)) a b
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(PowerGrateFl p q, MonoidalProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
MonoidalProfunctor r =>
f s a -> g b t -> r a b -> r s t
powerGrateP f a b
f g b b
g Costar f b b
c

type PowerGrate (s :: k) (t :: k) a b = Optic (Prostrong PowerGrateFl) s t a b
type PowerGrate' s a = PowerGrate s s a a

-- | Distribute any 'MonoidalProfunctor' through a power grate (or any stronger optic). At the
-- hom @('~>')@ this is 'Proarrow.Optic.Setter.over'; at an applicative @'Proarrow.Profunctor.Instance.Star.Star' f@ the foci are
-- combined through @f@.
--
-- Accepts any encoding (cf. 'Proarrow.Optic.Traversal.traverseOf'), including '(%)'-composites.
powerGrateOf
  :: forall {k} c (s :: k) (t :: k) a b r
   . (Monoidal k, MonoidalProfunctor r, (Ob a, Ob b) => c (ExOptic PowerGrateFl a b))
  => Optic c s t a b -> r a b -> r s t
powerGrateOf :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) (r :: k -> k -> Type).
(Monoidal k, MonoidalProfunctor r,
 (Ob a, Ob b) => c (ExOptic PowerGrateFl a b)) =>
Optic c s t a b -> r a b -> r s t
powerGrateOf Optic c s t a b
o r a b
rab = forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @PowerGrateFl Optic c s t a b
o \p s a
l q b t
r -> p s a -> q b t -> r a b -> r s t
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(PowerGrateFl p q, MonoidalProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
MonoidalProfunctor r =>
p s a -> q b t -> r a b -> r s t
powerGrateP p s a
l q b t
r r a b
rab

-- * @n@-ary aggregation via tensor powers

-- | A Peano natural, the arity of a 'Pow' witness.
data Nat = Z | S Nat

-- | The @n@-fold tensor power of @a@: @a ** a ** ... ** a@ (@n@ times, terminated by 'Unit').
type Tensor :: Nat -> k -> k
type family Tensor n a where
  Tensor Z a = Unit
  Tensor (S n) a = a ** Tensor n a

-- | Case analysis on a type-level 'Nat': the single method from which every tensor-power
-- operation below is defined by recursion on @n@.
type KnownNat :: Nat -> Constraint
class KnownNat (n :: Nat) where
  natCase :: ((n ~ Z) => r) -> (forall m. (n ~ S m, KnownNat m) => r) -> r

instance KnownNat Z where
  natCase :: forall r.
(('Z ~ 'Z) => r)
-> (forall (m :: Nat). ('Z ~ 'S m, KnownNat m) => r) -> r
natCase ('Z ~ 'Z) => r
z forall (m :: Nat). ('Z ~ 'S m, KnownNat m) => r
_ = r
('Z ~ 'Z) => r
z
instance (KnownNat n) => KnownNat (S n) where
  natCase :: forall r.
(('S n ~ 'Z) => r)
-> (forall (m :: Nat). ('S n ~ 'S m, KnownNat m) => r) -> r
natCase ('S n ~ 'Z) => r
_ forall (m :: Nat). ('S n ~ 'S m, KnownNat m) => r
s = r
forall (m :: Nat). ('S n ~ 'S m, KnownNat m) => r
s

-- | Distribute a 'MonoidalProfunctor' over the @n@-fold tensor power, by combining @n@ copies of
-- the carrier value with 'one' (at 'Z') and '**' (at 'S') -- the profunctor-general heart of the
-- @n@-ary power grate.
powDist :: forall n r a b. (KnownNat n, MonoidalProfunctor r) => r a b -> r (Tensor n a) (Tensor n b)
powDist :: forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist r a b
rab = forall (n :: Nat) r.
KnownNat n =>
((n ~ 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S m, KnownNat m) => r) -> r
natCase @n r Unit Unit
r (Tensor n a) (Tensor n b)
(n ~ 'Z) => r (Tensor n a) (Tensor n b)
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one (\ @m -> r a b
rab r a b
-> r (Tensor m a) (Tensor m b)
-> r (a ** Tensor m a) (b ** Tensor m b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
r x1 x2 -> r y1 y2 -> r (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)
** forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @m r a b
rab)

-- | Collapse the @n@-fold tensor power of a monoid via 'mappend'\/'mempty'.
powFold :: forall n m. (KnownNat n, Monoid m) => Tensor n m ~> m
powFold :: forall {k} (n :: Nat) (m :: k).
(KnownNat n, Monoid m) =>
Tensor n m ~> m
powFold = forall (n :: Nat) r.
KnownNat n =>
((n ~ 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S m, KnownNat m) => r) -> r
natCase @n Unit ~> m
Tensor n m ~> m
(n ~ 'Z) => Tensor n m ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty (\ @p -> (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((m ** m) ~> m)
-> ((m ** Tensor m m) ~> (m ** m)) -> (m ** Tensor m m) ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((m ~> m
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id :: m ~> m) (m ~> m) -> (Tensor m m ~> m) -> (m ** Tensor m m) ~> (m ** m)
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)
** forall {k} (n :: Nat) (m :: k).
(KnownNat n, Monoid m) =>
Tensor n m ~> m
forall (n :: Nat) (m :: k).
(KnownNat n, Monoid m) =>
Tensor n m ~> m
powFold @p @m))

-- | @Tensor n a@ is an object whenever @a@ is.
withObTensor :: forall n k (a :: k) r. (KnownNat n, Monoidal k, Ob a) => ((Ob (Tensor n a)) => r) -> r
withObTensor :: forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor Ob (Tensor n a) => r
r = forall (n :: Nat) r.
KnownNat n =>
((n ~ 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S m, KnownNat m) => r) -> r
natCase @n r
(n ~ 'Z) => r
Ob (Tensor n a) => r
r (\ @m -> forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor @m @k @a (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @(Tensor m a) r
Ob (a ** Tensor m a) => r
Ob (Tensor n a) => r
r))

-- | Distribute the internal hom over the tensor power: split @x ~~> aⁿ@ into @(x ~~> a)ⁿ@ using
-- 'CopyDiscard' projections -- this is what makes an @n@-ary power grate a
-- 'Proarrow.Optic.Grate.Grate'.
splitPow
  :: forall n k (x :: k) a. (KnownNat n, Closed k, CopyDiscard k, Ob x, Ob a) => (x ~~> Tensor n a) ~> Tensor n (x ~~> a)
splitPow :: forall (n :: Nat) k (x :: k) (a :: k).
(KnownNat n, Closed k, CopyDiscard k, Ob x, Ob a) =>
(x ~~> Tensor n a) ~> Tensor n (x ~~> a)
splitPow =
  forall (n :: Nat) r.
KnownNat n =>
((n ~ 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S m, KnownNat m) => r) -> r
natCase @n
    (forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @x @Unit (forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @(x ~~> Unit)))
    ( \ @m ->
        forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor @m @k @a
          ((forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @a @(Tensor m a) ((a ** Tensor m a) ~> a)
-> (x ~> x) -> (x ~~> (a ** Tensor m a)) ~> (x ~~> a)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) ((x ~~> (a ** Tensor m a)) ~> (x ~~> a))
-> ((x ~~> (a ** Tensor m a)) ~> Tensor m (x ~~> a))
-> (x ~~> (a ** Tensor m a)) ~> ((x ~~> a) ** Tensor m (x ~~> a))
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& (forall (n :: Nat) k (x :: k) (a :: k).
(KnownNat n, Closed k, CopyDiscard k, Ob x, Ob a) =>
(x ~~> Tensor n a) ~> Tensor n (x ~~> a)
splitPow @m @k @x @a ((x ~~> Tensor m a) ~> Tensor m (x ~~> a))
-> ((x ~~> (a ** Tensor m a)) ~> (x ~~> Tensor m a))
-> (x ~~> (a ** Tensor m a)) ~> Tensor m (x ~~> a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @a @(Tensor m a) ((a ** Tensor m a) ~> Tensor m a)
-> (x ~> x) -> (x ~~> (a ** Tensor m a)) ~> (x ~~> Tensor m a)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x)))
    )

-- | Zip two tensor powers into the tensor power of the tensor: the @<*>@ of the reader
-- applicative @Tensor n@.
powZip
  :: forall n k (a :: k) c. (KnownNat n, SymMonoidal k, Ob a, Ob c) => (Tensor n a ** Tensor n c) ~> Tensor n (a ** c)
powZip :: forall (n :: Nat) k (a :: k) (c :: k).
(KnownNat n, SymMonoidal k, Ob a, Ob c) =>
(Tensor n a ** Tensor n c) ~> Tensor n (a ** c)
powZip =
  forall (n :: Nat) r.
KnownNat n =>
((n ~ 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S m, KnownNat m) => r) -> r
natCase @n
    (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @Unit)
    ( \ @m ->
        forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor @m @k @a
          (forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor @m @k @c (((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (c ~> c) -> (a ** c) ~> (a ** c)
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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c) ((a ** c) ~> (a ** c))
-> ((Tensor m a ** Tensor m c) ~> Tensor m (a ** c))
-> ((a ** c) ** (Tensor m a ** Tensor m c))
   ~> ((a ** c) ** Tensor m (a ** c))
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)
** forall (n :: Nat) k (a :: k) (c :: k).
(KnownNat n, SymMonoidal k, Ob a, Ob c) =>
(Tensor n a ** Tensor n c) ~> Tensor n (a ** c)
powZip @m @k @a @c) (((a ** c) ** (Tensor m a ** Tensor m c))
 ~> ((a ** c) ** Tensor m (a ** c)))
-> (((a ** Tensor m a) ** (c ** Tensor m c))
    ~> ((a ** c) ** (Tensor m a ** Tensor m c)))
-> ((a ** Tensor m a) ** (c ** Tensor m c))
   ~> ((a ** c) ** Tensor m (a ** c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @a @(Tensor m a) @c @(Tensor m c)))
    )

-- | @n@ copies of an object, via 'copy' and 'discard': the @pure@ of the reader applicative.
powCopy :: forall n k (a :: k). (KnownNat n, CopyDiscard k, Ob a) => a ~> Tensor n a
powCopy :: forall (n :: Nat) k (a :: k).
(KnownNat n, CopyDiscard k, Ob a) =>
a ~> Tensor n a
powCopy = forall (n :: Nat) r.
KnownNat n =>
((n ~ 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S m, KnownNat m) => r) -> r
natCase @n (forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @a) (\ @m -> (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> Tensor m a) -> (a ** a) ~> (a ** Tensor m a)
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)
** forall (n :: Nat) k (a :: k).
(KnownNat n, CopyDiscard k, Ob a) =>
a ~> Tensor n a
powCopy @m @k @a) ((a ** a) ~> (a ** Tensor m a))
-> (a ~> (a ** a)) -> a ~> (a ** Tensor m a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy @k @a)

-- | The tensor power of the unit is (isomorphic to) the unit.
powUnit :: forall n k. (KnownNat n, Monoidal k) => Unit ~> Tensor n (Unit :: k)
powUnit :: forall (n :: Nat) k.
(KnownNat n, Monoidal k) =>
Unit ~> Tensor n Unit
powUnit = forall (n :: Nat) r.
KnownNat n =>
((n ~ 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S m, KnownNat m) => r) -> r
natCase @n Unit ~> Unit
Unit ~> Tensor n Unit
(n ~ 'Z) => Unit ~> Tensor n Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (\ @m -> (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Unit :: k) (Unit ~> Unit)
-> (Unit ~> Tensor m Unit)
-> (Unit ** Unit) ~> (Unit ** Tensor m Unit)
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)
** forall (n :: Nat) k.
(KnownNat n, Monoidal k) =>
Unit ~> Tensor n Unit
powUnit @m @k) ((Unit ** Unit) ~> (Unit ** Tensor m Unit))
-> (Unit ~> (Unit ** Unit)) -> Unit ~> (Unit ** Tensor m Unit)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @Unit)

-- | The arity-@n@ aggregation witness: @s@ presents @n@ foci via the tensor power.
type Pow :: forall {k}. Nat -> k +-> k
data Pow n s a where
  Pow :: forall (n :: Nat) {k} (s :: k) (a :: k). (Ob a) => (s ~> Tensor n a) -> Pow n s a

-- | The dual of 'Pow': @t@ is rebuilt from @n@ foci.
type CoPow :: forall {k}. Nat -> k +-> k
data CoPow n b t where
  CoPow :: forall (n :: Nat) {k} (b :: k) (t :: k). (Ob b) => (Tensor n b ~> t) -> CoPow n b t

instance (Monoidal k, KnownNat n) => Profunctor (Pow n :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Pow n a b -> Pow n c d
dimap c ~> a
l b ~> d
r (Pow a ~> Tensor n b
sa) = (c ~> Tensor n d) -> Pow n c d
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow (forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n b ~> d
r (Tensor n b ~> Tensor n d) -> (c ~> Tensor n b) -> c ~> Tensor n d
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Tensor n b
sa (a ~> Tensor n b) -> (c ~> a) -> c ~> Tensor n b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l) ((Ob c, Ob a) => Pow n c d) -> (c ~> a) -> Pow n c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l ((Ob b, Ob d) => Pow n c d) -> (b ~> d) -> Pow n c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Pow n a b -> r
\\ Pow a ~> Tensor n b
sa = r
(Ob a, Ob b) => r
(Ob a, Ob (Tensor n b)) => r
r ((Ob a, Ob (Tensor n b)) => r) -> (a ~> Tensor n b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> Tensor n b
sa
instance (Monoidal k, KnownNat n) => Profunctor (CoPow n :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CoPow n a b -> CoPow n c d
dimap c ~> a
l b ~> d
r (CoPow Tensor n a ~> b
bt) = (Tensor n c ~> d) -> CoPow n c d
forall (n :: Nat) {k} (b :: k) (t :: k).
Ob b =>
(Tensor n b ~> t) -> CoPow n b t
CoPow (b ~> d
r (b ~> d) -> (Tensor n c ~> b) -> Tensor n c ~> d
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Tensor n a ~> b
bt (Tensor n a ~> b) -> (Tensor n c ~> Tensor n a) -> Tensor n c ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n c ~> a
l) ((Ob c, Ob a) => CoPow n c d) -> (c ~> a) -> CoPow n c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l ((Ob b, Ob d) => CoPow n c d) -> (b ~> d) -> CoPow n c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> CoPow n a b -> r
\\ CoPow Tensor n a ~> b
bt = r
(Ob a, Ob b) => r
(Ob (Tensor n a), Ob b) => r
r ((Ob (Tensor n a), Ob b) => r) -> (Tensor n a ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Tensor n a ~> b
bt

instance (Monoidal k, KnownNat n) => SetterFl (Pow n :: k +-> k) (CoPow n :: k +-> k) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Pow n s a -> CoPow n b t -> (a ~> b) -> s ~> t
overP (Pow s ~> Tensor n a
sl) (CoPow Tensor n b ~> t
rt) a ~> b
f = Tensor n b ~> t
rt (Tensor n b ~> t) -> (s ~> Tensor n b) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n a ~> b
f (Tensor n a ~> Tensor n b) -> (s ~> Tensor n a) -> s ~> Tensor n b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> Tensor n a
sl
instance (Monoidal k, KnownNat n) => FoldFl (Pow n :: k +-> k) (CoPow n :: k +-> k) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Pow n s a -> (a ~> m) -> s ~> m
foldMapP (Pow s ~> Tensor n a
sl) a ~> m
am = forall {k} (n :: Nat) (m :: k).
(KnownNat n, Monoid m) =>
Tensor n m ~> m
forall (n :: Nat) (m :: k).
(KnownNat n, Monoid m) =>
Tensor n m ~> m
powFold @n (Tensor n m ~> m) -> (s ~> Tensor n m) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n a ~> m
am (Tensor n a ~> Tensor n m) -> (s ~> Tensor n a) -> s ~> Tensor n m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> Tensor n a
sl
instance (Monoidal k, KnownNat n) => TravFl (Pow n :: k +-> k) (CoPow n :: k +-> k)
instance (Monoidal k, KnownNat n) => MonTravFl (Pow n :: k +-> k) (CoPow n :: k +-> k) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
Pow n s a -> CoPow n b t -> r a b -> r s t
monTravP (Pow s ~> Tensor n a
sl) (CoPow Tensor n b ~> t
rt) r a b
rab = (s ~> Tensor n a)
-> (Tensor n b ~> t) -> r (Tensor n a) (Tensor n b) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> Tensor n a
sl Tensor n b ~> t
rt (forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n r a b
rab)

-- | A power grate is a glass: ignore the source, and for each of the @n@ positions feed the
-- consumer the selector "project this focus". The selectors come from 'splitPow' of @sl@, the
-- consumer is copied @n@ times with 'powCopy', 'powZip' pairs them, and 'powDist' applies each.
-- Everything is stated with the 'CopyDiscard' structure that 'CCC' now provides, so the tensor
-- and the product never have to be identified by hand.
instance (Monoidal k, HasCoproducts k, KnownNat n) => GlassFl (Pow n :: k +-> k) (CoPow n :: k +-> k) where
  glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
CCC k =>
Pow n s a -> CoPow n b t -> (s && ((s ~~> a) ~~> b)) ~> t
glassP @s @a @b (Pow sl :: s ~> Tensor n a
sl@s ~> Tensor n a
Objs) (CoPow rt :: Tensor n b ~> t
rt@Tensor n b ~> t
Objs) =
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @a
      ( forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> a) @b
          ( forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @s @((s ~~> a) ~~> b)
              ( Tensor n b ~> t
rt
                  (Tensor n b ~> t)
-> ((s && ((s ~~> a) ~~> b)) ~> Tensor n b)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @(s ~~> a) @b)
                  (Tensor n (((s ~~> a) ~~> b) ** (s ~~> a)) ~> Tensor n b)
-> ((s && ((s ~~> a) ~~> b))
    ~> Tensor n (((s ~~> a) ~~> b) ** (s ~~> a)))
-> (s && ((s ~~> a) ~~> b)) ~> Tensor n b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) k (a :: k) (c :: k).
(KnownNat n, SymMonoidal k, Ob a, Ob c) =>
(Tensor n a ** Tensor n c) ~> Tensor n (a ** c)
powZip @n @k @((s ~~> a) ~~> b) @(s ~~> a)
                  ((Tensor n ((s ~~> a) ~~> b) ** Tensor n (s ~~> a))
 ~> Tensor n (((s ~~> a) ~~> b) ** (s ~~> a)))
-> ((s && ((s ~~> a) ~~> b))
    ~> (Tensor n ((s ~~> a) ~~> b) ** Tensor n (s ~~> a)))
-> (s && ((s ~~> a) ~~> b))
   ~> Tensor n (((s ~~> a) ~~> b) ** (s ~~> a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ( (forall (n :: Nat) k (a :: k).
(KnownNat n, CopyDiscard k, Ob a) =>
a ~> Tensor n a
powCopy @n @k @((s ~~> a) ~~> b) (((s ~~> a) ~~> b) ~> Tensor n ((s ~~> a) ~~> b))
-> ((s && ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> b))
-> (s && ((s ~~> a) ~~> b)) ~> Tensor n ((s ~~> a) ~~> b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @s @((s ~~> a) ~~> b))
                        ((s && ((s ~~> a) ~~> b)) ~> Tensor n ((s ~~> a) ~~> b))
-> ((s && ((s ~~> a) ~~> b)) ~> Tensor n (s ~~> a))
-> (s && ((s ~~> a) ~~> b))
   ~> (Tensor n ((s ~~> a) ~~> b) ** Tensor n (s ~~> a))
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& (forall (n :: Nat) k (x :: k) (a :: k).
(KnownNat n, Closed k, CopyDiscard k, Ob x, Ob a) =>
(x ~~> Tensor n a) ~> Tensor n (x ~~> a)
splitPow @n @k @s @a ((s ~~> Tensor n a) ~> Tensor n (s ~~> a))
-> ((s && ((s ~~> a) ~~> b)) ~> (s ~~> Tensor n a))
-> (s && ((s ~~> a) ~~> b)) ~> Tensor n (s ~~> a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (s ~> Tensor n a) -> Unit ~> (s ~~> Tensor n a)
forall {k} (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> (a ~~> b)
mkExponential s ~> Tensor n a
sl (TerminalObject ~> (s ~~> Tensor n a))
-> ((s && ((s ~~> a) ~~> b)) ~> TerminalObject)
-> (s && ((s ~~> a) ~~> b)) ~> (s ~~> Tensor n a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @(s ** ((s ~~> a) ~~> b)))
                    )
              )
          )
      )

instance (CopyDiscard k, HasCoproducts k, KnownNat n) => GrateFl (Pow n :: k +-> k) (CoPow n :: k +-> k) where
  zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
(Closed k, SymMonoidal k) =>
Pow n s a
-> CoPow n b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP (Pow @_ @_ @a s ~> Tensor n a
sl) (CoPow Tensor n b ~> t
rt) @x (x ~~> a) ~> b
kk = Tensor n b ~> t
rt (Tensor n b ~> t) -> ((x ~~> s) ~> Tensor n b) -> (x ~~> s) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n (x ~~> a) ~> b
kk (Tensor n (x ~~> a) ~> Tensor n b)
-> ((x ~~> s) ~> Tensor n (x ~~> a)) -> (x ~~> s) ~> Tensor n b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) k (x :: k) (a :: k).
(KnownNat n, Closed k, CopyDiscard k, Ob x, Ob a) =>
(x ~~> Tensor n a) ~> Tensor n (x ~~> a)
splitPow @n @_ @x @a ((x ~~> Tensor n a) ~> Tensor n (x ~~> a))
-> ((x ~~> s) ~> (x ~~> Tensor n a))
-> (x ~~> s) ~> Tensor n (x ~~> a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (s ~> Tensor n a
sl (s ~> Tensor n a) -> (x ~> x) -> (x ~~> s) ~> (x ~~> Tensor n a)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x)
instance (CopyDiscard k, HasCoproducts k, KnownNat n) => PowerGrateFl (Pow n :: k +-> k) (CoPow n :: k +-> k) where
  powerGrateP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
MonoidalProfunctor r =>
Pow n s a -> CoPow n b t -> r a b -> r s t
powerGrateP (Pow s ~> Tensor n a
sl) (CoPow Tensor n b ~> t
rt) r a b
rab = (s ~> Tensor n a)
-> (Tensor n b ~> t) -> r (Tensor n a) (Tensor n b) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> Tensor n a
sl Tensor n b ~> t
rt (forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n r a b
rab)

-- | @'Pow' n@ is the representable profunctor of the tensor power @Tensor n@, which is the reader
-- applicative for @n@ readers; the instances below make it a
-- 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor', hence a kaleidoscope
-- witness.
-- | A tensor power is a fixed-shape traversable: distribute the carrier over the @n@ copies.
instance (Monoidal k, KnownNat n) => Traversable (Pow n :: k +-> k) where
  traverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(Pow n :.: p) :~> (p :.: Pow n)
traverse @_ @_ @b (Pow a ~> Tensor n b
f :.: p b b
p) = p b b
p p b b
-> ((Ob b, Ob b) => (:.:) p (Pow n) a b) -> (:.:) p (Pow n) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor @n @k @b ((a ~> Tensor n b)
-> p (Tensor n b) (Tensor n b) -> p a (Tensor n b)
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> Tensor n b
f (forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n p b b
p) p a (Tensor n b) -> Pow n (Tensor n b) b -> (:.:) p (Pow n) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (Tensor n b ~> Tensor n b) -> Pow n (Tensor n b) b
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow Tensor n b ~> Tensor n b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

instance (Monoidal k, KnownNat n) => Representable (Pow n :: k +-> k) where
  type Pow n % a = Tensor n a
  index :: forall (a :: k) (b :: k). Pow n a b -> a ~> (Pow n % b)
index (Pow a ~> Tensor n b
f) = a ~> (Pow n % b)
a ~> Tensor n b
f
  tabulate :: forall (b :: k) (a :: k). Ob b => (a ~> (Pow n % b)) -> Pow n a b
tabulate = (a ~> (Pow n % b)) -> Pow n a b
(a ~> Tensor n b) -> Pow n a b
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow
  repMap :: forall (a :: k) (b :: k). (a ~> b) -> (Pow n % a) ~> (Pow n % b)
repMap = forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n

instance (SymMonoidal k, KnownNat n) => MonoidalProfunctor (Pow n :: k +-> k) where
  one :: Pow n Unit Unit
one = (Unit ~> Tensor n Unit) -> Pow n Unit Unit
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow (forall (n :: Nat) k.
(KnownNat n, Monoidal k) =>
Unit ~> Tensor n Unit
powUnit @n)
  Pow @_ @_ @a x1 ~> Tensor n x2
f ** :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Pow n x1 x2 -> Pow n y1 y2 -> Pow n (x1 ** y1) (x2 ** y2)
** Pow @_ @_ @c y1 ~> Tensor n y2
g = x1 ~> Tensor n x2
f (x1 ~> Tensor n x2)
-> ((Ob x1, Ob (Tensor n x2)) => Pow n (x1 ** y1) (x2 ** y2))
-> Pow n (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// y1 ~> Tensor n y2
g (y1 ~> Tensor n y2)
-> ((Ob y1, Ob (Tensor n y2)) => Pow n (x1 ** y1) (x2 ** y2))
-> Pow n (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @c (((x1 ** y1) ~> Tensor n (x2 ** y2)) -> Pow n (x1 ** y1) (x2 ** y2)
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow (forall (n :: Nat) k (a :: k) (c :: k).
(KnownNat n, SymMonoidal k, Ob a, Ob c) =>
(Tensor n a ** Tensor n c) ~> Tensor n (a ** c)
powZip @n @k @a @c ((Tensor n x2 ** Tensor n y2) ~> Tensor n (x2 ** y2))
-> ((x1 ** y1) ~> (Tensor n x2 ** Tensor n y2))
-> (x1 ** y1) ~> Tensor n (x2 ** y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x1 ~> Tensor n x2
f (x1 ~> Tensor n x2)
-> (y1 ~> Tensor n y2)
-> (x1 ** y1) ~> (Tensor n x2 ** Tensor n 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)
** y1 ~> Tensor n y2
g)))
instance (SymMonoidal k, HasCoproducts k, KnownNat n) => MonoidalProfunctor (Coprod (Pow n :: k +-> k)) where
  one :: Coprod (Pow n) Unit Unit
one = forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor @n @k @InitialObject (Pow n InitialObject InitialObject
-> Coprod (Pow n) ('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 ~> Tensor n InitialObject)
-> Pow n InitialObject InitialObject
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow InitialObject ~> Tensor n InitialObject
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate))
  Coprod (Pow @_ @_ @a a1 ~> Tensor n b1
f) ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (Pow n) x1 x2
-> Coprod (Pow n) y1 y2 -> Coprod (Pow n) (x1 ** y1) (x2 ** y2)
** Coprod (Pow @_ @_ @c a1 ~> Tensor n b1
g) =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @c (Pow n (a1 || a1) (b1 || b1)
-> Coprod (Pow n) ('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) ~> Tensor n (b1 || b1)) -> Pow n (a1 || a1) (b1 || b1)
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow (forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @c) (Tensor n b1 ~> Tensor n (b1 || b1))
-> (a1 ~> Tensor n b1) -> a1 ~> Tensor n (b1 || b1)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> Tensor n b1
f (a1 ~> Tensor n (b1 || b1))
-> (a1 ~> Tensor n (b1 || b1)) -> (a1 || a1) ~> Tensor n (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
||| forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @c) (Tensor n b1 ~> Tensor n (b1 || b1))
-> (a1 ~> Tensor n b1) -> a1 ~> Tensor n (b1 || b1)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> Tensor n b1
g)))
instance (CopyDiscard k, KnownNat n) => Strong M.Tensor (Pow n :: k +-> k) where
  act :: forall (a :: k) (x :: k) (y :: k).
Ob a =>
Pow n x y -> Pow n (Act Tensor a x) (Act Tensor a y)
act @x (Pow @_ @_ @a x ~> Tensor n y
f) = x ~> Tensor n y
f (x ~> Tensor n y)
-> ((Ob x, Ob (Tensor n y)) => Pow n (a ** x) (a ** y))
-> Pow n (a ** x) (a ** y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x @a (((a ** x) ~> Tensor n (a ** y)) -> Pow n (a ** x) (a ** y)
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow (forall (n :: Nat) k (a :: k) (c :: k).
(KnownNat n, SymMonoidal k, Ob a, Ob c) =>
(Tensor n a ** Tensor n c) ~> Tensor n (a ** c)
powZip @n @k @x @a ((Tensor n a ** Tensor n y) ~> Tensor n (a ** y))
-> ((a ** x) ~> (Tensor n a ** Tensor n y))
-> (a ** x) ~> Tensor n (a ** y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (n :: Nat) k (a :: k).
(KnownNat n, CopyDiscard k, Ob a) =>
a ~> Tensor n a
powCopy @n @k @x (a ~> Tensor n a)
-> (x ~> Tensor n y) -> (a ** x) ~> (Tensor n a ** Tensor n y)
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)
** x ~> Tensor n y
f)))
instance (CopyDiscard k, HasCoproducts k, KnownNat n) => Strong CoprodAction (Pow n :: k +-> k) where
  act :: forall (a :: COPROD k) (x :: k) (y :: k).
Ob a =>
Pow n x y -> Pow n (Act CoprodAction a x) (Act CoprodAction a y)
act @(COPR x) (Pow @_ @_ @a x ~> Tensor n y
f) =
    x ~> Tensor n y
f (x ~> Tensor n y)
-> ((Ob x, Ob (Tensor n y)) =>
    Pow n (UN 'COPR a || x) (UN 'COPR a || y))
-> Pow n (UN 'COPR a || x) (UN 'COPR a || y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @x @a (((UN 'COPR a || x) ~> Tensor n (UN 'COPR a || y))
-> Pow n (UN 'COPR a || x) (UN 'COPR a || y)
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow (forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @x @a) (Tensor n (UN 'COPR a) ~> Tensor n (UN 'COPR a || y))
-> (UN 'COPR a ~> Tensor n (UN 'COPR a))
-> UN 'COPR a ~> Tensor n (UN 'COPR a || y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) k (a :: k).
(KnownNat n, CopyDiscard k, Ob a) =>
a ~> Tensor n a
powCopy @n @k @x (UN 'COPR a ~> Tensor n (UN 'COPR a || y))
-> (x ~> Tensor n (UN 'COPR a || y))
-> (UN 'COPR a || x) ~> Tensor n (UN 'COPR a || y)
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
||| forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @x @a) (Tensor n y ~> Tensor n (UN 'COPR a || y))
-> (x ~> Tensor n y) -> x ~> Tensor n (UN 'COPR a || y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> Tensor n y
f))
instance (CopyDiscard k, HasCoproducts k, KnownNat n) => CotravFl (Pow n :: k +-> k) (CoPow n :: k +-> k)
instance (CopyDiscard k, HasCoproducts k, KnownNat n) => KaleidoFl (Pow n :: k +-> k) (CoPow n :: k +-> k) where
  kaleidoP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
Kaleidoscopic r =>
Pow n s a -> CoPow n b t -> r a b -> r s t
kaleidoP (Pow s ~> Tensor n a
sl) (CoPow Tensor n b ~> t
rt) r a b
rab = (s ~> Tensor n a)
-> (Tensor n b ~> t) -> r (Tensor n a) (Tensor n b) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> Tensor n a
sl Tensor n b ~> t
rt (forall {k} (r :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Kaleidoscopic r, Representable p,
 StrongDistributiveProfunctor p) =>
r a b -> r (p % a) (p % b)
forall (r :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Kaleidoscopic r, Representable p,
 StrongDistributiveProfunctor p) =>
r a b -> r (p % a) (p % b)
kaleidoAct @_ @(Pow n) r a b
rab)
instance (Monoidal k, KnownNat n) => Proadjunction (Pow n :: k +-> k) (CoPow n) where
  unit :: forall (a :: k). Ob a => (:.:) (CoPow n) (Pow n) a a
unit @x = ((Tensor n a ~> Tensor n a) -> CoPow n a (Tensor n a)
forall (n :: Nat) {k} (b :: k) (t :: k).
Ob b =>
(Tensor n b ~> t) -> CoPow n b t
CoPow Tensor n a ~> Tensor n a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id CoPow n a (Tensor n a)
-> Pow n (Tensor n a) a -> (:.:) (CoPow n) (Pow n) a a
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (Tensor n a ~> Tensor n a) -> Pow n (Tensor n a) a
forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow Tensor n a ~> Tensor n a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob (Tensor n a), Ob (Tensor n a)) => (:.:) (CoPow n) (Pow n) a a)
-> (Tensor n a ~> Tensor n a) -> (:.:) (CoPow n) (Pow n) a a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {k} {k} (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
forall (n :: Nat) (r :: k +-> k) (a :: k) (b :: k).
(KnownNat n, MonoidalProfunctor r) =>
r a b -> r (Tensor n a) (Tensor n b)
powDist @n (a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id :: x ~> x)
  counit :: (Pow n :.: CoPow n) :~> (~>)
counit (Pow a ~> Tensor n b
sl :.: CoPow Tensor n b ~> b
rt) = Tensor n b ~> b
rt (Tensor n b ~> b) -> (a ~> Tensor n b) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Tensor n b
sl

-- | Build an @n@-ary power grate from a tensor-power decomposition of @s@ and recomposition
-- of @t@.
powerGrate
  :: forall {k} (n :: Nat) (s :: k) (t :: k) a b
   . (CopyDiscard k, HasCoproducts k, KnownNat n, Ob a, Ob b)
  => (s ~> Tensor n a) -> (Tensor n b ~> t) -> PowerGrate s t a b
powerGrate :: forall {k} (n :: Nat) (s :: k) (t :: k) (a :: k) (b :: k).
(CopyDiscard k, HasCoproducts k, KnownNat n, Ob a, Ob b) =>
(s ~> Tensor n a) -> (Tensor n b ~> t) -> PowerGrate s t a b
powerGrate s ~> Tensor n a
sl Tensor n b ~> t
rt = forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @PowerGrateFl (forall (n :: Nat) {k} (s :: k) (a :: k).
Ob a =>
(s ~> Tensor n a) -> Pow n s a
Pow @n s ~> Tensor n a
sl) (forall (n :: Nat) {k} (b :: k) (t :: k).
Ob b =>
(Tensor n b ~> t) -> CoPow n b t
CoPow @n Tensor n b ~> t
rt)

-- | Zip two sources through a 'Proarrow.Optic.Kaleidoscope.Kaleidoscope' (or any stronger optic, a
-- 'Proarrow.Optic.Grate.Grate' in particular, in any encoding): combine the foci pairwise. This is
-- 'kaleidoscopeOf' at the carrier @'RepCostar' ('Pow' 2)@, the costar of the binary tensor power --
-- a binary combination @(a ** a) ~> b@ of foci, which the optic's applicative lifts by @liftA2@.
zipWithOf
  :: forall {k} c (s :: k) (t :: k) a b
   . (Monoidal k, Ob a, (Ob a, Ob b) => c (ExOptic KaleidoFl a b))
  => Optic c s t a b -> ((a ** a) ~> b) -> (s ** s) ~> t
zipWithOf :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Monoidal k, Ob a, (Ob a, Ob b) => c (ExOptic KaleidoFl a b)) =>
Optic c s t a b -> ((a ** a) ~> b) -> (s ** s) ~> t
zipWithOf Optic c s t a b
o (a ** a) ~> b
f =
  case Optic c s t a b
-> RepCostar (Pow ('S ('S 'Z))) a b
-> RepCostar (Pow ('S ('S 'Z))) s t
forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) (r :: k -> k -> Type).
(CategoryOf k, Kaleidoscopic r,
 (Ob a, Ob b) => c (ExOptic KaleidoFl a b)) =>
Optic c s t a b -> r a b -> r s t
kaleidoscopeOf Optic c s t a b
o (forall (a :: k) (p :: k +-> k) (b :: k).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar @_ @(Pow (S (S Z))) ((a ** a) ~> b
f ((a ** a) ~> b)
-> ((a ** (a ** Unit)) ~> (a ** a)) -> (a ** (a ** Unit)) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> ((a ** Unit) ~> a) -> (a ** (a ** Unit)) ~> (a ** a)
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)
** forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @a))) of
    RepCostar @s' (Pow ('S ('S 'Z)) % s) ~> t
g -> (Pow ('S ('S 'Z)) % s) ~> t
(s ** (s ** Unit)) ~> t
g ((s ** (s ** Unit)) ~> t)
-> ((s ** s) ~> (s ** (s ** Unit))) -> (s ** s) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @s' Obj s -> (s ~> (s ** Unit)) -> (s ** s) ~> (s ** (s ** Unit))
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)
** forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @k @s')