{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __lens__: the optic for the categorical product, with legs
--
-- > Lens s t a b = (s ~> a, (s && b) ~> t)
--
-- witnessed by @'Rep'@\/@'Corep'@ @('Product' s)@ ('LensRes' \/ 'putP') -- the product residual is
-- the whole source @s@. A lens both views and sets, sitting below 'Proarrow.Optic.Getter.Getter'
-- and 'Proarrow.Optic.AffineTraversal.AffineTraversal' in the lattice. Build with 'lens' (or from
-- the van-Laarhoven form with 'lensVL'), eliminate to the two legs with 'withLens', via the
-- 'Shop' carrier.
module Proarrow.Optic.Lens where

import Data.Functor.Const (Const (..))
import Prelude (const)
import Prelude qualified as P

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Functor (Functor (map), Prelude (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), Product, first)
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( CompactFlavor
  , ExOptic (..)
  , FLAVOR
  , Optic
  , Optic_ (..)
  , Prostrong (..)
  , SubFlavor (..)
  , ex2prof
  )
import Proarrow.Optic.AffineFold (AffineFoldRes)
import Proarrow.Optic.AffineTraversal (AffineTravRes (..))
import Proarrow.Optic.Fold (FoldRes)
import Proarrow.Optic.Getter (GetterRes (..))
import Proarrow.Optic.Setter (SetterRes)
import Proarrow.Optic.Traversal (TravRes)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Star (Star, unStar, pattern Star)
import Proarrow.Profunctor.Representable (Rep (..))

type LensRes :: forall {k}. FLAVOR k k
class (AffineTravRes p q, GetterRes p q) => LensRes (p :: k +-> k) (q :: k +-> k) where
  -- | Like 'affineSet', but with an honest constraint: lens witnesses only ever need binary
  -- products, so lenses stay usable in categories without coproducts.
  putP :: (HasBinaryProducts k) => p (s :: k) a -> q b t -> (s && b) ~> t
instance (HasBinaryProducts k, Ob (s :: k)) => LensRes (Rep (Product s)) (Corep (Product s)) where
  putP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
HasBinaryProducts k =>
Rep (Product s) s a -> Corep (Product s) b t -> (s && b) ~> t
putP @_ @a @b (Rep s ~> (Product s @ a)
p) (Corep (Product s @ b) ~> t
q) = (Product s @ b) ~> t
(s && b) ~> t
q ((s && b) ~> t) -> ((s && b) ~> (s && b)) -> (s && b) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
first @b (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @s @a ((s && a) ~> s) -> (s ~> (s && a)) -> s ~> s
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (Product s @ a)
s ~> (s && a)
p)
instance (CategoryOf k) => LensRes (Id :: k +-> k) (Id :: k +-> k) where
  putP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
HasBinaryProducts k =>
Id s a -> Id b t -> (s && b) ~> t
putP @s @_ @b Id s a
sa (Id b ~> t
bt) = b ~> t
bt (b ~> t) -> ((s && b) ~> b) -> (s && b) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @s @b ((Ob s, Ob a) => (s && b) ~> t) -> Id s a -> (s && b) ~> t
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Id 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
\\ Id s a
sa ((Ob b, Ob t) => (s && b) ~> t) -> (b ~> t) -> (s && b) ~> t
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
instance (LensRes f g, LensRes f' g') => LensRes (f :.: f') (g' :.: g) where
  putP :: forall (s :: i) (a :: i) (b :: i) (t :: i).
HasBinaryProducts i =>
(:.:) f f' s a -> (:.:) g' g b t -> (s && b) ~> t
putP @s @_ @b (f :: f s b
f@f s b
Objs :.: f' b a
f') (g' :: g' b b
g'@g' b b
Objs :.: g b t
g) =
    forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(LensRes p q, HasBinaryProducts k) =>
p s a -> q b t -> (s && b) ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(LensRes p q, HasBinaryProducts i) =>
p s a -> q b t -> (s && b) ~> t
putP @f @g f s b
f g b t
g ((s && b) ~> t) -> ((s && b) ~> (s && b)) -> (s && b) ~> t
forall (b :: i) (c :: i) (a :: i). (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) ~> a
fst @_ @s @b ((s && b) ~> s) -> ((s && b) ~> b) -> (s && b) ~> (s && b)
forall (a :: i) (x :: i) (y :: i).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(LensRes p q, HasBinaryProducts k) =>
p s a -> q b t -> (s && b) ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(LensRes p q, HasBinaryProducts i) =>
p s a -> q b t -> (s && b) ~> t
putP @f' @g' f' b a
f' g' b b
g' ((b && b) ~> b) -> ((s && b) ~> (b && b)) -> (s && b) ~> b
forall (b :: i) (c :: i) (a :: i). (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 (c :: i) (a :: i) (b :: i).
(HasBinaryProducts i, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
first @b (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i).
GetterRes p q =>
p s a -> s ~> a
getP @f @g f s b
f)))

instance CompactFlavor LensRes

instance SubFlavor LensRes AffineTravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
LensRes p q =>
(AffineTravRes p q => r) -> r
subFlavor AffineTravRes p q => r
r = r
AffineTravRes p q => r
r
instance SubFlavor LensRes GetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
LensRes p q =>
(GetterRes p q => r) -> r
subFlavor GetterRes p q => r
r = r
GetterRes p q => r
r
instance SubFlavor LensRes TravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
LensRes p q =>
(TravRes p q => r) -> r
subFlavor TravRes p q => r
r = r
TravRes p q => r
r
instance SubFlavor LensRes SetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
LensRes p q =>
(SetterRes p q => r) -> r
subFlavor SetterRes p q => r
r = r
SetterRes p q => r
r
instance SubFlavor LensRes AffineFoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
LensRes p q =>
(AffineFoldRes p q => r) -> r
subFlavor AffineFoldRes p q => r
r = r
AffineFoldRes p q => r
r
instance SubFlavor LensRes FoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
LensRes p q =>
(FoldRes p q => r) -> r
subFlavor FoldRes p q => r
r = r
FoldRes p q => r
r

type Lens (s :: k) (t :: k) a b = Optic (Prostrong LensRes) s t a b
type Lens' s a = Lens s s a a
lens
  :: forall {k} (s :: k) (t :: k) a b
   . (HasBinaryProducts k, Ob b) => (s ~> a) -> ((s && b) ~> t) -> Lens s t a b
lens :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Lens s t a b
lens s ~> a
sa (s && b) ~> t
sbt =
  ExOptic LensRes a b s t -> Optic (Prostrong LensRes) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(LensRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic LensRes a b) q s t -> ExOptic LensRes a b s t
ExProstrong @(Rep (Product s)) @(Corep (Product s)) ((s ~> (Product s @ a)) -> Rep (Product s) s a
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (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) Rep (Product s) s a
-> ExOptic LensRes a b a b
-> (:.:) (Rep (Product s)) (ExOptic LensRes a b) s b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic LensRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) (Rep (Product s)) (ExOptic LensRes a b) s b
-> Corep (Product s) b t
-> (:.:)
     (Rep (Product s) :.: ExOptic LensRes a b) (Corep (Product s)) s t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((Product s @ b) ~> t) -> Corep (Product s) b t
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (Product s @ b) ~> t
(s && b) ~> t
sbt)) ((Ob s, Ob a) => Optic (Prostrong LensRes) s t a b)
-> (s ~> a) -> Optic (Prostrong LensRes) 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

-- | The eliminating carrier for lenses: a lens's two legs, as a profunctor in @s@\/@t@.
type Shop :: forall {k}. k -> k -> k +-> k
data Shop a b s t where
  Shop :: (Ob a, Ob b) => (s ~> a) -> ((s && b) ~> t) -> Shop a b s t

instance (HasBinaryProducts k, Ob (a :: k), Ob b) => Profunctor (Shop a b :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Shop a b a b -> Shop a b c d
dimap c ~> a
l b ~> d
r (Shop a ~> a
sa (a && b) ~> b
sbt) = (c ~> a) -> ((c && b) ~> d) -> Shop a b c d
forall {k} (a :: k) (b :: k) (s :: k) (t :: k).
(Ob a, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Shop a b s t
Shop (a ~> a
sa (a ~> a) -> (c ~> a) -> c ~> 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) -> ((c && b) ~> b) -> (c && 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
. (a && b) ~> b
sbt ((a && b) ~> b) -> ((c && b) ~> (a && b)) -> (c && b) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
first @b c ~> a
l) ((Ob c, Ob a) => Shop a b c d) -> (c ~> a) -> Shop a b c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l ((Ob b, Ob d) => Shop a b c d) -> (b ~> d) -> Shop a b c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Shop a b a b -> r
\\ Shop a ~> a
sa (a && b) ~> b
sbt = r
(Ob a, Ob a) => r
(Ob a, Ob b) => r
r ((Ob a, Ob a) => r) -> (a ~> 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 ~> a
sa ((Ob (a && b), Ob b) => r) -> ((a && b) ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (a && b) ~> b
sbt

-- | Any flavor whose optics have lens legs has strength for the 'Shop' carrier.
instance (HasBinaryProducts k, Ob (a :: k), Ob b, SubFlavor w LensRes) => Prostrong (w :: FLAVOR k k) (Shop a b :: k +-> k) where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Shop a b) :.: g) :~> Shop a b
proact @f @g @s (f :: f a b
f@f a b
Objs :.: Shop b ~> a
sa (b && b) ~> b
sbt :.: g :: g b b
g@g b b
Objs) =
    forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
forall (w1 :: FLAVOR k k) (w2 :: FLAVOR k k) (p :: k +-> k)
       (q :: k +-> k) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
subFlavor @w @LensRes @f @g
      ((a ~> a) -> ((a && b) ~> b) -> Shop a b a b
forall {k} (a :: k) (b :: k) (s :: k) (t :: k).
(Ob a, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Shop a b s t
Shop (b ~> a
sa (b ~> a) -> (a ~> b) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
getP @f @g f a b
f) (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(LensRes p q, HasBinaryProducts k) =>
p s a -> q b t -> (s && b) ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(LensRes p q, HasBinaryProducts k) =>
p s a -> q b t -> (s && b) ~> t
putP @f @g f a b
f g b b
g ((a && b) ~> b) -> ((a && b) ~> (a && b)) -> (a && b) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @s @b ((a && b) ~> a) -> ((a && b) ~> b) -> (a && b) ~> (a && b)
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)
&&& ((b && b) ~> b
sbt ((b && b) ~> b) -> ((a && b) ~> (b && b)) -> (a && b) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
first @b (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
getP @f @g f a b
f)))))

-- | Eliminate any optic that is at least an iso and at most a lens to its two legs, in either
-- encoding: 'Prostrong'-flavored optics via @'SubFlavor' w 'LensRes'@ (through the bridge
-- instance above), profunctor-class-flavored optics via their class instance for 'Shop'.
withLens
  :: forall {k} c (s :: k) (t :: k) a b r
   . (HasBinaryProducts k, (Ob a, Ob b) => c (Shop a b))
  => Optic c s t a b -> ((s ~> a) -> ((s && b) ~> t) -> r) -> r
withLens :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(HasBinaryProducts k, (Ob a, Ob b) => c (Shop a b)) =>
Optic c s t a b -> ((s ~> a) -> ((s && b) ~> t) -> r) -> r
withLens (Optic forall (p :: k +-> k). c p => p a b -> p s t
l) (s ~> a) -> ((s && b) ~> t) -> r
k = case forall (p :: k +-> k). c p => p a b -> p s t
l @(Shop a b) ((a ~> a) -> ((a && b) ~> b) -> Shop a b a b
forall {k} (a :: k) (b :: k) (s :: k) (t :: k).
(Ob a, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Shop a b s t
Shop a ~> a
a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b)) of Shop s ~> a
sa (s && b) ~> t
sbt -> (s ~> a) -> ((s && b) ~> t) -> r
k s ~> a
s ~> a
sa (s && b) ~> t
(s && b) ~> t
sbt

instance (P.Functor f) => Prostrong LensRes (Star (Prelude f)) where
  proact :: forall (f :: Type +-> Type) (g :: Type +-> Type).
(LensRes f g, Profunctor f, Profunctor g) =>
((f :.: Star (Prelude f)) :.: g) :~> Star (Prelude f)
proact @p @q (p :: f a b
p@f a b
Objs :.: Star b ~> Prelude f b
f :.: q :: g b b
q@g b b
Objs) = (a ~> Prelude f b) -> Star (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
a -> (b ~> b) -> Prelude f b ~> Prelude f b
forall a b. (a ~> b) -> Prelude f a ~> Prelude f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (((a, b) -> b) -> a -> b -> b
forall a b c. ((a, b) -> c) -> a -> b -> c
P.curry (f a b -> g b b -> (a && b) ~> b
forall s a b t.
HasBinaryProducts Type =>
f s a -> g b t -> (s && b) ~> t
forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(LensRes p q, HasBinaryProducts k) =>
p s a -> q b t -> (s && b) ~> t
putP f a b
p g b b
q) a
a) (b ~> Prelude f b
b -> Prelude f b
f (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (s :: k) (a :: k).
GetterRes p q =>
p s a -> s ~> a
forall (p :: Type +-> Type) (q :: Type +-> Type) s a.
GetterRes p q =>
p s a -> s ~> a
getP @p @q f a b
p a
a))

type LensVL s t a b = forall f. (P.Functor f) => (a -> f b) -> s -> f t
toLensVL :: Lens s t a b -> LensVL s t a b
toLensVL :: forall s t a b. Lens s t a b -> LensVL s t a b
toLensVL (Optic forall (p :: Type +-> Type). Prostrong LensRes 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). Prostrong LensRes 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
.)

lensVL :: LensVL s t a b -> Lens s t a b
lensVL :: forall s t a b. LensVL s t a b -> Lens s t a b
lensVL LensVL 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).
(HasBinaryProducts k, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Lens s t a b
lens (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
LensVL 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
LensVL 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)))