Optics in proarrow

Starting from mixed optics

Mixed optics fix a monoidal category $\mathcal M$ acting on two categories $C$ and $D$ and define

$$ \mathrm{Optic}_{\mathcal M}\big((S,T),(A,B)\big) = \int^{M \in \mathcal M} C(S,\ M\bullet A) \times D(M\bullet B,\ T) $$

with the profunctor encoding, by Pastro–Street, as natural transformations between Tambara modules:

$$ \mathrm{Optic}_{\mathcal M}\big((S,T),(A,B)\big) ;\cong; \int_{P \in \mathbf{Tamb}_{\mathcal M}} \mathbf{Set}\big(P(A,B),\ P(S,T)\big) $$

Every optic kind is then a choice of action: the cartesian product gives lenses, the coproduct gives prisms, the exponential gives grates, Traversable functors give traversals, and so on. Subtyping between kinds comes from inclusions between the corresponding classes of Tambara modules.

proarrow keeps the shape of this story but changes two things.

1. A Tambara module is strong for a pair of profunctors, not for an action. Where a Tambara module absorbs $C(S, M\bullet A)$ on the left and $D(M\bullet B, T)$ on the right, a Prostrong profunctor absorbs $p(s,a)$ and $q(b,t)$ for a pair $(p,q)$ drawn from a class the library calls a flavor. The classical case is $p = C(-, M\bullet -)$ and $q = D(M\bullet -, -)$, the two hom-profunctors of the action functor $M \bullet -$; but a flavor may contain hom-profunctors of functors between different categories, composed back into an endo-profunctor, which is what makes traversals and one-sided optics expressible. The existential encoding then follows, as the free Prostrong profunctor.

2. Flavors are defined by what you can do with a witness pair, as type classes with methods, and subtyping between optic kinds is expressed with superclass relations.

The rest of this page unpacks those two moves.

Notation

proarrow writes j +-> k for the kind of profunctors from j to k; it is k -> j -> Type. a ~> b is the hom of whatever category the kind of a and b carries. p :.: q is profunctor composition, (p :.: q) a b = ∃x. p a x × q x b, and p :~> q is a natural transformation. Rep f s a = s ~> f a and Corep f b t = f b ~> t are the two hom-profunctors of a functor f, which may go between different categories. p :**: q is the external product of two profunctors, a profunctor on the product category (k, k). Signatures below are lightly abridged (kind annotations and Ob constraints dropped).

Move one: Tambara modules become Prostrong

A Tambara module for the action of $\mathcal M$ is a profunctor $P$ with maps $P(a,b) \to P(M\bullet a, M\bullet b)$, natural in everything. Precomposing with $C(s, M\bullet a)$ and postcomposing with $D(M\bullet b, t)$, the same data is a map

$$ C(s, M\bullet a) \times P(a,b) \times D(M\bullet b, t) \longrightarrow P(s,t) $$

i.e. a natural transformation $C(-, M\bullet -) \odot P \odot D(M\bullet -, -) \Rightarrow P$. proarrow takes that form as the definition and lets the two outer profunctors be anything a flavor admits:

type FLAVOR j k = (k +-> k) -> (j +-> j) -> Constraint

class (Profunctor p) => Prostrong (w :: FLAVOR j k) (p :: j +-> k) where
  proact :: (w f g, Profunctor f, Profunctor g) => f :.: p :.: g :~> p

A flavor w is a constraint on pairs of profunctors, the witness pairs; f lives on the source category k and g on the target category j. If f is representable by m and g is corepresentable by m, proact says (s ~> m a) -> p a b -> (m b ~> t) -> p s t, which is the Tambara map when m is a monoidal action.

The rank-2 profunctor encoding is then what you expect:

-- simplified
type Optic c s t a b = forall p. c p => p a b -> p s t

type Lens  s t a b = Optic (Prostrong LensFl)  s t a b
type Prism s t a b = Optic (Prostrong PrismFl) s t a b
-- ...

Two remarks for the mixed-optics reader:

• Mixedness is native. The left witness and the right witness live in separate categories, and several flavors below use that.
• Witnesses need not be representable. Once you allow arbitrary profunctor pairs, you can put a terminal profunctor on one side (that is how getters work here — see below). Or you can flip the representability, making f corepresentable and g representable, which gives knot-tying optics such as the tracer, whose over computes a trace in a traced monoidal category.

The existential encoding follows

data ExOptic (w :: FLAVOR j k) a b s t where
  ExOptic :: (w p q, Profunctor p, Profunctor q) => p s a -> q b t -> ExOptic w a b s t

instance (forall p q. v p q => Sub w p q, Flavor w) => Prostrong v (ExOptic w a b) where
  proact (f :.: ExOptic p q :.: g) = ExOptic (f :.: p) (q :.: g)     -- absorb by composing witnesses

That is

$$ \exists (p,q) \in w.\quad p(s,a) \times q(b,t) $$

which is (again) the mixed-optics integrand with $C(S, M\bullet A)$ replaced by $p(s,a)$ and $D(M\bullet B, T)$ by $q(b,t)$. Conversion between the existential encoding and the profunctor encoding is as follows:

ex2prof :: ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (ExOptic p q) = Optic (\pab -> proact @w (p :.: pab :.: q))

prof2ex :: (Flavor w, c (ExOptic w a b)) => Optic c s t a b -> ExOptic w a b s t
prof2ex (Optic l) = l (ExOptic (Id id) (Id id))

ex2prof wraps the witness pair around the carrier with one proact; prof2ex is the Pastro–Street move, instantiating the polymorphic optic at the free Prostrong profunctor on the identity legs. Note that prof2ex accepts an optic at any constraint c, not only Prostrong w; that is what makes it, and everything built on it, encoding-agnostic.

Why the flavor must be closed. Absorbing a witness pair into an ExOptic composes it onto the legs, so the flavor has to contain the composite pair. prof2ex requires the flavor to contain the identity pair.

class (forall f f' g g'. (w f f', w g g') => w (f :.: g) (g' :.: f'), w Id Id) => Flavor w

This is the analogue of the monoidal structure of $\mathcal M$, with (Id, Id) as unit and (f :.: g, g' :.: f') as tensor (note the reversal on the right).

The profunctor-class encoding is still available. The constraint c in Optic c doesn't have to be a Prostrong. Optic Profunctor is an adapter (the library calls it PIso), and Optic StrongDistributiveProfunctor is a profunctor-class traversal (PTraversal, the analogue of forall p. Traversing p => p a b -> p s t). Converting from a class-based optic to a witness-based one is the same Pastro–Street instantiation, now at the free Prostrong w profunctor:

convert :: (Flavor w, c (ExOptic w a b)) => Optic c s t a b -> Optic (Prostrong w) s t a b
convert = ex2prof . prof2ex

so it works exactly when the free w-strong profunctor is an instance of c. That is how fromPTraversal proves, constructively, that a traversal in profunctor-class form has a Traversable-functor representative: ExOptic MonTravFl a b is shown to be a StrongDistributiveProfunctor, and then you instantiate.

Move two: flavors are defined by what they can do

The literature defines an optic kind by an action and derives what it can do. proarrow turns this around: a flavor is a class on witness pairs whose methods are exactly what the eliminators need, and the standard witness pairs are instances.

class (Profunctor p, Profunctor q) => FoldFl p q where
  foldMapP :: Monoid m => p s a -> (a ~> m) -> (s ~> m)

class (AffineFoldFl p q) => GetterFl p q where
  getP :: p s a -> s ~> a

class (Profunctor p, Profunctor q) => SetterFl p q where
  overP :: p s a -> q b t -> (a ~> b) -> (s ~> t)

class (SetterFl p q, FoldFl p q) => TravFl p q where
  travP :: (StrongDistributiveProfunctor r, Strong ProdAction r) => p s a -> q b t -> r a b -> r s t

class (AffineTravFl p q, GetterFl p q, GlassFl p q) => LensFl p q where
  putP :: HasBinaryProducts k => p s a -> q b t -> (s && b) ~> t

class (GetterFl p q, MonTravFl p q, AffineTravFl p q, GlassFl p q) => MonLensFl p q where
  withMonLensP :: SymMonoidal k => p s a -> q b t -> (forall m. Ob m => ComonoidOn m -> (s ~> m ** a) -> (m ** b ~> t) -> r) -> r

class (AffineTravFl p q, GetterFl q p, MonTravFl p q) => PrismFl p q where
  matchingP :: HasBinaryCoproducts k => p s a -> q b t -> s ~> (t || a)

class (SetterFl p q) => GlassFl p q where
  glassP :: CCC k => p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t

class (KaleidoFl p q, GlassFl p q) => GrateFl p q where
  zipWithP :: (Closed k, SymMonoidal k) => p s a -> q b t -> (forall x. ((x ~~> a) ~> b) -> (x ~~> s) ~> t)

class (SetterFl p q) => CotravFl p q where
  cotravP :: Cotraversable r => p s a -> q b t -> r a b -> r s t

class (CotravFl p q) => KaleidoFl p q where
  kaleidoP :: Kaleidoscopic r => p s a -> q b t -> r a b -> r s t

class (MonTravFl p q, GrateFl p q) => PowerGrateFl p q where
  powerGrateP :: MonoidalProfunctor r => p s a -> q b t -> r a b -> r s t

class (SetterFl p q, SetterFl q p) => TracerFl p q where
  withTracerP :: Monoidal k => p s a -> q b t -> (forall m. (m ** s ~> a) -> (b ~> m ** t) -> r) -> r

Notice CotravFl and KaleidoFl next to MonTravFl: they are the same square with the quantifier moved. All three rest on a distributive law t :.: p ~> p :.: t between a functor t and a StrongDistributiveProfunctor p (in Type, sequenceA :: t (f a) -> f (t a)). A monoidal traversal fixes a traversable t as the witness and eliminates through every p. The two new flavors fix a representable p -- an applicative functor rendered as a profunctor -- as the witness and eliminate through the carriers it passes through. A cotraversal passes through every Cotraversable carrier, the class whose law is that square with p arbitrary: the literal mirror of a traversal, true of finite shapes. A kaleidoscope passes through every Kaleidoscopic carrier, the same square for representable p only: that is Clarke et al.'s kaleidoscope, the optic for the action of applicative functors, and in Type it admits the unbounded shapes, Costar t for a Traversable t. Those are not Cotraversable: a list can pass a strong distributive profunctor through only by knowing it is an applicative, and a generic structural recursion diverges on strict witnesses. Every Cotraversable carrier is Kaleidoscopic, so the kaleidoscope is the stronger flavor. PowerGrateFl is its fixed-arity fragment, the tensor powers; with the arity fixed, any functor carrier distributes by unzipping, which is why it can be eliminated through a bare MonoidalProfunctor.

Notice GlassFl above both LensFl and GrateFl: the glass is Clarke et al.'s optic for the action $C \times (D \Rightarrow -)$, the join of the lens and the grate, and its single leg (s && ((s ~~> a) ~~> b)) ~> t hands the eliminator the source together with a consumer of selectors (s ~~> a) ~~> b. A lens witness applies the consumer to its own get; a grate witness ignores the source and feeds the consumer its exponent's selectors; a composite threads the outer selector through the inner one. The method carries CCC k itself rather than putting a constraint on the witnesses, and that is deliberate: the glass needs products, exponentials and the tensor to be the product, and asking for CopyDiscard of the category instead sends GHC's solver into a loop on the nested exponential, while CCC in the method leaves the instances free to demand only what their witness needs (Monoidal k for the tensor powers, Comonoid m for a residual).

Notice MonLensFl next to LensFl: the same shape, with the residual carried through the tensor and constrained to be a comonoid instead of being recoverable from s by projection. withMonLensP hands that comonoid back as a value, ComonoidOn m, rather than as a Comonoid m constraint, because the residual of a composite is a tensor mo ** mi and that of the identity is Unit, and type families cannot head an instance; the value-level tensorComonoid and unitComonoid need no instance, which is also why the method asks for symmetry (a tensor of comonoids is a comonoid only in a symmetric monoidal category).

Notice GetterFl q p (arguments swapped) in the superclasses of PrismFl: a prism's build leg is a getter read backwards, which is what makes re prism a getter. Notice too that FoldFl and GetterFl never mention q in their methods — those are the one-sided optics, and the type of t, b is genuinely unconstrained (and may live in a different category).

The witness pairs in each flavor are the ones you would guess from the coend representatives, plus (Id, Id) and closure under composition:

flavor	generating witness pairs	coend representative it corresponds to
LensFl	(Rep (Product s), Corep (Product s))	$M = S$ in $\int^M C(S, M\times A)\times D(M\times B, T)$
PrismFl	(Rep (Coproduct t), Corep (Coproduct t))	$M = T$ in $\int^M C(S, M+A)\times D(M+B,T)$
GlassFl	the lens and grate pairs, and everything below them; glass itself uses (Rep (Product s) :.: Rep (Exp (s ~~> a)), Corep (Exp (s ~~> a)) :.: Corep (Product s))	$\int^{C, D} C(S, C\times (D \Rightarrow A))\times D(C\times(D\Rightarrow B), T)$, the glass of Clarke et al.
GrateFl	(Rep (Exp m), Corep (Exp m)) for a comonoid m (then m ~~> - is the reader applicative, so a grate is a kaleidoscope)	$\int^M C(S, M \multimap A) \times D(M\multimap B, T)$
TravFl, MonTravFl	(t, RepCostar t) for representable Traversable t; (CorepStar t, t) for corepresentable Cotraversable t; plus the juxtaposition composites Beside/BesideSum (tensor or coproduct, then p1 :**: p2, then the diagonal Rep Diag), UnitW, ZeroW, and Rep (ActionAt Tensor m) for a comonoid m	Traversable functors
CotravFl, KaleidoFl	(p, RepCostar p) for any representable StrongDistributiveProfunctor p; (Rep (ActionAt Tensor m), Corep (ActionAt Tensor m)) for a monoid m (the writer applicative)	$\int^{F \in \mathrm{App}} C(S, FA)\times D(FB, T)$, the kaleidoscope of Clarke et al.; the two flavors differ only in their carriers
PowerGrateFl	(Pow n, CoPow n)	$\int^{n} C(S, A^{\otimes n})\times D(B^{\otimes n}, T)$: the tensor powers, i.e. the reader applicatives
TracerFl	(Corep (ActionAt Tensor m), Rep (ActionAt Tensor m)) in a traced monoidal category	$\int^M C(M\otimes S, A)\times D(B, M\otimes T)$
MonLensFl	(Rep (ActionAt Tensor m), Corep (ActionAt Tensor m)) for a comonoid m; in a cartesian category also an affine traversal and a glass, but never a LensFl (see below)	$\int^{M \text{ comonoid}} C(S, M\otimes A)\times D(M\otimes B,T)$
AlgLensFl m	(Rep (ActionAt Tensor x), Corep (ActionAt Tensor x)) for a comonoid x that is an Algebra m of the monad m (a representable promonad on k)	Riley's algebraic lenses: $\int^{x \in \mathrm{Alg}(m)} C(S, x\times A)\times D(x\times B, T)$
ClassifyFl l	the same pair, for x an l-algebra that is a monoid (the list monad's algebras)	the classifying lens: AlgLensFl l and KaleidoFl at once, since a product by a monoid is applicative
GetterFl	(Id, TerminalProfunctor)	one-sided
Flip GetterFl (review)	(TerminalProfunctor, Id)	one-sided
ActFl act	(Rep (ActionAt act x), Corep (ActionAt act x))	$\int^{x} C(S, x\bullet A)\times D(x\bullet B, T)$, literally

IsoFl is simply the conjunction of the five maximal flavors (LensFl, PrismFl, PowerGrateFl, MonLensFl, TracerFl). AffineTravFl (methods affineMatch, affineSet) and AffineFoldFl (previewP) are ordinary flavors, but their only generating witnesses are the lens, prism and monoidal-lens ones — an affine traversal witness only ever arises by composing those, which is why affineTraversal is literally convert (l % p).

The table also shows the payoff of making flavors classes rather than data: one and the same profunctor pair belongs to several flavors under different side conditions. The tensor-action pair (Rep (ActionAt Tensor m), Corep (ActionAt Tensor m)) — legs s ~> m ** a and m ** b ~> t — is a setter witness in any monoidal category, a fold, traversal, getter and monoidal-lens witness when m is a comonoid (the counit discards the residual), and then also an affine-traversal and a glass witness, because affineSet and glassP ask for a cartesian category in their own constraints, where the tensor is the product and the residual can be projected out — but not a lens witness, because putP promises to work with binary products alone, where tensor and product are unrelated; an algebraic-lens witness when m is moreover an algebra for a monad (the algebra lets put see a whole computation of sources, which is what classifying is), a kaleidoscope witness when m is a monoid (then m ** - is the writer applicative), the generator of tensor strength for the free traversal profunctor, and, read the other way round, a tracer witness in a traced monoidal category. mkMonoidal @m and monLens @m build the very same ExOptic value; they differ only in which flavor it is tagged with.

Subtyping is the superclass relation

Because LensFl p q has GetterFl p q as a superclass, every lens witness is a getter witness, so a lens is a getter. There is no separate subtyping class to maintain: the bridge instance above asks for the quantified constraint

forall p q. v p q => Sub w p q

which plays the role of optics' Is k l, except that it is derived from the superclasses rather than enumerated edge by edge — adding a superclass to a flavor class adds the edge. (Sub w p q is w p q as a one-instance class, a small concession to GHC's constraint solver; the Haddocks explain it.)

The lattice, weakest at the top (dotted nodes are one-sided flavors, whose methods never mention the second witness; dashed nodes are indexed by a monad and so have no edge to Iso):

AlgebraicLens m sits below MonoidalLens: it is indexed by the monad, so Iso has no edge to it. The monad is any representable promonad m on k that is oplax monoidal (so residuals can be paired under it), and the algebra of the residual travels through withAlgP as a value, m % x ~> x, which is why composites need no instance for products of algebras. In Type the monad is Star (Prelude f) for a Haskell monad f. Its list-monad case, ClassifyingLens, sits below Kaleidoscope (hence Cotraversal) as well, and that meet is what Clarke et al.'s Remark 3.28 asks for: a lens composed with a kaleidoscope is not a kaleidoscope, because a product functor is not applicative, but a product by a monoid is, so a classifying lens composed with a kaleidoscope is a kaleidoscope again. In the library that is a type: convert (measure % aggregate) :: Kaleidoscope' Flower Float, eliminated at Costar [] by kaleidoscopeOf, the >- of vitrea. Grate is below Kaleidoscope by the same move that put the algebraic lens below it: the reader m ~~> - is applicative exactly when the exponent m is a comonoid, so the grate witness asks for that of its exponent rather than for a cartesian category. In a CopyDiscard category every object qualifies and nothing is lost; elsewhere a grate with a non-comonoid exponent is not an optic of this library, which is the price of the edge.

Glass sits directly under Setter, above Lens, Grate and MonoidalLens. It is the one flavor whose generating witnesses are all inherited: a glass is built from the lens witness at s composed with the grate witness at s ~~> a, and PowerGrate, being below Grate, is a glass as well — each of its n positions feeds the consumer the selector "project this focus", which is what the cartesian splitPowC computes. MonoidalLens under AffineTraversal and Glass but not under Lens is the one place where the lattice records a fact about method constraints rather than about actions: with Cartesian in scope the two lens flavors coincide, and affineSet and glassP have it, while putP deliberately does not.

Composition of optics of different flavors needs no join computation. l % p has constraint c1 :&&: c2, a conjunction that every consumer discharges one conjunct at a time, so the composite is automatically usable at the meet of the two flavors. convert is only needed to store it at a named type.

re is a flavor operation too: Flip w swaps the two components of every witness pair, and since Flip w q p is just w p q as a class with one instance, the superclass entailments carry over to Flip for free, so re lens :: Review, re prism :: Getter, and re . re gets you back. A prism is also literally a lens in the opposite category — toOpLens/fromOpLens witness the equivalence by eliminating to legs and rebuilding over OPPOSITE k.

One carrier for every flavor

The neatest consequence of defining flavors by their methods is that no flavor needs an eliminating carrier of its own. Eliminating an optic is running it at its own existential form, i.e. prof2ex, and it is the bridge instance of ExOptic — "absorb a witness pair by composing it on" — that makes this work for every flavor at once. Constructors go the other way with legs2prof (lens sa sbt = legs2prof @LensFl (Rep (id &&& sa)) (Corep sbt)), and every eliminator is withLegs, the continuation-passing prof2ex, followed by the flavor's method, in any encoding:

view     o   = withLegs @GetterFl o \p _ -> getP p
over     o f = withLegs @SetterFl o \p q -> overP p q f
withLens o k = withLegs @LensFl   o \p q -> k (getP p) (putP p q)
withGlass o k = withLegs @GlassFl o \p q -> k (glassP p q)
traverseOf o r = withLegs @TravFl o \p q -> travP p q r

The carriers of the lens literature — Exchange, Shop, Market, Forget, Tagged, (->) — are all Yoneda-reduced normal forms of ExOptic at the corresponding flavor. A profunctor-class-flavored optic is eliminated through the same function: ExOptic w a b is a strong distributive profunctor, costrong, and so on, by one generic instance per strength that holds whenever w contains that strength's generating witness pair, so over on an Optic StrongDistributiveProfunctor needs nothing flavor-specific either.

On lawfulness

The types certify what a witness pair can do — its flavor methods — and never that a particular pair of legs is coherent. But there is one piece of extra structure on a witness pair that makes lawfulness statable, uniformly for every flavor: an adjunction between the two witnesses,

class Proadjunction p q where
  unit   :: (q :.: p) a a          -- the identity optic on a, as a witness pair
  counit :: p :.: q :~> (~>)       -- run a pair of legs end to end

i.e. $p \dashv q$ in $\mathbb{P}\mathrm{rof}$. For the representable pair $(F^*, F_*)$ the unit is $(\mathrm{id}, \mathrm{id})$ at $F a$ and the counit is composition; more generally, a left adjoint in $\mathbb{P}\mathrm{rof}$ is the hom-profunctor of a functor into the idempotent completion of the target, so Proadjunction p q says the residual is a functor $F$ up to splitting idempotents. Every witness pair in the library except the one-sided ones is such an adjunction (composites inherit it from their pieces), and the tracer's pair is one the other way round, $q \dashv p$.

Given the adjunction, an optic with legs $l \in p(s, a)$ and $r \in q(a, s)$ can be asked to satisfy two equations:

1. Round trip on the whole. $\varepsilon(l \odot r) = \mathrm{id}_s$: running the two legs end to end does nothing.
2. Round trip on the focus. $r \odot l = \eta_a$ in $(q \odot p)(a, a)$: reading back through the legs is the identity optic on the focus, up to the coend's identifications.

In the representable case these read $r \circ l = \mathrm{id}_s$ and $l \circ r = \mathrm{id}_{F a}$ modulo a change of representative, which is (essentially) Riley's definition of a lawful optic.

Reversed optics get reversed laws. re swaps the two legs, so the reversed optic has legs $r \in q(a, s)$ on the left and $l \in p(s, a)$ on the right, and the adjunction it can use is the other one, $q \dashv p$, with counit $\varepsilon' : q \odot p \Rightarrow \hom$ and unit $\eta'_s \in (p \odot q)(s, s)$. The same two equations then read $\varepsilon'(r \odot l) = \mathrm{id}_a$ and $l \odot r = \eta'_s$: whole and focus have exchanged roles. The tracer is the case where only this second adjunction exists, so its laws are the reversed setter's, stated from the other end.