Safe Haskell	None
Language	GHC2024

Proarrow.Optic

Description

The encoding-agnostic core of the optics machinery: the Optic type (a rank-2 profunctor transformation forall p. c p => p a b -> p s t), optic flavors as witness-pair constraints (FLAVOR) with subtyping via flavor superclasses, carrier strength (Prostrong), and the existential encoding ExOptic with ex2prof/prof2ex/convert mediating between the two. Also home to the flavor-generic combinators iso, re and (%). The concrete optic kinds live in the Proarrow.Optic.* submodules, and the user-facing vocabulary (with the full subtyping lattice drawn out) is re-exported from Proarrow.Optics.

Synopsis

data OPTIC j k (c :: (j +-> k) -> Constraint) = OPT k j
type family OptL (p :: OPTIC j k c) :: k where ...
type family OptR (p :: OPTIC j k c) :: j where ...
data Optic_ (ab :: OPTIC j k c) (st :: OPTIC j k c) where
- Optic :: forall k (a :: k) j (b :: j) (s :: k) (t :: j) (c :: (j +-> k) -> Constraint). (Ob a, Ob b, Ob s, Ob t) => {..} -> Optic_ ('OPT a b :: OPTIC j k c) ('OPT s t :: OPTIC j k c)
type Optic (c :: (j +-> k) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j) = Optic_ ('OPT a b :: OPTIC j k c) ('OPT s t :: OPTIC j k c)
type Optic' (c :: (j +-> j) -> Constraint) (s :: j) (a :: j) = Optic c s s a a
(%) :: forall {j} {k} (c1 :: (j +-> k) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j) (c2 :: (j +-> k) -> Constraint) (c :: k) (d :: j). Optic c1 s t a b -> Optic c2 a b c d -> Optic (c1 :&&: c2) s t c d
type PIso (s :: k) (t :: j) (a :: k) (b :: j) = Optic (Profunctor :: (j +-> k) -> Constraint) s t a b
type PIso' (s :: j) (a :: j) = PIso s s a a
iso :: forall {j} {k} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j). (CategoryOf j, CategoryOf k) => (s ~> a) -> (b ~> t) -> Optic c s t a b
type FLAVOR j k = (k +-> k) -> (j +-> j) -> Constraint
class (forall (f :: k +-> k) (f' :: j +-> j) (g :: k +-> k) (g' :: j +-> j). (w f f', w g g') => w (f :.: g) (g' :.: f'), w (Id :: k -> k -> Type) (Id :: j -> j -> Type)) => Flavor (w :: FLAVOR j k) where
- composeFlavor :: forall (f :: k +-> k) (f' :: j +-> j) (g :: k +-> k) (g' :: j +-> j) r. (w f f', w g g') => (w (f :.: g) (g' :.: f') => r) -> r
class Sub (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j) where
- sub :: (w p q => r) -> r
class (Profunctor p, CategoryOf j, CategoryOf k) => Prostrong (w :: FLAVOR j k) (p :: j +-> k) where
- proact :: forall (f :: k +-> k) (g :: j +-> j). (w f g, Profunctor f, Profunctor g) => ((f :.: p) :.: g) :~> p
data ExOptic (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) where
- ExOptic :: forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j) (s :: k) (t :: j) (a :: k) (b :: j). (w p q, Profunctor p, Profunctor q) => p s a -> q b t -> ExOptic w a b s t
legs2prof :: forall {j} {k} (w :: FLAVOR j k) p q (s :: k) (t :: j) (a :: k) (b :: j). (CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) => p s a -> q b t -> Optic (Prostrong w) s t a b
ex2prof :: forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k) (t :: j). (CategoryOf j, CategoryOf k) => ExOptic w a b s t -> Optic (Prostrong w) s t a b
prof2ex :: forall {j} {k} (w :: FLAVOR j k) (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j). (CategoryOf j, CategoryOf k, Flavor w, (Ob a, Ob b) => c (ExOptic w a b)) => Optic c s t a b -> ExOptic w a b s t
withLegs :: forall {j} {k} w (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j) r. (CategoryOf j, CategoryOf k, Flavor w, (Ob a, Ob b) => c (ExOptic w a b)) => Optic c s t a b -> (forall (p :: k +-> k) (q :: j +-> j). (w p q, Profunctor p, Profunctor q) => p s a -> q b t -> r) -> r
convert :: forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j). (CategoryOf j, CategoryOf k, Flavor w, (Ob a, Ob b) => c (ExOptic w a b)) => Optic c s t a b -> Optic (Prostrong w) s t a b
data Re (p :: k -> k1 -> Type) (s :: k1) (t :: k) (a :: k1) (b :: k) where
- Re :: forall {k1} {k} (a :: k1) (b :: k) (p :: k -> k1 -> Type) (t :: k) (s :: k1). (Ob a, Ob b) => {..} -> Re p s t a b
class (forall (p :: k +-> j) (a :: k) (b :: j). coc p => c (Re p a b)) => ReversibleOptic (c :: (j +-> k) -> Constraint) (coc :: (k +-> j) -> Constraint) | c -> coc
re :: forall {j} {k} (a :: j) (b :: k) (c :: (k +-> j) -> Constraint) (coc :: (j +-> k) -> Constraint) (s :: j) (t :: k). (Ob a, Ob b, ReversibleOptic c coc) => Optic c s t a b -> Optic coc b a t s
class w p q => Flip (w :: k -> k1 -> Constraint) (q :: k1) (p :: k)
class c (Op q) => OpConstraint (c :: (OPPOSITE j -> OPPOSITE k -> Type) -> Constraint) (q :: j +-> k)
class w (Op g) (Op f) => OpFlavor (w :: (OPPOSITE j -> OPPOSITE k -> Type) -> (OPPOSITE j1 -> OPPOSITE k1 -> Type) -> Constraint) (f :: j1 +-> k1) (g :: j +-> k)
opOptic :: forall {j} {k} (c :: (OPPOSITE k -> OPPOSITE j -> Type) -> Constraint) (s :: j) (t :: k) (a :: j) (b :: k). (forall (p :: OPPOSITE j +-> OPPOSITE k). c p => c (Op (UnOp p)), CategoryOf j, CategoryOf k) => Optic (OpConstraint c) s t a b -> Optic c ('OP t) ('OP s) ('OP b) ('OP a)
unOpOptic :: forall {j} {k} (c :: (OPPOSITE k +-> OPPOSITE j) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j). Optic c ('OP t) ('OP s) ('OP b) ('OP a) -> Optic (OpConstraint c) s t a b

Documentation

data OPTIC j k (c :: (j +-> k) -> Constraint) Source Github #

Constructors

OPT k j

Instances

Instances details

(CategoryOf j, CategoryOf k) => CategoryOf (OPTIC j k c) Source Github #

Optics form a category: an object OPT s t pairs the object s an optic reads from (contravariant) with the object t it writes back (covariant), an arrow OPT a b ~> OPT s t is a c-flavored optic with focus a/b inside s/t, and composition is optic composition.

Instance details

Defined in Proarrow.Optic

Associated Types

type (~>)
Instance details Defined in Proarrow.Optic type (~>) = Optic_ :: OPTIC j k c -> OPTIC j k c -> Type

(CategoryOf j, CategoryOf k) => Promonad (Optic_ :: OPTIC j k c -> OPTIC j k c -> Type) Source Github #

Instance details

Defined in Proarrow.Optic

Methods

id :: forall (a :: OPTIC j k c). Ob a => Optic_ a a Source Github #

(.) :: forall (b :: OPTIC j k c) (c0 :: OPTIC j k c) (a :: OPTIC j k c). Optic_ b c0 -> Optic_ a b -> Optic_ a c0 Source Github #

(CategoryOf j, CategoryOf k) => Profunctor (Optic_ :: OPTIC j k c -> OPTIC j k c -> Type) Source Github #

Instance details

Defined in Proarrow.Optic

Methods

dimap :: forall (c0 :: OPTIC j k c) (a :: OPTIC j k c) (b :: OPTIC j k c) (d :: OPTIC j k c). (c0 ~> a) -> (b ~> d) -> Optic_ a b -> Optic_ c0 d Source Github #

lmap :: forall (c0 :: OPTIC j k c) (a :: OPTIC j k c) (b :: OPTIC j k c). (c0 ~> a) -> Optic_ a b -> Optic_ c0 b Source Github #

rmap :: forall (b :: OPTIC j k c) (d :: OPTIC j k c) (a :: OPTIC j k c). (b ~> d) -> Optic_ a b -> Optic_ a d Source Github #

(\\) :: forall (a :: OPTIC j k c) (b :: OPTIC j k c) r. ((Ob a, Ob b) => r) -> Optic_ a b -> r Source Github #

type (~>) Source Github #

Instance details

Defined in Proarrow.Optic

type (~>) = Optic_ :: OPTIC j k c -> OPTIC j k c -> Type

type Ob (opt :: OPTIC j k c) Source Github #

Instance details

Defined in Proarrow.Optic

type Ob (opt :: OPTIC j k c) = (opt ~ ('OPT (OptL opt) (OptR opt) :: OPTIC j k c), Ob (OptL opt), Ob (OptR opt))

type family OptL (p :: OPTIC j k c) :: k where ... Source Github #

Equations

OptL ('OPT j2 k2 :: OPTIC j1 k1 c) = j2

type family OptR (p :: OPTIC j k c) :: j where ... Source Github #

Equations

OptR ('OPT j2 k2 :: OPTIC j1 k1 c) = k2

data Optic_ (ab :: OPTIC j k c) (st :: OPTIC j k c) where Source Github #

Constructors

Optic
Fields :: forall k (a :: k) j (b :: j) (s :: k) (t :: j) (c :: (j +-> k) -> Constraint). (Ob a, Ob b, Ob s, Ob t) => { unOptic :: forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t } -> Optic_ ('OPT a b :: OPTIC j k c) ('OPT s t :: OPTIC j k c)

Instances

Instances details

(CategoryOf j, CategoryOf k) => Promonad (Optic_ :: OPTIC j k c -> OPTIC j k c -> Type) Source Github #
Instance details Defined in Proarrow.Optic Methods id :: forall (a :: OPTIC j k c). Ob a => Optic_ a a Source Github # (.) :: forall (b :: OPTIC j k c) (c0 :: OPTIC j k c) (a :: OPTIC j k c). Optic_ b c0 -> Optic_ a b -> Optic_ a c0 Source Github #
(CategoryOf j, CategoryOf k) => Profunctor (Optic_ :: OPTIC j k c -> OPTIC j k c -> Type) Source Github #
Instance details Defined in Proarrow.Optic Methods dimap :: forall (c0 :: OPTIC j k c) (a :: OPTIC j k c) (b :: OPTIC j k c) (d :: OPTIC j k c). (c0 ~> a) -> (b ~> d) -> Optic_ a b -> Optic_ c0 d Source Github # lmap :: forall (c0 :: OPTIC j k c) (a :: OPTIC j k c) (b :: OPTIC j k c). (c0 ~> a) -> Optic_ a b -> Optic_ c0 b Source Github # rmap :: forall (b :: OPTIC j k c) (d :: OPTIC j k c) (a :: OPTIC j k c). (b ~> d) -> Optic_ a b -> Optic_ a d Source Github # (\\) :: forall (a :: OPTIC j k c) (b :: OPTIC j k c) r. ((Ob a, Ob b) => r) -> Optic_ a b -> r Source Github #

type Optic (c :: (j +-> k) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j) = Optic_ ('OPT a b :: OPTIC j k c) ('OPT s t :: OPTIC j k c) Source Github #

type Optic' (c :: (j +-> j) -> Constraint) (s :: j) (a :: j) = Optic c s s a a Source Github #

(%) :: forall {j} {k} (c1 :: (j +-> k) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j) (c2 :: (j +-> k) -> Constraint) (c :: k) (d :: j). Optic c1 s t a b -> Optic c2 a b c d -> Optic (c1 :&&: c2) s t c d infixl 9 Source Github #

Compose two optics, of any (possibly different) flavors or encodings. The composite's constraint is the conjunction :&&:, so the composite is usable at the meet of the two flavors' capabilities: a lens composed with a prism previews, folds, traverses and sets, but no longer views or reviews. Use convert to name the composite at a single flavor for storage, e.g. convert (l % p) :: AffineTraversal s t a b.

type PIso (s :: k) (t :: j) (a :: k) (b :: j) = Optic (Profunctor :: (j +-> k) -> Constraint) s t a b Source Github #

An iso in the profunctor-class-flavored encoding (the P-prefix convention: plain optic names belong to the Prostrong-flavored encoding, P-prefixed ones to the profunctor-class-flavored one). Convert with fromPIso and toPIso.

type PIso' (s :: j) (a :: j) = PIso s s a a Source Github #

iso :: forall {j} {k} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j). (CategoryOf j, CategoryOf k) => (s ~> a) -> (b ~> t) -> Optic c s t a b Source Github #

Create an isomorphism from two arrows, at any optic constraint. This doesn't check that the arrows are inverses!

The same iso builds a Iso, a PIso, a PTraversal, ... depending on the type it is used at; since c is only determined by the use site, bind the result with a type signature.

type FLAVOR j k = (k +-> k) -> (j +-> j) -> Constraint Source Github #

class (forall (f :: k +-> k) (f' :: j +-> j) (g :: k +-> k) (g' :: j +-> j). (w f f', w g g') => w (f :.: g) (g' :.: f'), w (Id :: k -> k -> Type) (Id :: j -> j -> Type)) => Flavor (w :: FLAVOR j k) where Source Github #

A flavor: a class of witness pairs that is closed under composition and contains the identity pair. This is the monoidal structure of the residuals, with (Id, Id) as unit and (f :.: g, g' :.: f') (note the reversal on the right) as tensor.

Methods

composeFlavor :: forall (f :: k +-> k) (f' :: j +-> j) (g :: k +-> k) (g' :: j +-> j) r. (w f f', w g g') => (w (f :.: g) (g' :.: f') => r) -> r Source Github #

Instances

Instances details

(forall (f :: k +-> k) (f' :: j +-> j) (g :: k +-> k) (g' :: j +-> j). (w f f', w g g') => w (f :.: g) (g' :.: f'), w (Id :: k -> k -> Type) (Id :: j -> j -> Type)) => Flavor (w :: (k -> k -> Type) -> (j -> j -> Type) -> Constraint) Source Github #
Instance details Defined in Proarrow.Optic Methods composeFlavor :: forall (f :: k +-> k) (f' :: j +-> j) (g :: k +-> k) (g' :: j +-> j) r. (w f f', w g g') => (w (f :.: g) (g' :.: f') => r) -> r Source Github #

class Sub (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j) where Source Github #

w p q, as a class with a single instance instead of a bare constraint. The subtyping quantified constraint is spelled forall p q. v p q => Sub w p q because GHC solves the head of a quantified constraint from a superclass of its premise only when that superclass is strictly smaller than the head, which a bare w p q head never is. Behind the Sub instance w p q is an ordinary wanted, solved from the superclasses of v p q. sub hands it back as a given.

Sub has no superclass w p q: with one, a quantified given forall p q. w p q => Sub IsoFl p q would reach Profunctor p through the flavor superclasses, and GHC would reject the ordinary Profunctor instances as overlapping.

Methods

sub :: (w p q => r) -> r Source Github #

Instances

Instances details

w p q => Sub (w :: (k +-> k) -> (j +-> j) -> Constraint) (p :: k +-> k) (q :: j +-> j) Source Github #
Instance details Defined in Proarrow.Optic Methods sub :: (w p q => r) -> r Source Github #

class (Profunctor p, CategoryOf j, CategoryOf k) => Prostrong (w :: FLAVOR j k) (p :: j +-> k) where Source Github #

The carrier p is w-strong: a Tambara module for the flavor w. proact absorbs a w-witness pair (f, g) sandwiching p back into p, so that an optic built from that witness can distribute the carrier. The name is the profunctor ("pro") version of Proarrow.Category.Monoidal.Strength's Strong: its proact specializes to act for certain Rep/Corep pairs and to coact for certain Corep/Rep ones.

Methods

proact :: forall (f :: k +-> k) (g :: j +-> j). (w f g, Profunctor f, Profunctor g) => ((f :.: p) :.: g) :~> p Source Github #

Instances

Instances details

(Flavor w, Profunctor p) => Prostrong (w :: FLAVOR j k) (Pastro w p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.PastroTambara Methods proact :: forall (f :: k +-> k) (g :: j +-> j). (w f g, Profunctor f, Profunctor g) => ((f :.: Pastro w p) :.: g) :~> Pastro w p Source Github #
(Flavor w, Profunctor p) => Prostrong (w :: FLAVOR j k) (Tambara w p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.PastroTambara Methods proact :: forall (f :: k +-> k) (g :: j +-> j). (w f g, Profunctor f, Profunctor g) => ((f :.: Tambara w p) :.: g) :~> Tambara w p Source Github #
(CategoryOf k, forall (p :: k +-> k) (q :: k +-> k). w p q => Sub (IsoFl :: (k +-> k) -> (k +-> k) -> Constraint) p q) => Prostrong (w :: FLAVOR k k) (Yo a ('OP b) :: k -> k -> Type) Source Github #	Any flavor whose optics are isos has strength for the `Yo` profunctor.
Instance details Defined in Proarrow.Optic.Iso Methods proact :: forall (f :: k +-> k) (g :: k +-> k). (w f g, Profunctor f, Profunctor g) => ((f :.: Yo a ('OP b)) :.: g) :~> Yo a ('OP b) Source Github #
(CategoryOf j, CategoryOf k, forall (p :: k +-> k) (q :: j +-> j). v p q => Sub w p q, Flavor w) => Prostrong (v :: FLAVOR j k) (ExOptic w a b :: k -> j -> Type) Source Github #	The free `w`-strong profunctor is `v`-strong for every subflavor `v` of `w`. With it `convert` and `withLegs` accept optics of any encoding (composites included). This one bridge instance replaces a per-carrier one for each flavor.
Instance details Defined in Proarrow.Optic Methods proact :: forall (f :: k +-> k) (g :: j +-> j). (v f g, Profunctor f, Profunctor g) => ((f :.: ExOptic w a b) :.: g) :~> ExOptic w a b Source Github #
(CategoryOf j, CategoryOf k, Prostrong (Flip w) p) => Prostrong (w :: (j +-> j) -> (k +-> k) -> Constraint) (Re p s t :: j -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic Methods proact :: forall (f :: j +-> j) (g :: k +-> k). (w f g, Profunctor f, Profunctor g) => ((f :.: Re p s t) :.: g) :~> Re p s t Source Github #
Traversable t => Prostrong (KaleidoFl :: (Type +-> Type) -> (Type +-> Type) -> Constraint) (Costar (Prelude t) :: Type -> Type -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Kaleidoscope Methods proact :: forall (f :: Type +-> Type) (g :: Type +-> Type). (KaleidoFl f g, Profunctor f, Profunctor g) => ((f :.: Costar (Prelude t)) :.: g) :~> Costar (Prelude t) Source Github #
Prostrong (KaleidoFl :: (Type +-> Type) -> (Type +-> Type) -> Constraint) (Costar []) Source Github #
Instance details Defined in Proarrow.Optic.Kaleidoscope Methods proact :: forall (f :: Type +-> Type) (g :: Type +-> Type). (KaleidoFl f g, Profunctor f, Profunctor g) => ((f :.: Costar []) :.: g) :~> Costar [] Source Github #
Functor f => Prostrong (LensFl :: (Type +-> Type) -> (Type +-> Type) -> Constraint) (Star (Prelude f) :: Type -> Type -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Lens Methods proact :: forall (f0 :: Type +-> Type) (g :: Type +-> Type). (LensFl f0 g, Profunctor f0, Profunctor g) => ((f0 :.: Star (Prelude f)) :.: g) :~> Star (Prelude f) Source Github #
(Traversable t, Representable t) => Prostrong (CotravFl :: (j +-> j) -> (j +-> j) -> Constraint) (RepCostar t :: j -> j -> Type) Source Github #	The carriers as instances, so that an optic of these flavors composed with another flavor that also runs at the carrier can be eliminated there directly.
Instance details Defined in Proarrow.Optic.Kaleidoscope Methods proact :: forall (f :: j +-> j) (g :: j +-> j). (CotravFl f g, Profunctor f, Profunctor g) => ((f :.: RepCostar t) :.: g) :~> RepCostar t Source Github #
(Traversable t, Representable t) => Prostrong (KaleidoFl :: (j +-> j) -> (j +-> j) -> Constraint) (RepCostar t :: j -> j -> Type) Source Github #
Instance details Defined in Proarrow.Optic.Kaleidoscope Methods proact :: forall (f :: j +-> j) (g :: j +-> j). (KaleidoFl f g, Profunctor f, Profunctor g) => ((f :.: RepCostar t) :.: g) :~> RepCostar t Source Github #
(Cartesian k, Functor f) => Prostrong (PowerGrateFl :: (k +-> k) -> (k +-> k) -> Constraint) (Costar f :: k -> k -> Type) Source Github #	The carrier of the literature's kaleidoscope eliminator (`>-`): `Costar f`, i.e. `f a -> b` for any functor `f` on a cartesian category. Power grates distribute any `MonoidalProfunctor`, and `Costar f` is one, so this is `powerGrateP` at that carrier. It is an instance (and not only reachable through `powerGrateOf`) so that a power grate composed with another flavor that also runs at `Costar f`, an algebraic lens say, can be eliminated there directly.
Instance details Defined in Proarrow.Optic.PowerGrate Methods proact :: forall (f0 :: k +-> k) (g :: k +-> k). (PowerGrateFl f0 g, Profunctor f0, Profunctor g) => ((f0 :.: Costar f) :.: g) :~> Costar f Source Github #
OplaxMonoidalRep m => Prostrong (AlgLensFl m :: (k +-> k) -> (k +-> k) -> Constraint) (RepCostar m :: k -> k -> Type) Source Github #	The carrier of the literature's algebraic-lens eliminator: `RepCostar m`, i.e. `m % a ~> b`. Absorbing an algebraic-lens witness pair collapses the residuals of the incoming computation through their algebra and hands the foci on as one `m`-computation.
Instance details Defined in Proarrow.Optic.Action Methods proact :: forall (f :: k +-> k) (g :: k +-> k). (AlgLensFl m f g, Profunctor f, Profunctor g) => ((f :.: RepCostar m) :.: g) :~> RepCostar m Source Github #
CategoryOf k => Prostrong (Flip (IsoFl :: (k +-> k) -> (k +-> k) -> Constraint) :: (k +-> k) -> (k +-> k) -> Constraint) (Yo a ('OP b) :: k -> k -> Type) Source Github #	`re`-versed isos are still isos: the same carrier eliminates them by reading the witness pair backwards. This is a conversion the subtyping lattice cannot express (the entailment `IsoFl q p => IsoFl p q` doesn't hold), but the carrier can compute it.
Instance details Defined in Proarrow.Optic.Iso Methods proact :: forall (f :: k +-> k) (g :: k +-> k). (Flip (IsoFl :: (k +-> k) -> (k +-> k) -> Constraint) f g, Profunctor f, Profunctor g) => ((f :.: Yo a ('OP b)) :.: g) :~> Yo a ('OP b) Source Github #
(Prostrong w p, CategoryOf j, CategoryOf k) => Prostrong (OpFlavor w :: (k +-> k) -> (j +-> j) -> Constraint) (UnOp p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Optic Methods proact :: forall (f :: k +-> k) (g :: j +-> j). (OpFlavor w f g, Profunctor f, Profunctor g) => ((f :.: UnOp p) :.: g) :~> UnOp p Source Github #
(Prostrong w p, CategoryOf j, CategoryOf k) => Prostrong (w :: FLAVOR (OPPOSITE k) (OPPOSITE j)) (Op (UnOp p) :: OPPOSITE j -> OPPOSITE k -> Type) Source Github #
Instance details Defined in Proarrow.Optic Methods proact :: forall (f :: OPPOSITE j +-> OPPOSITE j) (g :: OPPOSITE k +-> OPPOSITE k). (w f g, Profunctor f, Profunctor g) => ((f :.: Op (UnOp p)) :.: g) :~> Op (UnOp p) Source Github #

data ExOptic (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) where Source Github #

The existential encoding of an optic.

Constructors

ExOptic :: forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j) (s :: k) (t :: j) (a :: k) (b :: j). (w p q, Profunctor p, Profunctor q) => p s a -> q b t -> ExOptic w a b s t

Instances

Instances details

(CategoryOf j, CategoryOf k, forall (p :: k +-> k) (q :: j +-> j). v p q => Sub w p q, Flavor w) => Prostrong (v :: FLAVOR j k) (ExOptic w a b :: k -> j -> Type) Source Github #	The free `w`-strong profunctor is `v`-strong for every subflavor `v` of `w`. With it `convert` and `withLegs` accept optics of any encoding (composites included). This one bridge instance replaces a per-carrier one for each flavor.
Instance details Defined in Proarrow.Optic Methods proact :: forall (f :: k +-> k) (g :: j +-> j). (v f g, Profunctor f, Profunctor g) => ((f :.: ExOptic w a b) :.: g) :~> ExOptic w a b Source Github #
(Monoidal k, Ob a, Ob b, Flavor w, forall (m :: k). Ob m => w (Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m)) (Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m))) => Costrong (Tensor :: k -> (k, k) -> Type) (ExOptic w a b :: k -> k -> Type) Source Github #	The generic carrier absorbs the residual of a `Costrong` action whenever the flavor contains the tracer generator: one more tensor-action layer, composed onto the witnesses. With it, profunctor-class-flavored tracers (`PTracer`) eliminate through `ExOptic` too.
Instance details Defined in Proarrow.Optic.Tracer Methods coact :: forall (a0 :: k) (x :: k) (y :: k). (Ob a0, Ob x, Ob y) => ExOptic w a b (Act (Tensor :: k -> (k, k) -> Type) a0 x) (Act (Tensor :: k -> (k, k) -> Type) a0 y) -> ExOptic w a b x y Source Github #
(Monoidal k, Ob a, Ob b, Flavor w, forall (x :: k). Ob x => w (Rep (ActionAt (Tensor :: k -> (k, k) -> Type) x)) (Corep (ActionAt (Tensor :: k -> (k, k) -> Type) x))) => Strong (Tensor :: k -> (k, k) -> Type) (ExOptic w a b :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalTraversal Methods act :: forall (a0 :: k) (x :: k) (y :: k). Ob a0 => ExOptic w a b x y -> ExOptic w a b (Act (Tensor :: k -> (k, k) -> Type) a0 x) (Act (Tensor :: k -> (k, k) -> Type) a0 y) Source Github #
(Monoidal k, Ob a, Ob b, w (UnitW :: k -> k -> Type) (CoUnitW :: k -> k -> Type), forall (p1 :: k -> k -> Type) (p2 :: k -> k -> Type) (q1 :: k -> k -> Type) (q2 :: k -> k -> Type). (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2) => w (Beside p1 p2) (CoBeside q1 q2)) => MonoidalProfunctor (ExOptic w a b :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalTraversal Methods one :: ExOptic w a b (Unit :: k) (Unit :: k) Source Github # () :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k). ExOptic w a b x1 x2 -> ExOptic w a b y1 y2 -> ExOptic w a b (x1 y1) (x2 ** y2) Source Github #
(CategoryOf j, CategoryOf k) => Profunctor (ExOptic w a b :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Optic Methods dimap :: forall (c :: k) (a0 :: k) (b0 :: j) (d :: j). (c ~> a0) -> (b0 ~> d) -> ExOptic w a b a0 b0 -> ExOptic w a b c d Source Github # lmap :: forall (c :: k) (a0 :: k) (b0 :: j). (c ~> a0) -> ExOptic w a b a0 b0 -> ExOptic w a b c b0 Source Github # rmap :: forall (b0 :: j) (d :: j) (a0 :: k). (b0 ~> d) -> ExOptic w a b a0 b0 -> ExOptic w a b a0 d Source Github # (\\) :: forall (a0 :: k) (b0 :: j) r. ((Ob a0, Ob b0) => r) -> ExOptic w a b a0 b0 -> r Source Github #
(HasCoproducts k, Ob a, Ob b, Flavor w, forall (t :: k). Ob t => w (Rep (Coproduct t)) (Corep (Coproduct t))) => Strong (CoprodAction :: k -> (COPROD k, k) -> Type) (ExOptic w a b :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalTraversal Methods act :: forall (a0 :: COPROD k) (x :: k) (y :: k). Ob a0 => ExOptic w a b x y -> ExOptic w a b (Act (CoprodAction :: k -> (COPROD k, k) -> Type) a0 x) (Act (CoprodAction :: k -> (COPROD k, k) -> Type) a0 y) Source Github #
(HasProducts k, Ob a, Ob b, Flavor w, forall (s :: k). Ob s => w (Rep (Product s)) (Corep (Product s))) => Strong (ProdAction :: k -> (PROD k, k) -> Type) (ExOptic w a b :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalTraversal Methods act :: forall (a0 :: PROD k) (x :: k) (y :: k). Ob a0 => ExOptic w a b x y -> ExOptic w a b (Act (ProdAction :: k -> (PROD k, k) -> Type) a0 x) (Act (ProdAction :: k -> (PROD k, k) -> Type) a0 y) Source Github #
(HasCoproducts k, Ob a, Ob b, w (ZeroW :: k -> k -> Type) (CoZeroW :: k -> k -> Type), forall (p1 :: k -> k -> Type) (p2 :: k -> k -> Type) (q1 :: k -> k -> Type) (q2 :: k -> k -> Type). (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2) => w (BesideSum p1 p2) (CoBesideSum q1 q2)) => MonoidalProfunctor (Coprod (ExOptic w a b) :: COPROD k -> COPROD k -> Type) Source Github #
Instance details Defined in Proarrow.Optic.MonoidalTraversal Methods one :: Coprod (ExOptic w a b) (Unit :: COPROD k) (Unit :: COPROD k) Source Github # () :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k) (y2 :: COPROD k). Coprod (ExOptic w a b) x1 x2 -> Coprod (ExOptic w a b) y1 y2 -> Coprod (ExOptic w a b) (x1 y1) (x2 ** y2) Source Github #

legs2prof :: forall {j} {k} (w :: FLAVOR j k) p q (s :: k) (t :: j) (a :: k) (b :: j). (CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) => p s a -> q b t -> Optic (Prostrong w) s t a b Source Github #

Build a Prostrong-flavored optic from a w-witness pair (the two legs p s a and q b t) by wrapping them around the carrier with one proact. Every optic constructor (lens, prism, ...) is legs2prof of its generating witness pair; ex2prof is the same on the packaged ExOptic.

ex2prof :: forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k) (t :: j). (CategoryOf j, CategoryOf k) => ExOptic w a b s t -> Optic (Prostrong w) s t a b Source Github #

prof2ex :: forall {j} {k} (w :: FLAVOR j k) (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j). (CategoryOf j, CategoryOf k, Flavor w, (Ob a, Ob b) => c (ExOptic w a b)) => Optic c s t a b -> ExOptic w a b s t Source Github #

Run an optic, in any encoding, at its own witness pair (the Pastro-Street move): a Prostrong-flavored optic discharges c (ExOptic w a b) through the bridge instance above (i.e. forall p q. v p q => Sub w p q), a (%)-composite one conjunct at a time, and a profunctor-class-flavored one through the carrier's own instances of its class.

withLegs :: forall {j} {k} w (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j) r. (CategoryOf j, CategoryOf k, Flavor w, (Ob a, Ob b) => c (ExOptic w a b)) => Optic c s t a b -> (forall (p :: k +-> k) (q :: j +-> j). (w p q, Profunctor p, Profunctor q) => p s a -> q b t -> r) -> r Source Github #

prof2ex in continuation-passing form: the generic eliminator.

convert :: forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j). (CategoryOf j, CategoryOf k, Flavor w, (Ob a, Ob b) => c (ExOptic w a b)) => Optic c s t a b -> Optic (Prostrong w) s t a b Source Github #

Convert an optic to a chosen flavor w, by running it at ExOptic w a b and wrapping the resulting witness pair back around the carrier. A Prostrong-flavored optic converts along the subtyping lattice (an invalid conversion fails with Could not deduce (w p q)), a :&&:-composite when both conjuncts do, and a profunctor-class-flavored optic when ExOptic w a b has an instance of its class (cf. fromPIso, fromPTraversal, fromPTracer).

Consumers accept any sufficiently strong optic directly, but constructors and % return their exact type, so convert is how to store an optic at a weaker type, e.g. convert (lens f g) :: Traversal' s a.

data Re (p :: k -> k1 -> Type) (s :: k1) (t :: k) (a :: k1) (b :: k) where Source Github #

The reversing carrier implementing re: it stores a continuation p b a -> p t s, so running an optic at Re p _ _ builds the optic turned around. Its Prostrong instance absorbs the witness pair mirrored, via Flip.

Constructors

Re
Fields :: forall {k1} {k} (a :: k1) (b :: k) (p :: k -> k1 -> Type) (t :: k) (s :: k1). (Ob a, Ob b) => { unRe :: p b a -> p t s } -> Re p s t a b

Instances

Instances details

(CategoryOf j, CategoryOf k, Prostrong (Flip w) p) => Prostrong (w :: (j +-> j) -> (k +-> k) -> Constraint) (Re p s t :: j -> k -> Type) Source Github #
Instance details Defined in Proarrow.Optic Methods proact :: forall (f :: j +-> j) (g :: k +-> k). (w f g, Profunctor f, Profunctor g) => ((f :.: Re p s t) :.: g) :~> Re p s t Source Github #
Profunctor p => Profunctor (Re p s t :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Optic Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> Re p s t a b -> Re p s t c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> Re p s t a b -> Re p s t c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> Re p s t a b -> Re p s t a d Source Github # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Re p s t a b -> r Source Github #

class (forall (p :: k +-> j) (a :: k) (b :: j). coc p => c (Re p a b)) => ReversibleOptic (c :: (j +-> k) -> Constraint) (coc :: (k +-> j) -> Constraint) | c -> coc Source Github #

Instances

Instances details

ReversibleOptic (Profunctor :: (j +-> k) -> Constraint) (Profunctor :: (k +-> j) -> Constraint) Source Github #
Instance details Defined in Proarrow.Optic
(ReversibleOptic l l', ReversibleOptic r r') => ReversibleOptic (l :&&: r :: (j +-> k) -> Constraint) (l' :&&: r' :: (k +-> j) -> Constraint) Source Github #
Instance details Defined in Proarrow.Optic
ReversibleOptic (Prostrong w :: (k +-> j) -> Constraint) (Prostrong (Flip w) :: (j +-> k) -> Constraint) Source Github #
Instance details Defined in Proarrow.Optic

re :: forall {j} {k} (a :: j) (b :: k) (c :: (k +-> j) -> Constraint) (coc :: (j +-> k) -> Constraint) (s :: j) (t :: k). (Ob a, Ob b, ReversibleOptic c coc) => Optic c s t a b -> Optic coc b a t s Source Github #

class w p q => Flip (w :: k -> k1 -> Constraint) (q :: k1) (p :: k) Source Github #

Instances

Instances details

w p q => Flip (w :: k1 -> k2 -> Constraint) (q :: k2) (p :: k1) Source Github #
Instance details Defined in Proarrow.Optic

class c (Op q) => OpConstraint (c :: (OPPOSITE j -> OPPOSITE k -> Type) -> Constraint) (q :: j +-> k) Source Github #

Instances

Instances details

c (Op q) => OpConstraint (c :: (OPPOSITE j -> OPPOSITE k -> Type) -> Constraint) (q :: j +-> k) Source Github #
Instance details Defined in Proarrow.Optic

class w (Op g) (Op f) => OpFlavor (w :: (OPPOSITE j -> OPPOSITE k -> Type) -> (OPPOSITE j1 -> OPPOSITE k1 -> Type) -> Constraint) (f :: j1 +-> k1) (g :: j +-> k) Source Github #

Instances

Instances details

w (Op g) (Op f) => OpFlavor (w :: (OPPOSITE j1 -> OPPOSITE k1 -> Type) -> (OPPOSITE j2 -> OPPOSITE k2 -> Type) -> Constraint) (f :: j2 +-> k2) (g :: j1 +-> k1) Source Github #
Instance details Defined in Proarrow.Optic

opOptic :: forall {j} {k} (c :: (OPPOSITE k -> OPPOSITE j -> Type) -> Constraint) (s :: j) (t :: k) (a :: j) (b :: k). (forall (p :: OPPOSITE j +-> OPPOSITE k). c p => c (Op (UnOp p)), CategoryOf j, CategoryOf k) => Optic (OpConstraint c) s t a b -> Optic c ('OP t) ('OP s) ('OP b) ('OP a) Source Github #

unOpOptic :: forall {j} {k} (c :: (OPPOSITE k +-> OPPOSITE j) -> Constraint) (s :: k) (t :: j) (a :: k) (b :: j). Optic c ('OP t) ('OP s) ('OP b) ('OP a) -> Optic (OpConstraint c) s t a b Source Github #