Safe Haskell	None
Language	GHC2024

Proarrow.Optic.Grate

Description

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 Kaleidoscope (hence a Cotraversal and a Setter), and every 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.

Synopsis

class (KaleidoFl p q, GlassFl p q) => GrateFl (p :: k +-> k) (q :: k +-> k) where
- zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k). (Closed k, SymMonoidal k) => p s a -> q b t -> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t
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))
type Grate (s :: k) (t :: k) (a :: k) (b :: k) = Optic (Prostrong (GrateFl :: (k +-> k) -> (k +-> k) -> Constraint)) s t a b
type Grate' (s :: k) (a :: k) = Grate s s a a
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 :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> ((forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t) -> r) -> r
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

Documentation

class (KaleidoFl p q, GlassFl p q) => GrateFl (p :: k +-> k) (q :: k +-> k) where Source Github #

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 Traversal, this needs no 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. KaleidoFl is a superclass: the residual is a comonoid, so m ~~> - is an applicative functor.

Methods

zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k). (Closed k, SymMonoidal k) => p s a -> q b t -> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t Source Github #

Instances

Instances details

CategoryOf k => GrateFl (Id :: k -> k -> Type) (Id :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Grate Methods 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 Source Github #
(CopyDiscard k, HasCoproducts k, SNatI n) => GrateFl (Pow n :: k -> k -> Type) (CoPow n :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.PowerGrate Methods zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k). (Closed k, SymMonoidal k) => Pow n s a -> CoPow n b t -> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t Source Github #
(Closed k, SymMonoidal k, HasCoproducts k, CocommutativeComonoid m) => GrateFl (Rep (Exp m) :: k -> k -> Type) (Corep (Exp m) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Grate Methods 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 Source Github #
(GrateFl f g, GrateFl f' g') => GrateFl (f :.: f' :: i -> i -> Type) (g' :.: g :: i -> i -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Grate Methods 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 Source Github #

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)) Source Github #

Swap the argument order of a curried two-argument exponential: x ~~> (m ~~> a) ~> m ~~> (x ~~> a).

type Grate (s :: k) (t :: k) (a :: k) (b :: k) = Optic (Prostrong (GrateFl :: (k +-> k) -> (k +-> k) -> Constraint)) s t a b Source Github #

type Grate' (s :: k) (a :: k) = Grate s s a a Source Github #

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 :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> ((forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t) -> r) -> r Source Github #

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.

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 Source Github #

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 CopyDiscard category every object is.