Safe Haskell	None
Language	GHC2024

Proarrow.Optic.Glass

Description

The glass (Clarke et al., Profunctor optics: a categorical update): the optic for the combined action of the product and the exponential,

Glass s t a b = exists c d. (s ~> c && (d ~~> a), (c && (d ~~> b)) ~> t)

which collapses to the single leg (s && ((s ~~> a) ~~> b)) ~> t: given the source and a way to turn any selector s ~~> a into a b, produce a t. A lens is the case d = Unit (it applies the selector to the source it was given), a grate the case c = Unit (it ignores the source and feeds the selector through its exponent), so GlassFl is the join of LensFl and GrateFl -- what AffineTravFl is to lenses and prisms, one column over. Like that flavor it has no witnesses of its own: its generating pairs are the product pair and the exponential pair, and glass packs its single leg as their composite.

It sits directly below SetterFl: a glass sets, but it neither folds (grates do not) nor distributes an applicative (lenses do not).

Synopsis

class SetterFl p q => GlassFl (p :: k +-> k) (q :: k +-> k) where
- glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t
applySel :: forall {k} (s :: k) (a :: k) (b :: k). (Closed k, Ob s, Ob a, Ob b) => (s ~> a) -> ((s ~~> a) ~~> b) ~> b
type Glass (s :: k) (t :: k) (a :: k) (b :: k) = Optic (Prostrong (GlassFl :: (k +-> k) -> (k +-> k) -> Constraint)) s t a b
type Glass' (s :: k) (a :: k) = Glass s s a a
glass :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k). (CCC k, Ob s, Ob a, Ob b) => ((s && ((s ~~> a) ~~> b)) ~> t) -> Glass s t a b
withGlass :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (CCC k, (Ob a, Ob b) => c (ExOptic (GlassFl :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> (((s && ((s ~~> a) ~~> b)) ~> t) -> r) -> r

Documentation

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

The glass flavor. Its one method is the collapsed leg; everything is stated in a cartesian closed category, where the residual can be copied and selectors can be internalised.

Methods

glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t Source Github #

Instances

Instances details

CategoryOf k => GlassFl (Id :: k -> k -> Type) (Id :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Glass Methods glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => Id s a -> Id b t -> (s && ((s ~~> a) ~~> b)) ~> t Source Github #
(Monoidal k, HasCoproducts k, KnownNat n) => GlassFl (Pow n :: k -> k -> Type) (CoPow n :: k -> k -> Type) Source Github #	A power grate is a glass: ignore the source, and for each of the `n` positions feed the consumer the selector "project this focus". The selectors come from `splitPow` of `sl`, the consumer is copied `n` times with `powCopy`, `powZip` pairs them, and `powDist` applies each. Everything is stated with the `CopyDiscard` structure that `CCC` now provides, so the tensor and the product never have to be identified by hand.
Instance details Defined in Proarrow.Optic.PowerGrate Methods glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => Pow n s a -> CoPow n b t -> (s && ((s ~~> a) ~~> b)) ~> t Source Github #
Comonoid m => GlassFl (Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) :: k -> k -> Type) (Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) s a -> Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) b t -> (s && ((s ~~> a) ~~> b)) ~> t Source Github #
(Closed k, Ob d) => GlassFl (Rep (Exp d) :: k -> k -> Type) (Corep (Exp d) :: k -> k -> Type) Source Github #	The exponential pair, a grate witness: the source is ignored, and the consumer is fed the selector `\s -> h s d` for each point `d` of the exponent.
Instance details Defined in Proarrow.Optic.Glass Methods glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => Rep (Exp d) s a -> Corep (Exp d) b t -> (s && ((s ~~> a) ~~> b)) ~> t Source Github #
(HasBinaryProducts k, Ob c) => GlassFl (Rep (Product c) :: k -> k -> Type) (Corep (Product c) :: k -> k -> Type) Source Github #	The product pair, a lens witness: the selector is the lens's own `get`, applied to the source at hand; the residual is kept.
Instance details Defined in Proarrow.Optic.Glass Methods glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => Rep (Product c) s a -> Corep (Product c) b t -> (s && ((s ~~> a) ~~> b)) ~> t Source Github #
(GlassFl f g, GlassFl f' g') => GlassFl (f :.: f' :: k -> k -> Type) (g' :.: g :: k -> k -> Type) Source Github #	Composition threads the selector through: the outer glass is given the consumer `\sel -> inner (sel s, \sel' -> k (sel' . sel))`.
Instance details Defined in Proarrow.Optic.Glass Methods glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k). CCC k => (f :.: f') s a -> (g' :.: g) b t -> (s && ((s ~~> a) ~~> b)) ~> t Source Github #

applySel :: forall {k} (s :: k) (a :: k) (b :: k). (Closed k, Ob s, Ob a, Ob b) => (s ~> a) -> ((s ~~> a) ~~> b) ~> b Source Github #

Feed a fixed selector s ~> a to a selector-consumer.

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

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

glass :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k). (CCC k, Ob s, Ob a, Ob b) => ((s && ((s ~~> a) ~~> b)) ~> t) -> Glass s t a b Source Github #

Build a glass from its single leg. The residuals are the whole source and the "logarithm" s ~~> a, so the witness is the lens witness at s composed with the grate witness at s ~~> a.

withGlass :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (CCC k, (Ob a, Ob b) => c (ExOptic (GlassFl :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> (((s && ((s ~~> a) ~~> b)) ~> t) -> r) -> r Source Github #

Eliminate any glass-flavored optic (a lens, a grate, or a composite of both, in either encoding) to its single leg.