#A review of different kinds of Lenses
***

*guest post by [Emma Chollet](\url{https://www.researchgate.net/profile/Emma\_Chollet\_Ramampiandra}) and [Maurine Songa](\url{https://www.researchgate.net/profile/Maurine\_Songa})*

We recently read through and presented the paper, ``Unifying Set-Based, Delta-Based and Edit-Based Lenses" by Michael Johnson and Robert Rosebrugh for the Applied Category Theory online school. The paper's aim was to explore the relationship between three major classes of lenses. The paper can be found [here][ulens]. Here we try to explain our understanding of the subject while adding examples that we hope will be meaningful and useful to the reader.

##Introduction
***

For those unfamiliar with lenses, we find it important to introduce lenses in sort of a layman's way. Synchronization of data of essentially different kinds has become important in recent years. One can use bidirectional transformations **bx** to solve this problem. One asks themselves whether there are methods of determining when data are synchronized and identifies further methods to restore synchronization.

Lenses are an example of **bx** given by a mathematical structure. They provide the synchronization of a pair of models; one model, (the view), is determined by the other, (the source). These are subject to further properties.

Lenses are a good example of Applied Category Theory. They can be applied to databases, Haskell programs, Data Sharing, and Model-driven Engineering. Of great importance is the consistency relation, and this determines the type of lens that we end up with.

**Definition:** An *asymmetric (set-based) lens*, denoted $L:X \rightleftharpoons Y$, represented in the following figure, is a quadruple $(X,Y,g,p)$ with:
	
* A set of source models $X$,
* A set of view models $Y$,
* Two propagation functions, the *Get* and the *Put*:
$$g: X \rightarrow Y \ \  \and\ \  p: X \times Y \rightarrow X.$$

![Representation of Get and Put.](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/get_put.png)

The two functions are required to satisfy some so called lens laws, which ensure that the synchronisation of updates between systems is well-behaved:
	
1. *(PutGet):* The Get of a Put is the projection: 
		
![Diagram of PutGet law](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/diag_getput.png)
		
2. *(GetPut):* The Put for a trivially updated state is trivial:

![Diagram of GetPut law](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/diag_putget.png)
		
3. *(PutPut)* Composing Puts does not depend on the first view update:
		
![Diagram of PutPut law](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/diag_putput.png)

A lens is *well-behaved* when it satisfies condition 1 and 2, and *very well-behaved* if it satisfies conditions 1, 2 and 3.

###Types of Lenses
***

The definition above outlines main idea of how a lens works, but the states in the structures can be updated according to several criteria. In order to restore consistency between models, we can use:


* Only the new state after a change. This leads to **set-based** lenses. These are lenses among sets, with functions as the main update operation.

* Information about the change of the state itself. This leads to **delta-based** lenses. These are lenses among categories, with functors, and functions, as the main update operation.
	
* Descriptions of changes to structures. This leads to **edit-based** lenses. These are lenses among modules, with module homomorphisms as the main update operation.


Additionally, lenses can be classified as *symmetric* or *asymmetric*. The asymmetric lens ensures that a primary source remains synchronized with changes to some secondary view system. Symmetric lenses are more general and ensure that a pair of systems $X$ and $Y$ remain synchronized with changes to each other via some intermediate system $S$. *Complements* are key towards symmetric lenses.

###Examples of Lenses
***

![The Get and Put are shown in purple and orange, respectively.](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/ex_vlens.png)

* **Asymmetric set-based lens:** Suppose we have data structure, in this case a set representing postal addresses, with Zip Code being a subfield of any postal address. The goal is to view the Zip Code inside an address and being able to modify it for example, thus creating a new address. As a lens, this can be encoded as bellow and schematized as in the previous figure.
$$
\viewZipCode : \Postal \longrightarrow \Zip
$$
$$
\updateZipCode : \Postal \times \Zip \longrightarrow \Postal
$$
	
* **Asymmetric delta-based lens:** Suppose we want to model the current location of taxis and persons in what might be a real-time booking system. Consider the functor $\mathbf{Set^{CS}} \rightarrow \mathbf{Set^2}$ going from the category of cospans to the category of maps, both over **Set**. Here, the objects of $\mathbf{Set^{CS}}$ are thought of model states with three entity sets and two assignments e.g Taxis, Persons and Suburbs, and Taxis to Suburbs and Persons to Suburbs as assignments.

   + The Get of the lens is then the functor drawn in purple in the figures bellow and it shows only the Taxis and Suburbs information, while forgetting Persons and Persons to Suburbs information.

   + The Put is a function going from a pair of objects in $\mathbf{Set^{CS}}$ and $\mathbf{Set^2}$ to an arrow in $\mathbf{Set^{CS}}$. Represented in orange in the figures bellow, it can be interpreted as an update of the Taxis and the Suburbs information in $\mathbf{Set^{CS}}$ if e.g, in $\mathbf{Set^2}$, $h$ ``adds" Taxis and Suburbs, while leaving Persons unchanged. More on this at [[5]].

![Get functor of the delta-based lens.](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/ex_dlens_get.png)

![Put function of the delta-based lens.](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/ex_dlens_put.png)

	
* **Symmetric edit-lens**: Suppose we have two repositories that we would like to synchronize, see the figure bellow. On the left we have a mixed tagged list of composers and authors, on the right a pair of homogeneous untagged lists and on the top a set of complements storing just the tags. Now consider an edit that inserts a new element somewhere in the author list on the right. The update function in orange will then insert the information on the left replica, using a complement to exactly know where to insert it. The process is similar if a new tagged person is added to the list on the left, the purple update function, using a complement, will insert him or her in the right list on the right. Detailed examples can be found at [[1]][elens].

![Symmetric functions of the edit-based lens.](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/ex_elens.png)


##Mathematical definitions and implications
***

In this section, the lenses highlighted in orange in the following table are formally defined and some functors between them identified.

![Table of different lenses.](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/table_lenses.png)

###Fully faithful functor between vLens and dLens
***


**Definition:** A (very well-behaved) *asymmetric set-based lens* (v-lens) is defined as in the first definition among the category **Set** of sets. The Get and the Put are then usual functions that respect the three lens laws.


**Definition:** A (very well behaved) *asymmetric delta-based lens* (d-lens) between categories **X** and **Y**, is a pair $(G, P)$; where $G,$ the Get, is a functor $G: \mathbf{X} \longrightarrow \mathbf{Y}$, and $P,$ the Put, is a function $P: \vert G/\mathbf{Y} \vert \longrightarrow \vert \mathbf{X}^2 \vert$ going from the set of objects of the [comma category](https://ncatlab.org/nlab/show/comma+category) $G/\mathbf{Y}$ to the set of morphisms of **X**. $G$ and $P$ satisfy the lens laws adapted to this case (see [[4]][ulens] for details).


In regards to the construction of categories **vLens** and  **dLens** we have sets and categories as objects, respectively, and lenses between those objects as morphisms. The composition in each category is defined in [[6]][compvlens], page 2, for v-lenses and in [[2]][compdlens], page 7, for d-lenses.

For each set $X$, it is observed that there is a unique [codiscrete category](https://ncatlab.org/nlab/show/indiscrete+category) **X** whose objects are elements of $X$. Moreover, there is a bijective correspondence between functions from $X$ to $Y$ and functors from **X** to **Y**. This means that for our lenses, there exists a bijective correspondence between the Get functions of the v-lenses (from a set to another) and the Get functors of the d-lenses (from the corresponding codiscrete category to the other one). We can also construct a bijective correspondence between the Put functions of each category of lenses. This is detailed in the [reference paper][ulens]. Thus:


**Proposition:** There is a bijective correspondence between asymmetric v-lenses $L=(X,Y,g,p)$ and asymmetric d-lenses $(G,P)$ from **X** to **Y** between the codiscrete categories.

The functor $F: \mathbf{vLens} \longrightarrow \mathbf{dLens}$ is full and faithful. In other words, **vLens** can be seen as a full subcategory of **dLens**.

###The (neither full nor faithful) functor between eLens and sdLens
***

We move on to a not-so-nicely behaved functor $\mathbf{eLens} \rightarrow \mathbf{sdLens}.$ As discussed earlier, edit-based lenses are those among modules, with module homomorphism as the main update operation. The reader thus needs here some preliminary definitions of modules, module homomorphisms and stateful monoid homomorphisms as used in [[4]][ulens]:

**Definition:** Let $X$ be a set and $M_X$ a [monoid](https://en.wikipedia.org/wiki/Semigroup_action). A *module* $(X,M_X)$ is a partial monoid action of $M_X$ on $X$ such that monoid identity action and associativity are satisfied.
	
We note that the name, ``edit-based lenses'' is motivated by the fact that the elements of a monoid are called edits.

**Definition:** A *module homomorphism* $(f,\phi) : (X,M_X) \longrightarrow (Y,M_Y)$  is made up of a function $f : X \longrightarrow Y$ and a monoid homomorphism $\phi : M_X \longrightarrow M_Y$ which must satisfy for all $x$ in $X$ and $m$ in $M_X$, $f(x \cdot m) = f(x) \cdot \phi(m)$.

The composition of module homomorphisms is clearly associative and we can denote the category whose objects are modules and whose morphisms are module homomorphisms by **mod**.

**Definition:** Let $M_X$ and $M_Y$ be monoids and $C$ be a set whose elements are called *complements* or *consistencies*. A *stateful monoid homomorphism* from $M_X$ to $M_Y$ is a partial function $p: M_X \times C \longrightarrow M_Y \times C$ that respects the identity while preserving the complement, i.e. for all $c$ in $C$ $p(1,c)=(1,c)$, and, when $p(m,c)=(n,c')$ and $p(m',c')=(n',c'')$ are defined, we have $p(mm',c)=(nn',c'')$.

We have now everything we need to define a new kind of lens that will go from one module to another.

**Definition:** A *symmetric edit-based lens* (e-lens) between two modules $\lambda : (X, M_X) \leftrightarrow (Y, M_Y)$ is a 4-tuple $\lambda = (C, p, q, K)$ with:

* C, the set whose elements are called complements,
* $p: M_X \times C \rightarrow M_Y \times C$, a stateful monoid homomorphism,
* $q: M_Y \times C \rightarrow M_X \times C $, a stateful monoid homomorphism,
* $K$, a non empty relation $K \subseteq X \times C \times Y$ (consistency relation).

Furthermore, the functions have to satsify axioms so that the module actions interact properly with them: the effect of the action starting from a consistent triple must arrive at a consistent triple. Formally, it is required that these two conditions hold:

* $(x, c, y) \in K$ and $xm=x'$ defined

> $\Rightarrow p(m, c) = (n, c'),\ yn=y' $ defined and $(x',c',y') \in K$,

* $(x, c, y) \in K$ and $yn=y'$ defined

> $\Rightarrow q(n, c) = (m, c'),\ xm=x'$ defined and $ (x',c',y') \in K$.


Diagrammatically, these conditions can be seen in terms of squares, where the vertical arrows indicate the monoid action and the horizontal bars represent consistent triples from $K$:

![Diagram of conditions](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/diag_cond_elens.png)

**Definition:** Let $\lambda=(C,p,q,K)$ and $\mu=(C',p',q',K')$ be e-lenses, $\lambda : (X,M_X) \leftrightarrow (Y,M_Y)$ and $\mu : (Y,M_Y) \leftrightarrow (Z,M_Z)$. A *composite of two lenses* $\mu\lambda=(D,r,s,M)$, from $(X,M_X)$ to $(Z,M_Z)$, is defined as follows:

* $D= C \times C'$,
* $r(m,(c,c'))=(l,(c_1, c_1'))$ where $p(m,c)=(n,c_1)$ and $p'(n,c')=(l,c_1')$. We define $s$ in the same way with $q$ and $q'$,
* $M=\{(x,(c,c'),z)\  \vert \  \exists \  y \in Y $ with $(x,c,y) \in K$ and $(y,c',z) \in K'\}$.


**Proposition:** $\mu\lambda$ is an e-lens.

Indeed, $M \subseteq X \times (C \times C') \times Y.$ We are reminded to check that $r$ and $s$ are stateful homomorphisms and that they satisfy the conditions $(1)$ and $(2)$ required for an e-lens. Further details of the proof are given in [[4]][ulens].

Unfortunately, this time, the composition of e-lenses is not associative. As a matter of fact, let's suppose that we have a third e-lens $\nu : (Z,M_Z) \leftrightarrow (W,M_W)$, $\nu = (C'',p'',q'',K'')$. The new sets of consistent triples (third point of the composite) will then be:

For $\nu(\mu\lambda)$ :
$$
N=\{(x,((c,c'),c''),w)\  \vert \  \exists \  z \in Z \ \with\ (x,(c,c'),z) \in M \ \and\ (z,c'',w) \in K''\}.
$$

And for $(\nu\mu)\lambda$ :
$$
N'=\{(x,(c,(c',c'')),w)\  \vert \  \exists \  y \in Y \ \with\ (x,c,y) \in K \ \and\ (y,(c',c''),w) \in M'\}.
$$


Therefore we see that the sets $N$ and $N'$ aren't equal to each other, but they are canonically isomorphic due to the arrangement of brackets.

We notice that the construction of a category with modules as objects and e-lens as morphisms is going to be a problem, the composition of morphisms won't be well defined. The problem can be solved by using equivalence classes of e-lenses for morphisms, the composition will naturally come from the transitivity of the equivalence relation. What being equivalent means for two edit lenses is defined in Section 4 of [[4]][ulens], we denote it with $\equiv_e$. The category we finally get is **eLens**.


The link between edit lenses and symmetric delta lenses is then to be explored. The goal is to understand how to construct a sd-lense from e-lens. But first, what does symmetry imply in delta-based lenses ?

**Definition:** A *symmetric delta-based lens* (sd-lens or fb-lens) between categories **X** and **Y**, is a 4-tuple $M=(\delta_\mathbf{X}, \delta_\mathbf{Y},f,b)$ where:

* $\delta_\mathbf{X}$ and $\delta_\mathbf{Y}$ are forming span of sets with common domain denoted $R_{\mathbf{XY}}$, whose elements are called *corr*:
$$
\delta_{\mathbf{X}} : \vert\mathbf{X}\vert \longleftarrow R_{\mathbf{XY}} \longrightarrow \vert\mathbf{Y}\vert : \delta_{\mathbf{Y}},
$$
* $f$ and $b$ are operations called *forward propagation* and *backward propagation* (hence the name fb-lens):
$$
f: Arr(\mathbf{X}) \times_{\vert\mathbf{X}\vert} R_{\mathbf{XY}} \longrightarrow Arr(\mathbf{Y}) \times_{\vert\mathbf{Y}\vert} R_{\mathbf{XY}}
$$
$$
b: Arr(\mathbf{Y}) \times_{\vert\mathbf{Y}\vert} R_{\mathbf{XY}} \longrightarrow Arr(\mathbf{X}) \times_{\vert\mathbf{X}\vert} R_{\mathbf{XY}},
$$
* Both propagations respect identities and composition in $\mathbf{X}$ and $\mathbf{Y}$.

For the same ``non-associativity of composite" reasons, we have an equivalence relation $\equiv_{fb}$ for fb-lenses. There is a well defined category $\mathbf{sdLens}$ with categories as objects and equivalences classes of fb-lenses as morphisms, full details of which may be found in [[4]][ulens].

**Proposition:** $\lambda\equiv_e\lambda'$ implies $L_\lambda\equiv_{fb}L_{\lambda'}$

We then build a category $\mathbf{X}_M$ from a module $(X,M_X)$ in order to connect the two class of lenses. The set of objects of $\mathbf{X}_M$ is $X,$ and between each two elements $x$ and $x'$, the set of morphisms is $\{(x,m)\ \vert\ x \cdot m =x'\}$. The composition is defined as follows:

![Diagram of composition of edits](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/diag_comp_mod.png)

Let $(X,M_X)$ and $(Y,M_Y)$ be modules and $\lambda=(C,p,q,K)$ an e-lens from the first one to the second one. From $\lambda$ we construct an fb-lens $L_\lambda=(\delta_\mathbf{X}, \delta_\mathbf{Y},f,b)$:

$L_\lambda$ goes from $\mathbf{X}_M$ to $\mathbf{Y}_M$. The set of corrs of is $K$. We take the projections from $K$ as the span of sets $\delta_{\mathbf{X}} : \vert\mathbf{X}\vert \longleftarrow K \longrightarrow \vert\mathbf{Y}\vert : \delta_{\mathbf{Y}}$. Finally, suppose $xm=x'$ and $(x,c,y)$ in $K$, the forward and the backward propagations are defined as follows:

![Diagram of forward and backward propagations](http://math.ucr.edu/home/baez/mathematical/ACT2020/Chollet-Songa/diag_forback.png)

**Proposition:** For any e-lens $\lambda$, $L_\lambda$ is and fb-lens.

**Corollary:** $\lambda \longrightarrow L_\lambda$ is the arrow part of a functor $\mathbf{eLens} \longrightarrow \mathbf{sdLens}$.

Unfortunately we observe that, according to this construction, the propagations are defined based on a certain criteria of coherence, which is not the case for fb-lenses in general. This means that between two categories corresponding to some modules, there could be other fb-lenses that do not arise from the e-lenses, i.e. the functor is not a full subcategory inclusion.

Moreover, the definition of equivalence relation between two e-lenses leaves them the possibility of being inequivalent when they are identical except that one has one or more complements interfering in no consistent triples. In other words, their corresponding fb-lens will be the same, the functor is therefore not faithful either. 

##Some Conclusions
It is established among these lenses that;

* Set-based lenses are special cases of delta-lens using codiscrete category. In the construction of the functor $\mathbf{vLens} \rightarrow \mathbf{dLens}$ using codiscrete categories, it is ascertained that:
		
   + **vLens** is a full subcat. of **dLens**,
   + Some **d-lenses** are not **v-lenses**,
   + Every **d-lens** between codiscrete categories is a **v-lens** and vice-versa.
	
* Two edit lenses can be equivalent, i.e they can exhibit similar behaviour.
	
* There exists a functor between the category of edit lenses and the category of symmetric delta lenses, i.e $\mathbf{eLens} \rightarrow \mathbf{sdLens}.$ Here the functor:
   + Is not presumed to be full,
   + Is not a subcategory inclusion,
   + Is not faithful.
	
* One can use the equivalence classes of spans of asymmetric lenses to obtain a symmetric lens. We can also compose them from a ``span's'' point of view, more on this in [[3]][spans].

##References

[elens]: http://dmwit.com/papers/201107EL.pdf "Hofmann M., Pierce B. and Wagner D. (2012), *Edit Lenses*, In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 495–508."

[compdlens]: https://journal.ub.tu-berlin.de/eceasst/article/view/875/866 "Johnson M. and Rosebrugh R. (2013), *Delta Lenses and Opfibrations*, Electronic Communications of the EASST, Volume 57."

[spans]: http://ceur-ws.org/Vol-1396/p1-johnson.pdf "Johnson M. and Rosebrugh R. (2015), *Spans of delta lenses*, CEUR Proceedings, 1396, 1–15."

[ulens]: http://ceur-ws.org/Vol-1571/paper_13.pdf "Johnson M. and Rosebrugh R. (2016), *Unifying Set-Based, Delta-Based and Edit-Based Lenses*, CEUR Proceedings, 1571, 1–13."

[dlens]: http://www.jot.fm/issues/issue_2017_01/article2.pdf "Johnson M. and Rosebrugh R. (2017), *Symmetric delta lenses and spans of asymmetric delta lens*, Journal of Object Technology."

[compvlens]: https://arxiv.org/pdf/1809.00738.pdf "Riley M. (2018), *Categories of Optics*, arXiv:1809.00738v2 [math.CT]."
