{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QualifiedDo #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | The __cotraversal__ and the __kaleidoscope__: two flavors with the same witnesses (the
-- representable 'StrongDistributiveProfunctor's, i.e. applicative functors rendered as profunctors,
-- with their 'RepCostar's) that differ in what they can be eliminated through.
--
-- Both mirror 'Proarrow.Optic.Traversal.MonTravFl'. All three rest on the square
-- @t :.: p ~> p :.: t@ between a functor @t@ and a 'StrongDistributiveProfunctor' @p@ (in @Type@,
-- @sequenceA :: t (f a) -> f (t a)@). A monoidal traversal takes @t@ as the witness and quantifies
-- over @p@; the optics here take @p@ as the witness and quantify over @t@.
--
-- * A 'Cotraversal' passes through every 'Cotraversable' carrier: the square for /arbitrary/ @p@.
--   This holds for shapes with a list of contents ('Proarrow.Category.Monoidal.Distributive.Cotraversable'
--   @('RepCostar' t)@ for a traversable representable @t@, 'Id', products, sums, and in @Type@
--   @'Costar' ('Prelude' t)@ for a Prelude @Traversable t@, the @Aggregating@ module of the
--   literature).
--
-- * A 'Kaleidoscope' passes through every 'Kaleidoscopic' carrier: the square for /representable/
--   @p@ only. This is the kaleidoscope of Clarke et al. (/Profunctor optics: a categorical update/),
--   @∫^{F applicative} C(S, F A) × C(F B, T)@. It admits every applicative, including ones with no
--   list of contents such as the reader @(->) r@, which are not 'Cotraversable'.
--
-- Every 'Cotraversable' carrier is 'Kaleidoscopic' ('cotravAct'), so @'KaleidoFl' <: 'CotravFl'@:
-- the kaleidoscope is the stronger flavor. Both sit below 'Proarrow.Optic.Setter.SetterFl' only,
-- since one can @over@ through an applicative but not fold out of one.
-- 'Proarrow.Optic.PowerGrate.PowerGrateFl' (the reader applicative) and the tensor-action pair for
-- a monoid residual (the writer applicative) are subflavors of 'KaleidoFl', which is how an
-- algebraic lens for the list monad composes with a kaleidoscope
-- ('Proarrow.Optic.Action.ClassifyFl').
module Proarrow.Optic.Kaleidoscope
  ( -- * The cotraversal
    CotravFl (..)
  , Cotraversal
  , Cotraversal'
  , cotraversal
  , cotraverseOf

    -- * The kaleidoscope
  , KaleidoFl (..)
  , Kaleidoscope
  , Kaleidoscope'
  , kaleidoscope
  , kaleidoscopeOf

    -- * Carriers
  , Kaleidoscopic (..)
  , cotravAct
  , CotravAs (..)
  , WrapRep (..)
  ) where

import Data.Kind (Constraint, Type)
import Prelude qualified as P

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, Tensor)
import Proarrow.Category.Monoidal.Action (ActionAt, CoprodAction)
import Proarrow.Category.Monoidal.Closed (Closed (..), Exp)
import Proarrow.Category.Monoidal.Distributive
  ( Cotraversable (..)
  , StrongDistributiveProfunctor
  , Traversable
  , Traversing
  )
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 (Prelude (..))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..), Monoid)
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (ExOptic, FLAVOR, Optic, Prostrong (..), legs2prof, withLegs)
import Proarrow.Optic.Setter (SetterFl (..))
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Costar (Costar, pattern Costar)
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..), RepCostar (..), Representable (..), repUniv)
import Proarrow.Tools.SMC (SYN (..), lam, toSMC, (!), (-<))
import Proarrow.Tools.SMC qualified as SMC

-- * Carriers

-- | The carriers of the kaleidoscope: profunctors that every representable
-- 'StrongDistributiveProfunctor' @p@ (i.e. every applicative functor @p % -@) acts on by
-- application. Where a traversal's carriers are the applicatives themselves, a kaleidoscope's
-- carriers are the things applicatives can be sequenced through. These are every 'Cotraversable'
-- profunctor ('cotravAct'), and in @Type@ also @'Costar' t@ for any @Traversable t@ (@'Costar' []@
-- directly, and @'Costar' ('Prelude' t)@ for a @t@ that has no 'Proarrow.Functor.Functor' instance
-- of its own).
type Kaleidoscopic :: forall {k}. (k +-> k) -> Constraint
class (Profunctor r) => Kaleidoscopic (r :: k +-> k) where
  kaleidoAct :: forall p a b. (Representable p, StrongDistributiveProfunctor (p :: k +-> k)) => r a b -> r (p % a) (p % b)

-- | 'kaleidoAct' for any 'Cotraversable' carrier: let the witness through.
cotravAct
  :: forall {k} p r (a :: k) b
   . (Cotraversable r, Representable p, StrongDistributiveProfunctor p)
  => r a b -> r (p % a) (p % b)
cotravAct :: forall {k} (p :: k +-> k) (r :: k +-> k) (a :: k) (b :: k).
(Cotraversable r, Representable p,
 StrongDistributiveProfunctor p) =>
r a b -> r (p % a) (p % b)
cotravAct r a b
rab = r a b
rab r a b -> ((Ob a, Ob b) => r (p % a) (p % b)) -> r (p % a) (p % b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case (:.:) p r (p % a) b -> (:.:) r p (p % a) b
(p :.: r) :~> (r :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, StrongDistributiveProfunctor p) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: r) :~> (r :.: p)
cotraverse (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
repUniv @p @a p (p % a) a -> r a b -> (:.:) p r (p % 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
:.: r a b
rab) of r (p % a) b
x :.: p b b
y -> (b ~> (p % b)) -> r (p % a) b -> r (p % a) (p % b)
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> r a b -> r a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (p b b -> b ~> (p % b)
forall (a :: k) (b :: k). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p b b
y) r (p % a) b
x

-- | A 'Cotraversable' carrier, tagged as the 'Kaleidoscopic' carrier it also is. With it every
-- kaleidoscope witness is a cotraversal witness (the default 'cotravP').
newtype CotravAs r a b = CotravAs {forall {k} {k} (r :: k -> k -> Type) (a :: k) (b :: k).
CotravAs r a b -> r a b
unCotravAs :: r a b}

instance (Profunctor r) => Profunctor (CotravAs r) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> CotravAs r a b -> CotravAs r c d
dimap c ~> a
l b ~> d
r (CotravAs r a b
p) = r c d -> CotravAs r c d
forall {k} {k} (r :: k -> k -> Type) (a :: k) (b :: k).
r a b -> CotravAs r a b
CotravAs ((c ~> a) -> (b ~> d) -> r a b -> r c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(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 c ~> a
l b ~> d
r r a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> CotravAs r a b -> r
\\ CotravAs r a b
p = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> r a b -> r
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> 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
\\ r a b
p
instance (Cotraversable r) => Kaleidoscopic (CotravAs r) where
  kaleidoAct :: forall (p :: k +-> k) (a :: k) (b :: k).
(Representable p, StrongDistributiveProfunctor p) =>
CotravAs r a b -> CotravAs r (p % a) (p % b)
kaleidoAct @p (CotravAs r a b
r) = r (p % a) (p % b) -> CotravAs r (p % a) (p % b)
forall {k} {k} (r :: k -> k -> Type) (a :: k) (b :: k).
r a b -> CotravAs r a b
CotravAs (forall {k} (p :: k +-> k) (r :: k +-> k) (a :: k) (b :: k).
(Cotraversable r, Representable p,
 StrongDistributiveProfunctor p) =>
r a b -> r (p % a) (p % b)
forall (p :: k +-> k) (r :: k +-> k) (a :: k) (b :: k).
(Cotraversable r, Representable p,
 StrongDistributiveProfunctor p) =>
r a b -> r (p % a) (p % b)
cotravAct @p r a b
r)

-- | The general carrier: the 'RepCostar' of a traversable representable functor.
instance (Traversable t, Representable t) => Kaleidoscopic (RepCostar t) where
  kaleidoAct :: forall (p :: k +-> k) (a :: k) (b :: k).
(Representable p, StrongDistributiveProfunctor p) =>
RepCostar t a b -> RepCostar t (p % a) (p % b)
kaleidoAct @p = forall {k} (p :: k +-> k) (r :: k +-> k) (a :: k) (b :: k).
(Cotraversable r, Representable p,
 StrongDistributiveProfunctor p) =>
r a b -> r (p % a) (p % b)
forall (p :: k +-> k) (r :: k +-> k) (a :: k) (b :: k).
(Cotraversable r, Representable p,
 StrongDistributiveProfunctor p) =>
r a b -> r (p % a) (p % b)
cotravAct @p

-- | The applicative functor a representable 'StrongDistributiveProfunctor' on 'Type' represents:
-- @pure@ is 'one' and @liftA2@ is '**'.
newtype WrapRep p x = WrapRep {forall {j} (p :: j +-> Type) (x :: j). WrapRep p x -> p % x
unwrapRep :: p % x}

instance (Representable (p :: Type +-> Type)) => P.Functor (WrapRep p) where
  fmap :: forall a b. (a -> b) -> WrapRep p a -> WrapRep p b
fmap a -> b
f (WrapRep p % a
x) = (p % b) -> WrapRep p b
forall {j} (p :: j +-> Type) (x :: j). (p % x) -> WrapRep p x
WrapRep (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Type +-> Type) a b.
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a ~> b
a -> b
f p % a
x)
instance (Representable p, StrongDistributiveProfunctor (p :: Type +-> Type)) => P.Applicative (WrapRep p) where
  pure :: forall a. a -> WrapRep p a
pure a
x = (p % a) -> WrapRep p a
forall {j} (p :: j +-> Type) (x :: j). (p % x) -> WrapRep p x
WrapRep (p () a -> () ~> (p % a)
forall a b. p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index ((() ~> a) -> p () () -> p () a
forall b d a. (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (\() -> a
x) (forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
forall (p :: Type +-> Type). MonoidalProfunctor p => p Unit Unit
one @p)) ())
  liftA2 :: forall a b c.
(a -> b -> c) -> WrapRep p a -> WrapRep p b -> WrapRep p c
liftA2 a -> b -> c
f (WrapRep p % a
x) (WrapRep p % b
y) = (p % c) -> WrapRep p c
forall {j} (p :: j +-> Type) (x :: j). (p % x) -> WrapRep p x
WrapRep (p (p % a, p % b) c -> (p % a, p % b) ~> (p % c)
forall a b. p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index (((a, b) ~> c) -> p (p % a, p % b) (a, b) -> p (p % a, p % b) c
forall b d a. (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry a -> b -> c
f) (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: Type +-> Type) a.
(Representable p, Ob a) =>
p (p % a) a
repUniv @p p (p % a) a -> p (p % b) b -> p ((p % a) ** (p % b)) (a ** b)
forall x1 x2 y1 y2. p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: Type +-> Type) a.
(Representable p, Ob a) =>
p (p % a) a
repUniv @p)) (p % a
x, p % b
y))

-- | @'Costar' ('Prelude' t)@ for a traversable @t@: sequence the applicative through @t@, then
-- aggregate. This carrier is /not/ 'Cotraversable', see the module header.
instance (P.Traversable t) => Kaleidoscopic (Costar (Prelude t)) where
  kaleidoAct :: forall (p :: Type +-> Type) a b.
(Representable p, StrongDistributiveProfunctor p) =>
Costar (Prelude t) a b -> Costar (Prelude t) (p % a) (p % b)
kaleidoAct @p @a (Costar Prelude t a ~> b
g) = (Prelude t (p % a) ~> (p % b))
-> Costar' (OP ('NT (Prelude t))) (p % a) (p % b)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (\(Prelude t (p % a)
tpa) -> forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Type +-> Type) a b.
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (Prelude t a ~> b
Prelude t a -> b
g (Prelude t a -> b) -> (t a -> Prelude t a) -> t a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. t a -> Prelude t a
forall (f :: Type -> Type) a. f a -> Prelude f a
Prelude) (WrapRep p (t a) -> p % t a
forall {j} (p :: j +-> Type) (x :: j). WrapRep p x -> p % x
unwrapRep (((p % a) -> WrapRep p a) -> t (p % a) -> WrapRep p (t a)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b)
P.traverse (forall {j} (p :: j +-> Type) (x :: j). (p % x) -> WrapRep p x
forall (p :: Type +-> Type) x. (p % x) -> WrapRep p x
WrapRep @p @a) t (p % a)
tpa)))

-- | The same for @[]@, which is a 'Proarrow.Functor.Functor' in its own right, so the literature's
-- aggregating carrier can be written as a plain @[a] -> b@.
instance Kaleidoscopic (Costar []) where
  kaleidoAct :: forall (p :: Type +-> Type) a b.
(Representable p, StrongDistributiveProfunctor p) =>
Costar [] a b -> Costar [] (p % a) (p % b)
kaleidoAct @p @a (Costar [a] ~> b
g) = ([p % a] ~> (p % b)) -> Costar' (OP ('NT [])) (p % a) (p % b)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (\[p % a]
tpa -> forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: Type +-> Type) a b.
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p [a] ~> b
g (WrapRep p [a] -> p % [a]
forall {j} (p :: j +-> Type) (x :: j). WrapRep p x -> p % x
unwrapRep (((p % a) -> WrapRep p a) -> [p % a] -> WrapRep p [a]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
P.traverse (forall {j} (p :: j +-> Type) (x :: j). (p % x) -> WrapRep p x
forall (p :: Type +-> Type) x. (p % x) -> WrapRep p x
WrapRep @p @a) [p % a]
tpa)))

-- * The cotraversal

-- | The cotraversal flavor: pass any 'Cotraversable' carrier through the witness pair. The
-- mirror of 'Proarrow.Optic.Traversal.MonTravFl', with witness and carrier swapped.
type CotravFl :: forall {k}. FLAVOR k k
class (SetterFl p q) => CotravFl (p :: k +-> k) (q :: k +-> k) where
  cotravP :: (Cotraversable r) => p s a -> q b t -> r a b -> r s t
  default cotravP :: (KaleidoFl p q, Cotraversable r) => p s a -> q b t -> r a b -> r s t
  cotravP p s a
l q b t
r r a b
rab = CotravAs r s t -> r s t
forall {k} {k} (r :: k -> k -> Type) (a :: k) (b :: k).
CotravAs r a b -> r a b
unCotravAs (p s a -> q b t -> CotravAs r a b -> CotravAs r s t
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(KaleidoFl p q, Kaleidoscopic 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).
Kaleidoscopic 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 -> CotravAs r a b
forall {k} {k} (r :: k -> k -> Type) (a :: k) (b :: k).
r a b -> CotravAs r a b
CotravAs r a b
rab))

-- | The kaleidoscope flavor: act on any 'Kaleidoscopic' carrier through the witness pair.
type KaleidoFl :: forall {k}. FLAVOR k k
class (CotravFl p q) => KaleidoFl (p :: k +-> k) (q :: k +-> k) where
  kaleidoP :: (Kaleidoscopic r) => p s a -> q b t -> r a b -> r s t

-- | The generating witnesses: any representable 'StrongDistributiveProfunctor' (any applicative
-- functor) with its 'RepCostar'. The legs are @s ~> p % a@ and @p % b ~> t@.
instance (Representable p, StrongDistributiveProfunctor p) => CotravFl (p :: k +-> k) (RepCostar p)

instance (Representable p, StrongDistributiveProfunctor p) => KaleidoFl (p :: k +-> k) (RepCostar p) where
  kaleidoP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
Kaleidoscopic r =>
p s a -> RepCostar p b t -> r a b -> r s t
kaleidoP p s a
l (RepCostar (p % b) ~> t
r) r a b
rab = (s ~> (p % a)) -> ((p % b) ~> t) -> r (p % a) (p % 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 (p s a -> s ~> (p % a)
forall (a :: k) (b :: k). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p s a
l) (p % b) ~> t
r (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 @_ @p r a b
rab)

-- | The tensor-action pair for a monoid residual: @m ** -@ is the writer applicative.
instance
  (SymMonoidal k, HasCoproducts k, Monoid (m :: k))
  => CotravFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m))

instance
  (SymMonoidal k, HasCoproducts k, Monoid (m :: k))
  => KaleidoFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m))
  where
  kaleidoP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
Kaleidoscopic r =>
Rep (ActionAt Tensor m) s a
-> Corep (ActionAt Tensor m) b t -> r a b -> r s t
kaleidoP (Rep s ~> (ActionAt Tensor m @ a)
h) (Corep (ActionAt Tensor m @ b) ~> t
i) r a b
rab = (s ~> (m ** a)) -> ((m ** b) ~> t) -> r (m ** a) (m ** 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 ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
h (ActionAt Tensor m @ b) ~> t
(m ** b) ~> t
i (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 @_ @(Rep (ActionAt Tensor m)) r a b
rab)

-- | The exponential by a comonoid, @m ~~> -@, is an applicative functor (the reader applicative):
-- @pure@ discards the argument with the counit and @<*>@ duplicates it with the comultiplication.
-- Rendered on @'Rep' ('Exp' m)@ (legs @a ~> (m ~~> b)@) this is a
-- 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor', so a
-- 'Proarrow.Optic.Grate.Grate' is a 'Proarrow.Optic.Kaleidoscope.Kaleidoscope'.
instance (Closed k, SymMonoidal k, CocommutativeComonoid (m :: k)) => MonoidalProfunctor (Rep (Exp m) :: k +-> k) where
  one :: Rep (Exp m) Unit Unit
one = (Unit ~> (Exp m @ Unit)) -> Rep (Exp m) Unit Unit
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
toSMC @I @(F m :-> I) \TermP
  (~>)
  (2 + PSize (TermP (~>) (ZonkAny 1) '[ '(1, F m)] (F m)))
  '[ '(0, I)]
  I
u -> (TermP (~>) (ZonkAny 1) '[ '(1, F m)] (F m)
 -> TermP
      (~>)
      (2 + PSize (TermP (~>) (ZonkAny 1) '[ '(1, F m)] (F m)))
      '[ '(0, I)]
      I)
-> TermP
     (~>)
     (1
      + PSize
          (TermP
             (~>)
             (2 + PSize (TermP (~>) (ZonkAny 1) '[ '(1, F m)] (F m)))
             '[ '(0, I)]
             I))
     '[ '(0, I)]
     (F m :-> I)
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
(Closed k, Binds (~>) d r a b t cont) =>
(t -> cont) -> Term d r (a :-> b)
lam (TermP
  (~>)
  (2 + PSize (TermP (~>) (ZonkAny 1) '[ '(1, F m)] (F m)))
  '[ '(0, I)]
  I
-> TermP (~>) (ZonkAny 1) '[ '(1, F m)] (F m)
-> TermP
     (~>)
     (2 + PSize (TermP (~>) (ZonkAny 1) '[ '(1, F m)] (F m)))
     '[ '(0, I)]
     I
forall a b. a -> b -> a
P.const TermP
  (~>)
  (2 + PSize (TermP (~>) (ZonkAny 1) '[ '(1, F m)] (F m)))
  '[ '(0, I)]
  I
u))
  Rep @x2 @_ @x1 l :: x1 ~> (Exp m @ x2)
l@x1 ~> (Exp m @ x2)
x1 ~> (m ~~> x2)
Objs ** :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Rep (Exp m) x1 x2
-> Rep (Exp m) y1 y2 -> Rep (Exp m) (x1 ** y1) (x2 ** y2)
** Rep @y2 @_ @y1 r :: y1 ~> (Exp m @ y2)
r@y1 ~> (Exp m @ y2)
y1 ~> (m ~~> y2)
Objs =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x2 @y2 (((x1 ** y1) ~> (Exp m @ (x2 ** y2)))
-> Rep (Exp m) (x1 ** y1) (x2 ** y2)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (x1 ** y1) ~> (Exp m @ (x2 ** y2))
Interp (F x1 :** F y1) ~> Interp (F m :-> (F x2 :** F y2))
both)
    where
      both :: Interp (F x1 :** F y1) ~> Interp (F m :-> (F x2 :** F y2))
both = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
toSMC @(F x1 :** F y1) @(F m :-> F x2 :** F y2) \(TermP (~>) (ZonkAny 2) '[ '(1, F x1)] (F x1)
x, TermP (~>) (ZonkAny 3) '[ '(2, F y1)] (F y1)
y) ->
        (TermP (~>) 4 '[ '(3, F m)] (F m)
 -> TermP
      (~>)
      (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
      (Union '[ '(3, F m), '(1, F x1)] '[ '(3, F m), '(2, F y1)])
      (F x2 :** F y2))
-> TermP
     (~>)
     (1
      + ((2 + PSize (TermP (~>) (ZonkAny 2) '[ '(1, F x1)] (F x1)))
         + PSize (TermP (~>) (ZonkAny 3) '[ '(2, F y1)] (F y1))))
     '[ '(2, F y1), '(1, F x1)]
     (F m :-> (F x2 :** F y2))
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
(Closed k, Binds (~>) d r a b t cont) =>
(t -> cont) -> Term d r (a :-> b)
lam \TermP (~>) 4 '[ '(3, F m)] (F m)
i -> (x1 ~> (Exp m @ x2)
Interp (F x1) ~> (m ~~> x2)
l (Interp (F x1) ~> (m ~~> x2))
-> TermP (~>) (ZonkAny 2) '[ '(1, F x1)] (F x1)
-> TermP
     (~>)
     4
     (TupleCtx k (TermP (~>) (ZonkAny 2) '[ '(1, F x1)] (F x1)))
     (F (m ~~> x2))
forall {k} (a :: SYN k) (b :: k) t (p :: CAT k) (d :: Nat).
(Promonad p, Tuple p t a) =>
p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
-< TermP (~>) (ZonkAny 2) '[ '(1, F x1)] (F x1)
x) TermP
  (~>)
  4
  (TupleCtx k (TermP (~>) (ZonkAny 2) '[ '(1, F x1)] (F x1)))
  (F (m ~~> x2))
-> TermP (~>) 4 '[ '(3, F m)] (F m)
-> TermP
     (~>)
     (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
     '[ '(3, F m), '(1, F x1)]
     (F x2)
forall {k} (p :: CAT k) f x r.
(Apply p f x r, Closed k, MonoidalProfunctor p, KnownObj (TyOf x),
 KnownObj (TyOf r), Merge (CtxOf f) (CtxOf x)) =>
f -> x -> r
! TermP (~>) 4 '[ '(3, F m)] (F m)
i TermP
  (~>)
  (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
  '[ '(3, F m), '(1, F x1)]
  (F x2)
-> TermP
     (~>)
     (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
     '[ '(3, F m), '(2, F y1)]
     (F y2)
-> TermP
     (~>)
     (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
     (Union '[ '(3, F m), '(1, F x1)] '[ '(3, F m), '(2, F y1)])
     (F x2 :** F y2)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k) (p :: CAT k).
(MonoidalProfunctor p, Merge g1 g2) =>
TermP p d g1 a
-> TermP p d g2 b -> TermP p d (Union g1 g2) (a :** b)
SMC.** (y1 ~> (Exp m @ y2)
Interp (F y1) ~> (m ~~> y2)
r (Interp (F y1) ~> (m ~~> y2))
-> TermP (~>) (ZonkAny 3) '[ '(2, F y1)] (F y1)
-> TermP
     (~>)
     4
     (TupleCtx k (TermP (~>) (ZonkAny 3) '[ '(2, F y1)] (F y1)))
     (F (m ~~> y2))
forall {k} (a :: SYN k) (b :: k) t (p :: CAT k) (d :: Nat).
(Promonad p, Tuple p t a) =>
p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
-< TermP (~>) (ZonkAny 3) '[ '(2, F y1)] (F y1)
y) TermP
  (~>)
  4
  (TupleCtx k (TermP (~>) (ZonkAny 3) '[ '(2, F y1)] (F y1)))
  (F (m ~~> y2))
-> TermP (~>) 4 '[ '(3, F m)] (F m)
-> TermP
     (~>)
     (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
     '[ '(3, F m), '(2, F y1)]
     (F y2)
forall {k} (p :: CAT k) f x r.
(Apply p f x r, Closed k, MonoidalProfunctor p, KnownObj (TyOf x),
 KnownObj (TyOf r), Merge (CtxOf f) (CtxOf x)) =>
f -> x -> r
! TermP (~>) 4 '[ '(3, F m)] (F m)
i

instance (Closed k, HasCoproducts k, Ob (m :: k)) => MonoidalProfunctor (Coprod (Rep (Exp m)) :: COPROD k +-> COPROD k) where
  one :: Coprod (Rep (Exp m)) Unit Unit
one = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @InitialObject (Rep (Exp m) InitialObject InitialObject
-> Coprod (Rep (Exp m)) (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 ~> (Exp m @ InitialObject))
-> Rep (Exp m) InitialObject InitialObject
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep InitialObject ~> (Exp m @ InitialObject)
InitialObject ~> (m ~~> InitialObject)
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate))
  Coprod (Rep @x2 a1 ~> (Exp m @ b1)
l) ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (Rep (Exp m)) x1 x2
-> Coprod (Rep (Exp m)) y1 y2
-> Coprod (Rep (Exp m)) (x1 ** y1) (x2 ** y2)
** Coprod (Rep @y2 a1 ~> (Exp m @ b1)
r) =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @x2 @y2 (Rep (Exp m) (a1 || a1) (b1 || b1)
-> Coprod (Rep (Exp m)) (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) ~> (Exp m @ (b1 || b1)))
-> Rep (Exp m) (a1 || a1) (b1 || b1)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @x2 @y2 (b1 ~> (b1 || b1)) -> (m ~> m) -> (m ~~> b1) ~> (m ~~> (b1 || b1))
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 @m) ((m ~~> b1) ~> (m ~~> (b1 || b1)))
-> (a1 ~> (m ~~> b1)) -> a1 ~> (m ~~> (b1 || b1))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> (Exp m @ b1)
a1 ~> (m ~~> b1)
l (a1 ~> (m ~~> (b1 || b1)))
-> (a1 ~> (m ~~> (b1 || b1))) -> (a1 || a1) ~> (m ~~> (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 (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @x2 @y2 (b1 ~> (b1 || b1)) -> (m ~> m) -> (m ~~> b1) ~> (m ~~> (b1 || b1))
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 @m) ((m ~~> b1) ~> (m ~~> (b1 || b1)))
-> (a1 ~> (m ~~> b1)) -> a1 ~> (m ~~> (b1 || b1))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> (Exp m @ b1)
a1 ~> (m ~~> b1)
r)))
instance (Closed k, SymMonoidal k, Ob (m :: k)) => Strong Tensor (Rep (Exp m) :: k +-> k) where
  act :: forall (a :: k) (x :: k) (y :: k).
Ob a =>
Rep (Exp m) x y -> Rep (Exp m) (Act Tensor a x) (Act Tensor a y)
act @a (Rep @y @_ @x p :: x ~> (Exp m @ y)
p@x ~> (Exp m @ y)
x ~> (m ~~> y)
Objs) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @y (((a ** x) ~> (Exp m @ (a ** y))) -> Rep (Exp m) (a ** x) (a ** y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (a ** x) ~> (Exp m @ (a ** y))
Interp (F a :** F x) ~> Interp (F m :-> (F a :** F y))
strong)
    where
      strong :: Interp (F a :** F x) ~> Interp (F m :-> (F a :** F y))
strong = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
toSMC @(F a :** F x) @(F m :-> F a :** F y) \(TermP
  (~>)
  (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
  '[ '(1, F a)]
  (F a)
a, TermP (~>) (ZonkAny 0) '[ '(2, F x)] (F x)
x) ->
        (TermP (~>) 4 '[ '(3, F m)] (F m)
 -> TermP
      (~>)
      (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
      (Union '[ '(1, F a)] '[ '(3, F m), '(2, F x)])
      (F a :** F y))
-> TermP
     (~>)
     (1 + (2 + PSize (TermP (~>) (ZonkAny 0) '[ '(2, F x)] (F x))))
     '[ '(2, F x), '(1, F a)]
     (F m :-> (F a :** F y))
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
(Closed k, Binds (~>) d r a b t cont) =>
(t -> cont) -> Term d r (a :-> b)
lam \TermP (~>) 4 '[ '(3, F m)] (F m)
i -> TermP
  (~>)
  (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
  '[ '(1, F a)]
  (F a)
a TermP
  (~>)
  (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
  '[ '(1, F a)]
  (F a)
-> TermP
     (~>)
     (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
     '[ '(3, F m), '(2, F x)]
     (F y)
-> TermP
     (~>)
     (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
     (Union '[ '(1, F a)] '[ '(3, F m), '(2, F x)])
     (F a :** F y)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k) (p :: CAT k).
(MonoidalProfunctor p, Merge g1 g2) =>
TermP p d g1 a
-> TermP p d g2 b -> TermP p d (Union g1 g2) (a :** b)
SMC.** (x ~> (Exp m @ y)
Interp (F x) ~> (m ~~> y)
p (Interp (F x) ~> (m ~~> y))
-> TermP (~>) (ZonkAny 0) '[ '(2, F x)] (F x)
-> TermP
     (~>)
     4
     (TupleCtx k (TermP (~>) (ZonkAny 0) '[ '(2, F x)] (F x)))
     (F (m ~~> y))
forall {k} (a :: SYN k) (b :: k) t (p :: CAT k) (d :: Nat).
(Promonad p, Tuple p t a) =>
p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
-< TermP (~>) (ZonkAny 0) '[ '(2, F x)] (F x)
x) TermP
  (~>)
  4
  (TupleCtx k (TermP (~>) (ZonkAny 0) '[ '(2, F x)] (F x)))
  (F (m ~~> y))
-> TermP (~>) 4 '[ '(3, F m)] (F m)
-> TermP
     (~>)
     (4 + PSize (TermP (~>) 4 '[ '(3, F m)] (F m)))
     '[ '(3, F m), '(2, F x)]
     (F y)
forall {k} (p :: CAT k) f x r.
(Apply p f x r, Closed k, MonoidalProfunctor p, KnownObj (TyOf x),
 KnownObj (TyOf r), Merge (CtxOf f) (CtxOf x)) =>
f -> x -> r
! TermP (~>) 4 '[ '(3, F m)] (F m)
i
instance (Closed k, HasCoproducts k, Comonoid (m :: k)) => Strong CoprodAction (Rep (Exp m) :: k +-> k) where
  act :: forall (a :: COPROD k) (x :: k) (y :: k).
Ob a =>
Rep (Exp m) x y
-> Rep (Exp m) (Act CoprodAction a x) (Act CoprodAction a y)
act @(COPR a) (Rep @y x ~> (Exp m @ y)
p) =
    x ~> (Exp m @ y)
x ~> (m ~~> y)
p (x ~> (m ~~> y))
-> ((Ob x, Ob (m ~~> y)) =>
    Rep (Exp m) (UN COPR a || x) (UN COPR a || y))
-> Rep (Exp m) (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 @a @y
        ( forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @a
            ( forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @y
                ( ((UN COPR a || x) ~> (Exp m @ (UN COPR a || y)))
-> Rep (Exp m) (UN COPR a || x) (UN COPR a || y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep
                    ((forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @y (UN COPR a ~> (UN COPR a || y))
-> (m ~> m) -> (m ~~> UN COPR a) ~> (m ~~> (UN COPR a || y))
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 @m) ((m ~~> UN COPR a) ~> (m ~~> (UN COPR a || y)))
-> (UN COPR a ~> (m ~~> UN COPR a))
-> UN COPR a ~> (m ~~> (UN COPR a || y))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @a @m (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @a ((UN COPR a ** Unit) ~> UN COPR a)
-> ((UN COPR a ** m) ~> (UN COPR a ** Unit))
-> (UN COPR a ** m) ~> UN COPR a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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 (UN COPR a)
-> (m ~> Unit) -> (UN COPR a ** m) ~> (UN COPR a ** 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 (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @m)) (UN COPR a ~> (m ~~> (UN COPR a || y)))
-> (x ~> (m ~~> (UN COPR a || y)))
-> (UN COPR a || x) ~> (m ~~> (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 (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @y (y ~> (UN COPR a || y))
-> (m ~> m) -> (m ~~> y) ~> (m ~~> (UN COPR a || y))
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 @m) ((m ~~> y) ~> (m ~~> (UN COPR a || y)))
-> (x ~> (m ~~> y)) -> x ~> (m ~~> (UN COPR a || y))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> (Exp m @ y)
x ~> (m ~~> y)
p)
                )
            )
        )

-- | The exponential pair for a comonoid exponent: @m ~~> -@ is the reader applicative. So every
-- 'Proarrow.Optic.Grate.Grate' is a kaleidoscope.
instance
  (Closed k, SymMonoidal k, HasCoproducts k, CocommutativeComonoid (m :: k))
  => CotravFl (Rep (Exp m) :: k +-> k) (Corep (Exp m))

instance (Closed k, SymMonoidal k, HasCoproducts k, CocommutativeComonoid (m :: k)) => Traversing (Rep (Exp m) :: k +-> k)

instance
  (Closed k, SymMonoidal k, HasCoproducts k, CocommutativeComonoid (m :: k))
  => KaleidoFl (Rep (Exp m) :: k +-> k) (Corep (Exp m))
  where
  kaleidoP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
Kaleidoscopic r =>
Rep (Exp m) s a -> Corep (Exp m) b t -> r a b -> r s t
kaleidoP (Rep s ~> (Exp m @ a)
h) (Corep (Exp m @ b) ~> t
i) r a b
rab = (s ~> (m ~~> a))
-> ((m ~~> b) ~> t) -> r (m ~~> a) (m ~~> 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 ~> (Exp m @ a)
s ~> (m ~~> a)
h (Exp m @ b) ~> t
(m ~~> b) ~> t
i (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 @_ @(Rep (Exp m)) r a b
rab)

instance (CategoryOf k) => CotravFl (Id :: k +-> k) (Id :: k +-> k) where
  cotravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
Cotraversable r =>
Id s a -> Id b t -> r a b -> r s t
cotravP (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 (CategoryOf k) => KaleidoFl (Id :: k +-> k) (Id :: k +-> k) where
  kaleidoP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
Kaleidoscopic 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 (CotravFl f g, CotravFl f' g') => CotravFl (f :.: f') (g' :.: g) where
  cotravP :: forall (r :: i +-> i) (s :: i) (a :: i) (b :: i) (t :: i).
Cotraversable r =>
(:.:) f f' s a -> (:.:) g' g b t -> r a b -> r s t
cotravP (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).
(CotravFl p q, Cotraversable 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).
(CotravFl p q, Cotraversable r) =>
p s a -> q b t -> r a b -> r s t
cotravP @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 :: CAT 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).
(CotravFl p q, Cotraversable 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).
(CotravFl p q, Cotraversable r) =>
p s a -> q b t -> r a b -> r s t
cotravP @f' @g' f' b a
f' g' b b
g'
instance (KaleidoFl f g, KaleidoFl f' g') => KaleidoFl (f :.: f') (g' :.: g) where
  kaleidoP :: forall (r :: i +-> i) (s :: i) (a :: i) (b :: i) (t :: i).
Kaleidoscopic 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).
(KaleidoFl p q, Kaleidoscopic 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).
(KaleidoFl p q, Kaleidoscopic 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 :: CAT 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).
(KaleidoFl p q, Kaleidoscopic 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).
(KaleidoFl p q, Kaleidoscopic r) =>
p s a -> q b t -> r a b -> r s t
kaleidoP @f' @g' f' b a
f' g' b b
g'

type Cotraversal (s :: k) (t :: k) a b = Optic (Prostrong CotravFl) s t a b
type Cotraversal' s a = Cotraversal s s a a

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

-- | Build a cotraversal from its legs through an applicative functor, given as a representable
-- 'StrongDistributiveProfunctor' @p@.
cotraversal
  :: forall {k} p (s :: k) (t :: k) a b
   . (Representable p, StrongDistributiveProfunctor p, Ob a, Ob b)
  => (s ~> p % a) -> (p % b ~> t) -> Cotraversal s t a b
cotraversal :: forall {k} (p :: k +-> k) (s :: k) (t :: k) (a :: k) (b :: k).
(Representable p, StrongDistributiveProfunctor p, Ob a, Ob b) =>
(s ~> (p % a)) -> ((p % b) ~> t) -> Cotraversal s t a b
cotraversal s ~> (p % a)
l (p % b) ~> t
r = 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 @CotravFl (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: k +-> k) (b :: k) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p s ~> (p % a)
l) (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 @_ @p (p % b) ~> t
r)

-- | Build a kaleidoscope from the same legs.
kaleidoscope
  :: forall {k} p (s :: k) (t :: k) a b
   . (Representable p, StrongDistributiveProfunctor p, Ob a, Ob b)
  => (s ~> p % a) -> (p % b ~> t) -> Kaleidoscope s t a b
kaleidoscope :: forall {k} (p :: k +-> k) (s :: k) (t :: k) (a :: k) (b :: k).
(Representable p, StrongDistributiveProfunctor p, Ob a, Ob b) =>
(s ~> (p % a)) -> ((p % b) ~> t) -> Kaleidoscope s t a b
kaleidoscope s ~> (p % a)
l (p % b) ~> t
r = 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 @KaleidoFl (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: k +-> k) (b :: k) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p s ~> (p % a)
l) (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 @_ @p (p % b) ~> t
r)

-- | Pass a 'Cotraversable' carrier through a cotraversal (or any stronger optic, in any encoding,
-- '(%)'-composites included).
cotraverseOf
  :: forall {k} c (s :: k) (t :: k) a b r
   . (CategoryOf k, Cotraversable r, (Ob a, Ob b) => c (ExOptic CotravFl a b))
  => Optic c s t a b -> r a b -> r s t
cotraverseOf :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) (r :: k -> k -> Type).
(CategoryOf k, Cotraversable r,
 (Ob a, Ob b) => c (ExOptic CotravFl a b)) =>
Optic c s t a b -> r a b -> r s t
cotraverseOf 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 @CotravFl 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).
(CotravFl p q, Cotraversable 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).
Cotraversable r =>
p s a -> q b t -> r a b -> r s t
cotravP p s a
l q b t
r r a b
rab

-- | Act on a 'Kaleidoscopic' carrier through a kaleidoscope (or any stronger optic, in any
-- encoding, '(%)'-composites included). At @'Costar' []@ this is the literature's
-- aggregation operator @>-@: from @[a] -> b@ to @[s] -> t@.
kaleidoscopeOf
  :: forall {k} c (s :: k) (t :: k) a b r
   . (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 :: 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 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 @KaleidoFl 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).
(KaleidoFl p q, Kaleidoscopic 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).
Kaleidoscopic 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

-- | The carriers as instances, so that an optic of these flavors composed with another flavor that
-- also runs at the carrier can be eliminated there directly.
instance (Traversable t, Representable t) => Prostrong CotravFl (RepCostar t) where
  proact :: forall (f :: j +-> j) (g :: j +-> j).
(CotravFl f g, Profunctor f, Profunctor g) =>
((f :.: RepCostar t) :.: g) :~> RepCostar t
proact (f a b
f :.: RepCostar t b b
c :.: g b b
g) = f a b -> g b b -> RepCostar t b b -> RepCostar t a b
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(CotravFl p q, Cotraversable r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: j +-> j) (s :: j) (a :: j) (b :: j) (t :: j).
Cotraversable r =>
f s a -> g b t -> r a b -> r s t
cotravP f a b
f g b b
g RepCostar t b b
c

instance (Traversable t, Representable t) => Prostrong KaleidoFl (RepCostar t) where
  proact :: forall (f :: j +-> j) (g :: j +-> j).
(KaleidoFl f g, Profunctor f, Profunctor g) =>
((f :.: RepCostar t) :.: g) :~> RepCostar t
proact (f a b
f :.: RepCostar t b b
c :.: g b b
g) = f a b -> g b b -> RepCostar t b b -> RepCostar t a b
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(KaleidoFl p q, Kaleidoscopic r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: j +-> j) (s :: j) (a :: j) (b :: j) (t :: j).
Kaleidoscopic r =>
f s a -> g b t -> r a b -> r s t
kaleidoP f a b
f g b b
g RepCostar t b b
c
instance (P.Traversable t) => Prostrong KaleidoFl (Costar (Prelude t)) where
  proact :: forall (f :: Type +-> Type) (g :: Type +-> Type).
(KaleidoFl f g, Profunctor f, Profunctor g) =>
((f :.: Costar (Prelude t)) :.: g) :~> Costar (Prelude t)
proact (f a b
f :.: Costar (Prelude t) b b
c :.: g b b
g) = f a b
-> g b b
-> Costar (Prelude t) b b
-> Costar' (OP ('NT (Prelude t))) a b
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(KaleidoFl p q, Kaleidoscopic r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: Type +-> Type) s a b t.
Kaleidoscopic r =>
f s a -> g b t -> r a b -> r s t
kaleidoP f a b
f g b b
g Costar (Prelude t) b b
c
instance Prostrong KaleidoFl (Costar []) where
  proact :: forall (f :: Type +-> Type) (g :: Type +-> Type).
(KaleidoFl f g, Profunctor f, Profunctor g) =>
((f :.: Costar []) :.: g) :~> Costar []
proact (f a b
f :.: Costar [] b b
c :.: g b b
g) = f a b -> g b b -> Costar [] b b -> Costar' (OP ('NT [])) a b
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(KaleidoFl p q, Kaleidoscopic r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: Type +-> Type) s a b t.
Kaleidoscopic r =>
f s a -> g b t -> r a b -> r s t
kaleidoP f a b
f g b b
g Costar [] b b
c