{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE IncoherentInstances #-}
{-# OPTIONS_GHC -Wno-orphans -fprint-potential-instances #-}

module Proarrow.Category.Monoidal.Optic where

import Data.Kind (Type)
import Data.Monoid qualified as P
import GHC.Generics qualified as G
import Prelude (Either (..), Maybe (..), Monad (..), const, either, flip, uncurry, ($))
import Prelude qualified as P

import Data.Functor.Const (Const (..))
import Proarrow.Category.Instance.Kleisli (KLEISLI (..), Kleisli (..))
import Proarrow.Category.Instance.Nat (ApplyAction)
import Proarrow.Category.Instance.Sub (SUBCAT (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, Tensor, obj2, swap)
import Proarrow.Category.Monoidal.Action
  ( Act
  , CoprodAction
  , MonoidalAction (..)
  , NoAction
  , ProdAction
  , SubAction
  , composeActs
  , decomposeActs
  )
import Proarrow.Category.Monoidal.Distributive qualified as Dist
import Proarrow.Category.Monoidal.Endo (ENDO (..), TravAction)
import Proarrow.Category.Monoidal.Strength (Costrong (..), Strong (..), strongId)
import Proarrow.Colimit.BinaryCoproduct (COPROD (..), HasBinaryCoproducts (..), HasCoproducts, nil, (++))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, type (+->))
import Proarrow.Functor (FromProfunctor (..), Functor (map), Prelude (..))
import Proarrow.Limit.BinaryProduct (Cartesian, HasBinaryProducts (..), HasProducts, PROD (..))
import Proarrow.Optic (InvertableOptic, Iso, Optic, Optic_ (..), Re (..), (:&&:))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Instance.Star (Star, unStar, pattern Star)
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), repObj, withObRep)

type ExOptic :: (m, k) +-> k -> k -> k -> k -> k -> Type
data ExOptic act a b s t where
  ExOptic
    :: forall {k} {m} {act} (x :: m) s t a b
     . (Ob (a :: k), Ob (b :: k), Ob x)
    => s ~> Act act x a
    -> Act act x b ~> t
    -> ExOptic act a b s t

instance (CategoryOf k) => Profunctor (ExOptic act a b :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> ExOptic act a b a b -> ExOptic act a b c d
dimap c ~> a
l b ~> d
r (ExOptic @x a ~> Act act x a
f Act act x b ~> b
g) = forall (b :: m) (s :: k) (t :: k) (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
forall {k} {m} {act :: (m, k) +-> k} (b :: m) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
ExOptic @x (a ~> Act act x a
f (a ~> Act act x a) -> (c ~> a) -> c ~> Act act 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
. c ~> a
l) (b ~> d
r (b ~> d) -> (Act act x b ~> b) -> Act act x b ~> 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
. Act act x b ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> ExOptic act a b a b -> r
\\ ExOptic a ~> Act act x a
f Act act x b ~> b
g = r
(Ob a, Ob b) => r
(Ob a, Ob (Act act x a)) => r
r ((Ob a, Ob (Act act x a)) => r) -> (a ~> Act act x a) -> 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 ~> Act act x a
f ((Ob (Act act x b), Ob b) => r) -> (Act act x 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
\\ Act act x b ~> b
g
instance (MonoidalAction act) => Strong act (ExOptic act a b :: k +-> k) where
  act :: forall (a :: m) (x :: k) (y :: k).
Ob a =>
ExOptic act a b x y -> ExOptic act a b (Act act a x) (Act act a y)
act @z (ExOptic @x @s @t x ~> Act act x a
f Act act x b ~> y
g) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @z @x ((Ob (a ** x) => ExOptic act a b (Act act a x) (Act act a y))
 -> ExOptic act a b (Act act a x) (Act act a y))
-> (Ob (a ** x) => ExOptic act a b (Act act a x) (Act act a y))
-> ExOptic act a b (Act act a x) (Act act a y)
forall a b. (a -> b) -> a -> b
$
      forall (b :: m) (s :: k) (t :: k) (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
forall {k} {m} {act :: (m, k) +-> k} (b :: m) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
ExOptic @(z ** x)
        (forall {m} {k} (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k)
       (a :: k) (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(a ~> Act t x b) -> (b ~> Act t y c) -> a ~> Act t (x ** y) c
forall (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k) (a :: k)
       (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(a ~> Act t x b) -> (b ~> Act t y c) -> a ~> Act t (x ** y) c
composeActs @act @z @x @a (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: (m, k) +-> k) (a :: (m, k)).
(Representable p, Ob a) =>
Obj (p % a)
repObj @act @'(z, s)) x ~> Act act x a
f)
        (forall {m} {k} (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k)
       (a :: k) (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(Act t y c ~> b) -> (Act t x b ~> a) -> Act t (x ** y) c ~> a
forall (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k) (a :: k)
       (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(Act t y c ~> b) -> (Act t x b ~> a) -> Act t (x ** y) c ~> a
decomposeActs @act @z @x @b Act act x b ~> y
g (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: (m, k) +-> k) (a :: (m, k)).
(Representable p, Ob a) =>
Obj (p % a)
repObj @act @'(z, t)))
        ((Ob x, Ob (Act act x a)) =>
 ExOptic act a b (Act act a x) (Act act a y))
-> (x ~> Act act x a)
-> ExOptic act a b (Act act a x) (Act act a y)
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
\\ x ~> Act act x a
f
        ((Ob (Act act x b), Ob y) =>
 ExOptic act a b (Act act a x) (Act act a y))
-> (Act act x b ~> y)
-> ExOptic act a b (Act act a x) (Act act a y)
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
\\ Act act x b ~> y
g

ex2prof
  :: forall {k} {m} {act :: (m, k) +-> k} (a :: k) (b :: k) (s :: k) (t :: k)
   . (MonoidalAction act) => ExOptic act a b s t -> Optic (Strong act) s t a b
ex2prof :: forall {k} {m} {act :: (m, k) +-> k} (a :: k) (b :: k) (s :: k)
       (t :: k).
MonoidalAction act =>
ExOptic act a b s t -> Optic (Strong act) s t a b
ex2prof (ExOptic @x s ~> Act act x a
l Act act x b ~> t
r) = (forall (p :: k +-> k). Strong act p => p a b -> p s t)
-> Optic (Strong act) s t a b
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic ((s ~> Act act x a)
-> (Act act x b ~> t) -> p (Act act x a) (Act act x b) -> p s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p 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 ~> Act act x a
l Act act x b ~> t
r (p (Act act x a) (Act act x b) -> p s t)
-> (p a b -> p (Act act x a) (Act act x b)) -> p a b -> p 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 {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @act @_ @x) ((Ob s, Ob (Act act x a)) => Optic (Strong act) s t a b)
-> (s ~> Act act x a) -> Optic (Strong act) s t a b
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
\\ s ~> Act act x a
l ((Ob (Act act x b), Ob t) => Optic (Strong act) s t a b)
-> (Act act x b ~> t) -> Optic (Strong act) s t a b
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
\\ Act act x b ~> t
r

prof2ex
  :: forall {k} {act} (a :: k) (b :: k) (s :: k) (t :: k)
   . (MonoidalAction act) => Optic (Strong act) s t a b -> ExOptic act a b s t
prof2ex :: forall {m} {k} {act :: (m, k) +-> k} (a :: k) (b :: k) (s :: k)
       (t :: k).
MonoidalAction act =>
Optic (Strong act) s t a b -> ExOptic act a b s t
prof2ex (Optic forall (p :: k +-> k). Strong act p => p a b -> p s t
p2p) = ExOptic act a b a b -> ExOptic act a b s t
forall (p :: k +-> k). Strong act p => p a b -> p s t
p2p (forall (b :: m) (s :: k) (t :: k) (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
forall {k} {m} {act :: (m, k) +-> k} (b :: m) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
ExOptic @Unit (forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
unitorInv @act) (forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
unitor @act))

instance (Profunctor p) => Strong (Rep NoAction) p where
  act :: forall (a :: ()) (x :: k) (y :: k).
Ob a =>
p x y -> p (Act (Rep NoAction) a x) (Act (Rep NoAction) a y)
act = p x y -> p x y
p x y -> p (Rep NoAction % '(a, x)) (Rep NoAction % '(a, y))
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

toIso :: Optic (Strong (Rep NoAction)) s t a b -> Iso s t a b
toIso :: forall {j} (s :: j) (t :: j) (a :: j) (b :: j).
Optic (Strong (Rep NoAction)) s t a b -> Iso s t a b
toIso (Optic forall (p :: j +-> j). Strong (Rep NoAction) p => p a b -> p s t
l) = (forall (p :: j +-> j). Profunctor p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic p a b -> p s t
p a b -> p s t
forall (p :: j +-> j). Profunctor p => p a b -> p s t
forall (p :: j +-> j). Strong (Rep NoAction) p => p a b -> p s t
l

fromIso :: Iso s t a b -> Optic (Strong (Rep NoAction)) s t a b
fromIso :: forall {j} (s :: j) (t :: j) (a :: j) (b :: j).
Iso s t a b -> Optic (Strong (Rep NoAction)) s t a b
fromIso (Optic forall (p :: j +-> j). Profunctor p => p a b -> p s t
l) = (forall (p :: j +-> j). Strong (Rep NoAction) p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic p a b -> p s t
p a b -> p s t
forall (p :: j +-> j). Profunctor p => p a b -> p s t
forall (p :: j +-> j). Strong (Rep NoAction) p => p a b -> p s t
l

type MonoidalOptic (s :: k) (t :: k) a b = Optic (Strong Tensor) s t a b
mkMonoidal
  :: forall {k} (m :: k) (a :: k) (b :: k) s t
   . (Monoidal k, Ob m, Ob a, Ob b) => (s ~> m ** a) -> (m ** b ~> t) -> MonoidalOptic s t a b
mkMonoidal :: forall {k} (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
mkMonoidal s ~> (m ** a)
sma (m ** b) ~> t
mbt = ExOptic Tensor a b s t -> Optic (Strong Tensor) s t a b
forall {k} {m} {act :: (m, k) +-> k} (a :: k) (b :: k) (s :: k)
       (t :: k).
MonoidalAction act =>
ExOptic act a b s t -> Optic (Strong act) s t a b
ex2prof (forall (b :: k) (s :: k) (t :: k) (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act Tensor b a)
-> (Act Tensor b b ~> t) -> ExOptic Tensor a b s t
forall {k} {m} {act :: (m, k) +-> k} (b :: m) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
ExOptic @m s ~> Act Tensor m a
s ~> (m ** a)
sma Act Tensor m b ~> t
(m ** b) ~> t
mbt)

_1 :: forall {k} (a :: k) b c. (SymMonoidal k, Ob a, Ob b, Ob c) => MonoidalOptic (a ** c) (b ** c) a b
_1 :: forall {k} (a :: k) (b :: k) (c :: k).
(SymMonoidal k, Ob a, Ob b, Ob c) =>
MonoidalOptic (a ** c) (b ** c) a b
_1 = forall (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
forall {k} (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
mkMonoidal @c (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @c) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @b)

_2 :: forall {k} (a :: k) b c. (SymMonoidal k, Ob a, Ob b, Ob c) => MonoidalOptic (c ** a) (c ** b) a b
_2 :: forall {k} (a :: k) (b :: k) (c :: k).
(SymMonoidal k, Ob a, Ob b, Ob c) =>
MonoidalOptic (c ** a) (c ** b) a b
_2 = forall (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
forall {k} (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
mkMonoidal @c (forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @c @a) (forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @c @b)

instance (Cartesian k, Ob c) => Strong ProdAction (Rep (Constant c) :: k +-> k) where
  act :: forall (a :: PROD k) (x :: k) (y :: k).
Ob a =>
Rep (Constant c) x y
-> Rep (Constant c) (Act ProdAction a x) (Act ProdAction a y)
act @(PR x) (Rep @b @_ @a x ~> (Constant c @ y)
f) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @x @b (((UN 'PR a && x) ~> (Constant c @ (UN 'PR a && y)))
-> Rep (Constant c) (UN 'PR a && x) (UN 'PR a && y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (x ~> c
x ~> (Constant c @ y)
f (x ~> c) -> ((UN 'PR a && x) ~> x) -> (UN 'PR a && x) ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @x @a)) ((Ob x, Ob c) => Rep (Constant c) (UN 'PR a && x) (UN 'PR a && y))
-> (x ~> c) -> Rep (Constant c) (UN 'PR a && x) (UN 'PR a && y)
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
\\ x ~> c
x ~> (Constant c @ y)
f
instance Strong CoprodAction (Rep (Constant (P.First c)) :: Type +-> Type) where
  act :: forall (a :: COPROD Type) x y.
Ob a =>
Rep (Constant (First c)) x y
-> Rep
     (Constant (First c)) (Act CoprodAction a x) (Act CoprodAction a y)
act (Rep x ~> (Constant (First c) @ y)
f) = (Either (UN 'COPR a) x
 ~> (Constant (First c) @ Either (UN 'COPR a) y))
-> Rep
     (Constant (First c))
     (Either (UN 'COPR a) x)
     (Either (UN 'COPR a) y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((UN 'COPR a -> First c)
-> (x -> First c) -> Either (UN 'COPR a) x -> First c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (First c -> UN 'COPR a -> First c
forall a b. a -> b -> a
const (Maybe c -> First c
forall a. Maybe a -> First a
P.First Maybe c
forall a. Maybe a
Nothing)) x ~> (Constant (First c) @ y)
x -> First c
f)

type Lens (s :: k) (t :: k) a b = Optic (Strong ProdAction) s t a b
mkLens
  :: forall {k} (s :: k) (t :: k) a b
   . (HasProducts k, Ob b) => (s ~> a) -> ((s && b) ~> t) -> Lens s t a b
mkLens :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(HasProducts k, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Lens s t a b
mkLens s ~> a
sa (s && b) ~> t
sbt = ExOptic ProdAction a b s t -> Optic (Strong ProdAction) s t a b
forall {k} {m} {act :: (m, k) +-> k} (a :: k) (b :: k) (s :: k)
       (t :: k).
MonoidalAction act =>
ExOptic act a b s t -> Optic (Strong act) s t a b
ex2prof (forall {k} {m} {act :: (m, k) +-> k} (b :: m) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
forall (b :: PROD k) (s :: k) (t :: k) (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act ProdAction b a)
-> (Act ProdAction b b ~> t) -> ExOptic ProdAction a b s t
ExOptic @(PR s) (s ~> s
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (s ~> s) -> (s ~> a) -> s ~> (s && a)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& s ~> a
sa) Act ProdAction ('PR s) b ~> t
(s && b) ~> t
sbt) ((Ob s, Ob a) => Optic (Strong ProdAction) s t a b)
-> (s ~> a) -> Optic (Strong ProdAction) s t a b
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
\\ s ~> a
sa

type VLLens s t a b = forall f. (P.Functor f) => (a -> f b) -> s -> f t
toVLLens :: Lens s t a b -> VLLens s t a b
toVLLens :: forall s t a b. Lens s t a b -> VLLens s t a b
toVLLens (Optic forall (p :: Type +-> Type). Strong ProdAction p => p a b -> p s t
l) = (Prelude f t -> f t
forall (f :: Type -> Type) a. Prelude f a -> f a
unPrelude (Prelude f t -> f t) -> (s -> Prelude f t) -> s -> f 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
.) ((s -> Prelude f t) -> s -> f t)
-> ((a -> f b) -> s -> Prelude f t) -> (a -> f b) -> s -> f 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
. Star' ('NT (Prelude f)) s t -> s ~> Prelude f t
Star' ('NT (Prelude f)) s t -> s -> Prelude f t
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Star' ('NT f) a b -> a ~> f b
unStar (Star' ('NT (Prelude f)) s t -> s -> Prelude f t)
-> ((a -> f b) -> Star' ('NT (Prelude f)) s t)
-> (a -> f b)
-> s
-> Prelude f 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
. Star' ('NT (Prelude f)) a b -> Star' ('NT (Prelude f)) s t
Star' ('NT (Prelude f)) a b -> Star' ('NT (Prelude f)) s t
forall (p :: Type +-> Type). Strong ProdAction p => p a b -> p s t
l (Star' ('NT (Prelude f)) a b -> Star' ('NT (Prelude f)) s t)
-> ((a -> f b) -> Star' ('NT (Prelude f)) a b)
-> (a -> f b)
-> Star' ('NT (Prelude f)) 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
. (a ~> Prelude f b) -> Star' ('NT (Prelude f)) a b
(a -> Prelude f b) -> Star' ('NT (Prelude f)) a b
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a -> Prelude f b) -> Star' ('NT (Prelude f)) a b)
-> ((a -> f b) -> a -> Prelude f b)
-> (a -> f b)
-> Star' ('NT (Prelude f)) a b
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
. (f b -> Prelude f b
forall (f :: Type -> Type) a. f a -> Prelude f a
Prelude (f b -> Prelude f b) -> (a -> f b) -> a -> Prelude f b
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
.)

fromVLLens :: VLLens s t a b -> Lens s t a b
fromVLLens :: forall s t a b. VLLens s t a b -> Lens s t a b
fromVLLens VLLens s t a b
f = (s ~> a) -> ((s && b) ~> t) -> Lens s t a b
forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(HasProducts k, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Lens s t a b
mkLens (Const a t -> a
forall {k} a (b :: k). Const a b -> a
getConst (Const a t -> a) -> (s -> Const a t) -> s -> a
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
. (a -> Const a b) -> s -> Const a t
VLLens s t a b
f a -> Const a b
forall {k} a (b :: k). a -> Const a b
Const) ((s -> b -> t) -> (s, b) -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry ((a -> b -> b) -> s -> b -> t
VLLens s t a b
f ((b -> b) -> a -> b -> b
forall a b. a -> b -> a
const b -> b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)))

type Prism (s :: k) t a b = Optic (Strong CoprodAction) s t a b
mkPrism :: forall {k} (s :: k) (t :: k) a b. (HasCoproducts k, Ob a) => (s ~> (t || a)) -> (b ~> t) -> Prism s t a b
mkPrism :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(HasCoproducts k, Ob a) =>
(s ~> (t || a)) -> (b ~> t) -> Prism s t a b
mkPrism s ~> (t || a)
sta b ~> t
bt = ExOptic CoprodAction a b s t -> Optic (Strong CoprodAction) s t a b
forall {k} {m} {act :: (m, k) +-> k} (a :: k) (b :: k) (s :: k)
       (t :: k).
MonoidalAction act =>
ExOptic act a b s t -> Optic (Strong act) s t a b
ex2prof (forall {k} {m} {act :: (m, k) +-> k} (b :: m) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
forall (b :: COPROD k) (s :: k) (t :: k) (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act CoprodAction b a)
-> (Act CoprodAction b b ~> t) -> ExOptic CoprodAction a b s t
ExOptic @(COPR t) s ~> Act CoprodAction ('COPR t) a
s ~> (t || a)
sta (t ~> t
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (t ~> t) -> (b ~> t) -> (t || b) ~> t
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
||| b ~> t
bt)) ((Ob b, Ob t) => Optic (Strong CoprodAction) s t a b)
-> (b ~> t) -> Optic (Strong CoprodAction) s t a b
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 ~> t
bt

type Traversal s t a b = Optic Dist.StrongDistributiveProfunctor s t a b
traversing :: forall t a b. (Dist.Traversable t, Representable t, Ob a, Ob b) => Traversal (t % a) (t % b) a b
traversing :: forall {j} (t :: j +-> j) (a :: j) (b :: j).
(Traversable t, Representable t, Ob a, Ob b) =>
Traversal (t % a) (t % b) a b
traversing = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> j) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @t @a ((Ob (t % a) => Traversal (t % a) (t % b) a b)
 -> Traversal (t % a) (t % b) a b)
-> (Ob (t % a) => Traversal (t % a) (t % b) a b)
-> Traversal (t % a) (t % b) a b
forall a b. (a -> b) -> a -> b
$ forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> j) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @t @b ((Ob (t % b) => Traversal (t % a) (t % b) a b)
 -> Traversal (t % a) (t % b) a b)
-> (Ob (t % b) => Traversal (t % a) (t % b) a b)
-> Traversal (t % a) (t % b) a b
forall a b. (a -> b) -> a -> b
$ (forall (p :: j +-> j).
 StrongDistributiveProfunctor p =>
 p a b -> p (t % a) (t % b))
-> Traversal (t % a) (t % b) a b
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic (forall {k} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
forall (t :: j +-> j) (p :: j +-> j) (a :: j) (b :: j).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
Dist.repTraverse @t)

instance (Dist.StrongDistributiveProfunctor p) => Strong TravAction p where
  act :: forall (a :: TravSub k) (x :: k) (y :: k).
Ob a =>
p x y -> p (Act TravAction a x) (Act TravAction a y)
act @(SUB (E f)) = forall {k} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
forall (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
Dist.repTraverse @f

toTraversal :: Optic (Strong TravAction) s t a b -> Traversal s t a b
toTraversal :: forall {j} (s :: j) (t :: j) (a :: j) (b :: j).
Optic (Strong TravAction) s t a b -> Traversal s t a b
toTraversal (Optic forall (p :: j +-> j). Strong TravAction p => p a b -> p s t
l) = (forall (p :: j +-> j).
 StrongDistributiveProfunctor p =>
 p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic p a b -> p s t
p a b -> p s t
forall (p :: j +-> j). Strong TravAction p => p a b -> p s t
forall (p :: j +-> j).
StrongDistributiveProfunctor p =>
p a b -> p s t
l

type HaskTraversal s t a b = Optic (Dist.StrongDistributiveProfunctor :&&: Representable) s t a b
haskTraversing :: (P.Traversable t) => HaskTraversal (t a) (t b) a b
haskTraversing :: forall (t :: Type -> Type) a b.
Traversable t =>
HaskTraversal (t a) (t b) a b
haskTraversing @t =
  (forall (p :: Type +-> Type).
 (:&&:) StrongDistributiveProfunctor Representable p =>
 p a b -> p (t a) (t b))
-> Optic_ (OPT a b) (OPT (t a) (t b))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic
    ( (t a ~> (p % t b)) -> p (t a) (t b)
(t a -> (p % t b)) -> p (t a) (t b)
forall b a. Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate
        ((t a -> (p % t b)) -> p (t a) (t b))
-> (p a b -> t a -> (p % t b)) -> p a b -> p (t a) (t b)
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
. ((FromProfunctor p () (t b) -> () -> p % t b)
-> () -> FromProfunctor p () (t b) -> p % t b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (p () (t b) -> () ~> (p % t b)
p () (t b) -> () -> p % t b
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 (p () (t b) -> () -> p % t b)
-> (FromProfunctor p () (t b) -> p () (t b))
-> FromProfunctor p () (t b)
-> ()
-> p % t b
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
. FromProfunctor p () (t b) -> p () (t b)
forall {k1} {k2} (p :: k1 -> k2 -> Type) (a :: k1) (b :: k2).
FromProfunctor p a b -> p a b
unFromProfunctor) () (FromProfunctor p () (t b) -> p % t b)
-> (t a -> FromProfunctor p () (t b)) -> t a -> (p % t b)
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
.)
        ((t a -> FromProfunctor p () (t b)) -> t a -> (p % t b))
-> (p a b -> t a -> FromProfunctor p () (t b))
-> p a b
-> t a -> (p % t b)
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 (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
P.traverse @t
        ((a -> FromProfunctor p () b) -> t a -> FromProfunctor p () (t b))
-> (p a b -> a -> FromProfunctor p () b)
-> p a b
-> t a
-> FromProfunctor p () (t b)
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
. (\p a b
p a
a -> p () b -> FromProfunctor p () b
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> FromProfunctor p a b
FromProfunctor ((() ~> a) -> p a b -> p () b
forall c a b. (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (a -> () -> a
forall a b. a -> b -> a
const a
a) p a b
p))
    )

class (Monad m) => Algebra m a where algebra :: m a -> a
instance (Monad m) => Algebra m (m a) where algebra :: m (m a) -> m a
algebra = (m (m a) -> (m a -> m a) -> m a
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= m a -> m a
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
instance (Monad m) => Algebra m () where algebra :: m () -> ()
algebra m ()
_ = ()
instance (Monad m, Algebra m a, Algebra m b) => Algebra m (a, b) where
  algebra :: m (a, b) -> (a, b)
algebra m (a, b)
mab = (m a -> a
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a, b) -> a) -> m (a, b) -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (a && b) ~> a
(a, b) -> a
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall a b. (Ob a, Ob b) => (a && b) ~> a
fst m (a, b)
mab), m b -> b
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a, b) -> b) -> m (a, b) -> m b
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (a && b) ~> b
(a, b) -> b
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall a b. (Ob a, Ob b) => (a && b) ~> b
snd m (a, b)
mab))

type AlgAction m = SubAction (Algebra m) Tensor
type AlgebraicLens m s t a b = Optic (Strong (AlgAction m)) s t a b
mkAlgebraicLens :: forall m s t a b. (Monad m) => (s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
mkAlgebraicLens :: forall (m :: Type -> Type) s t a b.
Monad m =>
(s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
mkAlgebraicLens s -> a
v m s -> b -> t
u = ExOptic (AlgAction m) a b s t
-> Optic (Strong (AlgAction m)) s t a b
forall {k} {m} {act :: (m, k) +-> k} (a :: k) (b :: k) (s :: k)
       (t :: k).
MonoidalAction act =>
ExOptic act a b s t -> Optic (Strong act) s t a b
ex2prof ((s ~> Act (AlgAction m) (SUB (m s)) a)
-> (Act (AlgAction m) (SUB (m s)) b ~> t)
-> ExOptic (AlgAction m) a b s t
forall {k} {m} {act :: (m, k) +-> k} (b :: m) (s :: k) (t :: k)
       (a :: k) (b :: k).
(Ob a, Ob b, Ob b) =>
(s ~> Act act b a) -> (Act act b b ~> t) -> ExOptic act a b s t
ExOptic (\s
s -> (forall (m :: Type -> Type) a. Monad m => a -> m a
return @m s
s, s -> a
v s
s)) ((m s -> b -> t) -> (m s, b) -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry m s -> b -> t
u))

data Previewing a (b :: Type) s (t :: Type) where
  Previewing :: {forall s a b t. Previewing a b s t -> s -> Maybe a
unPreview :: s -> Maybe a} -> Previewing a b s t
instance Profunctor (Previewing a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Previewing a b a b -> Previewing a b c d
dimap c ~> a
l b ~> d
_ (Previewing a -> Maybe a
f) = (c -> Maybe a) -> Previewing a b c d
forall s a b t. (s -> Maybe a) -> Previewing a b s t
Previewing (a -> Maybe a
f (a -> Maybe a) -> (c -> a) -> c -> Maybe a
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
. c ~> a
c -> a
l)
  (Ob a, Ob b) => r
r \\ :: forall a b r. ((Ob a, Ob b) => r) -> Previewing a b a b -> r
\\ Previewing a -> Maybe a
f = r
(Ob a, Ob b) => r
(Ob a, Ob (Maybe a)) => r
r ((Ob a, Ob (Maybe a)) => r) -> (a -> Maybe a) -> r
forall a b 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 -> Maybe a
f
instance Strong CoprodAction (Previewing a b) where
  act :: forall (a :: COPROD Type) x y.
Ob a =>
Previewing a b x y
-> Previewing a b (Act CoprodAction a x) (Act CoprodAction a y)
act (Previewing x -> Maybe a
f) = (Either (UN 'COPR a) x -> Maybe a)
-> Previewing a b (Either (UN 'COPR a) x) (Either (UN 'COPR a) y)
forall s a b t. (s -> Maybe a) -> Previewing a b s t
Previewing ((UN 'COPR a -> Maybe a)
-> (x -> Maybe a) -> Either (UN 'COPR a) x -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe a -> UN 'COPR a -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) x -> Maybe a
f)
instance Strong ProdAction (Previewing a b) where
  act :: forall (a :: PROD Type) x y.
Ob a =>
Previewing a b x y
-> Previewing a b (Act ProdAction a x) (Act ProdAction a y)
act (Previewing x -> Maybe a
f) = ((UN 'PR a, x) -> Maybe a)
-> Previewing a b (UN 'PR a, x) (UN 'PR a, y)
forall s a b t. (s -> Maybe a) -> Previewing a b s t
Previewing (x -> Maybe a
f (x -> Maybe a) -> ((UN 'PR a, x) -> x) -> (UN 'PR a, x) -> Maybe a
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
. (UN 'PR a && x) ~> x
(UN 'PR a, x) -> x
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall a b. (Ob a, Ob b) => (a && b) ~> b
snd)

infixl 8 ?.
(?.)
  :: s -> (Previewing a b a b -> Previewing a b s t) -> Maybe a
?. :: forall s a b t.
s -> (Previewing a b a b -> Previewing a b s t) -> Maybe a
(?.) s
s Previewing a b a b -> Previewing a b s t
l = Previewing a b s t -> s -> Maybe a
forall s a b t. Previewing a b s t -> s -> Maybe a
unPreview (Previewing a b a b -> Previewing a b s t
l (Previewing a b a b -> Previewing a b s t)
-> Previewing a b a b -> Previewing a b s t
forall a b. (a -> b) -> a -> b
$ (a -> Maybe a) -> Previewing a b a b
forall s a b t. (s -> Maybe a) -> Previewing a b s t
Previewing a -> Maybe a
forall a. a -> Maybe a
Just) s
s

type KlCat m = KLEISLI (Star (Prelude m))
data Updating a b s t where
  Update
    :: {forall b s (m :: Type -> Type) t a.
Updating ('KL a) ('KL b) ('KL s) ('KL t) -> b -> s -> m t
unUpdate :: b -> s -> m t} -> Updating (KL a :: KlCat m) (KL b :: KlCat m) (KL s :: KlCat m) (KL t :: KlCat m)
instance (Monad m) => Profunctor (Updating a b :: KlCat m +-> KlCat m) where
  dimap :: forall (c :: KlCat m) (a :: KlCat m) (b :: KlCat m) (d :: KlCat m).
(c ~> a) -> (b ~> d) -> Updating a b a b -> Updating a b c d
dimap (Kleisli (Star a1 ~> Prelude m b1
l)) (Kleisli (Star a1 ~> Prelude m b1
r)) (Update b -> s -> m t
u) = (b -> a1 -> m b1) -> Updating ('KL a) ('KL b) ('KL a1) ('KL b1)
forall b s (m :: Type -> Type) t a.
(b -> s -> m t) -> Updating ('KL a) ('KL b) ('KL s) ('KL t)
Update (\b
b a1
x -> do y <- Prelude m s -> m s
forall (f :: Type -> Type) a. Prelude f a -> f a
unPrelude (a1 ~> Prelude m b1
a1 -> Prelude m s
l a1
x); z <- u b y; unPrelude (r z))
  (Ob a, Ob b) => r
r \\ :: forall (a :: KlCat m) (b :: KlCat m) r.
((Ob a, Ob b) => r) -> Updating a b a b -> r
\\ Update b -> s -> m t
u = r
(Ob b, Ob (s -> m t)) => r
(Ob a, Ob b) => r
r ((Ob b, Ob (s -> m t)) => r) -> (b -> s -> m t) -> r
forall a b 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 -> s -> m t
u
instance (Monad m) => Strong Tensor (Updating a b :: KlCat m +-> KlCat m) where
  act :: forall (a :: KlCat m) (x :: KlCat m) (y :: KlCat m).
Ob a =>
Updating a b x y -> Updating a b (Act Tensor a x) (Act Tensor a y)
act (Update b -> s -> m t
u) = (b -> (UN 'KL a, s) -> m (UN 'KL a, t))
-> Updating ('KL a) ('KL b) ('KL (UN 'KL a, s)) ('KL (UN 'KL a, t))
forall b s (m :: Type -> Type) t a.
(b -> s -> m t) -> Updating ('KL a) ('KL b) ('KL s) ('KL t)
Update (\b
b (UN 'KL a
a, s
x) -> (UN 'KL a
a,) (t -> (UN 'KL a, t)) -> m t -> m (UN 'KL a, t)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
`P.fmap` b -> s -> m t
u b
b s
x)

mupdate
  :: (Monad m)
  => (Updating (KL a :: KlCat m) (KL b :: KlCat m) (KL a) (KL b) -> Updating (KL a) (KL b) (KL s :: KlCat m) (KL t :: KlCat m))
  -> b
  -> s
  -> m t
mupdate :: forall (m :: Type -> Type) a b s t.
Monad m =>
(Updating ('KL a) ('KL b) ('KL a) ('KL b)
 -> Updating ('KL a) ('KL b) ('KL s) ('KL t))
-> b -> s -> m t
mupdate Updating ('KL a) ('KL b) ('KL a) ('KL b)
-> Updating ('KL a) ('KL b) ('KL s) ('KL t)
f = Updating ('KL a) ('KL b) ('KL s) ('KL t) -> b -> s -> m t
forall b s (m :: Type -> Type) t a.
Updating ('KL a) ('KL b) ('KL s) ('KL t) -> b -> s -> m t
unUpdate (Updating ('KL a) ('KL b) ('KL s) ('KL t) -> b -> s -> m t)
-> Updating ('KL a) ('KL b) ('KL s) ('KL t) -> b -> s -> m t
forall a b. (a -> b) -> a -> b
$ Updating ('KL a) ('KL b) ('KL a) ('KL b)
-> Updating ('KL a) ('KL b) ('KL s) ('KL t)
f ((b -> a -> m b) -> Updating ('KL a) ('KL b) ('KL a) ('KL b)
forall b s (m :: Type -> Type) t a.
(b -> s -> m t) -> Updating ('KL a) ('KL b) ('KL s) ('KL t)
Update (\b
b a
_ -> b -> m b
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return b
b))

newtype Replacing a b s t = Replace {forall a b s t. Replacing a b s t -> (a -> b) -> s -> t
unReplace :: (a -> b) -> (s -> t)}
instance Profunctor (Replacing a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Replacing a b a b -> Replacing a b c d
dimap c ~> a
l b ~> d
r (Replace (a -> b) -> a -> b
f) = ((a -> b) -> c -> d) -> Replacing a b c d
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
ab -> b ~> d
b -> d
r (b -> d) -> (c -> b) -> c -> d
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
. (a -> b) -> a -> b
f a -> b
ab (a -> b) -> (c -> a) -> c -> b
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
. c ~> a
c -> a
l)
instance Strong Tensor (Replacing a b) where
  act :: forall a x y.
Ob a =>
Replacing a b x y
-> Replacing a b (Act (Rep MultRep) a x) (Act (Rep MultRep) a y)
act (Replace (a -> b) -> x -> y
f) = ((a -> b) -> (a, x) -> (a, y)) -> Replacing a b (a, x) (a, y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
u -> (x ~> y) -> (a, x) ~> (a, y)
forall a b. (a ~> b) -> (a, a) ~> (a, b)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map ((a -> b) -> x -> y
f a -> b
u))
instance Strong CoprodAction (Replacing a b) where
  act :: forall (a :: COPROD Type) x y.
Ob a =>
Replacing a b x y
-> Replacing a b (Act CoprodAction a x) (Act CoprodAction a y)
act (Replace (a -> b) -> x -> y
f) = ((a -> b) -> Either (UN 'COPR a) x -> Either (UN 'COPR a) y)
-> Replacing a b (Either (UN 'COPR a) x) (Either (UN 'COPR a) y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
u -> (x ~> y) -> Either (UN 'COPR a) x ~> Either (UN 'COPR a) y
forall a b.
(a ~> b) -> Either (UN 'COPR a) a ~> Either (UN 'COPR a) b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map ((a -> b) -> x -> y
f a -> b
u))
instance Strong ApplyAction (Replacing a b) where
  act :: forall (a :: Type -> Type) x y.
Ob a =>
Replacing a b x y
-> Replacing a b (Act ApplyAction a x) (Act ApplyAction a y)
act (Replace (a -> b) -> x -> y
f) = ((a -> b) -> a x -> a y) -> Replacing a b (a x) (a y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
u -> (x ~> y) -> a x ~> a y
forall a b. (a ~> b) -> a a ~> a b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map ((a -> b) -> x -> y
f a -> b
u))

infixl 8 %~
(%~) :: (Replacing a b a b -> Replacing a b s t) -> (a -> b) -> (s -> t)
%~ :: forall a b s t.
(Replacing a b a b -> Replacing a b s t) -> (a -> b) -> s -> t
(%~) Replacing a b a b -> Replacing a b s t
l = Replacing a b s t -> (a -> b) -> s -> t
forall a b s t. Replacing a b s t -> (a -> b) -> s -> t
unReplace (Replacing a b a b -> Replacing a b s t
l (Replacing a b a b -> Replacing a b s t)
-> Replacing a b a b -> Replacing a b s t
forall a b. (a -> b) -> a -> b
$ ((a -> b) -> a -> b) -> Replacing a b a b
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (a -> b) -> a -> b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

infixl 8 .~
(.~) :: (Replacing a b a b -> Replacing a b s t) -> b -> s -> t
Replacing a b a b -> Replacing a b s t
l .~ :: forall a b s t.
(Replacing a b a b -> Replacing a b s t) -> b -> s -> t
.~ b
b = Replacing a b a b -> Replacing a b s t
l (Replacing a b a b -> Replacing a b s t) -> (a -> b) -> s -> t
forall a b s t.
(Replacing a b a b -> Replacing a b s t) -> (a -> b) -> s -> t
%~ b -> a -> b
forall a b. a -> b -> a
const b
b

newtype Classifying m a b s t = Classifying
  {forall {k} (m :: Type -> Type) (a :: k) b s t.
Classifying m a b s t -> Monad m => m s -> b -> t
unClassify :: (Monad m) => m s -> b -> t}
instance (Monad m) => Profunctor (Classifying m a b) where
  dimap :: forall c a b d.
(c ~> a)
-> (b ~> d) -> Classifying m a b a b -> Classifying m a b c d
dimap c ~> a
l b ~> d
r (Classifying Monad m => m a -> b -> b
f) = (Monad m => m c -> b -> d) -> Classifying m a b c d
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying (\m c
u -> b ~> d
b -> d
r (b -> d) -> (b -> b) -> b -> d
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
. m a -> b -> b
Monad m => m a -> b -> b
f ((c -> a) -> m c -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap c ~> a
c -> a
l m c
u))
instance (Monad m) => Strong (AlgAction m) (Classifying m a b) where
  act :: forall (a :: SUBCAT (Algebra m)) x y.
Ob a =>
Classifying m a b x y
-> Classifying
     m a b (Act (AlgAction m) a x) (Act (AlgAction m) a y)
act (Classifying Monad m => m x -> b -> y
f) = (Monad m => m (UN SUB a, x) -> b -> (UN SUB a, y))
-> Classifying m a b (UN SUB a, x) (UN SUB a, y)
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying (\m (UN SUB a, x)
m b
b -> (m (UN SUB a) -> UN SUB a
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((UN SUB a, x) -> UN SUB a) -> m (UN SUB a, x) -> m (UN SUB a)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (UN SUB a && x) ~> UN SUB a
(UN SUB a, x) -> UN SUB a
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall a b. (Ob a, Ob b) => (a && b) ~> a
fst m (UN SUB a, x)
m), m x -> b -> y
Monad m => m x -> b -> y
f (((UN SUB a, x) -> x) -> m (UN SUB a, x) -> m x
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (UN SUB a && x) ~> x
(UN SUB a, x) -> x
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall a b. (Ob a, Ob b) => (a && b) ~> b
snd m (UN SUB a, x)
m) b
b))

infixl 8 .?
(.?) :: (Monad m) => (Classifying m a b a b -> Classifying m a b s t) -> b -> m s -> t
.? :: forall (m :: Type -> Type) a b s t.
Monad m =>
(Classifying m a b a b -> Classifying m a b s t) -> b -> m s -> t
(.?) Classifying m a b a b -> Classifying m a b s t
l b
b m s
ms = Classifying m a b s t -> Monad m => m s -> b -> t
forall {k} (m :: Type -> Type) (a :: k) b s t.
Classifying m a b s t -> Monad m => m s -> b -> t
unClassify (Classifying m a b a b -> Classifying m a b s t
l (Classifying m a b a b -> Classifying m a b s t)
-> Classifying m a b a b -> Classifying m a b s t
forall a b. (a -> b) -> a -> b
$ (Monad m => m a -> b -> b) -> Classifying m a b a b
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying ((b -> b) -> m a -> b -> b
forall a b. a -> b -> a
const b -> b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)) m s
ms b
b

instance (Strong act p) => Costrong act (Re p s t) where
  coact :: forall (a :: m) (x :: k1) (y :: k1).
(Ob a, Ob x, Ob y) =>
Re p s t (Act act a x) (Act act a y) -> Re p s t x y
coact @a (Re p (Act act a y) (Act act a x) -> p t s
f) = (p y x -> p t s) -> Re p s t x y
forall {k1} {k} (a :: k1) (b :: k) (p :: k -> k1 -> Type) (t :: k)
       (s :: k1).
(Ob a, Ob b) =>
(p b a -> p t s) -> Re p s t a b
Re (p (Act act a y) (Act act a x) -> p t s
f (p (Act act a y) (Act act a x) -> p t s)
-> (p y x -> p (Act act a y) (Act act a x)) -> p y x -> p t s
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 {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, k1) +-> k1) (p :: k1 +-> k1) (a :: m) (x :: k1)
       (y :: k1).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @act @_ @a)
instance (Costrong act p) => Strong act (Re p s t) where
  act :: forall (a :: m) (x :: k1) (y :: k1).
Ob a =>
Re p s t x y -> Re p s t (Act act a x) (Act act a y)
act @a @x @y (Re p y x -> p t s
f) = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: (m, k1) +-> k1) (a :: (m, k1)) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @act @'(a, x) ((Ob (act % '(a, x)) => Re p s t (act % '(a, x)) (Act act a y))
 -> Re p s t (act % '(a, x)) (Act act a y))
-> (Ob (act % '(a, x)) => Re p s t (act % '(a, x)) (Act act a y))
-> Re p s t (act % '(a, x)) (Act act a y)
forall a b. (a -> b) -> a -> b
$ forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: (m, k1) +-> k1) (a :: (m, k1)) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @act @'(a, y) ((Ob (Act act a y) => Re p s t (act % '(a, x)) (Act act a y))
 -> Re p s t (act % '(a, x)) (Act act a y))
-> (Ob (Act act a y) => Re p s t (act % '(a, x)) (Act act a y))
-> Re p s t (act % '(a, x)) (Act act a y)
forall a b. (a -> b) -> a -> b
$ (p (Act act a y) (act % '(a, x)) -> p t s)
-> Re p s t (act % '(a, x)) (Act act a y)
forall {k1} {k} (a :: k1) (b :: k) (p :: k -> k1 -> Type) (t :: k)
       (s :: k1).
(Ob a, Ob b) =>
(p b a -> p t s) -> Re p s t a b
Re (p y x -> p t s
f (p y x -> p t s)
-> (p (Act act a y) (act % '(a, x)) -> p y x)
-> p (Act act a y) (act % '(a, x))
-> p t s
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 {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (m, k1) +-> k1) (p :: k1 +-> k1) (a :: m) (x :: k1)
       (y :: k1).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @act @_ @a)
instance InvertableOptic (Strong t) (Costrong t)
instance InvertableOptic (Costrong t) (Strong t)

v1Optic :: Traversal (G.V1 a) (G.V1 a') a a'
v1Optic :: forall a a'. Traversal (V1 a) (V1 a') a a'
v1Optic = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p (V1 a) (V1 a'))
-> Optic_ (OPT a a') (OPT (V1 a) (V1 a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
_ -> (V1 a ~> Void)
-> (Void ~> V1 a') -> p Void Void -> p (V1 a) (V1 a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 (\case {}) (\case {}) p Void Void
p InitialObject InitialObject
forall {j} {k} (p :: j +-> k).
MonoidalProfunctor (Coprod p) =>
p InitialObject InitialObject
nil

u1Optic :: Traversal (G.U1 a) (G.U1 a') a a'
u1Optic :: forall a a'. Traversal (U1 a) (U1 a') a a'
u1Optic = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p (U1 a) (U1 a'))
-> Optic_ (OPT a a') (OPT (U1 a) (U1 a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
_ -> (U1 a ~> ()) -> (() ~> U1 a') -> p () () -> p (U1 a) (U1 a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 (() -> U1 a -> ()
forall a b. a -> b -> a
const ()) (\() -> U1 a'
forall k (p :: k). U1 p
G.U1) p () ()
p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one

par1Optic :: Traversal (G.Par1 a) (G.Par1 a') a a'
par1Optic :: forall a a'. Traversal (Par1 a) (Par1 a') a a'
par1Optic = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p (Par1 a) (Par1 a'))
-> Optic_ (OPT a a') (OPT (Par1 a) (Par1 a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic ((Par1 a ~> a) -> (a' ~> Par1 a') -> p a a' -> p (Par1 a) (Par1 a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 Par1 a ~> a
Par1 a -> a
forall p. Par1 p -> p
G.unPar1 a' ~> Par1 a'
a' -> Par1 a'
forall p. p -> Par1 p
G.Par1)

rec1Optic :: Traversal (f a) (f a') a a' -> Traversal (G.Rec1 f a) (G.Rec1 f a') a a'
rec1Optic :: forall (f :: Type -> Type) a a'.
Traversal (f a) (f a') a a'
-> Traversal (Rec1 f a) (Rec1 f a') a a'
rec1Optic (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p (Rec1 f a) (Rec1 f a'))
-> Optic_ (OPT a a') (OPT (Rec1 f a) (Rec1 f a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> (Rec1 f a ~> s)
-> (t ~> Rec1 f a') -> p s t -> p (Rec1 f a) (Rec1 f a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 Rec1 f a ~> s
Rec1 f a -> f a
forall k (f :: k -> Type) (p :: k). Rec1 f p -> f p
G.unRec1 t ~> Rec1 f a'
f a' -> Rec1 f a'
forall k (f :: k -> Type) (p :: k). f p -> Rec1 f p
G.Rec1 (p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l p a a'
p a b
p)

m1Optic :: Traversal (f a) (f a') a a' -> Traversal (G.M1 i k f a) (G.M1 i k f a') a a'
m1Optic :: forall (f :: Type -> Type) a a' i (k :: Meta).
Traversal (f a) (f a') a a'
-> Traversal (M1 i k f a) (M1 i k f a') a a'
m1Optic (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p (M1 i k f a) (M1 i k f a'))
-> Optic_ (OPT a a') (OPT (M1 i k f a) (M1 i k f a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> (M1 i k f a ~> s)
-> (t ~> M1 i k f a') -> p s t -> p (M1 i k f a) (M1 i k f a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 M1 i k f a ~> s
M1 i k f a -> f a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
G.unM1 t ~> M1 i k f a'
f a' -> M1 i k f a'
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
G.M1 (p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l p a a'
p a b
p)

k1Optic :: forall i k a a'. Traversal (G.K1 i k a) (G.K1 i k a') a a'
k1Optic :: forall i k a a'. Traversal (K1 i k a) (K1 i k a') a a'
k1Optic = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p (K1 i k a) (K1 i k a'))
-> Optic_ (OPT a a') (OPT (K1 i k a) (K1 i k a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
_ -> (K1 i k a ~> k)
-> (k ~> K1 i k a') -> p k k -> p (K1 i k a) (K1 i k a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 K1 i k a ~> k
K1 i k a -> k
forall k i c (p :: k). K1 i c p -> c
G.unK1 k ~> K1 i k a'
k -> K1 i k a'
forall k i c (p :: k). c -> K1 i c p
G.K1 p k k
forall {k} {p :: k +-> k} (a :: k).
(MonStrong p, MonoidalProfunctor p, Ob a) =>
p a a
strongId

plusOptic
  :: Traversal (p a) (p a') a a'
  -> Traversal (q a) (q a') a a'
  -> Traversal ((p G.:+: q) a) ((p G.:+: q) a') a a'
plusOptic :: forall (p :: Type -> Type) a a' (q :: Type -> Type).
Traversal (p a) (p a') a a'
-> Traversal (q a) (q a') a a'
-> Traversal ((:+:) p q a) ((:+:) p q a') a a'
plusOptic (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p ((:+:) p q a) ((:+:) p q a'))
-> Optic_ (OPT a a') (OPT ((:+:) p q a) ((:+:) p q a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> ((:+:) p q a ~> Either (p a) (q a))
-> (Either (p a') (q a') ~> (:+:) p q a')
-> p (Either (p a) (q a)) (Either (p a') (q a'))
-> p ((:+:) p q a) ((:+:) p q a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 (\case G.L1 p a
f -> p a -> Either (p a) (q a)
forall a b. a -> Either a b
Left p a
f; G.R1 q a
f -> q a -> Either (p a) (q a)
forall a b. b -> Either a b
Right q a
f) ((p a' -> (:+:) p q a')
-> (q a' -> (:+:) p q a') -> Either (p a') (q a') -> (:+:) p q a'
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either p a' -> (:+:) p q a'
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
G.L1 q a' -> (:+:) p q a'
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
G.R1) (p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l p a a'
p a b
p p s t -> p s t -> p (s || s) (t || t)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r p a a'
p a b
p)

multOptic
  :: Traversal (p a) (p a') a a'
  -> Traversal (q a) (q a') a a'
  -> Traversal ((p G.:*: q) a) ((p G.:*: q) a') a a'
multOptic :: forall (p :: Type -> Type) a a' (q :: Type -> Type).
Traversal (p a) (p a') a a'
-> Traversal (q a) (q a') a a'
-> Traversal ((:*:) p q a) ((:*:) p q a') a a'
multOptic (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p ((:*:) p q a) ((:*:) p q a'))
-> Optic_ (OPT a a') (OPT ((:*:) p q a) ((:*:) p q a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> ((:*:) p q a ~> (p a, q a))
-> ((p a', q a') ~> (:*:) p q a')
-> p (p a, q a) (p a', q a')
-> p ((:*:) p q a) ((:*:) p q a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 a
f G.:*: q a
g) -> (p a
f, q a
g)) ((p a' -> q a' -> (:*:) p q a') -> (p a', q a') -> (:*:) p q a'
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry p a' -> q a' -> (:*:) p q a'
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(G.:*:)) (p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l p a a'
p a b
p p s t -> p s t -> p (s ** s) (t ** t)
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)
** p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r p a a'
p a b
p)

compOptic
  :: Traversal (p (q a)) (p (q a')) (q a) (q a')
  -> Traversal (q a) (q a') a a'
  -> Traversal ((p G.:.: q) a) ((p G.:.: q) a') a a'
compOptic :: forall (p :: Type -> Type) (q :: Type -> Type) a a'.
Traversal (p (q a)) (p (q a')) (q a) (q a')
-> Traversal (q a) (q a') a a'
-> Traversal ((:.:) p q a) ((:.:) p q a') a a'
compOptic (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor p =>
 p a a' -> p ((:.:) p q a) ((:.:) p q a'))
-> Optic_ (OPT a a') (OPT ((:.:) p q a) ((:.:) p q a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). c p => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> ((:.:) p q a ~> s)
-> (t ~> (:.:) p q a') -> p s t -> p ((:.:) p q a) ((:.:) p q a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p 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 q a ~> s
(:.:) p q a -> p (q a)
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
G.unComp1 t ~> (:.:) p q a'
p (q a') -> (:.:) p q a'
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
G.Comp1 (p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
l (p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r p a a'
p a b
p))