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

-- | The __setter__: the weakest write-side optic, applying a morphism to every focus ('SetterRes'
-- \/ 'overP', whose 'Proadjunction' superclass certifies the witness pair is a genuine adjoint
-- pair, i.e. the optic is lawful). It sits at the write-only top of the subtyping lattice
-- alongside 'Proarrow.Optic.Fold.Fold', so it has no builder of its own
-- ('Proarrow.Optic.convert' a stronger optic); its canonical eliminator is 'over' -- with 'set',
-- '(%~)' and '(.~)' as shorthands -- via the hom carrier 'Id'.
module Proarrow.Optic.Setter where

import Data.Kind (Type)
import Prelude (const)
import Prelude qualified as P

import Proarrow.Adjunction (Proadjunction)
import Proarrow.Category.Instance.Kleisli (KLEISLI (..), Kleisli (..))
import Proarrow.Category.Monoidal.Closed (Closed (..), Exp)
import Proarrow.Colimit.BinaryCoproduct (Coproduct, HasCoproducts, right)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (\\), type (+->))
import Proarrow.Functor (Prelude (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts, Product, second)
import Proarrow.Optic (CompactFlavor, FLAVOR, Optic, Optic_ (..), Prostrong (..), SubFlavor (..))
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Star (Star, unStar, pattern Star)
import Proarrow.Profunctor.Representable (CorepStar (..), Rep (..), RepCostar (..), Representable (..))

-- | A setter can only apply a pure function to the @a@'s it can see -- it can neither view nor
-- fold them. A traversal is both a setter and a fold.
--
-- | The 'Proadjunction' superclass certifies that a setter's witness pair is a genuine adjoint
-- pair -- the residual is an actual functor whose @unit@\/@counit@ round-trip -- i.e. the optic
-- is lawful.
type SetterRes :: forall {k}. FLAVOR k k
class (Proadjunction p q) => SetterRes (p :: k +-> k) (q :: k +-> k) where
  overP :: p s a -> q b t -> (a ~> b) -> (s ~> t)

instance CompactFlavor SetterRes

-- | Every /representable/ residual is a setter: map the focus through the residual functor with
-- 'repMap'. This needs only 'Representable' @t@ -- no 'Proarrow.Category.Monoidal.Distributive.Traversable' -- which is exactly why
-- 'Proarrow.Optic.Setter.Setter' sits at the top of the lattice: functoriality of the residual is
-- all @over@ ever uses. Richer optics ('Proarrow.Optic.Lens.Lens', 'Proarrow.Optic.Traversal.Traversal', ...)
-- are this witness plus extra algebra on @t@.
instance (Representable t) => SetterRes (t :: k +-> k) (RepCostar t) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
t s a -> RepCostar t b t -> (a ~> b) -> s ~> t
overP t s a
l (RepCostar (t % b) ~> t
r) a ~> b
f = (t % b) ~> t
r ((t % b) ~> t) -> (s ~> (t % b)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @t a ~> b
f ((t % a) ~> (t % b)) -> (s ~> (t % a)) -> s ~> (t % 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
. t s a -> s ~> (t % a)
forall (a :: k) (b :: k). t a b -> a ~> (t % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index t s a
l

instance (HasBinaryProducts k, Ob (s :: k)) => SetterRes (Rep (Product s)) (Corep (Product s)) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Rep (Product s) s a -> Corep (Product s) b t -> (a ~> b) -> s ~> t
overP (Rep s ~> (Product s @ a)
p) (Corep (Product s @ b) ~> t
q) a ~> b
f = (Product s @ b) ~> t
(s && b) ~> t
q ((s && b) ~> t) -> (s ~> (s && b)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (c && a) ~> (c && b)
second @s a ~> b
f ((s && a) ~> (s && b)) -> (s ~> (s && a)) -> s ~> (s && b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (Product s @ a)
s ~> (s && a)
p
instance (HasCoproducts k, Ob t) => SetterRes (Rep (Coproduct t) :: k +-> k) (Corep (Coproduct t)) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Rep (Coproduct t) s a
-> Corep (Coproduct t) b t -> (a ~> b) -> s ~> t
overP (Rep s ~> (Coproduct t @ a)
p) (Corep (Coproduct t @ b) ~> t
q) a ~> b
f = (Coproduct t @ b) ~> t
(t || b) ~> t
q ((t || b) ~> t) -> (s ~> (t || b)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (c || a) ~> (c || b)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob c) =>
(a ~> b) -> (c || a) ~> (c || b)
right @t a ~> b
f ((t || a) ~> (t || b)) -> (s ~> (t || a)) -> s ~> (t || b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (Coproduct t @ a)
s ~> (t || a)
p
instance (CategoryOf k) => SetterRes (Id :: k +-> k) (Id :: k +-> k) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Id s a -> Id b t -> (a ~> b) -> s ~> t
overP (Id s ~> a
l) (Id b ~> t
r) a ~> b
f = b ~> t
r (b ~> t) -> (s ~> b) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f (a ~> b) -> (s ~> a) -> s ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> a
l
instance (SetterRes f g, SetterRes f' g') => SetterRes (f :.: f') (g' :.: g) where
  overP :: forall (s :: i) (a :: i) (b :: i) (t :: i).
(:.:) f f' s a -> (:.:) g' g b t -> (a ~> b) -> s ~> t
overP (f s b
f :.: f' b a
f') (g' b b
g' :.: g b t
g) = forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @f @g f s b
f g b t
g ((b ~> b) -> s ~> t) -> ((a ~> b) -> b ~> b) -> (a ~> b) -> s ~> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @f' @g' f' b a
f' g' b b
g'

-- | Dually, every /corepresentable/ residual is a setter: map with 'corepMap'. Needs only
-- 'Corepresentable' @t@, not 'Proarrow.Category.Monoidal.Distributive.Cotraversable'.
instance (Corepresentable t) => SetterRes (CorepStar t) t where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
CorepStar t s a -> t b t -> (a ~> b) -> s ~> t
overP (CorepStar s ~> (t %% a)
l) t b t
co a ~> b
f = t b t -> (t %% b) ~> t
forall (a :: k) (b :: k). t a b -> (t %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex t b t
co ((t %% b) ~> t) -> (s ~> (t %% b)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: k +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @t a ~> b
f ((t %% a) ~> (t %% b)) -> (s ~> (t %% a)) -> s ~> (t %% b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (t %% a)
l

-- | The grate witness is a setter witness: map under the exponential. The 'Closed' structure
-- this needs rides in the instance context, not in @overP@'s own (weaker) constraint.
instance (Closed k, Ob (m :: k)) => SetterRes (Rep (Exp m) :: k +-> k) (Corep (Exp m)) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Rep (Exp m) s a -> Corep (Exp m) b t -> (a ~> b) -> s ~> t
overP (Rep s ~> (Exp m @ a)
sm) (Corep (Exp m @ b) ~> t
mbt) a ~> b
f = (Exp m @ b) ~> t
(m ~~> b) ~> t
mbt ((m ~~> b) ~> t) -> (s ~> (m ~~> b)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
f (a ~> b) -> (m ~> m) -> (m ~~> a) ~> (m ~~> b)
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 ~~> a) ~> (m ~~> b)) -> (s ~> (m ~~> a)) -> s ~> (m ~~> b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (Exp m @ a)
s ~> (m ~~> a)
sm ((Ob a, Ob b) => s ~> t) -> (a ~> b) -> s ~> 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
\\ a ~> b
f

type Setter (s :: k) (t :: k) a b = Optic (Prostrong SetterRes) s t a b
type Setter' s a = Setter s s a a

-- | Any flavor whose optics can set has strength for the hom carrier 'Id'.
instance (CategoryOf k, SubFlavor w SetterRes) => Prostrong (w :: FLAVOR k k) (Id :: k +-> k) where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Id) :.: g) :~> Id
proact @f @g (f a b
f :.: Id b ~> b
h :.: g b b
g) = 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 @SetterRes @f @g ((a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @f @g f a b
f g b b
g b ~> b
h))

-- | Map over any optic that can act as a setter, in either encoding: a 'Prostrong'-flavored optic
-- needs @'SubFlavor' w 'SetterRes'@ (discharged by the bridge instance above), a
-- profunctor-class-flavored optic needs its class to hold for 'Id'.
over
  :: forall {k} c (s :: k) (t :: k) a b
   . (c (Id :: k +-> k))
  => Optic c s t a b -> (a ~> b) -> (s ~> t)
over :: forall {k} (c :: (k +-> k) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k).
c Id =>
Optic c s t a b -> (a ~> b) -> s ~> t
over (Optic forall (p :: k +-> k). c p => p a b -> p s t
l) a ~> b
f = Id s t -> s ~> t
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId (Id a b -> Id s t
forall (p :: k +-> k). c p => p a b -> p s t
l ((a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> b
a ~> b
f))

-- | Apply a function through a concrete, @Type@-level 'Setter'.
infixl 8 %~

(%~) :: (c (Id :: Type +-> Type)) => Optic c s t a b -> (a -> b) -> (s -> t)
%~ :: forall (c :: (Type +-> Type) -> Constraint) s t a b.
c Id =>
Optic c s t a b -> (a -> b) -> s -> t
(%~) = Optic c s t a b -> (a ~> b) -> s ~> t
Optic c s t a b -> (a -> b) -> s -> t
forall {k} (c :: (k +-> k) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k).
c Id =>
Optic c s t a b -> (a ~> b) -> s ~> t
over

-- | Replace the focus\/foci of a concrete, @Type@-level 'Setter' with a constant value.
infixl 8 .~

(.~) :: (c (Id :: Type +-> Type)) => Optic c s t a b -> b -> (s -> t)
Optic c s t a b
l .~ :: forall (c :: (Type +-> Type) -> Constraint) s t a b.
c Id =>
Optic c s t a b -> b -> s -> t
.~ b
b = Optic c s t a b
l Optic c s t a b -> (a -> b) -> s -> t
forall (c :: (Type +-> Type) -> Constraint) s t a b.
c Id =>
Optic c s t a b -> (a -> b) -> s -> t
%~ b -> a -> b
forall a b. a -> b -> a
const b
b

-- | Named version of '(.~)'.
set :: (c (Id :: Type +-> Type)) => Optic c s t a b -> b -> (s -> t)
set :: forall (c :: (Type +-> Type) -> Constraint) s t a b.
c Id =>
Optic c s t a b -> b -> s -> t
set = Optic c s t a b -> b -> s -> t
forall (c :: (Type +-> Type) -> Constraint) s t a b.
c Id =>
Optic c s t a b -> b -> s -> t
(.~)

-- | Monadically replace the focus\/foci of a 'Setter' in the Kleisli category of @m@ with a
-- constant value, ignoring the old contents entirely.
mupdate
  :: forall m s t a b
   . (P.Monad m)
  => Setter (KL s :: KLEISLI (Star (Prelude m))) (KL t) (KL a) (KL b) -> b -> s -> m t
mupdate :: forall (m :: Type -> Type) s t a b.
Monad m =>
Setter ('KL s) ('KL t) ('KL a) ('KL b) -> b -> s -> m t
mupdate Setter ('KL s) ('KL t) ('KL a) ('KL b)
l b
b s
s = Prelude m t -> m t
forall (f :: Type -> Type) a. Prelude f a -> f a
unPrelude (Star' ('NT (Prelude m)) s t -> s ~> Prelude m t
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Star' ('NT f) a b -> a ~> f b
unStar (Kleisli ('KL s) ('KL t) -> Star' ('NT (Prelude m)) s t
forall {k} (p :: CAT k) (a :: k) (b :: k).
Kleisli ('KL a) ('KL b) -> p a b
unKleisli (Setter ('KL s) ('KL t) ('KL a) ('KL b)
-> ('KL a ~> 'KL b) -> 'KL s ~> 'KL t
forall {k} (c :: (k +-> k) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k).
c Id =>
Optic c s t a b -> (a ~> b) -> s ~> t
over Setter ('KL s) ('KL t) ('KL a) ('KL b)
l (Star' ('NT (Prelude m)) a b -> Kleisli ('KL a) ('KL b)
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli ((a ~> Prelude m b) -> Star' ('NT (Prelude m)) a b
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (\a
_ -> m b -> Prelude m b
forall (f :: Type -> Type) a. f a -> Prelude f a
Prelude (b -> m b
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
P.return b
b)))))) s
s)