{-# 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)@ ('GrateRes' \/ 'zipWithP'). It subtypes only to
-- 'Proarrow.Optic.Setter.Setter', and every 'Proarrow.Optic.Kaleidoscope.Kaleidoscope' is one.
-- Build with 'grate' (whose residual is the \"logarithm\" @s ~~> a@), eliminate to the zipping
-- function with 'withGrate', via the 'Grating' carrier.
module Proarrow.Optic.Grate where

import Prelude (($))

import Proarrow.Category.Monoidal (Monoidal (..), SymMonoidal (..), first, second, swap, type (**))
import Proarrow.Category.Monoidal.Closed (Closed (..), Exp)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (\\), type (+->))
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (CompactFlavor, ExOptic (..), FLAVOR, Optic, Optic_ (..), Prostrong (..), SubFlavor (..), ex2prof)
import Proarrow.Optic.Setter (SetterRes)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))

-- | A grate is a "residual lens" whose residual @m@ sits under an exponential rather than a
-- tensor: @s ~> (m ~~> a)@ and @(m ~~> b) ~> t@. Unlike a 'Proarrow.Optic.Traversal.Traversal',
-- this needs no 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor' machinery
-- at all -- 'zipWithP' is built directly out of 'Closed'\/'SymMonoidal' algebra
-- (curry\/apply\/swap), since we're manipulating morphisms directly rather than lifting an
-- arbitrary effect through a witness functor.
type GrateRes :: forall {k}. FLAVOR k k
class (SetterRes p q) => GrateRes (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 :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @a ((Ob (m ~~> a) => (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
 -> (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
-> (Ob (m ~~> a) => (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
-> (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a))
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @x @(m ~~> a) ((Ob (x ~~> (m ~~> a)) => (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
 -> (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
-> (Ob (x ~~> (m ~~> a)) => (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
-> (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a))
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @(x ~~> (m ~~> a)) @m ((Ob ((x ~~> (m ~~> a)) ** m) =>
  (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
 -> (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
-> (Ob ((x ~~> (m ~~> a)) ** m) =>
    (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a)))
-> (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a))
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @(x ~~> (m ~~> a)) @m
          ( forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @((x ~~> (m ~~> a)) ** m) @x
              ( forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @m @a
                  (((m ~~> a) ** m) ~> a)
-> ((((x ~~> (m ~~> a)) ** m) ** x) ~> ((m ~~> a) ** m))
-> (((x ~~> (m ~~> a)) ** m) ** 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
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @m (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @x @(m ~~> a))
                  ((((x ~~> (m ~~> a)) ** x) ** m) ~> ((m ~~> a) ** m))
-> ((((x ~~> (m ~~> a)) ** m) ** x)
    ~> (((x ~~> (m ~~> a)) ** x) ** m))
-> (((x ~~> (m ~~> a)) ** m) ** x) ~> ((m ~~> a) ** m)
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) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @(x ~~> (m ~~> a)) @x @m
                  (((x ~~> (m ~~> a)) ** (x ** m))
 ~> (((x ~~> (m ~~> a)) ** x) ** m))
-> ((((x ~~> (m ~~> a)) ** m) ** x)
    ~> ((x ~~> (m ~~> a)) ** (x ** m)))
-> (((x ~~> (m ~~> a)) ** m) ** x)
   ~> (((x ~~> (m ~~> a)) ** x) ** m)
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).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @(x ~~> (m ~~> a)) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @m @x)
                  (((x ~~> (m ~~> a)) ** (m ** x))
 ~> ((x ~~> (m ~~> a)) ** (x ** m)))
-> ((((x ~~> (m ~~> a)) ** m) ** x)
    ~> ((x ~~> (m ~~> a)) ** (m ** x)))
-> (((x ~~> (m ~~> a)) ** m) ** x)
   ~> ((x ~~> (m ~~> a)) ** (x ** m))
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) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @(x ~~> (m ~~> a)) @m @x
              )
          )

instance (Closed k, SymMonoidal k, Ob m) => GrateRes (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 :: k +-> 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 :: k +-> 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 :: 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 (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) => GrateRes (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 :: k +-> 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 :: k +-> 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 (GrateRes f g, GrateRes f' g') => GrateRes (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).
(GrateRes 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).
(GrateRes 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).
(GrateRes 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).
(GrateRes 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)

instance CompactFlavor GrateRes

instance SubFlavor GrateRes SetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
GrateRes p q =>
(SetterRes p q => r) -> r
subFlavor SetterRes p q => r
r = r
SetterRes p q => r
r

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

-- | The eliminating carrier for grates: the polymorphic zipping function, as a profunctor in
-- @s@\/@t@.
type Grating :: forall {k}. k -> k -> k +-> k
data Grating a b s t where
  Grating
    :: (Ob s, Ob t)
    => (forall (x :: k). (Ob x) => ((x ~~> a) ~> b) -> (x ~~> s) ~> t) -> Grating (a :: k) b s t

instance (Closed k, SymMonoidal k, Ob (a :: k), Ob b) => Profunctor (Grating a b :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Grating a b a b -> Grating a b c d
dimap c ~> a
l b ~> d
r (Grating forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> a) ~> b
z) = ((forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> c) ~> d)
-> Grating a b c d
forall k (s :: k) (t :: k) (a :: k) (b :: k).
(Ob s, Ob t) =>
(forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t)
-> Grating a b s t
Grating \ @x (x ~~> a) ~> b
kk -> b ~> d
r (b ~> d) -> ((x ~~> c) ~> b) -> (x ~~> c) ~> 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
. forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> a) ~> b
z @x (x ~~> a) ~> b
kk ((x ~~> a) ~> b) -> ((x ~~> c) ~> (x ~~> a)) -> (x ~~> c) ~> 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
. (c ~> a
l (c ~> a) -> (x ~> x) -> (x ~~> c) ~> (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)) ((Ob c, Ob a) => Grating a b c d) -> (c ~> a) -> Grating 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) => Grating a b c d) -> (b ~> d) -> Grating 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) -> Grating a b a b -> r
\\ Grating{} = r
(Ob a, Ob b) => r
r

-- | Any flavor whose optics can zip has strength for the 'Grating' carrier.
instance
  (Closed k, SymMonoidal k, Ob (a :: k), Ob b, SubFlavor w GrateRes)
  => Prostrong (w :: FLAVOR k k) (Grating a b :: k +-> k)
  where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Grating a b) :.: g) :~> Grating a b
proact @f @g (f :: f a b
f@f a b
Objs :.: Grating forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> b) ~> b
z :.: 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 @GrateRes @f @g ((forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> a) ~> b)
-> Grating a b a b
forall k (s :: k) (t :: k) (a :: k) (b :: k).
(Ob s, Ob t) =>
(forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t)
-> Grating a b s t
Grating \ @x (x ~~> a) ~> b
kk -> forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GrateRes 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).
(GrateRes p q, Closed k, SymMonoidal k) =>
p s a
-> q b t
-> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
zipWithP @f @g f a b
f g b b
g @x (forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> b) ~> b
z @x (x ~~> a) ~> b
kk))

-- | Eliminate any grate-flavored optic to its zipping function, in either encoding.
withGrate
  :: forall {k} c (s :: k) (t :: k) a b r
   . (CategoryOf k, (Ob a, Ob b) => c (Grating 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.
(CategoryOf k, (Ob a, Ob b) => c (Grating a b)) =>
Optic c s t a b
-> ((forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t)
    -> r)
-> r
withGrate (Optic forall (p :: k +-> k). c p => p a b -> p s t
l) (forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t) -> r
k = case forall (p :: k +-> k). c p => p a b -> p s t
l @(Grating a b) ((forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> a) ~> b)
-> Grating a b a b
forall k (s :: k) (t :: k) (a :: k) (b :: k).
(Ob s, Ob t) =>
(forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t)
-> Grating a b s t
Grating \(x ~~> a) ~> b
kk -> (x ~~> a) ~> b
(x ~~> a) ~> b
kk) of Grating forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
z -> (forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t) -> r
k (\ @x (x ~~> a) ~> b
kk -> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
z @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 exactly @s ~~> a@.
grate
  :: forall {k} (s :: k) (t :: k) a b
   . (Closed k, SymMonoidal k, Ob s, Ob a, Ob b)
  => (((s ~~> a) ~~> b) ~> t) -> Grate s t a b
grate :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob s, Ob a, Ob b) =>
(((s ~~> a) ~~> b) ~> t) -> Grate s t a b
grate f :: ((s ~~> a) ~~> b) ~> t
f@((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
$
    let sa :: s ~> ((s ~~> a) ~~> a)
sa = forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @s @(s ~~> a) (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @s @a (((s ~~> a) ** s) ~> a)
-> ((s ** (s ~~> a)) ~> ((s ~~> a) ** s)) -> (s ** (s ~~> 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 k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @s @(s ~~> a))
    in ExOptic GrateRes a b s t -> Grate 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).
(GrateRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic GrateRes a b) q s t
-> ExOptic GrateRes a b s t
ExProstrong @(Rep (Exp (s ~~> a))) @(Corep (Exp (s ~~> a))) ((s ~> (Exp (s ~~> a) @ a)) -> Rep (Exp (s ~~> a)) s a
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep s ~> (Exp (s ~~> a) @ a)
s ~> ((s ~~> a) ~~> a)
sa Rep (Exp (s ~~> a)) s a
-> ExOptic GrateRes a b a b
-> (:.:) (Rep (Exp (s ~~> a))) (ExOptic GrateRes 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 GrateRes 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 (Exp (s ~~> a))) (ExOptic GrateRes a b) s b
-> Corep (Exp (s ~~> a)) b t
-> (:.:)
     (Rep (Exp (s ~~> a)) :.: ExOptic GrateRes a b)
     (Corep (Exp (s ~~> a)))
     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
:.: ((Exp (s ~~> a) @ b) ~> t) -> Corep (Exp (s ~~> a)) b t
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (Exp (s ~~> a) @ b) ~> t
((s ~~> a) ~~> b) ~> t
f))