{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __grate__: the closed-category optic whose residual sits under an exponential,
--
-- > Grate s t a b = exists m. (s ~> (m ~~> a), (m ~~> b) ~> t)
--
-- witnessed by @'Rep'@\/@'Corep'@ @('Exp' m)@ ('GrateFl' \/ 'zipWithP') for a /comonoid/ @m@. The
-- exponential by a comonoid is the reader applicative, so every grate is a
-- 'Proarrow.Optic.Kaleidoscope.Kaleidoscope' (hence a 'Proarrow.Optic.Kaleidoscope.Cotraversal' and a
-- 'Proarrow.Optic.Setter.Setter'), and every 'Proarrow.Optic.PowerGrate.PowerGrate' is a
-- grate. Build with 'grate' (whose residual is the \"logarithm\" @s ~~> a@), eliminate to the
-- zipping function with 'withGrate', via the generic 'ExOptic' carrier.
module Proarrow.Optic.Grate where

import Prelude (($))

import Proarrow.Category.Monoidal (SymMonoidal (..))
import Proarrow.Category.Monoidal.Closed (Closed (..), Exp)
import Proarrow.Colimit.BinaryCoproduct (HasCoproducts)
import Proarrow.Core (CategoryOf (..), Promonad (..), obj, type (+->))
import Proarrow.Monoid (CocommutativeComonoid)
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( ExOptic
  , FLAVOR
  , Optic
  , Prostrong (..)
  , legs2prof
  , withLegs
  )
import Proarrow.Optic.Glass (GlassFl, Mod, evalAt)
import Proarrow.Optic.Kaleidoscope (KaleidoFl)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))
import Proarrow.Tools.SMC (SYN (..), lam, toSMC, (!))

-- | A grate is a "residual lens" whose residual @m@ sits under an exponential instead of a
-- tensor: @s ~> (m ~~> a)@ and @(m ~~> b) ~> t@. Unlike a 'Proarrow.Optic.Traversal.Traversal',
-- this needs no 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor' machinery.
-- 'zipWithP' is built directly out of 'Closed'\/'SymMonoidal' algebra (curry\/apply\/swap),
-- since it manipulates morphisms directly and does not lift an arbitrary effect through a
-- witness functor. 'Proarrow.Optic.Kaleidoscope.KaleidoFl' is a
-- superclass: the residual is a comonoid, so @m ~~> -@ is an applicative functor.
type GrateFl :: forall {k}. FLAVOR k k
class (KaleidoFl p q, GlassFl p q) => GrateFl (p :: k +-> k) (q :: k +-> k) where
  zipWithP
    :: forall s a b t
     . (Closed k, SymMonoidal k) => p s a -> q b t -> (forall (x :: k). (Ob x) => ((x ~~> a) ~> b) -> (x ~~> s) ~> t)

-- | Swap the argument order of a curried two-argument exponential: @x ~~> (m ~~> a) ~> m ~~> (x ~~> a)@.
flipExp
  :: forall {k} (x :: k) m a
   . (Closed k, SymMonoidal k, Ob x, Ob m, Ob a)
  => (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a))
flipExp :: forall {k} (x :: k) (m :: k) (a :: k).
(Closed k, SymMonoidal k, Ob x, Ob m, Ob a) =>
(x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a))
flipExp = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
toSMC @(F x :-> F m :-> F a) @(F m :-> F x :-> F a) \TermP
  (~>) 3 '[ '(0, F x :-> (F m :-> F a))] (F x :-> (F m :-> F a))
f -> (TermP (~>) 3 '[ '(1, F m)] (F m)
 -> TermP
      (~>)
      (2 + PSize (TermP (~>) 3 '[ '(1, F m)] (F m)))
      '[ '(1, F m), '(0, F x :-> (F m :-> F a))]
      (F x :-> F a))
-> TermP
     (~>)
     (1
      + PSize
          (TermP
             (~>) 3 '[ '(0, F x :-> (F m :-> F a))] (F x :-> (F m :-> F a))))
     '[ '(0, F x :-> (F m :-> F a))]
     (F m :-> (F x :-> F a))
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
(Closed k, Binds (~>) d r a b t cont) =>
(t -> cont) -> Term d r (a :-> b)
lam \TermP (~>) 3 '[ '(1, F m)] (F m)
m -> (TermP (~>) 3 '[ '(2, F x)] (F x)
 -> TermP
      (~>)
      (3 + PSize (TermP (~>) 3 '[ '(2, F x)] (F x)))
      '[ '(2, F x), '(1, F m), '(0, F x :-> (F m :-> F a))]
      (F a))
-> TermP
     (~>)
     (2 + PSize (TermP (~>) 3 '[ '(1, F m)] (F m)))
     '[ '(1, F m), '(0, F x :-> (F m :-> F a))]
     (F x :-> F a)
forall {k} (d :: Nat) (r :: Ctx k) (a :: SYN k) (b :: SYN k) t
       cont.
(Closed k, Binds (~>) d r a b t cont) =>
(t -> cont) -> Term d r (a :-> b)
lam \TermP (~>) 3 '[ '(2, F x)] (F x)
x -> TermP
  (~>) 3 '[ '(0, F x :-> (F m :-> F a))] (F x :-> (F m :-> F a))
f TermP
  (~>) 3 '[ '(0, F x :-> (F m :-> F a))] (F x :-> (F m :-> F a))
-> TermP (~>) 3 '[ '(2, F x)] (F x)
-> TermP
     (~>) 3 '[ '(2, F x), '(0, F x :-> (F m :-> F a))] (F m :-> F a)
forall {k} (p :: CAT k) f x r.
(Apply p f x r, Closed k, MonoidalProfunctor p, KnownObj (TyOf x),
 KnownObj (TyOf r), Merge (CtxOf f) (CtxOf x)) =>
f -> x -> r
! TermP (~>) 3 '[ '(2, F x)] (F x)
x TermP
  (~>) 3 '[ '(2, F x), '(0, F x :-> (F m :-> F a))] (F m :-> F a)
-> TermP (~>) 3 '[ '(1, F m)] (F m)
-> TermP
     (~>)
     (3 + PSize (TermP (~>) 3 '[ '(2, F x)] (F x)))
     '[ '(2, F x), '(1, F m), '(0, F x :-> (F m :-> F a))]
     (F a)
forall {k} (p :: CAT k) f x r.
(Apply p f x r, Closed k, MonoidalProfunctor p, KnownObj (TyOf x),
 KnownObj (TyOf r), Merge (CtxOf f) (CtxOf x)) =>
f -> x -> r
! TermP (~>) 3 '[ '(1, F m)] (F m)
m

instance
  (Closed k, SymMonoidal k, HasCoproducts k, CocommutativeComonoid m)
  => GrateFl (Rep (Exp m) :: k +-> k) (Corep (Exp m) :: k +-> k)
  where
  zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
(Closed k, SymMonoidal k) =>
Rep (Exp m) s a
-> Corep (Exp m) b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP @_ @a (Rep s ~> (Exp m @ a)
sm) (Corep (Exp m @ b) ~> t
mbt) @x (x ~~> a) ~> b
kk = (Exp m @ b) ~> t
(m ~~> b) ~> t
mbt ((m ~~> b) ~> t) -> ((x ~~> s) ~> (m ~~> b)) -> (x ~~> s) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((x ~~> a) ~> b
kk ((x ~~> a) ~> b) -> (m ~> m) -> (m ~~> (x ~~> 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 ~~> (x ~~> a)) ~> (m ~~> b))
-> ((x ~~> s) ~> (m ~~> (x ~~> a))) -> (x ~~> s) ~> (m ~~> b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (x :: k) (m :: k) (a :: k).
(Closed k, SymMonoidal k, Ob x, Ob m, Ob a) =>
(x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a))
forall {k} (x :: k) (m :: k) (a :: k).
(Closed k, SymMonoidal k, Ob x, Ob m, Ob a) =>
(x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a))
flipExp @x @m @a ((x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
-> ((x ~~> s) ~> (x ~~> (m ~~> a)))
-> (x ~~> s) ~> (m ~~> (x ~~> a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (s ~> (Exp m @ a)
s ~> (m ~~> a)
sm (s ~> (m ~~> a)) -> (x ~> x) -> (x ~~> s) ~> (x ~~> (m ~~> a))
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x)
instance (CategoryOf k) => GrateFl (Id :: k +-> k) (Id :: k +-> k) where
  zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
(Closed k, SymMonoidal k) =>
Id s a
-> Id b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP (Id s ~> a
l) (Id b ~> t
r) @x (x ~~> a) ~> b
kk = b ~> t
r (b ~> t) -> ((x ~~> s) ~> b) -> (x ~~> s) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~~> a) ~> b
kk ((x ~~> a) ~> b) -> ((x ~~> s) ~> (x ~~> a)) -> (x ~~> s) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (s ~> a
l (s ~> a) -> (x ~> x) -> (x ~~> s) ~> (x ~~> a)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x)
instance (GrateFl f g, GrateFl f' g') => GrateFl (f :.: f') (g' :.: g) where
  zipWithP :: forall (s :: i) (a :: i) (b :: i) (t :: i).
(Closed i, SymMonoidal i) =>
(:.:) f f' s a
-> (:.:) g' g b t
-> forall (x :: i). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP (f s b
f :.: f' b a
f') (g' b b
g' :.: g b t
g) @x (x ~~> a) ~> b
kk = forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GrateFl p q, Closed k, SymMonoidal k) =>
p s a
-> q b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(GrateFl p q, Closed i, SymMonoidal i) =>
p s a
-> q b t
-> forall (x :: i). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP @f @g f s b
f g b t
g @x (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GrateFl p q, Closed k, SymMonoidal k) =>
p s a
-> q b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
forall (p :: i +-> i) (q :: i +-> i) (s :: i) (a :: i) (b :: i)
       (t :: i).
(GrateFl p q, Closed i, SymMonoidal i) =>
p s a
-> q b t
-> forall (x :: i). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP @f' @g' f' b a
f' g' b b
g' @x (x ~~> a) ~> b
kk)

type Grate (s :: k) (t :: k) a b = Optic (Prostrong GrateFl) s t a b
type Grate' s a = Grate s s a a

-- | Eliminate any grate-flavored optic to its zipping function, in either encoding: run it at its
-- witness pair ('ExOptic' 'GrateFl', via 'withLegs') and read the zipper off with 'zipWithP'.
withGrate
  :: forall {k} c (s :: k) (t :: k) a b r
   . (Closed k, SymMonoidal k, (Ob a, Ob b) => c (ExOptic GrateFl a b))
  => Optic c s t a b -> ((forall (x :: k). (Ob x) => ((x ~~> a) ~> b) -> (x ~~> s) ~> t) -> r) -> r
withGrate :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(Closed k, SymMonoidal k,
 (Ob a, Ob b) => c (ExOptic GrateFl a b)) =>
Optic c s t a b
-> ((forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t)
    -> r)
-> r
withGrate Optic c s t a b
o (forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t) -> r
k = forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @GrateFl Optic c s t a b
o \ @p @q p s a
p q b t
q -> (forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t) -> r
k (\ @x (x ~~> a) ~> b
kk -> forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GrateFl p q, Closed k, SymMonoidal k) =>
p s a
-> q b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GrateFl p q, Closed k, SymMonoidal k) =>
p s a
-> q b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP @p @q p s a
p q b t
q @x (x ~~> a) ~> b
kk)

-- | The canonical\/atomic grate constructor: the residual is the self-referential @s ~~> a@
-- (the "logarithm" of the get side), whose own get-map @m ~> (s ~~> a)@ trivializes to 'id' once
-- @m@ is fixed to be @s ~~> a@. That residual must be a comonoid; in a
-- 'Proarrow.Category.Monoidal.CopyDiscard.CopyDiscard' category every object is.
grate
  :: forall {k} (s :: k) (t :: k) a b
   . (Closed k, SymMonoidal k, HasCoproducts k, CocommutativeComonoid (s ~~> a), Ob s, Ob a, Ob b)
  => (Mod s a b ~> t) -> Grate s t a b
grate :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, HasCoproducts k,
 CocommutativeComonoid (s ~~> a), Ob s, Ob a, Ob b) =>
(Mod s a b ~> t) -> Grate s t a b
grate f :: Mod s a b ~> t
f@Mod s a b ~> t
Objs =
  forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @a ((Ob (s ~~> a) => Grate s t a b) -> Grate s t a b)
-> (Ob (s ~~> a) => Grate s t a b) -> Grate s t a b
forall a b. (a -> b) -> a -> b
$
    forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @GrateFl (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a @(Exp (s ~~> a)) (forall (s :: k) (a :: k).
(Closed k, SymMonoidal k, Ob s, Ob a) =>
s ~> ((s ~~> a) ~~> a)
forall {k} (s :: k) (a :: k).
(Closed k, SymMonoidal k, Ob s, Ob a) =>
s ~> ((s ~~> a) ~~> a)
evalAt @s @a)) (forall (a :: k) (f :: k +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @b @(Exp (s ~~> a)) (Exp (s ~~> a) @ b) ~> t
Mod s a b ~> t
f)