Safe Haskell	None
Language	GHC2024

Proarrow.Optic.MonoidalLens

Contents

Orphan instances

Description

The monoidal lens: the coend optic for the tensor action with a comonoidal residual,

MonoidalLens s t a b = exists m. Comonoid m => (s ~> m ** a, m ** b ~> t)

The residual can be discarded (counit :: m ~> Unit) and copied, which is what a lens's get needs, so a monoidal lens views, sets, folds and traverses:

Lens         <: { Getter, AffineTraversal, Glass }                     -- product residual
MonoidalLens <: { Getter, MonoidalTraversal, AffineTraversal, Glass }  -- comonoidal tensor residual

It is not a Lens, because putP works with binary products alone, unrelated to the tensor. It is an AffineTraversal and a Glass, because their methods ask for a cartesian category, where the tensor is the product and the residual can be projected out.

Synopsis

class (GetterFl p q, MonTravFl p q, AffineTravFl p q, GlassFl p q) => MonLensFl (p :: k +-> k) (q :: k +-> k) where
- withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r. SymMonoidal k => p s a -> q b t -> (forall (m :: k). Ob m => ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r) -> r
type MonoidalLens (s :: k) (t :: k) (a :: k) (b :: k) = Optic (Prostrong (MonLensFl :: (k +-> k) -> (k +-> k) -> Constraint)) s t a b
type MonoidalLens' (s :: k) (a :: k) = MonoidalLens s s a a
monLens :: forall {k} (m :: k) (s :: k) (t :: k) (a :: k) (b :: k). (Comonoid m, Ob a, Ob b) => (s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalLens s t a b
withMonLens :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (SymMonoidal k, (Ob a, Ob b) => c (ExOptic (MonLensFl :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> (forall (m :: k). Ob m => ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r) -> r

Documentation

class (GetterFl p q, MonTravFl p q, AffineTravFl p q, GlassFl p q) => MonLensFl (p :: k +-> k) (q :: k +-> k) where Source Github #

The monoidal-lens flavor: a lens whose residual is a comonoid, so it is a Getter and a MonoidalTraversal, and in cartesian categories an AffineTraversal and a Glass.

Methods

withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r. SymMonoidal k => p s a -> q b t -> (forall (m :: k). Ob m => ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r) -> r Source Github #

Recover a monoidal lens's two legs and the comonoid structure of its existential residual m. The comonoid comes as a value (ComonoidOn) rather than a Comonoid constraint, because the residual of a composite is a tensor and that of the identity the unit, and type families cannot head an instance. A tensor of comonoids is a comonoid by symmetry.

Instances

Instances details

CategoryOf k => MonLensFl (Id :: k -> k -> Type) (Id :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r. SymMonoidal k => Id s a -> Id b t -> (forall (m :: k). Ob m => ComonoidOn m -> (s ~> (m a)) -> ((m b) ~> t) -> r) -> r Source Github #
Comonoid m => MonLensFl (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 withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r. SymMonoidal k => Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) s a -> Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) b t -> (forall (m0 :: k). Ob m0 => ComonoidOn m0 -> (s ~> (m0 a)) -> ((m0 b) ~> t) -> r) -> r Source Github #
(MonLensFl f g, MonLensFl f' g') => MonLensFl (f :.: f' :: k -> k -> Type) (g' :.: g :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r. SymMonoidal k => (f :.: f') s a -> (g' :.: g) b t -> (forall (m :: k). Ob m => ComonoidOn m -> (s ~> (m a)) -> ((m b) ~> t) -> r) -> r Source Github #

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

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

monLens :: forall {k} (m :: k) (s :: k) (t :: k) (a :: k) (b :: k). (Comonoid m, Ob a, Ob b) => (s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalLens s t a b Source Github #

Build a monoidal lens from its two legs and a chosen comonoidal residual m.

withMonLens :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (SymMonoidal k, (Ob a, Ob b) => c (ExOptic (MonLensFl :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> (forall (m :: k). Ob m => ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r) -> r Source Github #

Eliminate any optic that is at least an iso and at most a monoidal lens to its two legs, recovering the existential residual m together with its comonoid structure: run it at its witness pair (ExOptic MonLensFl, via withLegs) and read the legs off with withMonLensP.

Orphan instances

Comonoid m => AffineFoldFl (Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) :: k -> k -> Type) (Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) :: k -> k -> Type) Source Github #	The tensor-action witness pair `Rep`/`Corep` `(ActionAt Tensor m)` views (and previews) when the residual `m` is a `Comonoid`: discard it with the counit. (Its setter and traversal instances live in Proarrow.Optic.Setter and Proarrow.Optic.Traversal.)
Instance details Methods previewP :: forall (s :: k) (a :: k). Bicartesian k => Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) s a -> s ~> (a \|\| (TerminalObject :: k)) Source Github #
Comonoid m => GetterFl (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 Methods getP :: forall (s :: k) (a :: k). Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) s a -> s ~> a Source Github #
Comonoid m => AffineTravFl (Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) :: k -> k -> Type) (Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) :: k -> k -> Type) Source Github #	In a cartesian category the tensor is the product, so the comonoidal residual can be projected out and put back: `affineSet` and `glassP` carry that assumption in their own constraints (`Bicartesian`, `CCC`), which is why these instances exist while a `LensFl` one cannot (`putP` has only `HasBinaryProducts`).
Instance details Methods affineMatch :: forall (s :: k) (a :: k) (b :: k) (t :: k). Bicartesian k => Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) s a -> Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) b t -> s ~> (t \|\| a) Source Github # affineSet :: forall (s :: k) (a :: k) (b :: k) (t :: k). Bicartesian k => Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) s a -> Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) b t -> (s && 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 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 && Mod s a b) ~> t Source Github #