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

Synopsis

class SetterRes p q => GrateRes (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 (GrateRes :: (k +-> k) -> (k +-> k) -> Constraint)) s t a b
type Grate' (s :: k) (a :: k) = Grate s s a a
data Grating (a :: k) (b :: k) (s :: k) (t :: k) where
- Grating :: 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
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
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

Documentation

class SetterRes p q => GrateRes (p :: k +-> k) (q :: k +-> k) where Source Github #

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 Traversal, this needs no 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.

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

CopyDiscard k => GrateRes (Two :: k -> k -> Type) (CoTwo :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Kaleidoscope Methods zipWithP :: forall (s :: k) (a :: k) (b :: k) (t :: k). (Closed k, SymMonoidal k) => Two s a -> CoTwo b t -> forall (x :: k). Ob x => ((x ~~> a) ~> b) -> (x ~~> s) ~> t Source Github #
CategoryOf k => GrateRes (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, KnownNat n) => GrateRes (Pow n :: k -> k -> Type) (CoPow n :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Kaleidoscope 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, Ob m) => GrateRes (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 #
(GrateRes f g, GrateRes f' g') => GrateRes (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 (GrateRes :: (k +-> k) -> (k +-> k) -> Constraint)) s t a b Source Github #

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

data Grating (a :: k) (b :: k) (s :: k) (t :: k) where Source Github #

The eliminating carrier for grates: the polymorphic zipping function, as a profunctor in s/t.

Constructors

Grating :: 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

Instances

Instances details

(Closed k, SymMonoidal k, Ob a, Ob b, SubFlavor w (GrateRes :: (k +-> k) -> (k +-> k) -> Constraint)) => Prostrong (w :: FLAVOR k k) (Grating a b :: k -> k -> Type) Source Github #	Any flavor whose optics can zip has strength for the `Grating` carrier.
Instance details Defined in Proarrow.Optic.Grate Methods proact :: forall (f :: k +-> k) (g :: k +-> k). (w f g, Profunctor f, Profunctor g) => ((f :.: Grating a b) :.: g) :~> Grating a b Source Github #
(Closed k, SymMonoidal k, Ob a, Ob b) => Profunctor (Grating a b :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Grate Methods dimap :: forall (c :: k) (a0 :: k) (b0 :: k) (d :: k). (c ~> a0) -> (b0 ~> d) -> Grating a b a0 b0 -> Grating a b c d Source Github # lmap :: forall (c :: k) (a0 :: k) (b0 :: k). (c ~> a0) -> Grating a b a0 b0 -> Grating a b c b0 Source Github # rmap :: forall (b0 :: k) (d :: k) (a0 :: k). (b0 ~> d) -> Grating a b a0 b0 -> Grating a b a0 d Source Github # (\\) :: forall (a0 :: k) (b0 :: k) r. ((Ob a0, Ob b0) => r) -> Grating a b a0 b0 -> r Source Github #

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

Eliminate any grate-flavored optic to its zipping function, in either encoding.

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 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 exactly s ~~> a.