Lenses are a well-established structure for modelling bidirectional transformations, such as the interactions between a database and a view of it. Lenses may be symmetric or asymmetric, and may be composed, forming the morphisms of a monoidal category. More recently, the notion of a learner has been proposed: these provide a compositional way of modelling supervised learning algorithms, and again form the morphisms of a monoidal category. In this paper, we show that the two concepts are tightly linked. We show both that there is a faithful, identity-on-objects symmetric monoidal functor embedding a category of asymmetric lenses into the category of learners, and furthermore there is such a functor embedding the category of learners into a category of symmetric lenses.
Copyright c by the paper's authors. Copying permitted for private and academic purposes. form, a-lenses. These a-lenses do have extra axioms | the ones we have looked at most are called Stable PutGet (or SPG) a-lenses | and it turns out that the extra structure provided by amendment lenses can be added in a canonical way to the lenses that we study here, and in a way that allows then to recover at least the amendment-lens versions of GetPut and PutGet axioms.
Before we begin, a few words about notation. In particular, we may need to thank readers for their indulgence in translating notations | since this paper brings together two areas that already have established notation, in order to make the comparisons with those areas easier we have generally retained the appropriate notations for lenses and for learners, but that means that readers sometimes have to carry both notations in their minds and translate between them. We have endeavoured to help.
In a small number of cases where we judged it would do little harm we have taken the opposite approach and made minor changes to established notation. In those cases, if the notation comes from the readers' own area of expertise we have to ask for even more indulgence. We hope we do not engender confusion.
On more mathematical matters, note that we are both category theorists, but that the lenses and learners that we are dealing with here are all set-based, and there is very little explicit use of category theory beyond some pullbacks, the construction of functions from other functions, and the judicious, and mostly unremarked, use of isomorphisms to for example re-order variables inside tuples, and to rebracket tuples of tuples. But sadly that makes for some long strings of variables as parameters for functions.
To manage the visual complexity of some of these complicated function compositions we have also presented them using string diagrams in Set. While we hope that, written alongside the usual elementwise function notation, these will be easy enough to read, the reader unfamiliar with this notation might consult introductory references [Sel11, FS19]. We look forward to a treatment of some of the things presented here as notions internal to a category, and anticipate that they will probably bring with them signi cant simpli cations, especially in notation.
Finally, a remark about how \well-behaved" is a technical term. Many of the lenses we consider here are not well-behaved, but that simply means that they don't satisfy certain conditions, conditions which for the applications considered here would be undesirable. So it's important to remember that being not-well-behaved may be desirable and is certainly not derogatory (contrary to normal English usage).
In the next two sections we introduce lenses, rstly in their asymmetric form (Section 2), and then in their symmetric form (Section 3). Along the way we note how to compose both asymmetric lenses, and symmetric lenses, and we introduce the particularly simple constant complement lenses, and show brie y how constant complement lenses compose to give constant complement lenses. Because of the bare lenses that we are using in this paper, we need to extend somewhat the usual de nition of composition of symmetric lenses which is generally de ned only when the lenses are well-behaved, or at least each satisfy the PutGet axiom. We show that, with a slightly complicated construction, the usual de nition of composition can be extended to symmetric lenses in which one leg satis es PutGet even if the other leg satis es no axioms at all.
In Section 4 we introduce learners, their composition and monoidal structure, and how they form a category. As might be expected, to make a category (rather than say a bicategory) we need to take equivalence classes of learners, and the equivalence relation is introduced. It corresponds so closely to the usual equivalence for symmetric lenses presented as spans of asymmetric lenses that we can suppress any detailed treatment of the equivalences in this paper and present the results in terms of representatives of equivalence classes. Some readers at rst nd the de nition of composition for learners a little daunting, so we include string diagrams to illustrate how the composition works.
In Section 5 we present in detail the theorem already alluded to, and illustrate the precise and remarkably parallel relationship between learners and lenses. And then in Section 6 we discuss some of the observations that follow from this work, and conclude with some speculations on possible directions for further studies owing from these results.
Asymmetric lenses have been studied in a variety of di erent categories, and with a range of di erent forms including d-lenses [DXC11], c-lenses [JR13], and most recently amendment lenses, also known as a-lenses [DKL18]. Furthermore those lenses have been studied as algebraic structures with a number of axioms such as the so-called PutGet law [FG+07], the PutPut law [FG+07, JR12], and many others. In this paper we predominantly restrict our attention to the very simplest cases of set based lenses, as originally presented in [PS03], with no further axioms.
De nition 2.1. An asymmetric lens pp; gq : A g : A / B.
/ B is a pair of functions: a Put p : B
A / A and a Get
These basic asymmetric lenses are the main thing that we need in order to see the relationships with learners, but we will sometimes need to refer to lenses that are \well-behaved", or at least that satisfy one of the following two conditions required for so-called well-behaved lenses.
De nition 2.2. An asymmetric lens pp; gq : A conditions (PutGet) The Get of a Put is the projection. That is, gpppa; bqq b, or in string diagrams / B is called well-behaved if it satis es the following two (GetPut) The Put of an unchanged Get result is unchanged. That is, ppgpaq; aq a, or in string diagrams B
B
A A
A
B A B A A p g g p (Here the splitting wire represents the diagonal map A / A
A, i.e. a ÞÑ pa; aq.)
Even without meeting the de nition of well-behaved, lenses compose in a straightforward way, and wellbehaved lenses do compose to give well-behaved lenses too. In fact, each of the two well-behaved conditions (PutGet and GetPut) is respected by composition separately, so we can, when we need to, talk about the composition of lenses that satisfy merely PutGet say, and know that the result will also satisfy PutGet. De nition 2.3. The composite lens pp; gq # pp1; g1q : A / C constructed from lenses pp; gq : A pp1; g1q : B / C has as Get simply the composite g1g of the Gets / B and A g g1
C and as Put, q : C
A / A given by qpc; aq
ppp1pgpaq; cq; aq.
C A g p
A p1 Thus in the notation just introduced, pp; gq # pp1; g1q
pq; g1gq.
De nition 2.4. With the composition just de ned, asymmetric lenses are the arrows of a symmetric monoidal category whose objects are sets, and whose monoidal product is given by cartesian product. That category is denoted Lens. Furthermore, there is a subcategory of Lens called WBLens whose arrows are well-behaved asymmetric lenses, as well as subcategories whose arrows satisfy merely PutGet or GetPut.
Given a cartesian product B A, we write the projection notation 2 : B A / A for the function mapping pb; aq to a; that is, for projection onto the second factor. More generally, we overload the notation i using it for any projection onto an ith factor, with it being disambiguated once the domain, expressed as a cartesian product, is known.
The identity lens p 1; idAq : A / A on a set A has identity function as Get and projection onto the rst factor as Put.
Example 2.5. One of the most basic forms of asymmetric lenses, introduced many years ago in the database community [BS81], is the constant complement view updating lens. These are asymmetric lenses of the form pk; 1q : A1 A2 / A1, where kpa11; pa1; a2qq pa11; a2q | the reader can see the source of the name \constant complement" in the presence of a2 in both the input and the output of k. It is easy to see that pk; 1q is well-behaved.
The composite of constant complement lenses is again constant complement. Indeed, suppose further that A1 B1 B2, and that pk1; 1q : B1 B2 / B1 is a constant complement lens (so k1pb11; pb1; b2qq pb11; b2q). Then the composite lens pk; 1q # pk1; 1q : B1 B2 A2 / B1 has Put k2 : B1 pB1 B2 A2q / B1 B2 A2 given by k2 b11; pb1; b2; a2q k k1pb11; pb1; b2qq; pb1; b2; a2q k pb11; b2q; pb1; b2; a2q pb11; b2; a2q; and Get given by pk2; 1q : B1 B2 1 : B1 A2
pB2 / B1.
A2q
/ B1. This is, up to isomorphism, the constant complement lens
Such simple composites of constant complement lenses, or indeed of other more complicated lenses, arise very frequently in practice (for example in the database world whenever one deals with views of views). In common with the overloaded notation for projections i which are the Gets of constant complement lenses, it is convenient to introduce overloaded notation for the Puts: When there is little risk of confusion we will simply write k for the constant complement Put corresponding to a given Get i.
We will return to constant complement lenses when we use them as the \left leg" of certain symmetric lenses to obtain our main result in Section 5. 3
Asymmetric lenses model well situations where one system, denoted A in the previous section, includes all the relevant information, and another system, B, has information simply derived from A. Of course in practice it's important to deal with the more symmetric situation where two systems share some common structures, but each has information that the other doesn't have. To address this, not long after the seminal work on asymmetric lenses, Hofmann et al. developed a symmetrized version of lenses [HPW11] which can be described conveniently as (approximately) spans of asymmetric lenses.
Recall that a span in a category is a pair of arrows with common domain, A1 ÐÝ S ÝÑ A2. Despite their evident symmetry, spans are usually considered to be oriented from one of the feet to the other, so the span just drawn would be called a span from A1 to A2, and the same two arrows also form a span from A2 to A1, usually drawn as A2 ÐÝ S ÝÑ A1. The object S is called the head, (or sometimes peak or apex) of the span. When we need to name the arrows, for example if they are asymmetric lenses pp1; g1q : S ÝÑ A1 and pp2; g2q : S ÝÑ A2, it is convenient to notate the span as A1 ÐppÝ1Ý;gÝ1Ýq S ÝpÝp2Ý;Ýg2Ñq A2. The lens pp1; g1q will be called the left leg of the span, and the lens pp2; g2q will similarly be called the right leg of the span.
The reader may choose to think of a symmetric lens, shortly to be introduced, as a span of asymmetric lenses. But in fact, in common with other descriptions of similar structures, symmetric lenses are really equivalence classes of spans of asymmetric lenses. In this paper it will be convenient to talk about, for example, \the symmetric lens A1 ÐppÝ1Ý;gÝ1Ýq S ÝpÝp2Ý;Ýg2Ñq A2", when strictly speaking that span is just a representative of an equivalence class of similar spans, and that equivalence class is the symmetric lens.
(i) f is surjective. (ii) f preserves Gets: g11f g1 and g21f
g2. (iii) f preserves Puts: for all a1, s we have p11pa1; f psqq f pp1pa1; sqq and p12pa2; f psqq f pp2pa2; sqq.
Let sp be the equivalence relation on spans of asymmetric lenses generated by those functions f between their heads that satisfy conditions (E).
De nition 3.2. A symmetric lens from A1 to A2 is a A2. sp-class of spans of asymmetric lenses from A1 to
The composition of symmetric lenses is usually de ned for (equivalence classes of) spans of well-behaved asymmetric lenses [JR17], but we aim to be more general here. In particular, we will show that the composition rule for well-behaved symmetric lenses generalises to a composition rule for symmetric lenses with left legs satisfying PutGet.
Note rst that if a symmetric lens has as a representative a span of asymmetric lenses in which one leg satis es
A1 ÐpqÝ1Ý;hÝ1Ýq S1 ÝpÝp2Ý;Ýg2Ñq A2 and
A2 ÐpqÝ2Ý;hÝ2Ýq S2 ÝpÝp3Ý;Ýg3Ñq A3 are spans of asymmetric lenses whose left legs satisfy PutGet. We de ne their composite symmetric lens, from A1 to A3, as follows.
Let S1 ÐhÝ2 T ÝgÑ2 S2 be the pullback in Set of the cospan S1 ÝgÑ2 A2 ÐhÝ2 S2. More concretely, without loss of generality, we may suppose that
T tps1; s2q P S1
S2 | g2ps1q h2ps2qu; and that h2 and g2 are the projections onto the rst and second components respectively. Next, we equip h2 with the Put q2 : S1 T ÝÑ T de ned by q2 s11; ps1; s2q s11; q2pg2ps11q; s2q , and equip g2 with the Put p2 : S2 T ÝÑ T de ned by p2 s12; ps1; s2q p2ph2ps12q; s1q; q2pg2pp2ph2ps12q; s1qq; s12q P T S1
S2: A representative for the composite symmetric lens A1 / A3 is then given by
A1 ÐpqÝ2Ý;hÝ2Ýq#ÝpqÝ1Ý;hÝ1Ýq T ÝpÝp2Ý;Ýg2ÝqÝ#pÝp3Ý;gÝ3Ñq A2:
S2 S1 S2
S1 S1 S2 h2 g2 p2
S1 S2
S1 S2 It is straightforward to check that the images of the functions q2 and p2 do indeed lie in their codomain T , and hence that they are well-de ned. Note that the construction above gives a diagram of asymmetric lenses A1 The composite symmetric lens is just given by composing the pairs of arrows on the left and right of the diagram. It is straightforward to verify that pq2; h2q satis es PutGet, and hence that the left leg of the composite also satis es PutGet.
Remark 3.4. The somewhat complicated second component q2pg2pp2ph2ps12q; s1q; s12qq of p2 arises because we do not assume that pp2; g2q satis es PutGet. If we do assume pp2; g2q obeys PutGet, then the expression simpli es to the more familiar q2ph2ps12q; s12q. This second component correspondingly also shows that pp2; g2q may also fail to satisfy PutGet.
Remark 3.5. It is worth remarking, as noted elsewhere [JR17], that the composition just de ned is reminiscent of, but di erent from, the normal composition of spans in a category with pullbacks. The peak of the span, T , is indeed a pullback, but not in the category Lens. Since the pullback is calculated in Set, the pullback projections are not a priori lenses, but the construction shows how to extend them to be lenses in a canonical way.
The construction presented here is also more general than the usual construction because it has to deal with (right leg) lenses that might not satisfy PutGet. We will comment further on this in the discussion section below.
Using the techniques of [JR17], it can be shown that sp is a congruence for this more general composition of spans of asymmetric lenses. Thus the composition is well-de ned on equivalence classes and provides a symmetric lens composition for those symmetric lenses whose left leg satis es PutGet. We thus make the following de nition. De nition 3.6. We de ne the symmetric monoidal category SLens to have sets as objects, symmetric lenses with left leg satisfying PutGet as arrows, and monoidal product given by cartesian product of sets.
Again, the reader should note that this is slightly more general than other de nitions of categories of symmetric lenses, which normally require both legs to satisfy PutGet (and possibly other conditions too). Nonetheless, using the standard techniques it is straightforward to check that this composition rule is associative and unital, and moreover that SLens is a well-de ned symmetric monoidal category. Identity symmetric lenses are simply given by the span in which both legs are identity asymmetric lenses. 4
Learners provide a categorical framework for modelling supervised learning algorithms. They can be seen as parametrised version of asymmetric lenses. In this section we introduce the basic ideas; more detail can be found in [FST19].
De nition 4.1. A learner pP; I; U; rq : A I : P A / B, an update U : B P A / B is a set P , together with three functions: an implementation / P , and a request r : B P A / A.
The goal of supervised learning is to approximate a function f : A / B using pairs pa; f paqq P A B of sample values, or training data. We view P as a set of parameters, and the implementation function as detailing how this set P parametrises functions, seen as hypotheses, A / B. Next, given a current hypothesis p P P and training datum pa; bq P A B, the update and request functions describe two ways to react to di erences between Ipp; aq and b: rst by updating the hypothesis p to U pb; p; aq, and second by requesting an alternative input rpb; p; aq.
Remark 4.2. While the implementation and update functions are evidently necessary structure for supervised learning, the role of the request function is more subtle. Indeed, the request function only becomes necessary through compositional considerations: it is what permits the construction of new learners by interconnecting given ones. Crucially, it captures the backpropagation part of the widely-used backpropagation algorithm for e cient training neural networks. Further discussion regarding interpretation of the request function can be found in [FST19, Remark II.2]. Example 4.3. Learners are not required to obey any axioms, and so are straightforward to construct. There are, however, learners which have been shown to be more useful than others in practice. One useful way of constructing learners is by using gradient descent on any di erentiably parametrised class of functions, such as one de ned using a neural net.
Indeed, given a set Rk and di erentiable function I : Rk Rm / Rn, as well as a real number ¡ 0 that we call a step size, we may de ne a learner pP; I; U; rq : Rm / Rn by setting
U pb; p; aq p rp 21 kIpp; aq
bk2; rpb; p; aq a ra 21 kIpp; aq bk2; where kxk is the Euclidean norm on Rn.
A key property of the category of learners is that this interpretation of a di erentiable function I is functorial, and indeed this functor captures the structure of the backpropagation algorithm. For more details see [FST19,
To state the aforementioned functoriality result, we must rst describe what it means to compose learners.
/ B a function f : P / P 1 is said to satisfy De nition 4.4. Given two learners pP; I; U; rq; pP 1; I1; U 1; r1q : A conditions pE1q when (ii) f preserves implementations: I1pf ppq; aq Ipp; aq. (iii) f preserves updates: U 1pb; f ppq; aq f pU pb; p; aqq. (iv) f preserves requests: r1pb; f ppq; aq rpb; p; aq.
De nition 4.5. The symmetric monoidal category Learn has sets as objects and phisms.
The composite of learners
A ÝpÝPÝ;IÝ;ÝU;ÝrÑq B ÝpÝQÝ;JÝ;ÝVÝ;sÑq C: is de ned to be pQ
P; I
J; U pI
V; r sq, where J qpq; p; aq
J pq; Ipp; aqq; pU
V qpc; q; p; aq
U spc; q; Ipp; aqq; p; a ; V c; q; Ipp; aq ; pr sqpc; q; p; aq
r spc; q; Ipp; aqq :
The monoidal product of objects A and B is their cartesian product A B, while the monoidal product of morphisms pP; I; U; rq : A / B and pQ; J; V; sq : C / D is pP Q; I}J; U }V; r}sq, where the implementation function is pI}J qpp; q; a; cq
pIpp; aq; J pq; cqq; pU }V qpb; d; p; q; a; cq pr}sqpb; d; p; q; a; cq pU pb; p; aq; V pd; q; cqq; prpb; p; aq; spd; q; cqq: Remark 4.6. A proof that this de nition indeed speci es a well de ned symmetric monoidal category follows from the same arguments as those given in [FST19, Proposition II.4]. Note, however, a key change: in the setting of [FST19], conditions (E1) are strengthened to require f be a bijection. The requirement that f be a bijection was made to avoid a digression about di erentiability in [FST19, De nition III.1], and yet still permit a straightforward statement of the main theorem [FST19, Theorem III.2]. Nonetheless, the authors of [FST19] believe conditions (E1) give the more natural notion of equivalence of learner, as it allows identi cation of parameters that have the same implementation. We believe that the correspondence with conditions (E) from [JR17] via Theorem 5.3 provides further evidence of this claim; indeed, we view this added clarity as a positive outcome of this work and the interaction between our two communities. l on learners. Equivalence classes of l-classes of learners as mor
For clarity, let us also present the composition rule using string diagrams in pSet; q. Given learners pP; I; U; rq and pQ; J; V; sq as above, the composite implementation function can be written as
Q P while the composite update{request function pU
V; r sq can be written as:
U; r B D P Q A C
The monoidal product of learners is represented in string diagrams as follows. The product implementation function I}J is while the composite update and request function pU }V; r}sq is
C Q P A
I
B
V; s
B
Q P
A P Q A C B D P Q A C
I J U; r V; s Remark 4.7. Note that lenses are learners with trivial, that is singleton, parameter set (as observed already by
Proposition 4.8. There is a faithful, identity-on-objects, symmetric monoidal functor Lens / Learn.
Proof. It is straightforward to check that the correspondence laid out above preserves composition and monoidal products.
While it is interesting, it is perhaps not surprising, and may not be especially enlightening, to nd that lenses are learners with trivial parameter set (which amounts to barely being a learner at all). There are other ways of seeing relationships between lenses and learners, and in particular of seeing the entire gamut of learners (not just ones with trivial parameters) as lenses.
Lemma 5.1. Every learner pP; I; U; rq : A / B is an asymmetric lens pp; gq : P A / B.
xU; ry : B pP Aq / P
The resulting lenses pxU; ry; Iq : P A / B will not in general be well-behaved. In particular the training process in supervised learning would not usually be expected to satisfy PutGet. Whether learners, when viewed as in this lemma as lenses should satisfy GetPut is a subject of ongoing research, so for now we make no assumptions. We make a comment again on this in Section 6.
Of course, merely observing that learners are lenses in this way is not especially useful if the composition of learners does not correspond to the composition of lenses. And it cannot. Given two learners pP; I; U; rq : A / B and pP 1; I1; U 1; r1q : B / C their corresponding lenses under the lemma are not even composable, since they have types pp; gq : P A / B and pp1; g1q : P 1 B / C.
As it happens, however, there is a Kleisli-like composition of these lenses that uses the monoidal product in the category Lens to convert the rst of these lenses, by taking its cartesian product with P 1, to obtain a lens P 1 P A / P 1 B which is then composable with the second lens. Remarkably the resulting composition does correspond precisely to the composition of the original learners. But all this can be expressed better by relating learners to certain symmetric lenses, and we do that now.
Lemma 5.2. Every learner pP; I; U; rq : A
/ B is a symmetric lens A ÐpÝkÝ;Ý2Ýq P
A ÝpÝxUÝ;ÝryÝ;IÑq B with left leg a constant complement (and therefore well-behaved) lens.
Proof. The right leg pxU; ry; Iq is the asymmetric lens given in Lemma 5.1, while the left leg pk; 2q is the constant complement (see Example 2.5) lens of the speci ed type.
It should be remarked that in both the preceding lemmas we would normally use the word \yields" rather than \is", and we would be explicit about the process that converts a learner into a lens. However, here we have used \is" to emphasise that what we are describing is nothing more than minor repackaging of the data. Furthermore, as the following theorem shows, the important interactions among the data (composition and monoidal product) are exactly the same, whether one treats the data as learners or lenses.
Theorem 5.3. There is a faithful, identity-on-objects, symmetric monoidal functor Learn / SLens mapping to pP; I; U; rq : A
With the correspondences established, the proof is largely a routine veri cation. Since Learn and SLens both have sets as objects, we may de ne the functor to act as the identity on objects. On arrows, the functor acts as in correspondence presented in Lemma 5.2 and outlined in the table above; the fact that this operation is independent of representive chosen follows immediately from the similarity between equivalence relation conditions (E) and (E1) (see De nitions 3.1 and 4.4). It is easy to see that this proposed functor preserves identities and the monoidal product.
The main di culty is proving that the proposed functor preserves composition. Before walking through this in detail on the next page, we rst present a useful lemma regarding composition of symmetric lenses.
Note that in Section 3 the composition of symmetric lenses with left legs satisfying PutGet was presented in its maximum generality. The motivation for that will be discussed in Section 6. To prove the above theorem, it will be helpful to understand the simpler case where the left legs are known to be constant complement. We summarise our notation for the composition in the following diagram (in which notation is abused in the usual way for constant complement lenses):
A1
P1 pky s;ssqss
A1 pp2;KgK2KqKK% pkys;ssqsss T KKKpKpK2K;g%2q
P2 ss yssspk; q A2
Lemma 5.4. Suppose that A1 ÐpÝkÝ;Ý2Ýq P1 A1 ÝpÝp2Ý;Ýg2Ñq A2 and A2 ÐpÝkÝ;Ý2Ýq P2 A2 ÝpÝp3Ý;Ýg3Ñq A3 are spans of asymmetric lenses whose left legs, both denoted pk; 2q, are constant complement lenses. Note that constant complement lenses satisfy PutGet and hence we may compose them using De nition 3.3.
Their composite symmetric lens from A1 to A3 is represented by
A1 ÐpÝkÝ;Ý3Ýq P2
P1
A1 ÝpÝpÝ;gÑq A3; (Note that to avoid overloading the notation pi, we have written mi for elements of Pi.)
A1 Consider then, as in De nition 3.3, the pullback T in Set of the cospan P1 A1 ÝgÑ2 A2 ÐÝ2 P2 A2. Knowing how to calculate pullbacks in Set, we may suppose without loss of generality that the elements of T are tuples pm2; m1; a1q, in which there is no a2 explicitly mentioned since it must be equal to g2pm1; a1q, and that h2 and g2 are 23 and P2 g2 respectively. More explicitly still, T is just the product P2 P1 A1, h2 is the projection onto P1 A1, and g2 is the arrow P2 P1 A1 / P2 A2 which preserves the P2 value and uses g2 to convert the other two values into an A2 value.
According to De nition 3.3, the left leg of the composite is the composition of two asymmetric lenses denoted there as pq2; h2q # pq1; h1q. In the current context, pq1; h1q is the constant complement lens P1 A1 / A1, and we have seen the q2 may be taken to be the projection P2 P1 A1 / P1 A1. Furthermore the de nition of h2 in De nition 3.3 is easily seen, up to reordering of variables, to be in this context the constant complement Put. Finally, we have already seen in Example 2.5 how the composition of two constant complement lenses is a constant complement lens, so the left leg of the composition here is simply the constant complement lens pk; 3q : P2 P1 A1 / A1.
We turn now to the right hand leg pp; gq. Again De nition 3.3 tells us that it is given by the asymmetric lens composition denoted there as pp2; g2q # pp3; g3q, in which p2 was de ned by what we referred to there as the \somewhat complicated expression". Referring to De nition 2.3 for how to compose asymmetric lenses, and using the notation of the statement of the lemma, we see that The second to last line holds since, as noted above, a fourth component in T is super uous since it has to be (and indeed is) g2 applied to the rst component. Reordering the variables in that last line, because we have chosen to keep the Ai in the last position, completes the proof.
Proof of Theorem 5.3. We will check that the proposed functor preserves composition. This is simply a matter of comparing the Get and Put of the right leg of composite symmetric learners, as detailed in Lemma 5.4, with the formulas for composition of learners as detailed in De nition 4.5.
First compare the de nition of I J in De nition 4.5 with the description of the Get of the composite right legs, gpm2; m1; aq of Lemma 5.4, recalling the correspondence between the implementation operations I and J and the right leg Gets g2 and g3. In other words, compare with gpm2; m1; aq
g3pm2; g2pm1; a1qq pI
J qpp; q; aq
J pq; Ipp; aqq noting the naming of variables means p and q correspond respectively to m1 and m2 (and that while the order of parameters for g is not important, the choice made for symmetric lens composition was to add new parameters on the left, corresponding to the choice used in function composition).
Next, we compare the right leg Put p of Lemma 5.4 with the composite update{request function xU V; r sy.
The A1 component is 2pp2pa12; pm1; a1qqq, which since a12 2pp3pa3; pm2; g2pm1; a1qqqq is which should be compared with
2p2 m1; a1; 2p3pa3; m2; g2pm1; a1qq pr sqpc; p; q; aq r p; a; spc; q; I pp; aqq recalling again that I corresponds to g2, that p and q correspond to m1 and m2, that a and c correspond to a1 and a3, and that r and s correspond to 2p2 and 2p3 respectively.
1p2 2p3pa3; m2; g2pm1; a1qq; m1; a1 which should be compared respectively with
U spc; q; Ipp; aqq; p; a and and 1p3 a3; m2; g2pm1; a1q
V c; q; Ipp; aq ; recalling all the correspondences we've already pointed out, along with the correspondences between U and V and 1p2 and 1p3 respectively.
These functions are all the same up to the speci ed renaming correspondences, and hence our functor preserves composition. 6
In this section we discuss two directions of research suggested by the main theorem: laws for well-behaved learners, and links between learners and multiary lenses.
We have shown that the usual notion of composition of symmetric lenses admits a generalization that receives a functor from Learn. Instead, one might consider adding conditions to the notion of learner that permit learners to embed into a more familiar notion of symmetric lens. Put another way: the lens laws suggest analogues for learners.
De nition 6.1. We say that a learner pP; I; U; rq obeys the I-UR law if for every parameter p P P we have both rpIpp; aq; p; aq a and U pIpp; aq; p; aq p, or in string diagrams
P A B P
A
This law asks that the lens pxU; ry; Iq obey the GetPut law. Intuitively, it states that if, at a given parameter p, the training pair pa; bq provided is already classi ed correctly by the learner|that is, if the training pair is of the form pa; Ipp; aqq|then the update function does not change the parameter and the request function does not request any change to the input. This sort of property can be a desirable property of learning algorithm, and a number of simple, important examples of learners, including those of Example 4.3, satisfy the I-UR law.
De nition 6.2. We say that a learner pP; I; U; rq obeys the UR-I law if for every parameter p P P and input a P A we have IpU pb; p; aq; rpb; p; aqq b, or in string diagrams
This law asks that the lens pxU; ry; Iq obey the PutGet law. The intuition here is that when given a training pair pa; bq, if the requested input rpb; p; aq is given to the implementation function at the new parameter U pb; p; aq, then the training pair prpb; p; aq; bq will be correctly classi ed by the learner. This is too strong for the incremental learning witnessed in practical supervised learning algorithms such as neural networks. Nonetheless, it is clear that a learner with this property would be in some sense desirable, or well-behaved.
Indeed, learning algorithms in practice must take into account practical considerations such as learning speed and convergence, and the prioritisation of these considerations leads to methods that violate abstract properties such as the I-UR and UR-I laws that might characterise what it means to learn e ectively. Nonetheless, we believe
U; r
P A
P
A U; r
I
B
B P A
P A B the formulation of these properties, from well-motivated considerations such as our main theorem, suggest ideas that could help frame and guide development of learning algorithms, especially should the intent be to construct algorithms which can be reasoned about to some extent.
This view of learners obeying generalised lens laws suggests a view of a learner as just a parametrised family of lenses, together with a rule for choosing which lens in this family to use given some examples of what you want the lens to do. During the course of preparing this work for this workshop an interesting similarity has come to light. In this paper the main tool we are using is symmetric lenses with left leg constant complement, and right leg bare lenses. In another paper presented at this workshop [JR19] that studies an entirely di erent area, the main tool the authors use is symmetric lenses (in fact, wide spans of lenses, so they may have in general more than two legs, but they do have at least two legs) with left leg what is known as a closed spg-lens, and right leg(s) arbritrary spg-lenses.
The similarity is more than just the linguistic parallel just described. We'll not de ne spg-lenses or closed spg-lenses here, but we remark that constant complement lenses are indeed closed spg-lenses. In both cases composition along those left legs is important, and the fact that they are, in both cases, closed and satisfy PutGet is what is important for the composition to work. The nature of the left legs is critical for the main idea in both papers.
What of the right legs? At rst they seem very di erent. In this paper the right legs are bare lenses | they have a Put p and Get g and nothing else, neither more structure, nor axioms. In apparent contrast, the right legs in [JR19] seem to have a substantial amount of structure. They do have a p and a g, but they also have something called an amendment and several axioms. The basic idea is that an update, expressed there as an arrow v in a category (here we only have the codomain of such an arrow when we are doing an update because these are set-based lenses), might result in not only a modi cation of the other component (or in the case of the multiary lenses of [JR19], the other components), but also an amendment. This amendment a can be composed with v so that while the Get of the Put might not be v, it will be av. In other words the amendment repairs
Now are the right hand lenses really that di erent? There is a standard way of seeing set based lenses as so called delta lenses (lenses that take arrows, not just codomain objects, as the input for Put). It appears as part of a uni ed treatment of many di erent kinds of lenses [JR16] and involves co-discrete categories. In a codiscrete category there is a unique way of extending each of the view updates from the bare lenses of this paper to make them line up with their own Put, in other words a unique way of extending bare lenses that satisfy no axioms to spg-lenses that satisfy PutGet. So, the two \main tools" are actually remarkably similar.
They still di er in one respect (only): spg-lenses are required to satisfy an axiom that corresponds to GetPut here. But we have just discussed how GetPut is in fact a desirable property that might be asked of Learners. If it were, then the two very di erent projects are in fact using exactly alignable, novel, tools: Closed amendment lenses (of the constant complement variety here) as left leg and spg amendment lenses as right leg(s).
7
To summarise, in this paper we have described a faithful, identity-on-objects, symmetric monoidal functor from a category which captures the notion of composable supervised learning algorithms to a suitable category of lenses. To do this, we presented a slight generalisation of the usual notion of symmetric lens, in which we require a very weak form of well behavedness: a span of asymmetric lenses in which the left leg satis es the PutGet law. Despite the general de nition, these symmetric lenses still compose, and indeed equivalence classes of them form the morphisms of a symmetric monoidal category SLens. Our main theorem describes the aforementioned close, functorial relationship between the category of learners, as de ned in [FST19], with this category of lenses. In this theorem, we witness a surprising yet highly robust link between two previously unrelated elds. We believe, as hinted by our brief discussion in Section 6, this to be a rich connection deserving of further exploration.
This work has been supported by the Australian Research Council and USA AFOSR grants FA9550-14-1-0031,