Chapter 169Optional

Profunctors, Coends, and Optics

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

A configuration record has a field, and a program wants to read it and to replace it. Write $S$ for the record type and $A$ for the field type. The pair of operations is $get : S \to A, put : S \times A \to S,$ and every question in this chapter comes from asking what makes a particular pair a legitimate accessor and how two accessors compose.

Take $S : = A \times B$ with $get : = {pr}_{1}$ and $put ((a, b), a^{'}) : = (a^{'}, b)$ . Now take the same $S$ with $get : = {pr}_{1}$ and $put ((a, b), a^{'}) : = (a, b)$ , which ignores the new value. Both pairs have the same type. The second is not an accessor, and saying why requires an equation, not a type: $get (put (s, a)) = a$ fails for it. A third pair, with $put ((a, b), a^{'}) : = (a^{'}, b_{0})$ for a fixed $b_{0}$ , satisfies that equation and fails $put (s, get s) = s$ . A fourth, storing a counter of how many writes have occurred, satisfies both and fails $put (put (s, a), a^{'}) = put (s, a^{'})$ .

Definition 169.1 — Concrete lens and its laws ¶

A lens from $S$ to $A$ is a pair $get : S \to A$ and $put : S \times A \to S$ . It is lawful when $get (put (s, a)) = a, put (s, get s) = s, put (put (s, a), a^{'}) = put (s, a^{'}),$ called put-get, get-put and put-put.

Referenced from 4 locations

Profunctors, Coends, and Optics

Proposition 169.2 — Composition of lenses ¶

Let $({get}_{1}, {put}_{1})$ be a lens from $S$ to $A$ and $({get}_{2}, {put}_{2})$ a lens from $A$ to $B$ . Then $get : = {get}_{2} \circ {get}_{1}, put (s, b) : = {put}_{1} (s, {put}_{2} ({get}_{1} s, b))$ is a lens from $S$ to $B$ , and it is lawful when both are.

Referenced from 3 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.2 — Composition of lenses

Proof. Put-get. $\begin{aligned} get (put (s, b)) & \overset{d e f .}{=} {get}_{2} ({get}_{1} {put}_{1} (s, {put}_{2} ({get}_{1} s, b))) \\ \overset{p u t - g e t_{1}}{=} {get}_{2} ({put}_{2} ({get}_{1} s, b)) \overset{p u t - g e t_{2}}{=} b . \end{aligned}$

Get-put. $put (s, get s) \overset{d e f .}{=} {put}_{1} (s, {put}_{2} ({get}_{1} s, {get}_{2} {get}_{1} s)) \overset{g e t - p u t_{2}}{=} {put}_{1} (s, {get}_{1} s) \overset{g e t - p u t_{1}}{=} s .$

Put-put. Abbreviate $a : = {get}_{1} s$ . Then $\begin{aligned} put (put (s, b), b^{'}) & \overset{d e f .}{=} {put}_{1} ⟨ {put}_{1} (s, {put}_{2} (a, b)), {put}_{2} ({get}_{1} {put}_{1} (s, {put}_{2} (a, b)), b^{'}) ⟩ \\ \overset{p u t - g e t_{1}}{=} {put}_{1} ⟨ {put}_{1} (s, {put}_{2} (a, b)), {put}_{2} ({put}_{2} (a, b), b^{'}) ⟩ \\ \overset{p u t - p u t_{2}}{=} {put}_{1} ⟨ {put}_{1} (s, {put}_{2} (a, b)), {put}_{2} (a, b^{'}) ⟩ \\ \overset{p u t - p u t_{1}}{=} {put}_{1} (s, {put}_{2} (a, b^{'})) \overset{d e f .}{=} put (s, b^{'}) . \end{aligned}$ ◻

Three failures produced three laws, and the laws compose. The next paragraph produces the accessor that a lens cannot be.

Example 169.3 — A client that defeats the lens ¶

Let $S : = A + B$ and let a client wish to modify the left summand when it is present and leave the value alone otherwise. A $get : S \to A$ does not exist: there is nothing to return at an element of $B$ . The two operations that do exist are $match : S \to A + S, build : A \to S,$ with $match (inl a) = inl a$ , $match (inr b) = inr (inr b)$ and $build = inl$ . Such a pair is a prism, and it is lawful when $match (build a) = inl a and match s = inl a implies build a = s .$

Referenced from 3 locations

Profunctors, Coends, and Optics

Example 169.4 — A client that defeats both ¶

Let $S$ be a list of $A$ ’s and let a client wish to replace every element. Neither a lens nor a prism applies: there is not one focus but many. The operation that exists is $extract : S \to \underset{n \in N}{∐} A^{n} \times (A^{n} \to S),$ sending a list to its length, its elements, and the function rebuilding a list of that length. A traversal is such an operation. Its laws are stated in section 169.7 once the machinery that makes them short is available.

Referenced from 4 locations

Profunctors, Coends, and Optics

Three accessors with three shapes, three law sets, and no common composition. The rest of the chapter produces one definition covering all of them, one composition, and one notion of lawfulness, and proves that each specialises correctly.

Profunctors

Definition 169.5 — Profunctor ¶

Let $C$ be a category. A profunctor on $C$ is a functor $P : C^{op} \times C \to Set$ . Concretely, $P$ assigns a set $P (A, B)$ to each pair of objects and a function $dimap : {hom}_{C} (A^{'}, A) \times {hom}_{C} (B, B^{'}) \times P (A, B) ⟶ P (A^{'}, B^{'})$ satisfying $\begin{aligned} dimap ({id}_{A}, {id}_{B}) & = {id}_{P (A, B)}, \\ dimap (f^{'}, g^{'}) \circ dimap (f, g) & = dimap (f \circ f^{'}, g^{'} \circ g) . \end{aligned}$

Referenced from 5 locations

Profunctors, Coends, and Optics

The variance is forced by the intended reading: an element of $P (A, B)$ is a transformation consuming an $A$ and producing a $B$ , so a map into the consumed position and a map out of the produced position both act on it, in opposite directions.

Example 169.6 — Four profunctors on ¶

$Fun (A, B) : = {hom}_{Set} (A, B)$ , with $dimap (f, g) (h) : = g \circ h \circ f$ .
${Const}_{R} (A, B) : = R$ for a fixed set $R$ , with $dimap (f, g) : = {id}_{R}$ . This forgets both arguments.
$Tagged (A, B) : = B$ , with $dimap (f, g) : = g$ . This uses only the produced position.
${Kl}_{T} (A, B) : = {hom}_{Set} (A, T B)$ for a monad $T$ , with $dimap (f, g) (h) : = T (g) \circ h \circ f$ . Taking $T : = (-) \times W$ for a monoid $W$ gives an effect-sensitive example: the transformation may also emit an element of $W$ .

Each satisfies the two laws of definition 169.5: for item 1, both are associativity and unitality of composition; for item 2 both sides are the identity; for item 3 they are functoriality of the identity functor; for item 4 they are functoriality of $T$ together with item 1.

Referenced from 4 locations

Profunctors, Coends, and Optics

Definition 169.7 — Strength for an accessor shape ¶

Let $(M, \otimes, I)$ be a monoidal category acting on $C$ by $\cdot : M \times C \to C$ (definition 169.13). A Tambara structure for the action on a profunctor $P$ is a family $ζ_{A, B, M} : P (A, B) ⟶ P (M \cdot A, M \cdot B)$ natural in $A$ and $B$ , dinatural in $M$ , and satisfying $\begin{aligned} ζ_{A, B, I} & = P (λ_{A}^{- 1}, λ_{B}), \\ ζ_{M \cdot A, M \cdot B, N} \circ ζ_{A, B, M} & = P (α_{N, M, A}^{- 1}, α_{N, M, B}) \circ ζ_{A, B, N \otimes M}, \end{aligned}$ where $λ$ and $α$ are the unit and associativity data of the action.

Referenced from 9 locations

Profunctors, Coends, and Optics

Proposition 169.8 — Where the structure comes from ¶

Take $C : = Set$ .

For the action $M \cdot A : = M \times A$ of $(Set, \times, {*})$ , a Tambara structure on $Fun$ is the operation $h \mapsto {id}_{M} \times h$ , which is exactly what the $put$ of a lens applies to a modification of the focus.
For the action $M \cdot A : = M + A$ of $(Set, +, \emptyset)$ , a Tambara structure on $Fun$ is $h \mapsto {id}_{M} + h$ , which is what the $match$ of a prism applies on the branch where the focus is present.
${Const}_{R}$ carries a Tambara structure for every action, namely the identity; $Tagged$ carries one for the product action only after a choice of element of $M$ , and none uniformly.

Referenced from 4 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.8 — Where the structure comes from

Proof. For 1 and 2, the two equations of definition 169.7 are the unit and associativity coherences of the product and of the coproduct. For 3, the identity map makes both sides of each equation the identity; and a natural family $B ⟶ M \times B$ would give, at $B = {*}$ , an element of $M$ natural in $M$ , hence a natural transformation from the terminal object to the identity functor on $Set$ , which does not exist since $\emptyset$ has no element. ◻

Proposition 169.8 is the answer to a question that library documentation usually leaves open: the classes named “strong” and “choice” are not stipulations but the two instances of definition 169.7 for the two monoidal actions that the two accessor shapes use.

Dinaturality, ends, and coends

Let $P, Q : C^{op} \times C \to Set$ . A transformation between them should be a family $θ_{A, B} : P (A, B) ⟶ Q (A, B)$ , and naturality is the usual square. Now consider instead a family $θ_{A} : P (A, A) ⟶ Q (A, A)$ , in which the same object occupies both positions. Attempting to state naturality for $f : A \to B$ requires a square $\begin{array}{ccc} P (A, A) & \overset{θ_{A}}{\to} & Q (A, A) \\ ↓ & ↓ \\ P (B, B) & \overset{θ_{B}}{\to} & Q (B, B) \end{array}$ and neither vertical map exists: $P$ is contravariant in the first argument and covariant in the second, so $f$ induces $P (B, A) ⟶ P (A, A)$ and $P (A, A) ⟶ P (A, B)$ , not a map $P (A, A) ⟶ P (B, B)$ . The repair is to put the mixed object in the middle.

Definition 169.9 — Dinatural transformation ¶

A dinatural transformation $θ : P \to Q$ is a family $θ_{A} : P (A, A) ⟶ Q (A, A)$ such that for every $f : A \to B$ the hexagon $Q (f, {id}_{A}) \circ θ_{A} \circ P ({id}_{A}, f) = Q ({id}_{B}, f) \circ θ_{B} \circ P (f, {id}_{B}) : P (B, A) ⟶ Q (A, B)$ commutes.

Referenced from 4 locations

Profunctors, Coends, and Optics

Definition 169.10 — End and coend ¶

An end of $P$ is an object $\int_{A} P (A, A)$ with a dinatural family $π_{A} : \int_{A} P (A, A) ⟶ P (A, A)$ universal among such: every dinatural family out of a constant factors uniquely through it. A coend is an object $\int^{A} P (A, A)$ with a dinatural family $ι_{A} : P (A, A) ⟶ \int^{A} P (A, A)$ universal among dinatural families into a constant.

Referenced from 2 locations

Profunctors, Coends, and Optics

Proposition 169.11 — Ends and coends in ¶

Let $C$ be small and $P : C^{op} \times C \to Set$ .

$\int_{A} P (A, A)$ is the set of families $(x_{A})_{A}$ with $x_{A} \in P (A, A)$ such that $P ({id}_{A}, f) (x_{A}) = P (f, {id}_{B}) (x_{B})$ for every $f : A \to B$ .
$\int^{A} P (A, A)$ is the quotient of $\underset{A}{∐} P (A, A)$ by the equivalence relation generated by $(A, P (f, {id}_{A}) (y)) \sim (B, P ({id}_{B}, f) (y))$ for $f : A \to B$ and $y \in P (B, A)$ .

Referenced from 10 locations

Proof of Proposition 169.11 — Ends and coends in

Proof. End. The displayed set carries the projections $π_{A}$ , and the condition is exactly the hexagon of definition 169.9 for a constant source, whose two composites reduce to the two sides of the displayed equation. A dinatural family out of a set $X$ assigns $x \mapsto (θ_{A} x)$ , which lands in the displayed set by dinaturality and is the unique factoring map.

Coend. The quotient carries the injections $ι_{A}$ , and the generating relation is exactly the identification the hexagon forces on the disjoint union. A dinatural family into a set $Y$ identifies the two sides of every generating relation, hence factors through the quotient; the factoring is unique because the injections are jointly surjective. ◻

Lemma 169.12 — Yoneda reduction ¶

For $K : C \to Set$ and $X \in C$ , $\int^{C} {hom}_{C} (X, C) \times K C ≅ K X, \int_{C} ({hom}_{C} (C, X) ⟶ K C) ≅ K X$ when $K$ is contravariant in the second display.

Referenced from 9 locations

Proof of Lemma 169.12 — Yoneda reduction

Proof. For the first, the map from left to right sends the class of $(f, k)$ to $K (f) (k)$ ; it is well defined because the generating relation of proposition 169.11 identifies $(g \circ f, k)$ with $(f, K (g) (k))$ , and both have image $K (g \circ f) (k)$ . Its inverse sends $x \in K X$ to the class of $({id}_{X}, x)$ . One round trip is $K ({id}_{X}) = id$ ; the other sends the class of $(f, k)$ to the class of $({id}_{X}, K (f) (k))$ , and those are identified by the generating relation at $f$ . The second display is the same argument with the quotient replaced by the compatible-family description of proposition 169.11(1). ◻

Exercise 169.1 ¶

★★☆ Let $C$ be the two-object category with objects $0, 1$ , one non-identity map $f : 0 \to 1$ , and let $P (A, B) : = {hom}_{C} (A, B)$ .

List the four sets $P (A, B)$ and the disjoint union $P (0, 0) ⊔ P (1, 1)$ .
Compute the generating relation of proposition 169.11(2) explicitly and the resulting quotient.
Compute $\int_{A} P (A, A)$ and say why the two answers differ in cardinality.

Referenced from 2 locations

Profunctors, Coends, and Optics

The monoidal action

Chapter 159 supplies a symmetric monoidal category $(M, \otimes, I)$ with its associator, unitors and symmetry. An optic needs more: a way for $M$ to act on the category $C$ in which the data live. The two are different, and the difference is what allows a lens and a prism to be instances of one definition.

Definition 169.13 — Monoidal action ¶

A monoidal action of $(M, \otimes, I)$ on a category $C$ consists of a functor $\cdot : M \times C \to C$ together with natural isomorphisms $λ_{A} : I \cdot A ≅ A, α_{N, M, A} : (N \otimes M) \cdot A ≅ N \cdot (M \cdot A),$ subject to the two coherence conditions: the pentagon $α_{N, M, P \cdot A} \circ α_{N \otimes M, P, A} = ({id}_{N} \cdot α_{M, P, A}) \circ α_{N, M \otimes P, A} \circ (a_{N, M, P} \cdot {id}_{A}),$ where $a$ is the associator of $M$ , and the triangle $({id}_{M} \cdot λ_{A}) \circ α_{M, I, A} = r_{M} \cdot {id}_{A},$ where $r$ is the right unitor of $M$ .

Referenced from 9 locations

Proposition 169.14 — Two actions on ¶

$(Set, \times, {*})$ acts on $Set$ by $M \cdot A : = M \times A$ , with $λ$ and $α$ the evident bijections.
$(Set, +, \emptyset)$ acts on $Set$ by $M \cdot A : = M + A$ , with $λ$ and $α$ the evident bijections.

Both satisfy definition 169.13.

Referenced from 4 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.14 — Two actions on

Proof. In each case $λ$ and $α$ are bijections of finite constructions, and each coherence condition is an equation between two bijections built from the same components; following an arbitrary element through both sides gives the same result. For item 1 at the pentagon, an element $(((n, m), p), a)$ is sent by both composites to $(n, (m, (p, a)))$ ; for item 2, an element of a four-fold coproduct is sent by both composites to its copy in the corresponding summand. ◻

Remark 169.15 — An action is not an internal tensor ¶

In proposition 169.14 the acting category happens to be $Set$ again, and the action happens to be the monoidal product. Neither is required. Taking $C$ to be the category of pointed sets and $M$ to be $(Set, \times, {*})$ acting by $M \cdot (A, a_{0}) : = (M \times A, (m_{0}, a_{0}))$ for a chosen $m_{0}$ gives an action whose acting objects are not objects of $C$ ; the notion of definition 169.13 still applies, and no tensor on $C$ is used. The distinction matters because the residual object of an optic will live in $M$ , and quotienting over it is quotienting over acting objects, not over data.

Referenced from 2 locations

Profunctors, Coends, and Optics

Optics as a coend

Definition 169.16 — Optic ¶

Fix an action of $(M, \otimes, I)$ on $C$ . For pairs of objects $(S, S^{'})$ and $(A, A^{'})$ of $C$ , set $Optic ((S, S^{'}), (A, A^{'})) : = \int^{M \in M} {hom}_{C} (S, M \cdot A) \times {hom}_{C} (M \cdot A^{'}, S^{'}) .$ By proposition 169.11 this is the set of pairs $(l, r)$ with $l : S \to M \cdot A$ and $r : M \cdot A^{'} \to S^{'}$ , quotiented by the relation generated by $((f \cdot {id}_{A}) \circ l, r) \sim (l, r \circ (f \cdot {id}_{A^{'}}))$ for $l : S \to M \cdot A$ , $r : N \cdot A^{'} \to S^{'}$ and $f : M \to N$ in $M$ . Write $⟨ l ∣ r ⟩$ for the class of $(l, r)$ and call $M$ its residual.

Referenced from 8 locations

The residual is scratch space: information taken out of $S$ that must be kept in order to rebuild $S^{'}$ . Relation (169.1) says that no client may inspect it, since moving a map $f$ from one side to the other does not change the optic.

Proposition 169.17 — Composition ¶

The assignment $⟨ l_{2} ∣ r_{2} ⟩ \circ ⟨ l_{1} ∣ r_{1} ⟩ : = ⟨ (M_{1} \cdot l_{2}) \circ l_{1} | r_{1} \circ (M_{1} \cdot r_{2}) ⟩$ is well defined and makes pairs of objects of $C$ the objects of a category $Optic$ , with ${id}_{(S, S^{'})} : = ⟨ λ_{S}^{- 1} ∣ λ_{S^{'}} ⟩$ .

Referenced from 7 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.17 — Composition

Proof. Well-definedness. Replace the representative of the second optic by one related through $f : M_{2} \to N_{2}$ . The composite changes by $M_{1} \cdot f$ , and (169.1) applied at $M_{1} \otimes M_{2} \to M_{1} \otimes N_{2}$ identifies the two composites, using $α$ to rewrite $M_{1} \cdot (M_{2} \cdot A)$ as $(M_{1} \otimes M_{2}) \cdot A$ . Replacing the representative of the first optic is the same argument with $f \cdot {id}_{}$ on the outside.

Identity. For $⟨ l ∣ r ⟩$ with residual $M$ , $\begin{aligned} ⟨ l ∣ r ⟩ \circ ⟨ λ_{S}^{- 1} ∣ λ_{S^{'}} ⟩ & \overset{d e f .}{=} ⟨ (I \cdot l) \circ λ_{S}^{- 1} | λ_{S^{'}} \circ (I \cdot r) ⟩ \\ \overset{λ n a t u r a l}{=} ⟨ λ_{M \cdot A}^{- 1} \circ l | r \circ λ_{M \cdot A^{'}} ⟩ \overset{(169.1)}{=} ⟨ l ∣ r ⟩, \end{aligned}$ the last step moving the isomorphism $λ : I \otimes M \to M$ across, which is legal because it is a map of $M$ . The other unit law is the same calculation on the other side.

Associativity. Choose representatives of three optics with residuals $M_{1}, M_{2}, M_{3}$ simultaneously, which is legitimate because a coend in $Set$ over a product of indices may be computed one index at a time. Both bracketings give the pair $((M_{1} \cdot (M_{2} \cdot l_{3})) \circ (M_{1} \cdot l_{2}) \circ l_{1}, r_{1} \circ (M_{1} \cdot r_{2}) \circ (M_{1} \cdot (M_{2} \cdot r_{3})))$ after using $α$ to associate the residual, and $α$ is an isomorphism of $M$ , so (169.1) identifies the two. ◻

Proposition 169.18 — Lenses are optics for the product action ¶

For $C : = Set$ with the action $M \cdot A = M \times A$ , $Optic ((S, S), (A, A)) ≅ {hom}_{Set} (S, A) \times {hom}_{Set} (S \times A, S),$ and the isomorphism sends $⟨ l ∣ r ⟩$ to $({pr}_{2} \circ l, r \circ ({pr}_{1} l \times {id}_{A}))$ and $(get, put)$ to $⟨ ⟨ {id}_{S}, get ⟩ ∣ put ⟩$ .

Referenced from 10 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.18 — Lenses are optics for the product action

Proof. Compute the coend: $\begin{aligned} \int^{M} {hom}_{} (S, M \times A) \times {hom}_{} (M \times A, S) \\ ≅ \int^{M} {hom}_{} (S, M) \times {hom}_{} (S, A) \times {hom}_{} (M \times A, S) \\ ≅ {hom}_{} (S, A) \times {hom}_{} (S \times A, S), \end{aligned}$ The second step applies lemma 169.12 with $X : = S$ and $K M : = {hom}_{} (S, A) \times {hom}_{} (M \times A, S)$ , which is covariant in $M$ only through the second factor, contravariantly; the reduction therefore substitutes $S$ for $M$ . Tracing the two composites through the chain gives the displayed formulas. ◻

Proposition 169.19 — Prisms are optics for the coproduct action ¶

For $C : = Set$ with the action $M \cdot A = M + A$ , $Optic ((S, S), (A, A)) ≅ {hom}_{Set} (S, A + S) \times {hom}_{Set} (A, S) .$

Referenced from 6 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.19 — Prisms are optics for the coproduct action

Proof. The same computation with $+$ in place of $\times$ : ${hom}_{} (M + A, S) ≅ {hom}_{} (M, S) \times {hom}_{} (A, S)$ by the universal property of the coproduct, and then lemma 169.12 on the contravariant factor ${hom}_{} (M, S)$ substitutes for $M$ , leaving ${hom}_{} (S, A + S) \times {hom}_{} (A, S)$ . ◻

Remark 169.20 — A near miss ¶

Suppose the quotient (169.1) is dropped and an optic is taken to be a pair $(M, l, r)$ with the residual named. Composition can still be defined by the formula of proposition 169.17, but it depends on the representative: the two pairs $({*} \times M, ⟨ *, l ⟩, r \circ {pr}_{2}) and (M, l, r)$ describe the same accessor and compose to pairs with residuals ${*} \times M \times N$ and $M \times N$ , which are different objects. The resulting structure is not a category, since its identities do not satisfy the unit law on the nose. The quotient is therefore not tidying: it is what makes composition well defined.

Referenced from 4 locations

Profunctors, Coends, and Optics

Exercise 169.2 ¶

★★☆ Take $M$ to be the terminal monoidal category, with one object $I$ and one map, acting on $C$ by $I \cdot A = A$ .

Show that $Optic ((S, S^{'}), (A, A^{'}))$ is then ${hom}_{C} (S, A) \times {hom}_{C} (A^{'}, S^{'})$ , and identify the accessor family this describes.
Show that the quotient (169.1) is the identity relation in this case, and say which hypothesis of remark 169.20 therefore fails to bite.
Give an action for which $Optic ((S, S^{'}), (A, A^{'}))$ is the set of functions $S \to S^{'}$ ignoring $A$ and $A^{'}$ entirely, and name the accessor family.

Referenced from 2 locations

Profunctors, Coends, and Optics

The profunctor representation

Definition 169.21 — The category of Tambara modules ¶

Fix an action of $M$ on $C$ . Objects of $Tamb$ are pairs $(P, ζ)$ of a profunctor and a Tambara structure (definition 169.7); a morphism $(P, ζ) \to (Q, ξ)$ is a natural transformation $θ : P \Rightarrow Q$ with $ξ_{A, B, M} \circ θ_{A, B} = θ_{M \cdot A, M \cdot B} \circ ζ_{A, B, M}$ . Write $U : Tamb \to Prof$ for the forgetful functor.

Referenced from 2 locations

Profunctors, Coends, and Optics

Definition 169.22 — The generated Tambara module ¶

For a profunctor $P$ define $(Φ P) (X, Y) : = \int^{M \in M} \int^{C, D \in C} {hom}_{C} (X, M \cdot C) \times P (C, D) \times {hom}_{C} (M \cdot D, Y),$ with the Tambara structure that reindexes the residual by $N \otimes (-)$ . For the representable profunctor $E_{A, A^{'}} (C, D) : = {hom}_{C} (C, A) \times {hom}_{C} (A^{'}, D)$ this gives, by lemma 169.12 twice, $\begin{aligned} (Φ E_{A, A^{'}}) (X, Y) & ≅ \int^{M} {hom}_{C} (X, M \cdot A) \times {hom}_{C} (M \cdot A^{'}, Y) \\ = Optic ((X, Y), (A, A^{'})) . \end{aligned}$

Referenced from 5 locations

Profunctors, Coends, and Optics

Lemma 169.23 — Φ is left adjoint to U ¶

$Tamb (Φ P, T) ≅ Prof (P, U T)$ , naturally.

Referenced from 6 locations

Profunctors, Coends, and Optics

Proof of Lemma 169.23 — Φ is left adjoint to U

Proof. A morphism $Φ P \to T$ in $Tamb$ is, by proposition 169.11, a family of functions out of the coend, that is a dinatural family ${hom}_{} (X, M \cdot C) \times P (C, D) \times {hom}_{} (M \cdot D, Y) ⟶ T (X, Y),$ compatible with the Tambara structures. Given $θ : P \Rightarrow U T$ , define it by sending $(l, p, r)$ to $T (l, r) (ξ_{C, D, M} (θ_{C, D} p))$ , where $ξ$ is the structure of $T$ ; compatibility with the structures is the second equation of definition 169.7 for $ξ$ . Conversely, restricting a morphism $Φ P \to T$ along $M : = I$ and $l, r$ the unitors gives a natural transformation $P \Rightarrow U T$ , and the two constructions are mutually inverse by the unit equation of definition 169.7 and the coend relation. ◻

Theorem 169.24 — Profunctor representation ¶

For all objects $S, S^{'}, A, A^{'}$ of $C$ , $Optic ((S, S^{'}), (A, A^{'})) ≅ \int_{(P, ζ) \in Tamb} (P (A, A^{'}) ⟶ P (S, S^{'})),$ the end being the set of families $t_{P} : P (A, A^{'}) ⟶ P (S, S^{'})$ natural in $P$ over $Tamb$ .

Referenced from 10 locations

Proof of Theorem 169.24 — Profunctor representation

Proof. Proof idea. Both sides are computed by Yoneda: the right-hand side is a set of natural transformations out of an evaluation functor, and lemma 169.23 identifies that evaluation functor with a representable one, whose representing object is the optic set of definition 169.22.

Write ${ev}_{A, A^{'}} : = (U -) (A, A^{'}) : Tamb \to Set$ . By lemma 169.23 at $P : = E_{A, A^{'}}$ and the Yoneda lemma in $Prof$ , $Tamb (Φ E_{A, A^{'}}, T) ≅ Prof (E_{A, A^{'}}, U T) ≅ (U T) (A, A^{'}) = {ev}_{A, A^{'}} (T),$ so ${ev}_{A, A^{'}}$ is represented by $Φ E_{A, A^{'}}$ . Hence $\begin{aligned} \int_{P} ({ev}_{A, A^{'}} (P) ⟶ {ev}_{S, S^{'}} (P)) & \overset{r e p r .}{=} \int_{P} (Tamb (Φ E_{A, A^{'}}, P) ⟶ {ev}_{S, S^{'}} (P)) \\ \overset{Y o n e d a}{=} {ev}_{S, S^{'}} (Φ E_{A, A^{'}}), \end{aligned}$ and the last set is $Optic ((S, S^{'}), (A, A^{'}))$ by definition 169.22. ◻

Corollary 169.25 — Both directions, explicitly ¶

Let $p = ⟨ l ∣ r ⟩$ with $l : S \to M \cdot A$ and $r : M \cdot A^{'} \to S^{'}$ . The corresponding family is ${\tilde{p}}_{P} : = P (l, r) \circ ζ_{A, A^{'}, M} .$ Conversely, a family $t$ is determined by its component at $Φ E_{A, A^{'}}$ , and that component is determined by its value at $⟨ λ_{A}^{- 1} ∣ λ_{A^{'}} ⟩$ , which recovers $⟨ l ∣ r ⟩$ .

Referenced from 7 locations

Profunctors, Coends, and Optics

Proof of Corollary 169.25 — Both directions, explicitly

Proof. The displayed formula is the image of $p$ under the two isomorphisms of theorem 169.24, read off from the Yoneda step. The converse is the content of the same two isomorphisms taken in the other direction: the Yoneda isomorphism evaluates a natural family at the identity, which here is $⟨ λ_{A}^{- 1} ∣ λ_{A^{'}} ⟩$ . ◻

Remark 169.26 — Rank polymorphism is not enough ¶

The right-hand side of theorem 169.24 is an end over $Tamb$ , that is a family natural in the Tambara module. A programming language encodes it as a rank-two polymorphic type $Optic A A^{'} S S^{'} : = \forall P . Tamb (P) \Rightarrow P A A^{'} \to P S S^{'},$ and the encoding is faithful only to the extent that inhabitants of the polymorphic type are natural. Chapter 6 supplies the exact statement: for the polymorphic calculus considered there, the abstraction theorem gives, for each closed term of the displayed type, the relational condition at every relation between two instances of $P$ , and instantiating it at the graph of a Tambara morphism yields naturality. Two hypotheses are needed and neither is automatic in a real language: that the language admits the abstraction theorem, and that the constraint $Tamb (P)$ is interpreted so that its relational condition is exactly compatibility with the structure maps. Where either fails, the polymorphic type has inhabitants that are not optics; example 169.29 exhibits one.

Referenced from 3 locations

Profunctors, Coends, and Optics

Lawfulness

Definition 169.27 — Lawful optic ¶

For an optic $p = ⟨ l ∣ r ⟩ : (S, S) \to (A, A)$ with residual $M$ define $\begin{aligned} outside (p) & : = r \circ l : S \to S, \\ once (p) & : = ⟨ l ∣ {id}_{M \cdot A} ∣ r ⟩, \\ twice (p) & : = ⟨ l ∣ r \circ l ∣ r ⟩, \end{aligned}$ the last two being elements of the two-hole optic set $\int^{M_{1}, M_{2}} {hom}_{} (S, M_{1} \cdot A) \times {hom}_{} (M_{1} \cdot A, M_{2} \cdot A) \times {hom}_{} (M_{2} \cdot A, S) .$ The optic $p$ is lawful when $outside (p) = {id}_{S}$ and $once (p) = twice (p)$ .

Referenced from 6 locations

Profunctors, Coends, and Optics

Theorem 169.28 — Lawfulness specialises to the lens laws ¶

For the product action on $Set$ , an optic $(S, S) \to (A, A)$ corresponding under proposition 169.18 to $(get, put)$ is lawful in the sense of definition 169.27 if and only if the three laws of definition 169.1 hold.

Referenced from 6 locations

Profunctors, Coends, and Optics

Proof of Theorem 169.28 — Lawfulness specialises to the lens laws

Proof. Proof idea. Compute the two-hole optic set by the same two moves as in proposition 169.18 and read off what the two conditions say.

Take $l = ⟨ {id}_{S}, get ⟩$ and $r = put$ , the representative supplied by proposition 169.18, with residual $S$ .

Outside. $outside (p) = put \circ ⟨ {id}_{S}, get ⟩$ , whose value at $s$ is $put (s, get s)$ . Equality with ${id}_{S}$ is get-put.

The two-hole set. Applying the universal property of the product and lemma 169.12 twice, as in proposition 169.18, gives $\begin{aligned} \int^{M_{1}, M_{2}} {hom}_{} (S, M_{1} \times A) \times {hom}_{} (M_{1} \times A, M_{2} \times A) \times {hom}_{} (M_{2} \times A, S) \\ ≅ {hom}_{} (S, A) \times {hom}_{} (S \times A, A) \times {hom}_{} (S \times A, S), \end{aligned}$ the three components being the first read, the second read after the first write, and the final write.

Once and twice. Under that isomorphism, $once (p)$ has components $(get, {pr}_{2}, put)$ and $twice (p)$ has components $(get, get \circ put, put \circ (put \times {id}_{A}) \circ δ)$ , where $δ$ duplicates the state component. Equality of the second components is $get (put (s, a)) = a$ , which is put-get; equality of the third is $put (put (s, a), a^{'}) = put (s, a^{'})$ , which is put-put. Conversely the three laws give the two equalities by the same reading. ◻

Example 169.29 — An inhabitant that is not a lawful optic ¶

Take $S : = A \times B$ and $get : = {pr}_{1}$ , $put ((a, b), a^{'}) : = (a^{'}, b_{0})$ for a fixed $b_{0} \in B$ with $B$ having at least two elements. By proposition 169.18 this is an element of $Optic ((S, S), (A, A))$ , hence by theorem 169.24 a natural family over $Tamb$ , hence an inhabitant of the polymorphic type of remark 169.26. By theorem 169.28 it is not lawful: get-put fails at any $(a, b)$ with $b \neq b_{0}$ . Naturality is therefore strictly weaker than lawfulness, and no amount of parametricity supplies the missing equations.

Referenced from 6 locations

Profunctors, Coends, and Optics

Proposition 169.30 — Lawful optics compose ¶

If $p : (S, S) \to (A, A)$ and $q : (A, A) \to (B, B)$ are lawful then so is $q \circ p$ .

Referenced from 4 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.30 — Lawful optics compose

Proof. Write $p = ⟨ l_{1} ∣ r_{1} ⟩$ and $q = ⟨ l_{2} ∣ r_{2} ⟩$ with residuals $M_{1}, M_{2}$ .

Outside. $\begin{aligned} outside (q \circ p) & \overset{p r o p o s i t i o n 169.17}{=} r_{1} \circ (M_{1} \cdot r_{2}) \circ (M_{1} \cdot l_{2}) \circ l_{1} \\ \overset{outside (q) = id}{=} r_{1} \circ l_{1} \overset{outside (p) = id}{=} {id}_{S} . \end{aligned}$

Once and twice. Both sides of $once (q \circ p) = twice (q \circ p)$ expand, by the same composition formula applied inside the two-hole set, into expressions in which the inner occurrence is $once (q)$ or $twice (q)$ and the outer one is $once (p)$ or $twice (p)$ . Substituting the two hypotheses turns the second expression into the first. ◻

Proposition 169.31 — Lawfulness specialises to the prism laws ¶

For the coproduct action on $Set$ , an optic corresponding under proposition 169.19 to $(match, build)$ is lawful if and only if $match (build a) = inl a$ and $match s = inl a$ implies $build a = s$ .

Referenced from 4 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.31 — Lawfulness specialises to the prism laws

Proof. As in theorem 169.28, with the coproduct computation of proposition 169.19 in place of the product one. The condition $outside (p) = {id}_{S}$ becomes: the composite that matches and then rebuilds is the identity, which is the second displayed law. The condition $once (p) = twice (p)$ becomes: matching a built value returns that value, which is the first. ◻

Traversals

Example 169.4 left a shape without an action. It has one.

Definition 169.32 — The traversal action ¶

Let $M$ be the category of applicative functors on $Set$ and natural transformations respecting the applicative structure, with $\otimes$ the composition of applicative functors and $I$ the identity functor. Let it act on $Set$ by $F \cdot A : = F A$ . The unit and associativity isomorphisms of definition 169.13 are the identities of functor composition.

Referenced from 3 locations

Profunctors, Coends, and Optics

Proposition 169.33 — Traversals are optics for that action ¶

For the action of definition 169.32, $Optic ((S, S^{'}), (A, A^{'})) ≅ \int_{F} ({hom}_{} (A, F A^{'}) ⟶ {hom}_{} (S, F S^{'})),$ the end over applicative functors. For $S$ a list type and $A$ its element type, an element of the right-hand side is exactly an operation $traverse : \prod_{F :} (A \to F A^{'}) \to (S \to F S^{'})$ natural and applicative-preserving in $F$ .

Referenced from 5 locations

Profunctors, Coends, and Optics

Proof of Proposition 169.33 — Traversals are optics for that action

Proof. The displayed isomorphism is theorem 169.24 for this action, after observing that a Tambara module for it is exactly a profunctor with a strength for every applicative functor, and that the end over $Tamb$ reduces to the end over $M$ by evaluating at the representable Tambara modules of definition 169.22. The reading of the right-hand side as $traverse$ is corollary 169.25 with $P$ taken to be ${Kl}_{F}$ of example 169.6(4). ◻

Remark 169.34 — The exact traversal boundary ¶

Proposition 169.33 identifies traversals with optics for the applicative action. Two further statements belong to their sources and are not proved here. The first is that traversable functors are exactly the finitary containers, so that the coend of definition 169.16 for this action is the coproduct over arities displayed in example 169.4; this is the theorem of Jaskelioff and O’Connor, and Proposition 169.33 does not establish it. The second is the composition of optics across different actions — a lens after a traversal, say — which requires a comparison between the two acting categories. Román treats that case and its concrete profunctor interpretation [Rom20], and the general mixed and enriched setting, in which the forward and backward directions live in different categories, is the subject of Clarke, Elkins, Gibbons, Loregian, Milewski, Pillmore and Román. Nothing in definition 169.16–proposition 169.31 covers a mixed optic: both $l$ and $r$ there are morphisms of the same $C$ .

Referenced from 3 locations

Profunctors, Coends, and Optics

Example 169.35 — A client that needs different directions ¶

Let the forward direction be a function $S \to M \cdot A$ in $Set$ and the backward direction a function $M \cdot A^{'} \to S^{'}$ that may fail, that is a map in the Kleisli category of the partiality monad. No single $C$ contains both as morphisms with the composition of proposition 169.17: composing two backward maps must compose two partial functions, and composing a forward with a backward map must not. The repair is to let the two hom-sets in definition 169.16 be taken in two different categories, both acted on by $M$ , which is the definition of a mixed optic.

Referenced from 4 locations

Boundary

Proved here. The concrete lens laws and their composition (definition 169.1, proposition 169.2); profunctors and four examples (definition 169.5, example 169.6); the Tambara structure and its origin in the two accessor shapes (definition 169.7, proposition 169.8); dinaturality, ends and coends with the explicit description in $Set$ (definition 169.9, proposition 169.11, lemma 169.12); the monoidal action and two instances (definition 169.13, proposition 169.14); the optic coend, its composition, and the specialisations to lenses and prisms (definition 169.16, proposition 169.17, proposition 169.18, proposition 169.19); the near miss when the quotient is dropped (remark 169.20); the representation theorem in both directions (lemma 169.23, theorem 169.24, corollary 169.25); lawfulness with its two specialisations and its composition (definition 169.27, theorem 169.28, proposition 169.31, proposition 169.30); an inhabitant that is not lawful (example 169.29); and traversals as optics for the applicative action (proposition 169.33).

Owned elsewhere. The identification of traversable functors with finitary containers, the composition of optics across different actions, and the mixed and enriched settings, as recorded in remark 169.34. The modular library encoding and its executable baseline are due to Pickering, Gibbons and Wu; the optic category and the notion of lawfulness used in definition 169.27 are Riley’s.

Not a foundation. Nothing above changes the ambient type theory. Optics are a construction inside a category, and the chapter’s role is to give existential types, variance, profunctors and monoidal actions a proof-bearing application. It is not a survey of accessor libraries, and no library encoding is treated as evidence for a theorem: example 169.29 is the standing reminder that a well-typed inhabitant of the encoding need not be an accessor.

Suggested first pass.

Problems exercise 169.3, exercise 169.4, and exercise 169.6 form the suggested first pass. None of these problems is a prerequisite for a later chapter.

Exercise 169.3 ¶

★★☆ A setter is an operation $over : (A \to A^{'}) \to (S \to S^{'})$ .

Find a monoidal action for which $Optic ((S, S^{'}), (A, A^{'}))$ is the set of setters, and verify the two coherence conditions of definition 169.13.
Compute the coend for that action as in proposition 169.18, displaying each use of lemma 169.12.
State what definition 169.27 says for a setter, and show that it is equivalent to $over ({id}_{}) = {id}_{}$ together with $over (f) \circ over (g) = over (f \circ g)$ .

Referenced from 4 locations

Profunctors, Coends, and Optics

Exercise 169.4 ¶

★★★ Theorem 169.24 was proved by two applications of Yoneda.

Write out lemma 169.23 in full, checking that the constructed transformation respects the Tambara structures and that the two constructions are mutually inverse.
Give the direction from an optic to a natural family without appealing to the theorem, by exhibiting ${\tilde{p}}_{P}$ of corollary 169.25 and checking naturality directly.
Give the direction back, and check that the round trip through $⟨ λ_{A}^{- 1} ∣ λ_{A^{'}} ⟩$ is the identity.
Identify the step at which the smallness of $C$ is used, and say what replaces it when $C$ is large.

Referenced from 3 locations

Profunctors, Coends, and Optics

Exercise 169.5 ¶

★★★ Example 169.35 exhibits a client needing two categories.

Write the definition of a mixed optic: two categories $C, D$ acted on by one $M$ , and the coend $\int^{M} {hom}_{C} (S, M \cdot A) \times {hom}_{D} (M \cdot A^{'}, S^{'})$ .
Show that the composition of proposition 169.17 is still well defined, and identify which of its three verifications now uses two actions rather than one.
Exhibit a mixed composition that a same-category encoding rejects, taking $D$ to be the Kleisli category of the partiality monad, and state which typing constraint fails in the same-category version.

Referenced from 2 locations

Profunctors, Coends, and Optics

Exercise 169.6 ¶

★★★ Practical project.optic-law-corpus Implement, in Agda, the optic hierarchy of this chapter together with a law corpus, and run a data update through the profunctor representation and back.

Calculus to implement. The profunctor interface of definition 169.5; the Tambara structures of definition 169.7 for the product action and the coproduct action; the representation maps of corollary 169.25 in both directions; the concrete lens, prism and setter representations of proposition 169.18, proposition 169.19 and exercise 169.3; the composition of proposition 169.17; and decidable checks for the three lens laws, the two prism laws, and the two setter laws. Represent an optic in the concrete form and convert to the profunctor form only where a composition requires it.

Invariant. Each conversion must be a round trip: converting a concrete optic to its profunctor form and back must return the original, and the program must check that equation for every optic it constructs. That check is the executable form of corollary 169.25. Composition must be performed in the profunctor form and the result converted back, so that proposition 169.30 is exercised rather than assumed.

Concrete result. For a nested record value, a report giving: the value before and after an update performed through a composite optic; the round-trip check for each optic used; and the verdict of each law check, positive or negative, with the witness when negative.

Acceptance test. Use the record $S : = A \times (B \times C)$ with $A = B = C = 2$ , the first-component lens $p$ on $S$ , the first-component lens $q$ on $B \times C$ , and the composite $q \circ p$ obtained through the profunctor form. Updating $(tt, (tt, tt))$ through $q \circ p$ with the constant- $ff$ modification must give $(tt, (ff, tt))$ , and the round-trip check must pass for $p$ , $q$ and the composite. The prism of example 169.3 on $2 + 2$ must pass both prism laws, and its composition with $p$ must be rejected by the type checker, since the shapes do not match. The unlawful lens of example 169.29 must pass the round-trip check and fail the get-put check, with the failing pair printed; that pair of outcomes is the executable form of the separation between naturality and lawfulness. Produce three mutations that still typecheck — drop the residual quotient by fixing a residual, use ${pr}_{1}$ where ${pr}_{2}$ is required in the lens conversion, and omit the applicative-preservation condition from the traversal structure — and confirm that each makes a named case fail. State explicitly that the program checks the laws at finitely many values and proves neither theorem 169.24 nor theorem 169.28.

Referenced from 3 locations