Safe Haskell	None
Language	GHC2024

Proarrow.Optic.Tracer

Contents

Orphan instances

Description

The tracer: the write-only optic whose residual sits on the source and target side,

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

witnessed by Corep/Rep (ActionAt Tensor m) (TracerFl / withTracerP) -- a setter witness pair read the other way round, equivalently an ActFl Tensor pair with the roles of the two witnesses swapped. Running it forwards closes a feedback loop through the residual, so it distributes any Costrong profunctor (tracerP) and is a Setter exactly in a TracedMonoidal category; run backwards (over . re) it needs no trace at all. Build with tracer, eliminate with tracerOf (or over at the hom) or recover the legs with withTracer; fromPTracer/toPTracer mediate with the profunctor-class-flavored PTracer (Optic (Costrong Tensor)).

Synopsis

class (SetterFl p q, SetterFl q p) => TracerFl (p :: k +-> k) (q :: k +-> k) where
- withTracerP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r. Monoidal k => p s a -> q b t -> (forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r) -> r
tracerP :: forall {k} p q (s :: k) (a :: k) (b :: k) (t :: k) r. (TracerFl p q, Costrong (Tensor :: k -> (k, k) -> Type) r) => p s a -> q b t -> r a b -> r s t
type Tracer (s :: k) (t :: k) (a :: k) (b :: k) = Optic (Prostrong (TracerFl :: (k +-> k) -> (k +-> k) -> Constraint)) s t a b
type Tracer' (s :: k) (a :: k) = Tracer s s a a
tracer :: forall {k} (m :: k) (s :: k) (t :: k) (a :: k) (b :: k). (TracedMonoidal k, Ob m, Ob s, Ob t, Ob a, Ob b) => ((m ** s) ~> a) -> (b ~> (m ** t)) -> Tracer s t a b
tracerOf :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (Monoidal k, Costrong (Tensor :: k -> (k, k) -> Type) r, c (ExOptic (TracerFl :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> r a b -> r s t
withTracer :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (Monoidal k, (Ob a, Ob b) => c (ExOptic (TracerFl :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> (forall (m :: k). Ob m => ((m ** s) ~> a) -> (b ~> (m ** t)) -> r) -> r
type PTracer (s :: j) (t :: j) (a :: j) (b :: j) = Optic (Costrong (Tensor :: j -> (j, j) -> Type)) s t a b
fromPTracer :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k). TracedMonoidal k => PTracer s t a b -> Tracer s t a b
toPTracer :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k). CategoryOf k => Tracer s t a b -> PTracer s t a b

Documentation

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

The tracer flavor: a witness pair whose legs are m ** s ~> a and b ~> m ** t for an existential residual m -- the residual functor is applied to the source and target rather than to the foci, i.e. an ActFl Tensor pair with the roles of the two witnesses swapped. withTracerP recovers the legs (the withMonLensP of tracers), and distributing a Costrong profunctor (tracerP) is derived from them. This is the Prostrong counterpart of Costrong Tensor the way MonLensFl is of Strong Tensor.

Every tracer witness pair is a setter pair (SetterFl superclass, so over, set, (%~) all work) and its flip is one too (SetterFl q p, so over . re works without a trace, and convert t :: Optic (Prostrong (Flip SetterFl)) s t a b -- the converse fails, since a flipped setter need not have a trace, e.g. a flipped lens witness, so tracers are the subflavor of flipped setters that can also run forwards); TracedMonoidal rides in the instance context of the tensor-action witness, not in the method, so ordinary setters keep their honest constraints. Monoidal sits on the method rather than the class so that the identity witness needs only CategoryOf and IsoFl can include this flavor.

Methods

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

Recover the two legs, with the residual m existential.

Instances

Instances details

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

tracerP :: forall {k} p q (s :: k) (a :: k) (b :: k) (t :: k) r. (TracerFl p q, Costrong (Tensor :: k -> (k, k) -> Type) r) => p s a -> q b t -> r a b -> r s t Source Github #

Distribute any Costrong profunctor through a tracer witness pair: dimap the legs on and coact the residual away. At the hom this is overP.

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

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

tracer :: forall {k} (m :: k) (s :: k) (t :: k) (a :: k) (b :: k). (TracedMonoidal k, Ob m, Ob s, Ob t, Ob a, Ob b) => ((m ** s) ~> a) -> (b ~> (m ** t)) -> Tracer s t a b Source Github #

Build a tracer from its two legs and a chosen residual m: m ** s ~> a decomposes the source (given the residual), b ~> m ** t rebuilds the target and produces the residual to feed back.

tracerOf :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k) (a :: k) (b :: k) r. (Monoidal k, Costrong (Tensor :: k -> (k, k) -> Type) r, c (ExOptic (TracerFl :: (k +-> k) -> (k +-> k) -> Constraint) a b)) => Optic c s t a b -> r a b -> r s t Source Github #

Distribute any Costrong profunctor through a tracer (or any stronger optic). At the hom this is over, computing the feedback loop through the residual.

Accepts any encoding (cf. traverseOf): a PTracer works directly, as does a (%)-composite.

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

Eliminate any optic that is at least an iso and at most a tracer to its two legs, recovering the existential residual m, in either encoding: run it at its witness pair (ExOptic TracerFl, via withLegs) and read the legs off with withTracerP.

type PTracer (s :: j) (t :: j) (a :: j) (b :: j) = Optic (Costrong (Tensor :: j -> (j, j) -> Type)) s t a b Source Github #

A tracer in the profunctor-class-flavored encoding (cf. PIso). Equivalent to Tracer via toPTracer and fromPTracer.

fromPTracer :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k). TracedMonoidal k => PTracer s t a b -> Tracer s t a b Source Github #

Instantiate a profunctor-class tracer at the generic carrier ExOptic TracerFl a b, which is Costrong by the instance above (the Pastro-Street move).

toPTracer :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k). CategoryOf k => Tracer s t a b -> PTracer s t a b Source Github #

Eliminate a Tracer to its profunctor-class form: run tracerP at the caller's profunctor.

Orphan instances

(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. This is what lets profunctor-class-flavored tracers (`PTracer`) eliminate through `ExOptic` too.
Instance details 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 #
(TracedMonoidal k, Ob m) => SetterFl (Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) :: k -> k -> Type) (Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) :: k -> k -> Type) Source Github #	The tracer witness: the tensor-action pair read the other way round, `Corep (ActionAt Tensor m)` on the left and `Rep (ActionAt Tensor m)` on the right. Its `overP` is the trace of `m s ~> a ~> b ~> m t` over `m`, so it needs the category to be `TracedMonoidal`.
Instance details Methods overP :: forall (s :: k) (a :: k) (b :: k) (t :: k). Corep (ActionAt (Tensor :: k -> (k, k) -> Type) m) s a -> Rep (ActionAt (Tensor :: k -> (k, k) -> Type) m) b t -> (a ~> b) -> s ~> t Source Github #