{-# LANGUAGE AllowAmbiguousTypes #-}

-- | A __kaleidoscope__ is the optic that distributes an arbitrary 'MonoidalProfunctor' -- the
-- @Applicative@\/zip structure ('one' and '**') -- rather than the full
-- 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor' a
-- 'Proarrow.Optic.Traversal.Traversal' needs. Where a
-- traversal /decomposes/ a whole into its foci, a kaleidoscope /also aggregates/: it can combine
-- the foci with @**@ (and 'one' for the empty case), not just replace them.
--
-- The witnesses here ('Two', 'Pow' @n@) present @s@ as a fixed tensor /power/ of the focus
-- (@s ~> a ** ... ** a@), which is a genuine decomposition -- so this kaleidoscope is really a
-- __fixed-arity 'Proarrow.Optic.Traversal.Traversal'__ (@'KaleidoRes' <: 'TravRes'@, so it
-- folds and sets like any traversal). Its /distinctive/ power is that 'kaleidoP' distributes an
-- arbitrary 'MonoidalProfunctor', including the non-'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor' ones (e.g.
-- @Costar f@) a traversal can't touch -- that is where the aggregation lives.
--
-- Crucially the aggregation is stated over an abstract @'MonoidalProfunctor' r@, /not/ the
-- Hask-specific @Costar f = f a -> b@: 'kaleidoscopeOf' 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@).
--
-- Two witness families are provided: @'Two'@ (the ergonomic binary case, @s ~> a ** a@) and the
-- general @'Pow' n@ (the @n@-fold tensor power @s ~> 'Tensor' n a@, for any Peano 'Nat' arity),
-- alongside 'Id' (unary) and composition. @'Two'@ is @'Pow'@ at arity two up to the right
-- unitor.
module Proarrow.Optic.Kaleidoscope
  ( KaleidoRes (..)
  , Kaleidoscope
  , Kaleidoscope'
  , Two (..)
  , CoTwo (..)
  , kaleidoscope
  , kaleidoscopeOf

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

import Data.Kind (Constraint)
import Proarrow.Adjunction (Proadjunction (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), type (**))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard, discard, fst, snd, (&&&))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (\\), type (+->))
import Proarrow.Monoid (Monoid (..))
import Proarrow.Optic
  ( CompactFlavor
  , ExOptic (..)
  , FLAVOR
  , Optic
  , Prostrong (..)
  , SubFlavor (..)
  , convert
  , ex2prof
  , withLegs
  )
import Proarrow.Optic.Fold (FoldRes (..))
import Proarrow.Optic.Grate (GrateRes (..))
import Proarrow.Optic.Setter (SetterRes (..))
import Proarrow.Optic.Traversal (MonTravRes (..), TravRes (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))

-- | The kaleidoscope flavor: distribute any 'MonoidalProfunctor' @r@ through the witness pair.
-- 'Proarrow.Optic.Traversal.TravRes' is a superclass: every kaleidoscope witness is a traversal
-- witness (instantiate @r@ at a 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor', a special 'MonoidalProfunctor'),
-- so a kaleidoscope folds, sets, and traverses. The extra power is distributing the /non/-SDP
-- monoidal profunctors as well.
type KaleidoRes :: forall {k}. FLAVOR k k
class (MonTravRes p q, GrateRes p q) => KaleidoRes (p :: k +-> k) (q :: k +-> k) where
  kaleidoP :: (MonoidalProfunctor r) => p s a -> q b t -> r a b -> r s t

instance (CategoryOf k) => KaleidoRes (Id :: k +-> k) (Id :: k +-> k) where
  kaleidoP :: 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
kaleidoP (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 (KaleidoRes f g, KaleidoRes f' g') => KaleidoRes (f :.: f') (g' :.: g) where
  kaleidoP :: 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
kaleidoP (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).
(KaleidoRes 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).
(KaleidoRes p q, MonoidalProfunctor r) =>
p s a -> q b t -> r a b -> r s t
kaleidoP @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).
(KaleidoRes 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).
(KaleidoRes p q, MonoidalProfunctor r) =>
p s a -> q b t -> r a b -> r s t
kaleidoP @f' @g' f' b a
f' g' b b
g'

-- | The binary aggregation witness: @s@ presents two foci via the tensor.
type Two :: forall {k}. k +-> k
data Two s a where
  Two :: (Ob a) => (s ~> (a ** a)) -> Two s a

-- | The dual of 'Two': @t@ is rebuilt from two foci via the tensor.
type CoTwo :: forall {k}. k +-> k
data CoTwo b t where
  CoTwo :: (Ob b) => ((b ** b) ~> t) -> CoTwo b t

instance (Monoidal k) => Profunctor (Two :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Two a b -> Two c d
dimap c ~> a
l b ~> d
r (Two a ~> (b ** b)
sa) = (c ~> (d ** d)) -> Two c d
forall {k} (a :: k) (s :: k). Ob a => (s ~> (a ** a)) -> Two s a
Two ((b ~> d
r (b ~> d) -> (b ~> d) -> (b ** b) ~> (d ** d)
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)
** b ~> d
r) ((b ** b) ~> (d ** d)) -> (c ~> (b ** b)) -> c ~> (d ** 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 ~> (b ** b)
sa (a ~> (b ** b)) -> (c ~> a) -> c ~> (b ** 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) => Two c d) -> (c ~> a) -> Two 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) => Two c d) -> (b ~> d) -> Two 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) -> Two a b -> r
\\ Two a ~> (b ** b)
sa = r
(Ob a, Ob b) => r
(Ob a, Ob (b ** b)) => r
r ((Ob a, Ob (b ** b)) => r) -> (a ~> (b ** 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 ~> (b ** b)
sa
instance (Monoidal k) => Profunctor (CoTwo :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CoTwo a b -> CoTwo c d
dimap c ~> a
l b ~> d
r (CoTwo (a ** a) ~> b
bt) = ((c ** c) ~> d) -> CoTwo c d
forall {k} (b :: k) (t :: k). Ob b => ((b ** b) ~> t) -> CoTwo b t
CoTwo (b ~> d
r (b ~> d) -> ((c ** c) ~> b) -> (c ** 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
. (a ** a) ~> b
bt ((a ** a) ~> b) -> ((c ** c) ~> (a ** a)) -> (c ** 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
. (c ~> a
l (c ~> a) -> (c ~> a) -> (c ** c) ~> (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)
** c ~> a
l)) ((Ob c, Ob a) => CoTwo c d) -> (c ~> a) -> CoTwo 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) => CoTwo c d) -> (b ~> d) -> CoTwo 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) -> CoTwo a b -> r
\\ CoTwo (a ** a) ~> b
bt = r
(Ob a, Ob b) => r
(Ob (a ** a), Ob b) => r
r ((Ob (a ** a), Ob b) => r) -> ((a ** 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
\\ (a ** a) ~> b
bt

instance (Monoidal k) => SetterRes (Two :: k +-> k) (CoTwo :: k +-> k) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Two s a -> CoTwo b t -> (a ~> b) -> s ~> t
overP (Two s ~> (a ** a)
sl) (CoTwo (b ** b) ~> t
rt) a ~> b
f = (b ** b) ~> t
rt ((b ** b) ~> t) -> (s ~> (b ** 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
. (a ~> b
f (a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** 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)
** a ~> b
f) ((a ** a) ~> (b ** b)) -> (s ~> (a ** a)) -> s ~> (b ** 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 ~> (a ** a)
sl
instance (Monoidal k) => FoldRes (Two :: k +-> k) (CoTwo :: k +-> k) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Two s a -> (a ~> m) -> s ~> m
foldMapP (Two s ~> (a ** a)
sl) a ~> m
am = (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((m ** m) ~> m) -> (s ~> (m ** 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
. (a ~> m
am (a ~> m) -> (a ~> m) -> (a ** a) ~> (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)
** a ~> m
am) ((a ** a) ~> (m ** m)) -> (s ~> (a ** a)) -> s ~> (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
. s ~> (a ** a)
sl
instance (Monoidal k) => TravRes (Two :: k +-> k) (CoTwo :: k +-> k)
instance (Monoidal k) => MonTravRes (Two :: k +-> k) (CoTwo :: k +-> k) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
Two s a -> CoTwo b t -> r a b -> r s t
monTravP (Two s ~> (a ** a)
sl) (CoTwo (b ** b) ~> t
rt) r a b
rab = (s ~> (a ** a)) -> ((b ** b) ~> t) -> r (a ** a) (b ** 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 ** a)
sl (b ** b) ~> t
rt (r a b
rab r a b -> r a b -> r (a ** a) (b ** 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)
** r a b
rab)
instance (CopyDiscard k) => GrateRes (Two :: k +-> k) (CoTwo :: k +-> k) where
  zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
(Closed k, SymMonoidal k) =>
Two s a
-> CoTwo b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP (Two @a s ~> (a ** a)
sl) (CoTwo (b ** b) ~> t
rt) @x (x ~~> a) ~> b
kk = (b ** b) ~> t
rt ((b ** b) ~> t) -> ((x ~~> s) ~> (b ** 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
. ((x ~~> a) ~> b
kk ((x ~~> a) ~> b)
-> ((x ~~> a) ~> b) -> ((x ~~> a) ** (x ~~> a)) ~> (b ** 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)
** (x ~~> a) ~> b
kk) (((x ~~> a) ** (x ~~> a)) ~> (b ** b))
-> ((x ~~> s) ~> ((x ~~> a) ** (x ~~> a))) -> (x ~~> s) ~> (b ** 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) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @a @a ((a ** a) ~> a) -> (x ~> x) -> (x ~~> (a ** 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 ** a)) ~> (x ~~> a))
-> ((x ~~> (a ** a)) ~> (x ~~> a))
-> (x ~~> (a ** a)) ~> ((x ~~> a) ** (x ~~> a))
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& (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 @a ((a ** a) ~> a) -> (x ~> x) -> (x ~~> (a ** 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 ** a)) ~> ((x ~~> a) ** (x ~~> a)))
-> ((x ~~> s) ~> (x ~~> (a ** a)))
-> (x ~~> s) ~> ((x ~~> a) ** (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 ~> (a ** a)
sl (s ~> (a ** a)) -> (x ~> x) -> (x ~~> s) ~> (x ~~> (a ** 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) => KaleidoRes (Two :: k +-> k) (CoTwo :: k +-> k) where
  kaleidoP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
MonoidalProfunctor r =>
Two s a -> CoTwo b t -> r a b -> r s t
kaleidoP (Two s ~> (a ** a)
sl) (CoTwo (b ** b) ~> t
rt) r a b
rab = (s ~> (a ** a)) -> ((b ** b) ~> t) -> r (a ** a) (b ** 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 ** a)
sl (b ** b) ~> t
rt (r a b
rab r a b -> r a b -> r (a ** a) (b ** 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)
** r a b
rab)
instance (Monoidal k) => Proadjunction (Two :: k +-> k) CoTwo where
  unit :: forall (a :: k). Ob a => (:.:) CoTwo Two a a
unit @x = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x @x (((a ** a) ~> (a ** a)) -> CoTwo a (a ** a)
forall {k} (b :: k) (t :: k). Ob b => ((b ** b) ~> t) -> CoTwo b t
CoTwo (a ** a) ~> (a ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id CoTwo a (a ** a) -> Two (a ** a) a -> (:.:) CoTwo Two 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
:.: ((a ** a) ~> (a ** a)) -> Two (a ** a) a
forall {k} (a :: k) (s :: k). Ob a => (s ~> (a ** a)) -> Two s a
Two (a ** a) ~> (a ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  counit :: (Two :.: CoTwo) :~> (~>)
counit (Two a ~> (b ** b)
sl :.: CoTwo (b ** b) ~> b
rt) = (b ** b) ~> b
rt ((b ** b) ~> b) -> (a ~> (b ** 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 ~> (b ** b)
sl

instance CompactFlavor KaleidoRes

instance SubFlavor KaleidoRes MonTravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
KaleidoRes p q =>
(MonTravRes p q => r) -> r
subFlavor MonTravRes p q => r
r = r
MonTravRes p q => r
r
instance SubFlavor KaleidoRes GrateRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
KaleidoRes p q =>
(GrateRes p q => r) -> r
subFlavor GrateRes p q => r
r = r
GrateRes p q => r
r
instance SubFlavor KaleidoRes TravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
KaleidoRes p q =>
(TravRes p q => r) -> r
subFlavor TravRes p q => r
r = r
TravRes p q => r
r
instance SubFlavor KaleidoRes FoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
KaleidoRes p q =>
(FoldRes p q => r) -> r
subFlavor FoldRes p q => r
r = r
FoldRes p q => r
r
instance SubFlavor KaleidoRes SetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
KaleidoRes p q =>
(SetterRes p q => r) -> r
subFlavor SetterRes p q => r
r = r
SetterRes p q => r
r

type Kaleidoscope (s :: k) (t :: k) a b = Optic (Prostrong KaleidoRes) s t a b
type Kaleidoscope' s a = Kaleidoscope s s a a

-- | Build a binary kaleidoscope from a tensor decomposition of @s@ and recomposition of @t@.
kaleidoscope
  :: forall {k} (s :: k) (t :: k) a b
   . (CopyDiscard k, Ob a, Ob b)
  => (s ~> (a ** a)) -> ((b ** b) ~> t) -> Kaleidoscope s t a b
kaleidoscope :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(s ~> (a ** a)) -> ((b ** b) ~> t) -> Kaleidoscope s t a b
kaleidoscope s ~> (a ** a)
sl (b ** b) ~> t
rt = ExOptic KaleidoRes a b s t -> Optic (Prostrong KaleidoRes) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof ((:.:) (Two :.: ExOptic KaleidoRes a b) CoTwo s t
-> ExOptic KaleidoRes a b s t
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong ((s ~> (a ** a)) -> Two s a
forall {k} (a :: k) (s :: k). Ob a => (s ~> (a ** a)) -> Two s a
Two s ~> (a ** a)
sl Two s a
-> ExOptic KaleidoRes a b a b
-> (:.:) Two (ExOptic KaleidoRes a b) s 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
:.: (a ~> a) -> (b ~> b) -> ExOptic KaleidoRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) Two (ExOptic KaleidoRes a b) s b
-> CoTwo b t -> (:.:) (Two :.: ExOptic KaleidoRes a b) CoTwo s t
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
:.: ((b ** b) ~> t) -> CoTwo b t
forall {k} (b :: k) (t :: k). Ob b => ((b ** b) ~> t) -> CoTwo b t
CoTwo (b ** b) ~> t
rt))

-- | Distribute any 'MonoidalProfunctor' through a kaleidoscope (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@.
kaleidoscopeOf
  :: forall {k} w (s :: k) (t :: k) a b r
   . (Monoidal k, MonoidalProfunctor r, SubFlavor w KaleidoRes)
  => Optic (Prostrong w) s t a b -> r a b -> r s t
kaleidoscopeOf :: forall {k} (w :: FLAVOR k k) (s :: k) (t :: k) (a :: k) (b :: k)
       (r :: k +-> k).
(Monoidal k, MonoidalProfunctor r, SubFlavor w KaleidoRes) =>
Optic (Prostrong w) s t a b -> r a b -> r s t
kaleidoscopeOf Optic (Prostrong w) s t a b
o r a b
rab = (forall (p :: k +-> k) (q :: k +-> k).
 (KaleidoRes p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r s t)
-> Optic (Prostrong KaleidoRes) s t a b -> r s t
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs (\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).
(KaleidoRes 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
kaleidoP p s a
l q b t
r r a b
rab) (forall {j} {k} (c :: (k -> j -> Type) -> Constraint)
       (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
forall (c :: (k +-> k) -> Constraint) (w :: FLAVOR k k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
convert @(Prostrong w) @KaleidoRes Optic (Prostrong w) s t a b
o)

-- * @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

-- | 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 kaleidoscope.
type KnownNat :: Nat -> Constraint
class KnownNat (n :: Nat) where
  powDist :: (MonoidalProfunctor r) => r a b -> r (Tensor n a) (Tensor n b)

  -- | Collapse the @n@-fold tensor power of a monoid via 'mappend'\/'mempty'.
  powFold :: (Monoid m) => Tensor n m ~> m

  -- | Distribute the internal hom over the tensor power: split @x ~~> aⁿ@ into @(x ~~> a)ⁿ@ using
  -- 'CopyDiscard' projections. The @n@-fold form of the 'Two' split -- this is what makes an
  -- @n@-ary kaleidoscope a 'Proarrow.Optic.Grate.Grate'.
  splitPow :: forall k (x :: k) a. (Closed k, CopyDiscard k, Ob x, Ob a) => (x ~~> Tensor n a) ~> Tensor n (x ~~> a)

  -- | @Tensor n a@ is an object whenever @a@ is.
  withObTensor :: forall k (a :: k) r. (Monoidal k, Ob a) => ((Ob (Tensor n a)) => r) -> r

instance KnownNat Z where
  powDist :: forall {k} {k} (r :: k +-> k) (a :: k) (b :: k).
MonoidalProfunctor r =>
r a b -> r (Tensor 'Z a) (Tensor 'Z b)
powDist r a b
_ = r Unit Unit
r (Tensor 'Z a) (Tensor 'Z b)
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  powFold :: forall {k} (m :: k). Monoid m => Tensor 'Z m ~> m
powFold = Unit ~> m
Tensor 'Z m ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  splitPow :: forall k (x :: k) (a :: k).
(Closed k, CopyDiscard k, Ob x, Ob a) =>
(x ~~> Tensor 'Z a) ~> Tensor 'Z (x ~~> a)
splitPow @k @x = 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))
  withObTensor :: forall k (a :: k) r.
(Monoidal k, Ob a) =>
(Ob (Tensor 'Z a) => r) -> r
withObTensor Ob (Tensor 'Z a) => r
r = r
Ob (Tensor 'Z a) => r
r
instance (KnownNat n) => KnownNat (S n) where
  powDist :: forall {k} {k} (r :: k +-> k) (a :: k) (b :: k).
MonoidalProfunctor r =>
r a b -> r (Tensor ('S n) a) (Tensor ('S n) b)
powDist r a b
rab = r a b
rab r a b
-> r (Tensor n a) (Tensor n b)
-> r (a ** Tensor n a) (b ** Tensor n 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 (n :: Nat) {k} {k} (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
  powFold :: forall {k} (m :: k). Monoid m => Tensor ('S n) m ~> m
powFold @m = (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((m ** m) ~> m)
-> ((m ** Tensor n m) ~> (m ** m)) -> (m ** Tensor n 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 n m ~> m) -> (m ** Tensor n 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 (n :: Nat) {k} (m :: k).
(KnownNat n, Monoid m) =>
Tensor n m ~> m
powFold @n @m)
  splitPow :: forall k (x :: k) (a :: k).
(Closed k, CopyDiscard k, Ob x, Ob a) =>
(x ~~> Tensor ('S n) a) ~> Tensor ('S n) (x ~~> a)
splitPow @k @x @a =
    forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor @n @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 n a) ((a ** Tensor n a) ~> a)
-> (x ~> x) -> (x ~~> (a ** Tensor n 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 n a)) ~> (x ~~> a))
-> ((x ~~> (a ** Tensor n a)) ~> Tensor n (x ~~> a))
-> (x ~~> (a ** Tensor n a)) ~> ((x ~~> a) ** Tensor n (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 @n @k @x @a ((x ~~> Tensor n a) ~> Tensor n (x ~~> a))
-> ((x ~~> (a ** Tensor n a)) ~> (x ~~> Tensor n a))
-> (x ~~> (a ** Tensor n a)) ~> 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
. (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 n a) ((a ** Tensor n a) ~> Tensor n a)
-> (x ~> x) -> (x ~~> (a ** Tensor n a)) ~> (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)))
  withObTensor :: forall k (a :: k) r.
(Monoidal k, Ob a) =>
(Ob (Tensor ('S n) a) => r) -> r
withObTensor @k @a Ob (Tensor ('S n) a) => r
r = forall (n :: Nat) k (a :: k) r.
(KnownNat n, Monoidal k, Ob a) =>
(Ob (Tensor n a) => r) -> r
withObTensor @n @k @a (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @(Tensor n a) r
Ob (a ** Tensor n a) => r
Ob (Tensor ('S n) a) => r
r)

-- | 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 (n :: Nat) {k} {k} (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 (n :: Nat) {k} {k} (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) => SetterRes (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 (n :: Nat) {k} {k} (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) => FoldRes (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 (n :: Nat) {k} (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 (n :: Nat) {k} {k} (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) => TravRes (Pow n :: k +-> k) (CoPow n :: k +-> k)
instance (Monoidal k, KnownNat n) => MonTravRes (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 (n :: Nat) {k} {k} (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)
instance (CopyDiscard k, KnownNat n) => GrateRes (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 (n :: Nat) {k} {k} (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, KnownNat n) => KaleidoRes (Pow n :: k +-> k) (CoPow n :: k +-> k) where
  kaleidoP :: 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
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 (n :: Nat) {k} {k} (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)
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 (n :: Nat) {k} {k} (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 kaleidoscope from a tensor-power decomposition of @s@ and recomposition of
-- @t@. @'kaleidoscope'@ is the arity-two case.
kaleidoscopeN
  :: forall {k} (n :: Nat) (s :: k) (t :: k) a b
   . (CopyDiscard k, KnownNat n, Ob a, Ob b)
  => (s ~> Tensor n a) -> (Tensor n b ~> t) -> Kaleidoscope s t a b
kaleidoscopeN :: forall {k} (n :: Nat) (s :: k) (t :: k) (a :: k) (b :: k).
(CopyDiscard k, KnownNat n, Ob a, Ob b) =>
(s ~> Tensor n a) -> (Tensor n b ~> t) -> Kaleidoscope s t a b
kaleidoscopeN s ~> Tensor n a
sl Tensor n b ~> t
rt = ExOptic KaleidoRes a b s t -> Optic (Prostrong KaleidoRes) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof ((:.:) (Pow n :.: ExOptic KaleidoRes a b) (CoPow n) s t
-> ExOptic KaleidoRes a b s t
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (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 Pow n s a
-> ExOptic KaleidoRes a b a b
-> (:.:) (Pow n) (ExOptic KaleidoRes a b) s 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
:.: (a ~> a) -> (b ~> b) -> ExOptic KaleidoRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) (Pow n) (ExOptic KaleidoRes a b) s b
-> CoPow n b t
-> (:.:) (Pow n :.: ExOptic KaleidoRes a b) (CoPow n) s t
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
:.: 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))