A mixed optic from (s,r) to (a,b) with residual ch.

• opticForward :: arr s (t ch a) splits the domain left boundary into the residual and the codomain left boundary.
• opticBackward :: arr (t ch b) r recombines the residual with the codomain right boundary.

For t = (,) and arr = (->) this is the concrete lens pair s -> (ch, a) and (ch, b) -> r. For t = Either it is a prism: the residual is the branch that did not match.

A mixed optic with the residual existentially hidden.

There is no residual value here, only a residual type: the forward leg produces the residual and the backward leg consumes it. This is why SomeOptic is cheaper than SomeBody, which must store a seed and therefore has no inhabitant at tensors with an uninhabited unit. identitySomeOptic exists at Either, where Unit Either = Void and the corresponding SomeBody identity does not.

Eliminator for the existential residual type.

Identity optic at the boundary pair (a,b). The residual is the tensor unit.

This is the only operation in the module that needs Unital rather than Strength, and it needs only the unitors.

Vertical composition of mixed optics.

Given opt1 from (s,r) to (a,b) with residual ch1 and opt2 from (a,b) to (u,v) with residual ch2, the composite has residual t ch1 ch2 — the tensoring of residuals in the coend formula. The residual order matches cascadeBody: first-applied on the left.

Note what is absent: composition reassociates and applies strength, but never slide. cascadeBody needs two slides, because a single Body must push one carrier past the payload so that one arrow sees both. An optic keeps its two residuals on the same side throughout. That is the precise sense in which body composition is the fused case of optic composition.

Unit and associativity hold only up to the residual unitor and associator, exactly as for Circ; the observational statements are in Axioma.Optic.

>>> opticUpdate (composeOptic inner outer) (+ 1) ((3, True), "hi")
((4,True),"hi")

The same result by nesting the updates — functoriality of opticUpdate:

>>> opticUpdate outer (opticUpdate inner (+ 1)) ((3, True), "hi")
((4,True),"hi")

identityOptic with the residual hidden.

composeOptic with the residuals hidden. Once hidden, the bracketing that makes composeOptic associative only up to the associator is no longer observable in the type.

Apply an optic to a plain base-arrow morphism.

A lens turns a focus-update into a whole-update; a prism turns a branch-update into a sum-update.

>>> opticUpdate firstLens (+ 1) (3, "hello")
(4,"hello")

>>> (opticUpdate prismLeft (+ 1) (Left 3), opticUpdate prismLeft (+ 1) (Right "hi"))
(Left 4,Right "hi")

Lawfulness is not enforced. opticUpdate o id == id is the round-trip condition, and a well-typed optic can fail it; Axioma.Optic carries a witness that it can.

opticUpdate through the existential.

The action of an optic on channel poles.

This is iomap with its two arguments read as the legs of an optic: opticForward prefixes the conjoint, opticBackward suffixes the companion. Since Circuit.Poles already describes that pair as "the left action of arr on In poles" and "the right action of arr on Out poles", an optic is a morphism of that enriched profunctor.

>>> let p = poles0 (const ()) (const ("hi", 7)) :: Poles (->) (String, Int) (String, Int)
>>> snd (splay0 (opticPoles firstLens p)) ()
(7,"hi")

A cartesian optic as a polynomial lens.

Currying the residual away turns the pair s -> (ch, a), (ch, b) -> r into s -> (a, b -> r), which is exactly applyLens :: Morphism (Mono r s) (Mono b a) -> s -> (a, b -> r).

>>> let (a, put) = applyLens (opticAsLens (SomeOptic firstLens)) (3, "hello") in (a, put 9)
(3,(9,"hello"))

A polynomial lens as a cartesian optic.

The residual is reconstructed as the continuation type b -> r — the classical "existential is a function" encoding. So lensAsOptic . opticAsLens changes the residual and is only an identity after the coend quotient; Axioma.Optic checks that it is an identity observationally, which is that quotient in action.