=Paper=
{{Paper
|id=Vol-2355/paper2
|storemode=property
|title=Lenses and Learners
|pdfUrl=https://ceur-ws.org/Vol-2355/paper2.pdf
|volume=Vol-2355
|authors=Brendan Fong,Michael Johnson
|dblpUrl=https://dblp.org/rec/conf/bx/FongJ19
}}
==Lenses and Learners==
https://ceur-ws.org/Vol-2355/paper2.pdf
Lenses and Learners
Brendan Fong Michael Johnson
Department of Mathematics Faculty of Science and Engineering
Massachusetts Institute of Technology Macquarie University
bfo@mit.edu michael.johnson@mq.edu.au
Abstract
Lenses are a well-established structure for modelling bidirectional trans-
formations, 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 cate-
gory of symmetric lenses.
1 Introduction
This paper presents surprising links between two apparently disparate areas: a compositional treatment of super-
vised learning algorithms, called learners, and and a mathematical treatment of bidirectional transformations,
called lenses. Until this work there had been no known non-trivial relationships between the two areas, and,
naively at least, there seemed to be little reason to expect them to be closely related mathematically.
But lenses and learners are indeed mathematically closely related. The main result that we present here is
the existence of a faithful, identity-on-objects, symmetric monoidal functor, from the category whose arrows are
learners to a category whose arrows are symmetric lenses. In addition, the symmetric lenses in the image of that
functor have particularly simple structure: as spans of asymmetric lenses, their left legs are the long studied and
easily understood lenses known as constant complement lenses. Roughly speaking, this means that a supervised
learning algorithm may be understood as a special type of symmetric lens.
The right legs of the symmetric lenses in the image of the functor are also simple, but in a different way. The
right legs are bare asymmetric lenses — lenses which have, as all lenses do, a Put and Get, but which have no
axioms restricting the way the Put and Get interact. Such simple lenses were defined in the very first papers
on lenses, and were the ones blessed with the name “lens”, but the study of such bare lenses has so far been
somewhat neglected by the lens community, and certainly by us, because of a lack of examples or applications
requiring them. This paper provides some compelling examples and has led us to study them seriously.
The symmetric lenses that correspond to learners also have links, as will be explained in the discussion section,
with recent work on some quite sophisticated notions of lenses called amendment lenses, or in a slightly simplified
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: J. Cheney, H-S. Ko (eds.): Proceedings of the Eighth International Workshop on Bidirectional Transformations (Bx 2019),
Philadelphia, PA, USA, June 4, 2019, published at http://ceur-ws.org
16
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.
Terminology and notation
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 significant simplifications, 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).
Outline
The paper is structured as follows.
In the next two sections we introduce lenses, firstly 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 briefly 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 definition of composition of symmetric lenses which is
generally defined 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 definition of composition can be extended to symmetric
lenses in which one leg satisfies PutGet even if the other leg satisfies 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 first find the definition 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 flowing
from these results.
17
2 Asymmetric Lenses
Asymmetric lenses have been studied in a variety of different categories, and with a range of different 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.
Definition 2.1. An asymmetric lens pp, gq : A / B is a pair of functions: a Put p : B ˆ A / A and a Get
g: A / B.
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.
Definition 2.2. An asymmetric lens pp, gq : A / B is called well-behaved if it satisfies the following two
conditions
(PutGet) The Get of a Put is the projection. That is, gpppa, bqq “ b, or in string diagrams
B B
p g B “ B
A A
(GetPut) The Put of an unchanged Get result is unchanged. That is, ppgpaq, aq “ a, or in string diagrams
g p
A A “ A A
(Here the splitting wire represents the diagonal map A / A ˆ A, i.e. a ÞÑ pa, aq.)
Even without meeting the definition of well-behaved, lenses compose in a straightforward way, and well-
behaved 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.
Definition 2.3. The composite lens pp, gq # pp1 , g 1 q : A / C constructed from lenses pp, gq : A / B and
1 1
pp , g q : B / 1
C has as Get simply the composite g g of the Gets
A g g1 C
and as Put, q : C ˆ A / A given by qpc, aq “ ppp1 pgpaq, cq, aq.
C p1
g p A
A
Thus in the notation just introduced, pp, gq # pp1 , g 1 q “ pq, g 1 gq.
Definition 2.4. With the composition just defined, 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 de-
noted 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.
18
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 , idA q : A / A on a set A has identity function as Get and projection onto the first 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, π1 q : A1 ˆ A2 / A1 , where kpa11 , pa1 , a2 qq “ pa11 , a2 q — 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, π1 q is
well-behaved.
The composite of constant complement lenses is again constant complement. Indeed, suppose further that
A1 “ B1 ˆ B2 , and that pk 1 , π1 q : B1 ˆ B2 / B1 is a constant complement lens (so k 1 pb11 , pb1 , b2 qq “ pb11 , b2 q).
1
Then the composite lens pk, π1 q # pk , π1 q : B1 ˆ B2 ˆ A2 / B1 has Put k 2 : B1 ˆ pB1 ˆ B2 ˆ A2 q / B1 ˆ B2 ˆ A2
given by
` ˘ ` ˘
k 2 b11 , pb1 , b2 , a2 q “ k k 1 pb11 , pb1 , b2 qq, pb1 , b2 , a2 q
` ˘
“ k pb11 , b2 q, pb1 , b2 , a2 q
“ pb11 , b2 , a2 q,
and Get given by π1 : B1 ˆ pB2 ˆ A2 q / B1 . This is, up to isomorphism, the constant complement lens
pk 2 , π1 q : B1 ˆ B2 ˆ A2 / B1 .
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 Symmetric Lenses
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 , g1 q : S ÝÑ A1 and pp2 , g2 q : S ÝÑ A2 ,
pp1 ,g1 q pp2 ,g2 q
it is convenient to notate the span as A1 ÐÝÝÝÝ S ÝÝÝÝÑ A2 . The lens pp1 , g1 q will be called the left leg of the
span, and the lens pp2 , g2 q 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 sym-
pp1 ,g1 q pp2 ,g2 q
metric lens A1 ÐÝÝÝÝ S ÝÝÝÝÑ 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.
For completeness we include here the description of the equivalence relation.
19
pp1 ,g1 q pp2 ,g2 q pp1 ,g 1 q pp1 ,g 1 q
Definition 3.1. Suppose given two spans of asymmetric lenses A1 ÐÝÝÝÝ S ÝÝÝÝÑ A2 and A1 ÐÝ1ÝÝ1Ý S 1 ÝÝ2ÝÝ2Ñ
A2 with common feet A1 and A2 . A function f : S ÝÑ S 1 is said to satisfy conditions (E) [JR17] when
(i) f is surjective.
(ii) f preserves Gets: g11 f “ g1 and g21 f “ g2 .
(iii) f preserves Puts: for all a1 , s we have p11 pa1 , f psqq “ f pp1 pa1 , sqq and p12 pa2 , f psqq “ f pp2 pa2 , sqq.
Let ”sp be the equivalence relation on spans of asymmetric lenses generated by those functions f between
their heads that satisfy conditions (E).
Definition 3.2. A symmetric lens from A1 to A2 is a ”sp -class of spans of asymmetric lenses from A1 to
A2 .
The composition of symmetric lenses is usually defined 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 first that if a symmetric lens has as a representative a span of asymmetric lenses in which one leg satisfies
PutGet then all the representatives of that equivalence class have corresponding leg satisfying PutGet.
Definition 3.3. Suppose that
pq1 ,h1 q pp2 ,g2 q pq2 ,h2 q pp3 ,g3 q
A1 ÐÝÝÝÝ S1 ÝÝÝÝÑ A2 and A2 ÐÝÝÝÝ S2 ÝÝÝÝÑ A3
are spans of asymmetric lenses whose left legs satisfy PutGet. We define their composite symmetric lens,
from A1 to A3 , as follows.
h
2 2 g 2 2 g h
Let S1 ÐÝ T ÝÑ S2 be the pullback in Set of the cospan S1 ÝÑ A2 ÐÝ S2 . More concretely, without loss of
generality, we may suppose that
T “ tps1 , s2 q P S1 ˆ S2 | g2 ps1 q “ h2 ps2 qu,
and that h2 and g2 are the projections onto the ` first and ˘second ` components respectively.
˘ Next, we equip h2
with the Put q2 : S1 ˆ T ÝÑ T defined by q2 s11 , ps1 , s2 q “ s11 , q2 pg2 ps11 q, s2 q , and equip g2 with the Put
p2 : S2 ˆ T ÝÑ T defined by
` ˘ ` ˘
p2 s12 , ps1 , s2 q “ p2 ph2 ps12 q, s1 q, q2 pg2 pp2 ph2 ps12 q, s1 qq, s12 q P T Ď S1 ˆ S2 .
A representative for the composite symmetric lens A1 / A3 is then given by
pq2 ,h2 q#pq1 ,h1 q pp2 ,g2 q#pp3 ,g3 q
A1 ÐÝÝÝÝÝÝÝÝÝ T ÝÝÝÝÝÝÝÝÝÑ A2 .
To help parse these expressions, we draw string diagrams for q2
S1 S1
g2
S1 q2 S2
S2
and p2
S2 h2 p2 S1
S1
g2 q2 S2
S2
20
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-defined. Note that the construction above gives a diagram of asymmetric lenses
pq¯2 ,h¯2 q ss
T KK pp¯ ,g¯ q
s KK2 2
s KK
yss %
S1 KK S2 KK
pq1 ,h1 q ss KKK ss KppKK3 ,g3 q
ss K ss K%
yss pp2 ,g2 q % s
y spq2 ,h2 q
A1 A2 A3
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 , h2 q satisfies PutGet, and hence that the left leg of the composite also
satisfies PutGet.
Remark 3.4. The somewhat complicated second component q2 pg2 pp2 ph2 ps12 q, s1 q, s12 qq of p2 arises because we do
not assume that pp2 , g2 q satisfies PutGet. If we do assume pp2 , g2 q obeys PutGet, then the expression simplifies
to the more familiar q2 ph2 ps12 q, s12 q. This second component correspondingly also shows that pp2 , g2 q may also
fail to satisfy PutGet.
Remark 3.5. It is worth remarking, as noted elsewhere [JR17], that the composition just defined is reminiscent
of, but different 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-defined on equivalence classes and provides a symmetric
lens composition for those symmetric lenses whose left leg satisfies PutGet. We thus make the following definition.
Definition 3.6. We define 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 definitions 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-defined symmetric monoidal category. Identity symmetric lenses are simply given
by the span in which both legs are identity asymmetric lenses.
4 Learners
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].
Definition 4.1. A learner pP, I, U, rq : A / B is a set P , together with three functions: an implementation
I: P ˆA / B, an update U : B ˆ P ˆ A / 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 differences
between Ipp, aq and b: first 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
efficient training neural networks. Further discussion regarding interpretation of the request function can be
found in [FST19, Remark II.2].
21
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 differentiably parametrised class of functions, such as
one defined using a neural net.
Indeed, given a set Rk and differentiable function I : Rk ˆ Rm / Rn , as well as a real number ą 0 that we
call a step size, we may define a learner pP, I, U, rq : Rm / Rn by setting
U pb, p, aq “ p ´ ∇p 12 kIpp, aq ´ bk2 ,
rpb, p, aq “ a ´ ∇a 12 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 differentiable function I is functorial,
and indeed this functor captures the structure of the backpropagation algorithm. For more details see [FST19,
Theorem III.2].
To state the aforementioned functoriality result, we must first describe what it means to compose learners.
As with symmetric lenses, this first relies on stating what it means for two learners to be equivalent.
Definition 4.4. Given two learners pP, I, U, rq, pP 1 , I 1 , U 1 , r1 q : A / B a function f : P / P 1 is said to satisfy
conditions pE 1 q when
(i) f is surjective.
(ii) f preserves implementations: I 1 pf ppq, aq “ Ipp, aq.
(iii) f preserves updates: U 1 pb, f ppq, aq “ f pU pb, p, aqq.
(iv) f preserves requests: r1 pb, f ppq, aq “ rpb, p, aq.
Just as for symmetric lenses, this generates an equivalence relation ”l on learners. Equivalence classes of
learners form the morphisms of a symmetric monoidal category.
Definition 4.5. The symmetric monoidal category Learn has sets as objects and ”l -classes of learners as mor-
phisms.
The composite of learners
pP,I,U,rq pQ,J,V,sq
A ÝÝÝÝÝÝÑ B ÝÝÝÝÝÝÑ C.
is defined to be pQ ˆ P, I ˚ J, U ˚ V, r ˚ sq, where
pI ˚ Jqpq, p, aq “ Jpq, 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}Jqpp, q, a, cq “ pIpp, aq, Jpq, cqq,
pU }V qpb, d, p, q, a, cq “ pU pb, p, aq, V pd, q, cqq,
pr}sqpb, d, p, q, a, cq “ prpb, p, aq, spd, q, cqq.
Remark 4.6. A proof that this definition indeed specifies a well defined 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 differentiability in [FST19, Definition 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 identification
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.
22
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 J C
I
A
while the composite update–request function pU ˚ V, r ˚ sq can be written as:
C Q
Q V, s
B B
I
P
P
U, r
A A
The monoidal product of learners is represented in string diagrams as follows. The product implementation
function I}J is
P
Q I B
A
J D
C
while the composite update and request function pU }V, r}sq is
B
P
D U, r
Q
P
Q
A
A V, s
C
C
Remark 4.7. Note that lenses are learners with trivial, that is singleton, parameter set (as observed already by
Fong et al [FST19]):
Learner A /B Asymmetric lens A /B
Hypotheses P 1
Implementation I : P ˆ A /B Get g : A /B
Update U : B ˆ P ˆ A /P —
Request r : B ˆ P ˆ A /A Put p : B ˆ A /A
This in fact extends to an inclusion of categories.
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.
23
5 The Main Result
While it is interesting, it is perhaps not surprising, and may not be especially enlightening, to find 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.
We first note the following.
Lemma 5.1. Every learner pP, I, U, rq : A / B is an asymmetric lens pp, gq : P ˆ A / B.
Proof. Let g “ I : P ˆ A / B and let p “ xU, ry : B ˆ pP ˆ Aq / P ˆ A be the unique function into the product
P ˆ A determined by U and r.
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 , I 1 , U 1 , r1 q : B / C their corresponding lenses under the lemma are not even composable, since they have
types pp, gq : P ˆ A / B and pp1 , g 1 q : 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 first of these lenses, by taking its cartesian product with P 1 , to obtain a lens
P1 ˆ 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
pk,π2 q pxU,ry,Iq
A ÐÝÝÝÝ P ˆ A ÝÝÝÝÝÑ 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, π2 q is the constant
complement (see Example 2.5) lens of the specified type.
This gives the following correspondence:
Learner A /B Symmetric lens A /B
Hypotheses P Left leg complement P
Implementation I : P ˆ A /B Right leg Get g : P ˆ A /B
Update U : B ˆ P ˆ A /P Right leg Put p : B ˆ P ˆ A / P ˆ A (1st component)
Request r : B ˆ P ˆ A /A Right leg Put p : B ˆ P ˆ A / P ˆ A (2nd component)
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.
We are now in a position to state the main result.
Theorem 5.3. There is a faithful, identity-on-objects, symmetric monoidal functor Learn / SLens mapping
pP, I, U, rq : A /B
to
pk,π2 q pxU,ry,Iq
A ÐÝÝÝÝ P ˆ A ÝÝÝÝÝÑ B.
24
With the correspondences established, the proof is largely a routine verification. Since Learn and SLens both
have sets as objects, we may define 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 inde-
pendent of representive chosen follows immediately from the similarity between equivalence relation conditions
(E) and (E1 ) (see Definitions 3.1 and 4.4). It is easy to see that this proposed functor preserves identities and
the monoidal product.
The main difficulty is proving that the proposed functor preserves composition. Before walking through this
in detail on the next page, we first 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):
pk,πq ss
T KKpp¯2 ,g¯2 q
s KKK
ysss K%
P1 ˆ AK1 P2 ˆ AK2
pk,πq s
s KKK ss Kpp
KK3K,g3 q
ysss K yssspk,πq
pp ,g q %
2 2
%
A1 A2 A3
The following lemma gives an explicit formula for the composite of two symmetric lenses whose left legs are
constant complement.
pk,π2 q pp2 ,g2 q pk,π2 q pp3 ,g3 q
Lemma 5.4. Suppose that A1 ÐÝÝÝÝ P1 ˆ A1 ÝÝÝÝÑ A2 and A2 ÐÝÝÝÝ P2 ˆ A2 ÝÝÝÝÑ A3 are spans of
asymmetric lenses whose left legs, both denoted pk, π2 q, are constant complement lenses. Note that constant
complement lenses satisfy PutGet and hence we may compose them using Definition 3.3.
Their composite symmetric lens from A1 to A3 is represented by
pk,π3 q pp,gq
A1 ÐÝÝÝÝ P2 ˆ P1 ˆ A1 ÝÝÝÑ A3 ,
where p and g are given by ` ˘
ppa3 , pm1 , m2 , a1 qq “ m12 , p2 pa12 , pm1 , a1 qq ,
in which we let pm12 , a12 q “ p3 pa3 , pm2 , g2 pm1 , a1 qqq P P2 ˆ A2 , and
gpm2 , m1 , a1 q “ g3 pm2 , g2 pm1 , a1 qq.
(Note that to avoid overloading the notation pi , we have written mi for elements of Pi .)
Proof. Recall that in Definition 3.3 we use notation as in the following diagram.
pq¯2 ,h¯2 q ss
T KK pp¯ ,g¯ q
K2 2
KK
ss K%
yss
S1 KK S2 KK
pq1 ,h1 q ss
sss KKK
K sssss KppKK3 ,g3 q
K%
ys pp2 ,g2 q % ys pq2 ,h2 q
A1 A2 A3
2 g
2 π
Consider then, as in Definition 3.3, the pullback T in Set of the cospan P1 ˆ A1 ÝÑ A2 ÐÝ 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 , a1 q, in which there is no a2 explicitly mentioned since it must be equal to g2 pm1 , a1 q, 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 Definition 3.3, the left leg of the composite is the composition of two asymmetric lenses denoted
there as pq2 , h2 q # pq1 , h1 q. In the current context, pq1 , h1 q 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 definition of
25
h2 in Definition 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, π3 q : P2 ˆ P1 ˆ A1 / A1 .
We turn now to the right hand leg pp, gq. Again Definition 3.3 tells us that it is given by the asymmetric
lens composition denoted there as pp2 , g2 q # pp3 , g3 q, in which p2 was defined by what we referred to there as
the “somewhat complicated expression”. Referring to Definition 2.3 for how to compose asymmetric lenses, and
using the notation of the statement of the lemma, we see that
ppa3 , pm1 , m2 , a1 qq “ p2 ppm12 , a12 q, pm2 , m1 , a1 qq.
` ˘
We now show that this becomes, simply by substituting and simplifying, m12 , p2 pa12 , pm1 , a1 qq .
In detail
p2 ppm12 , a12 q, pm2 , m1 , a1 qq “ p2 ps12 , ps1 , s2 qq (in the notation of Definition 3.3)
` 1 1 1
˘
“ p2 ph2 ps2 q, s1 q, q2 pg2 pp2 ph2 ps2 q, s1 qq, s2 q (by Definition 3.3)
` 1 1 1
˘
“ p2 pa2 , s1 q, q2 pg2 pp2 pa2 , s1 qq, s2 q (since h2 ps2 q “ π2 pm12 , a12 q “ a12 )
1
` ˘
“ p2 pa12 , s1 q, q2 pg2 pp2 pa12 , s1 qq, pm12 , a12 qq (since s12 “ pm12 , a12 q)
` ˘
“ p2 pa12 , s1 q, pm12 , g2 pp2 pa12 , s1 qqq (since q2 is constant complement)
` 1 1
˘
“ p2 pa2 , s1 q, m2 (by comment below)
` 1 1
˘
“ p2 pa2 , pm1 , a1 qq, m2 (since s1 “ pm1 , a1 q)
The second to last line holds since, as noted above, a fourth component in T is superfluous since it has to be
(and indeed is) g2 applied to the first component. Reordering the variables in that last line, because we have
chosen to keep the Ai in the last position, completes the proof.
We now return to the proof of Theorem 5.3.
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 Definition 4.5.
First compare the definition of I ˚ J in Definition 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
gpm2 , m1 , aq “ g3 pm2 , g2 pm1 , a1 qq
with
pI ˚ Jqpp, q, aq “ Jpq, 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.
We do this by considering each of the two components separately.
The A1 component is π2 pp2 pa12 , pm1 , a1 qqq, which since a12 “ π2 pp3 pa3 , pm2 , g2 pm1 , a1 qqqq is
` ˘
π2 p2 m1 , a1 , π2 p3 pa3 , m2 , g2 pm1 , a1 qq
which should be compared with
` ˘
pr ˚ sqpc, p, q, aq “ r p, a, spc, q, Ipp, 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 π2 p2 and π2 p3 respectively.
26
Finally the P1 ˆ P2 component has, as its two coordinates,
` ˘ ` ˘
π1 p2 π2 p3 pa3 , m2 , g2 pm1 , a1 qq, m1 , a1 and π1 p3 a3 , m2 , g2 pm1 , a1 q
which should be compared respectively with
` ˘ ` ˘
U spc, q, Ipp, aqq, p, a and V c, q, Ipp, aq ,
recalling all the correspondences we’ve already pointed out, along with the correspondences between U and V
and π1 p2 and π1 p3 respectively.
These functions are all the same up to the specified renaming correspondences, and hence our functor preserves
composition.
6 Discussion
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.
6.1 Learner laws
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.
For example, the GetPut law generalises as follows.
Definition 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 I P P P
U, r “
A A A
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 classified 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.
We have focussed more on the PutGet law in this paper. This may be generalised as follows.
Definition 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
B B
P U, r I B “ P B
A A
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 classified 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 effectively. Nonetheless, we believe
27
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.
6.2 Links with multiary lenses
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 different 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 define 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 first they seem very different. 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 modification 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
PutGet.
Now are the right hand lenses really that different? 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 unified treatment of many different 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 differ 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 different 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).
The similarities and what they might mean (if anything) will be considered further in future work.
7 Conclusion
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 satisfies the PutGet law.
Despite the general definition, 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 defined in [FST19], with this category of lenses. In
this theorem, we witness a surprising yet highly robust link between two previously unrelated fields. We believe,
as hinted by our brief discussion in Section 6, this to be a rich connection deserving of further exploration.
Acknowledgements
This work has been supported by the Australian Research Council and USA AFOSR grants FA9550-14-1-0031,
FA9550-17-1-0058. BF thanks Jules Hedges for first bringing the contents of Remark 4.7 to his attention.
28
References
[BS81] Bancilhon, F. and Spyratos, N. (1981) Update semantics of relational views. ACM Trans. Database Syst.
6, 557–575.
[DXC11] Diskin, Z., Xiong, Y. and Czarnecki, K. (2011) From State- to Delta-Based Bidirectional Model
Transformations: the Asymmetric Case. Journal of Object Technology 10, 1–25. doi:10.5381/jot.2011.10.1.a6
[DKL18] Diskin, Z., König, H. and Lawford, M. (2018) Multiple model synchronization with multiary delta
lenses. Lecture Notes in Computer Science 10802, 21–37.
[FST19] Fong, B., Spivak, D. I. and Tuyéras, R. (2019) Backprop as functor: a compositional perspective on
supervised learning. To appear in Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2019. Preprint available as arXiv:1711.10455.
[FS19] Fong, B., and Spivak, D. I. (2019) An Invitation to Applied Category Theory: Seven Sketches in Compo-
sitionality, Cambridge University Press.
[FG+07] Foster, J., Greenwald, M., Moore, J., Pierce, B. and Schmitt, A. (2007) Combinators for bi-directional
tree transformations: A linguistic approach to the view update problem. ACM Transactions on Programming
Languages and Systems 29.
[HPW11] Hofmann, M., Pierce, B., and Wagner, D. (2011) Symmetric Lenses. ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (POPL), ACM SIGPLAN Notices 46, 371–384.
doi:10.1145/1925844.1926428
[JR12] Johnson M. and Rosebrugh, R. (2012) Lens put-put laws: monotonic and mixed. Proceedings of the 1st
International Workshop on Bidirectional Transformations, Tallin Electronic Communications of the EASST,
49, 13pp.
[JR13] Johnson, M. and Rosebrugh, R. (2013) Delta lenses and fibrations. Proceedings of the 2nd International
Workshop on Bidirectional Transformations, Rome Electronic Communications of the EASST 57, 18pp.
[JR16] Johnson, M. and Rosebrugh, R. (2016) Unifying set-based, delta-based and edit-based lenses. Proceedings
of the 5th International Workshop on Bidirectional Transformations, Eindhoven CEUR Proceedings 1571,
1–13.
[JR17] Johnson, M. and Rosebrugh, R. (2017) Symmetric delta lenses and spans of asymmetric delta lenses.
Journal of Object Technology, 16, 2:1–32.
[JR19] Johnson, M. and Rosebrugh, R. (2019) Multicategories of Multiary Lenses. To appear in Proceedings of
the Eighth International Workshop on Bidirectional Transformations (Bx2019).
[PS03] Pierce, B. and Schmitt, A. (2003) Lenses and view update translation. Preprint.
[Sel11] Selinger, P. (2011) A survey of graphical languages for monoidal categories. In Bob Coecke, editor, New
Structures for Physics, Lecture Notes in Physics 813:289–355, Springer.
29