Safe Haskell	None
Language	GHC2024

Proarrow.Optic.MonoidalLens

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 m is carried through the tensor, and being a Comonoid it can be discarded (counit :: m ~> Unit) and copied -- which is exactly what a lens's get needs. So a monoidal lens is a genuine lens (it views, sets, folds and traverses), and it sits below MonoidalTraversal and Getter in the lattice, mirroring the ordinary Lens below AffineTraversal:

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

Crucially it asks Comonoid of the residual only, not CopyDiscard of the whole category: it works in every CopyDiscard category (there every object is a comonoid) and in genuinely non-cartesian ones like LINEAR for the residuals that are comonoids (the duplicable Ur objects). The ordinary Lens is the tensor = product specialization, where the residual is recoverable from s by projection.

Synopsis

data LensW (m :: k) (s :: k) (a :: k) where
- LensW :: forall {k} (m :: k) (a :: k) (s :: k). (Comonoid m, Ob a) => (s ~> (m ** a)) -> LensW m s a
data CoLensW (m :: k) (b :: k) (t :: k) where
- CoLensW :: forall {k} (m :: k) (b :: k) (t :: k). (Comonoid m, Ob b) => ((m ** b) ~> t) -> CoLensW m b t
class (GetterRes p q, MonTravRes p q) => MonLensRes (p :: k +-> k) (q :: k +-> k) where
- withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r. Monoidal k => p s a -> q b t -> (forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r) -> r
type MonoidalLens (s :: k) (t :: k) (a :: k) (b :: k) = Optic (Prostrong (MonLensRes :: (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
data MonShop (a :: k) (b :: k) (s :: k) (t :: k) where
- MonShop :: forall {k} (a :: k) (b :: k) (m :: k) (s :: k) (t :: k). (Ob a, Ob b, Ob m) => (s ~> (m ** a)) -> ((m ** b) ~> t) -> MonShop a b s t
withMonLens :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (Monoidal k, (Ob a, Ob b) => c (MonShop a b)) => Optic c s t a b -> (forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r) -> r

Documentation

data LensW (m :: k) (s :: k) (a :: k) where Source Github #

Witness pair for a monoidal lens: the focus a sits inside m ** a with a comonoidal residual m. Being a comonoid, m can be discarded (for get/fold) and carried (for set).

Constructors

LensW :: forall {k} (m :: k) (a :: k) (s :: k). (Comonoid m, Ob a) => (s ~> (m ** a)) -> LensW m s a

Instances

Instances details

Comonoid m => Profunctor (LensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> LensW m a b -> LensW m c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: k). (c ~> a) -> LensW m a b -> LensW m c b Source Github # rmap :: forall (b :: k) (d :: k) (a :: k). (b ~> d) -> LensW m a b -> LensW m a d Source Github # (\\) :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> LensW m a b -> r Source Github #
Comonoid m => Proadjunction (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods unit :: forall (a :: k). Ob a => (CoLensW m :.: LensW m) a a Source Github # counit :: (LensW m :.: CoLensW m) :~> ((~>) :: CAT k) Source Github #
Comonoid m => AffineFoldRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods previewP :: forall (s :: k) (a :: k). Bicartesian k => LensW m s a -> s ~> (a \|\| (TerminalObject :: k)) Source Github #
Comonoid m => FoldRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods foldMapP :: forall (m0 :: k) (s :: k) (a :: k). Monoid m0 => LensW m s a -> (a ~> m0) -> s ~> m0 Source Github #
Comonoid m => GetterRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods getP :: forall (s :: k) (a :: k). LensW m s a -> s ~> a Source Github #
Comonoid m => MonLensRes (LensW m :: k -> k -> Type) (CoLensW 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. Monoidal k => LensW m s a -> CoLensW m b t -> (forall (m0 :: k). Ob m0 => (s ~> (m0 a)) -> ((m0 b) ~> t) -> r) -> r Source Github #
Comonoid m => SetterRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods overP :: forall (s :: k) (a :: k) (b :: k) (t :: k). LensW m s a -> CoLensW m b t -> (a ~> b) -> s ~> t Source Github #
Comonoid m => MonTravRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods monTravP :: forall r (s :: k) (a :: k) (b :: k) (t :: k). StrongDistributiveProfunctor r => LensW m s a -> CoLensW m b t -> r a b -> r s t Source Github #
Comonoid m => TravRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods travP :: forall r (s :: k) (a :: k) (b :: k) (t :: k). (StrongDistributiveProfunctor r, Strong (ProdAction :: k -> (PROD k, k) -> Type) r) => LensW m s a -> CoLensW m b t -> r a b -> r s t Source Github #

data CoLensW (m :: k) (b :: k) (t :: k) where Source Github #

The covariant half of the LensW witness pair: the set leg, (m ** b) ~> t.

Constructors

CoLensW :: forall {k} (m :: k) (b :: k) (t :: k). (Comonoid m, Ob b) => ((m ** b) ~> t) -> CoLensW m b t

Instances

Instances details

Comonoid m => Profunctor (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> CoLensW m a b -> CoLensW m c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: k). (c ~> a) -> CoLensW m a b -> CoLensW m c b Source Github # rmap :: forall (b :: k) (d :: k) (a :: k). (b ~> d) -> CoLensW m a b -> CoLensW m a d Source Github # (\\) :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> CoLensW m a b -> r Source Github #
Comonoid m => Proadjunction (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods unit :: forall (a :: k). Ob a => (CoLensW m :.: LensW m) a a Source Github # counit :: (LensW m :.: CoLensW m) :~> ((~>) :: CAT k) Source Github #
Comonoid m => AffineFoldRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods previewP :: forall (s :: k) (a :: k). Bicartesian k => LensW m s a -> s ~> (a \|\| (TerminalObject :: k)) Source Github #
Comonoid m => FoldRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods foldMapP :: forall (m0 :: k) (s :: k) (a :: k). Monoid m0 => LensW m s a -> (a ~> m0) -> s ~> m0 Source Github #
Comonoid m => GetterRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods getP :: forall (s :: k) (a :: k). LensW m s a -> s ~> a Source Github #
Comonoid m => MonLensRes (LensW m :: k -> k -> Type) (CoLensW 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. Monoidal k => LensW m s a -> CoLensW m b t -> (forall (m0 :: k). Ob m0 => (s ~> (m0 a)) -> ((m0 b) ~> t) -> r) -> r Source Github #
Comonoid m => SetterRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods overP :: forall (s :: k) (a :: k) (b :: k) (t :: k). LensW m s a -> CoLensW m b t -> (a ~> b) -> s ~> t Source Github #
Comonoid m => MonTravRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods monTravP :: forall r (s :: k) (a :: k) (b :: k) (t :: k). StrongDistributiveProfunctor r => LensW m s a -> CoLensW m b t -> r a b -> r s t Source Github #
Comonoid m => TravRes (LensW m :: k -> k -> Type) (CoLensW m :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods travP :: forall r (s :: k) (a :: k) (b :: k) (t :: k). (StrongDistributiveProfunctor r, Strong (ProdAction :: k -> (PROD k, k) -> Type) r) => LensW m s a -> CoLensW m b t -> r a b -> r s t Source Github #

class (GetterRes p q, MonTravRes p q) => MonLensRes (p :: k +-> k) (q :: k +-> k) where Source Github #

The monoidal-lens flavor: a lens whose residual is a comonoid, so it is both a Getter and a MonoidalTraversal.

Methods

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

Recover a monoidal lens's two legs, with the (comonoidal) residual m existential.

Instances

Instances details

CategoryOf k => MonLensRes (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. Monoidal k => Id s a -> Id b t -> (forall (m :: k). Ob m => (s ~> (m a)) -> ((m b) ~> t) -> r) -> r Source Github #
Comonoid m => MonLensRes (LensW m :: k -> k -> Type) (CoLensW 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. Monoidal k => LensW m s a -> CoLensW m b t -> (forall (m0 :: k). Ob m0 => (s ~> (m0 a)) -> ((m0 b) ~> t) -> r) -> r Source Github #
(MonLensRes f g, MonLensRes f' g') => MonLensRes (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. Monoidal k => (f :.: f') s a -> (g' :.: g) b t -> (forall (m :: k). Ob m => (s ~> (m a)) -> ((m b) ~> t) -> r) -> r Source Github #

type MonoidalLens (s :: k) (t :: k) (a :: k) (b :: k) = Optic (Prostrong (MonLensRes :: (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.

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

The eliminating carrier for monoidal lenses: the two legs with the residual m existential.

Constructors

MonShop :: forall {k} (a :: k) (b :: k) (m :: k) (s :: k) (t :: k). (Ob a, Ob b, Ob m) => (s ~> (m ** a)) -> ((m ** b) ~> t) -> MonShop a b s t

Instances

Instances details

(Monoidal k, Ob a, Ob b, SubFlavor w (MonLensRes :: (k +-> k) -> (k +-> k) -> Constraint)) => Prostrong (w :: FLAVOR k k) (MonShop a b :: k -> k -> Type) Source Github #	Any flavor whose optics have monoidal-lens legs has strength for the `MonShop` carrier: absorbing a witness pair combines its residual with the carrier's by tensoring.
Instance details Defined in Proarrow.Optic.MonoidalLens Methods proact :: forall (f :: k +-> k) (g :: k +-> k). (w f g, Profunctor f, Profunctor g) => ((f :.: MonShop a b) :.: g) :~> MonShop a b Source Github #
(Monoidal k, Ob a, Ob b) => Profunctor (MonShop a b :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalLens Methods dimap :: forall (c :: k) (a0 :: k) (b0 :: k) (d :: k). (c ~> a0) -> (b0 ~> d) -> MonShop a b a0 b0 -> MonShop a b c d Source Github # lmap :: forall (c :: k) (a0 :: k) (b0 :: k). (c ~> a0) -> MonShop a b a0 b0 -> MonShop a b c b0 Source Github # rmap :: forall (b0 :: k) (d :: k) (a0 :: k). (b0 ~> d) -> MonShop a b a0 b0 -> MonShop a b a0 d Source Github # (\\) :: forall (a0 :: k) (b0 :: k) r. ((Ob a0, Ob b0) => r) -> MonShop a b a0 b0 -> r Source Github #

withMonLens :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (Monoidal k, (Ob a, Ob b) => c (MonShop a b)) => Optic c s t a b -> (forall (m :: k). Ob 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.