Reflections on Monadic Lenses

Abstract

Bidirectional transformations (bx) have primarily been modeled as pure functions, and do not account for the possibility of the side-effects that are available in most programming languages. Recently several formulations of bx that use monads to account for effects have been proposed, both among practitioners and in academic research. The combination of bx with effects turns out to be surprisingly subtle, leading to problems with some of these proposals and increasing the complexity of others. This paper reviews the proposals for monadic lenses to date, and offers some improved definitions, paying particular attention to the obstacles to naively adding monadic effects to existing definitions of pure bx such as lenses and symmetric lenses, and the subtleties of equivalence of symmetric bidirectional transformations in the presence of effects.

1 Introduction

Programming with multiple concrete representations of the same conceptual information is a commonplace, and challenging, problem. It is commonplace because data is everywhere, and not all of it is relevant or appropriate for every task: for example, one may want to work with only a subset of one’s full email account on a mobile phone or other low-bandwidth device. It is challenging because the most direct approach to mapping data across sources $A$ and $B$ is to write separate functions, one mapping to $B$ and one to $A$, following some (not always explicit) specification of what it means for an $A$ value and a $B$ value to be consistent. Keeping these transformations coherent with each other, and with the specification, is a considerable maintenance burden, yet it remains the main approach found in practice.

Over the past decade, a number of promising proposals to ease programming such bidirectional transformations have emerged, including lenses (Foster et al. 2007), bx based on consistency relations (Stevens 2010), symmetric lenses (Hofmann et al. 2011), and a number of variants and extensions (e.g. (Pacheco et al. 2014; Johnson and Rosebrugh 2014)). Most of these proposals consist of an interface with pure functions and some equational laws that characterise good behaviour; the interaction of bidirectionality with other effects has received comparatively little attention.

Some programmers and researchers have already proposed ways to combine lenses and monadic effects (Diviánszky 2013; Pacheco et al. 2014). Recently, we have proposed symmetric notions of bidirectional computation based on entangled state monads (Cheney et al. 2014; Abou-Saleh et al. 2015a) and coalgebras (Abou-Saleh et al. 2015b). As a result, there are now several alternative proposals for bidirectional transformations with effects. While this diversity is natural and healthy, reflecting an active research area, the different proposals tend to employ somewhat different terminology, and the relationships among them are not well understood. Small differences in definitions can have disproportionate impact.

In this paper we summarise and compare the existing proposals, offer some new alternatives, and attempt to provide general and useful definitions of “monadic lenses” and “symmetric monadic lenses”. Perhaps surprisingly, it appears challenging even to define the composition of lenses in the presence of effects, especially in the symmetric case. We first review the definition of pure asymmetric lenses and two prior proposals for extending them with monadic effects. These definitions have some limitations, and we propose a new definition of monadic lens that overcomes them.

Next we consider the symmetric case. The effectful bx and coalgebraic bx in our previous work are symmetric, but their definitions rely on relatively heavyweight machinery (monad transformers and morphisms, coalgebra). It seems natural to ask whether just adding monadic effects to symmetric lenses in the style of (Hofmann et al. 2011) would also work. We show that, as for asymmetric lenses, adding monadic effects to symmetric lenses is challenging, and give examples illustrating the problems with the most obvious generalisation. We then briefly discuss our recent work on symmetric forms of bx with monadic effects (Cheney et al. 2014; Abou-Saleh et al. 2015a, b). Defining composition for these approaches also turns out to be tricky, and our definition of monadic lenses arose out of exploring this space. The essence of composition of symmetric monadic bx, we now believe, can be presented most easily in terms of monadic lenses, by considering spans, an approach also advocated (in the pure case) by Johnson and Rosebrugh (2014).

Symmetric pure bx need to be equipped with a notion of equivalence, to abstract away inessential differences of representation of their “state” or “complement” spaces. As noted by Hofmann et al. (2011) and Johnson and Rosebrugh (2014), isomorphism of state spaces is unsatisfactory, and there are competing proposals for equivalence of symmetric lenses and spans. In the case of spans of monadic lenses, the right notion of equivalence seem even less obvious. We compare three, increasingly coarse, equivalences of spans based on isomorphism (following Abou-Saleh et al. (2015a)), span equivalence (following Johnson and Rosebrugh (2014)), and bisimulation (following Hofmann et al. (2011) and Abou-Saleh et al. (2015b)). In addition, we show a (we think surprising) result: in the pure case, span equivalence and bisimulation equivalence coincide.

In this paper we employ Haskell-like notation to describe and compare formalisms, with a few conventions: we write function composition with a centred dot, and use a lowered dot for field lookup $x \mathord {.} f$, in contrast to Haskell’s notation $f \; x$. Throughout the paper, we introduce a number of different representations of lenses, and rather than pedantically disambiguating them all, we freely redefine identifiers as we go. We assume familiarity with common uses of monads in Haskell to encapsulate effects (following Wadler (1995)), and with the $\mathbf {do}$-notation (following Wadler’s monad comprehensions Wadler (1992)). Although some of these ideas are present or implicit in recent papers (Hofmann et al. 2011; Johnson and Rosebrugh 2014; Cheney et al. 2014; Abou-Saleh et al. 2015a, b), this paper reflects our desire to clarify these ideas and expose them in their clearest form — a desire that is strongly influenced by Wadler’s work on a wide variety of related topics (Wadler 1992; King and Wadler 1992; Wadler 1995), and by our interactions with him as a colleague.

2 Asymmetric Monadic Lenses

Recall that a lens (Foster et al. 2007, 2012) is a pair of functions, usually called get and put:

satisfying (at least) the following well-behavedness laws:

The idea is that a lens of type $A \mathbin {\leadsto } B$ maintains a source of type $A$, providing a view of type $B$ onto it; the well-behavedness laws capture the intuition that the view faithfully reflects the source: if we “get” a $b$ from a source $a$ and then “put” the same $b$ value back into $a$, this leaves $a$ unchanged; and if we “put” a $b$ into a source $a$ and then “get” from the result, we get $b$ itself. Lenses are often equipped with a $create$ function

satisfying an additional law:

When the distinction is important, we use the term full for well-behaved lenses equipped with a $create$ operation. It is easy to show that the source and view types of a full lens must either both be empty or both non-empty, and that the $get$ operation of a full lens is surjective.

Lenses have been investigated extensively; see for example Foster et al. (2012) for a recent tutorial overview. For the purposes of this paper, we just recall the definition of composition of lenses:

which preserves well-behavedness.

2.1 A Naive Approach

As a first attempt, consider simply adding a monadic effect $\mu$ to the result types of both $get$ and $put$.

Such an approach has been considered and discussed in some recent Haskell libraries and online discussions (Diviánszky 2013). A natural question arises immediately: what laws should a lens satisfy? The following generalisations of the laws appear natural:

that is, if we “get” $b$ from $a$ and then “put” the same $b$ value back into $a$, this has the same effect as just returning $a$ (and doing nothing else), and if we “put” a value b and then “get” the result, this has the same effect as just returning b after doing the “put”. The obvious generalisation of composition from the pure case for these operations is:

This proposal has at least two apparent problems. First, the $\mathsf {(MGetPut_0)}$ law appears to sharply constrain $mget$: indeed, if $mget \; a$ has an irreversible side-effect then $\mathsf {(MGetPut_0)}$ cannot hold. This suggests that $mget$ must either be pure, or have side-effects that are reversible by $mput$, ruling out behaviours such as performing I/O during $mget$. Second, it appears difficult to compose these structures in a way that preserves the laws, unless we again make fairly draconian assumptions about $\mu$. In order to show $\mathsf {(MGetPut_0)}$ for the composition $l _{1}\mathbin {;} l _{2}$, it seems necessary to be able to commute $l _{2}\mathord {.} mget$ with $l _{1}\mathord {.} mget$ and we also need to know that doing $l _{1}\mathord {.} mget$ twice is the same as doing it just once. Likewise, to show $\mathsf {(MPutGet_0)}$ we need to commute $l _{2}\mathord {.} mget$ with $l _{1}\mathord {.} mput$.

2.2 Monadic Put-Lenses

Pacheco et al. (2014) proposed a variant of lenses called monadic putback-oriented lenses. For the purposes of this paper, the putback-orientation of their approach is irrelevant: we focus on their use of monads, and we provide a slightly simplified version of their definition:

The main difference from their version is that we remove the $Maybe$ type constructors from the return type of $mget$ and the first argument of $mput$. Pacheco et al. state laws for these monadic lenses. First, they assume that the monad $\mu$ has a monad membership operation

satisfying the following two laws:

Then the laws for $MLens_1$ (adapted from Pacheco et al. (2014 Proposition 3, p. 49)) are as follows:

In the first law we correct an apparent typo in the original paper, as well as removing the $Just$ constructors from both laws. By making $mget$ pure, this definition avoids the immediate problems with composition discussed above, and Pacheco et al. outline a proof that their laws are preserved by composition. However, it is not obvious how to generalise their approach beyond monads that admit a sensible $\in$ operation.

Many interesting monads do have a sensible $\in$ operation (e.g. $Maybe$, $[]$). Pacheco et al. suggest that $\in$ can be defined for any monad as $x \in m \equiv (\exists h: h\,m = x)$, where h is what they call a “(polymorphic) algebra for the monad at hand, essentially, a function of type $m \; a \rightarrow a$ for any type $a$.” However, this definition doesn’t appear satisfactory for monads such as $IO$, for which there is no such (pure) function: the $({\in }\text {-ID})$ law can never hold in this case. It is not clear that we can define a useful $\in$ operation directly for $IO$ either: given that $m \mathbin {{:}{:}} IO \; a$ could ultimately return any $a$-value, it seems safe, if perhaps overly conservative, to define $x \in m \mathrel {=} True$ for any $x$ and $m$. This satisfies the $\in$ laws, at least, if we make a simplifying assumption that all types are inhabited, and indeed, it seems to be the only thing we could write in Haskell that would satisfy the laws, since we have no way of looking inside the monadic computation $m \mathbin {{:}{:}} IO \; a$ to find out what its eventual return value is. But then the precondition of the $\mathsf {(MPutGet_1)}$ law is always true, which forces the view space to be trivial. These complications suggest, at least, that it would be advantageous to find a definition of monadic lenses that makes sense, and is preserved under composition, for any monad.

2.3 Monadic Lenses

We propose the following definition of monadic lenses for any monad $M$:

Definition 2.1

(Monadic Lens). A monadic lens from source type $A$ to view type $B$ in which the put operation may have effects from monad $M$ (or “$M$-lens from $A$ to $B$”), is represented by the type , where

(dropping the $\mu$ from the return type of $mget$, compared to the definition in Sect. 2.1). We say that $M$-lens $l$ is well-behaved if it satisfies

    $\diamondsuit$

Note that in $\mathsf {(MPutGet)}$, we use a continuation $k \mathbin {{:}{:}}\alpha \rightarrow \beta \rightarrow \mu \;\gamma$ to quantify over all possible subsequent computations in which $a'$ and $l \mathord {.} mget \; a'$ might appear. In fact, using the laws of monads and simply-typed lambda calculus we can prove this law from just the special case $k \mathrel {=}\lambda a \; b \rightarrow return \;( a , b )$, so in the sequel when we prove $\mathsf {(MPutGet)}$ we may just prove this case while using the strong form freely in the proof.

The ordinary asymmetric lenses are exactly the monadic lenses over $\mu \mathrel {=} Id$; the laws then specialise to the standard equational laws. Monadic lenses where $\mu \mathrel {=} Id$ are called pure, and we may refer to ordinary lenses as pure lenses also.

Definition 2.2

We can also define an operation that lifts a pure lens to a monadic lens:

    $\diamondsuit$

Lemma 2.3

If $l \mathbin {{:}{:}} Lens \;\alpha \;\beta$ is well-behaved, then so is $lens2mlens \; l$.     $\diamondsuit$

Example 2.4

To illustrate, some simple pure lenses include:

Many more examples of pure lenses are to be found in the literature (Foster et al. 2007, 2012), all of which lift to well-behaved monadic lenses.     $\diamondsuit$

As more interesting examples, we present asymmetric versions of the partial and logging lenses presented by Abou-Saleh et al. (2015a). Pure lenses are usually defined using total functions, which means that $get$ must be surjective whenever $A$ is nonempty, and $put$ must be defined for all source and view pairs. One way to accommodate partiality is to adjust the return type of $get$ to $Maybe \; b$ or give $put$ the return type $Maybe \; a$ to allow for failure if we attempt to put a $b$-value that is not in the range of $get$. In either case, the laws need to be adjusted somehow. Monadic lenses allow for partiality without requiring such an ad hoc change. A trivial example is

which is well-behaved because both sides of $\mathsf {(MPutGet)}$ fail if the view is changed to a value different from $b$. Of course, this example also illustrates that the $mget$ function of a monadic lens need not be surjective.

As a more interesting example, consider:

In the $mget$ direction, this lens maps a source number to its absolute value; in the reverse direction, it fails if the view $b$ is negative, and otherwise uses the sign of the previous source $a$ to determine the sign of the updated source.

The following logging lens takes a pure lens $l$ and, whenever the source value $a$ changes, records the previous $a$ value.

We presented a number of more involved examples of effectful symmetric bx in (Abou-Saleh et al. 2015a). They show how monadic lenses can employ user interaction, state, or nondeterminism to restore consistency. Most of these examples are equivalently definable as spans of monadic lenses, which we will discuss in the next section.

In practical use, it is usually also necessary to equip lenses with an initialisation mechanism. Indeed, as already mentioned, Pacheco et al.’s monadic put-lenses make the $\alpha$ argument optional (using $Maybe$), to allow for initialisation when only a $\beta$ is available; we chose to exclude this from our version of monadic lenses above.

We propose the following alternative:

and we consider such initialisable monadic lenses to be well-behaved when they satisfy the following additional law:

As with $\mathsf {(MPutGet)}$, this property follows from the special case $k \mathrel {=}\lambda x \; y \rightarrow return \;( x , y )$, and we will use this fact freely.

This approach, in our view, helps keep the $\mathsf {(GetPut)}$ and $\mathsf {(PutGet)}$ laws simple and clear, and avoids the need to wrap $mput$’s first argument in $Just$ whenever it is called.

Next, we consider composition of monadic lenses.

Note that we consider only the simple case in which the lenses share a common monad ${\mu }$. Composing lenses with effects in different monads would require determining how to compose the monads themselves, which is nontrivial (King and Wadler 1992; Jones and Duponcheel 1993).

Theorem 2.5

If are well-behaved, then so is $l _{1}\mathbin {;}~ l _{2}$.     $\diamondsuit$

3 Symmetric Monadic Lenses and Spans

Hofmann et al. (2011) proposed symmetric lenses that use a complement to store (at least) the information that is not present in both views.

Informally, $put _\mathrm {R}$ turns an $\alpha$ into a $\beta$, modifying a complement $\gamma$ as it goes, and symmetrically for $put _\mathrm {L}$; and $missing$ is an initial complement, to get the ball rolling. Well-behavedness for symmetric lenses amounts to the following equational laws:

Furthermore, the composition of two symmetric lenses preserves well-behavedness, and can be defined as follows:

We can define an identity symmetric lens as follows:

It is natural to wonder whether symmetric lens composition satisfies identity and associativity laws making symmetric lenses into a category. This is complicated by the fact that the complement types of the composition $id_{\mathrm {sl}}; sl$ and of $sl$ differ, so it is not even type-correct to ask whether $id_{\mathrm {sl}}; sl$ and $sl$ are equal. To make it possible to relate the behaviour of symmetric lenses with different complement types, Hofmann et al. defined equivalence of symmetric lenses as follows:

Definition 3.1

Suppose $R \subseteq C _{1} \times C _{2}$. Then $f \sim _{ R } g$ means that for all $c _{1}, c _{2}, x$, if $( c _{1}, c _{2})\in R$ and $( y , c _{1}')\mathrel {=} f \;( x , c _{1})$ and $( y' , c _{2}')\mathrel {=} g \;( y , c _{2})$, then $y \mathrel {=} y'$ and $( c _{1}', c _{2}')\in R$.     $\diamondsuit$

Definition 3.2

(Symmetric Lens Equivalence). Two symmetric lenses $sl _{1}\mathbin {{:}{:}} X \mathbin {\mathop {\longleftrightarrow }\limits ^{ C _{1}}} Y$ and $sl _{2}\mathbin {{:}{:}} X \mathbin {\mathop {\longleftrightarrow }\limits ^{ C _{2}}} Y$ are considered equivalent ($sl _{1}\equiv _{\mathrm {sl}} sl _{2}$) if there is a relation $R \subseteq C _{1} \times C _{2}$ such that

• 1. $( sl _{1}\mathord {.} missing , sl _{2}\mathord {.} missing )\in R$,

• 2. $sl _{1}\mathord {.} put _\mathrm {R} \sim _{ R } sl _{2}\mathord {.} put _\mathrm {R}$, and

• 3. $sl _{1}\mathord {.} put _\mathrm {L} \sim _{ R } sl _{2}\mathord {.} put _\mathrm {L}$.

    $\diamondsuit$

Hofmann et al. show that $\equiv _{\mathrm {sl}}$ is an equivalence relation; moreover it is sufficiently strong to validate identity, associativity and congruence laws:

Theorem 3.3

(Hofmann et al. 2011 ). If $sl _{1}\mathbin {{:}{:}} X \mathbin {\mathop {\longleftrightarrow }\limits ^{ C _{1}}} Y$ and $sl _{2}\mathbin {{:}{:}} Y \mathbin {\mathop {\longleftrightarrow }\limits ^{ C _{2}}} Z$ are well-behaved, then so is $sl _{1}\mathbin {;} sl _{2}$. In addition, composition satisfies the laws:

    $\diamondsuit$

3.1 Naive Monadic Symmetric Lenses

We now consider an obvious monadic generalisation of symmetric lenses, in which the $put _\mathrm {L}$ and $put _\mathrm {R}$ functions are allowed to have effects in some monad $M$:

Definition 3.4

A monadic symmetric lens from $A$ to $B$ with complement type $C$ and effects $M$ consists of two functions converting $A$ to $B$ and vice versa, each also operating on $C$ and possibly having effects in $M$, and a complement value $missing$ used for initialisation:

Such a lens $sl$ is called well-behaved if:

    $\diamondsuit$

The above monadic generalisation of symmetric lenses appears natural, but it turns out to have some idiosyncrasies, similar to those of the naive version of monadic lenses we considered in Sect. 2.1.

Composition and Well-Behavedness. Consider the following candidate definition of composition for monadic symmetric lenses:

which seems to be the obvious generalisation of pure symmetric lens composition to the monadic case. However, it does not always preserve well-behavedness.

Example 3.5

Consider the following construction:

The lens $setBool \; True$ has no effect on the complement or values, but sets the state to $True$. Both $setBool \; True$ and $setBool \; False$ are well-behaved, but their composition (in either direction) is not: $\mathsf {(PutRLM)}$ fails for $setBool True ; setBool \; False$ because $setBool \; True$ and $setBool \; False$ share a single $Bool$ state value.     $\diamondsuit$

Proposition 3.6

$setBool \; b$ is well-behaved for $b \in \{ True , False \}$, but $setBool \; True \mathbin {;} setBool \; False$ is not well-behaved.     $\diamondsuit$

Composition does preserve well-behavedness for commutative monads, i.e. those for which

but this rules out many interesting monads, such as $State$ and $IO$.

3.2 Entangled State Monads

The types of the $mput _\mathrm {R}$ and $mput _\mathrm {L}$ operations of symmetric lenses can be seen (modulo mild reordering) as stateful operations in the state monad $State \;\gamma \;\alpha \mathrel {=}\gamma \rightarrow (\alpha ,\gamma )$, where the state $\gamma \mathrel {=} C$. This observation was also anticipated by Hofmann et al. In a sequence of papers, we considered generalising these operations and their laws to an arbitrary monad (Cheney et al. 2014; Abou-Saleh et al. 2015a, b). In our initial workshop paper, we proposed the following definition:

subject to a subset of the $State$ monad laws (Plotkin and Power 2002), such as:

This presentation makes clear that bidirectionality can be viewed as a state effect in which two “views” of some common state are entangled. That is, rather than storing a pair of views, each independently variable, they are entangled, in the sense that a change to either may also change the other. Accordingly, the entangled state monad operations do not satisfy all of the usual laws of state: for example, the $set _{L}$ and $set _{R}$ operations do not commute.

However, one difficulty with the entangled state monad formalism is that, as discussed in Sect. 2.1, effectful $mget$ operations cause problems for composition. It turned out to be nontrivial to define a satisfactory notion of composition, even for the well-behaved special case where $\mu \mathrel {=} StateT \;\sigma \;\nu$ for some $\nu$, where $StateT$ is the state monad transformer (Liang et al. 1995), i.e. $StateT \;\sigma \;\nu \;\alpha \mathrel {=}\sigma \rightarrow \nu \;(\alpha ,\sigma )$. We formulated the definition of monadic lenses given earlier in this paper in the process of exploring this design space.

3.3 Spans of Monadic Lenses

Hofmann et al. (2011) showed that a symmetric lens is equivalent to a span of two ordinary lenses, and later work by Johnson and Rosebrugh (2014) investigated such spans of lenses in greater depth. Accordingly, we propose the following definition:

Definition 3.7

(Monadic Lens Spans). A span of monadic lenses (“$M$-lens span”) is a pair of $M$-lenses having the same source:

We say that an $M$-lens span is well-behaved if both of its components are.     $\diamondsuit$

We first note that we can extend either leg of a span with a monadic lens (preserving well-behavedness if the arguments are well-behaved):

To define composition, the basic idea is as follows. Given two spans and with a common type $B$ “in the middle”, we want to form a single span from $A$ to $C$. The obvious thing to try is to form a pullback of the two monadic lenses from $S _{1}$ and $S _{2}$ to the common type $B$, obtaining a span from some common state type $S$ to the state types $S _{1}$ and $S _{2}$, and composing with the outer legs. (See Fig. 1.) However, the category of monadic lenses doesn’t have pullbacks (as Johnson and Rosebrugh note, this is already the case for ordinary lenses). Instead, we construct the appropriate span as follows.

where we write $S _{1}\mathbin {\!\bowtie \!} S _{2}$ for the type of consistent state pairs $\{( s _{1}, s _{2})\in S _{1}\times S _{2}\mid l _{1}\mathord {.} mget \;( s _{1})\mathrel {=} l _{2}\mathord {.} mget \;( s _{2})\}$. In the absence of dependent types, we represent this type as $( S _{1}, S _{2})$ in Haskell, and we need to check that the $mput$ and $mcreate$ operations respect the consistency invariant.

Lemma 3.8

If and are well-behaved then so is .     $\diamondsuit$

Note that $\mathsf {(MPutGet)}$ and $\mathsf {(MCreateGet)}$ hold by construction and do not need the corresponding properties for $l _{1}$ and $l _{2}$, but these properties are needed to show that consistency is established by $mcreate$ and preserved by $mput$.

We can now define composition as follows:

Fig. 1.

Composing spans of lenses

The well-behavedness of the composition of two well-behaved spans is immediate because $\triangleleft$ and $\triangleright$ preserve well-behavedness of their arguments:

Theorem 3.9

If and are well-behaved spans of monadic lenses, then their composition $sp _{\mathrm {1}}\mathbin {;} sp _{\mathrm {2}}$ is well- behaved.     $\diamondsuit$

Given a span of monadic lenses , we can construct a monadic symmetric lens as follows:

Essentially, these operations use the span’s $mput$ and $mget$ operations to update one side and obtain the new view value for the other side, and use the $mcreate$ operations to build the initial $S$ state if the complement is $Nothing$.

Well-behavedness is preserved by the conversion from monadic lens spans to $SMLens$, for arbitrary monads $M$:

Theorem 3.10

If is well-behaved, then $span2smlens \; sp$ is also well-behaved.     $\diamondsuit$

Given , let $S \subseteq A \times B \times C$ be the set of consistent triples $( a , b , c )$, that is, those for which $sl \mathord {.} mput _\mathrm {R}\;( a , c )\mathrel {=} return \;( b , c )$ and $sl \mathord {.} mput _\mathrm {L}\;( b , c )\mathrel {=} return \;( a , c )$. We construct by

However, $smlens2span$ may not preserve well-behavedness even for simple monads such as $Maybe$, as the following counterexample illustrates.

Example 3.11

Consider the following monadic symmetric lens construction:

This is well-behaved but $smlens2span \; fail$ is not. In fact, the set of consistent states of $fail$ is empty, and each leg of the induced span is of the following form:

which fails to satisfy $\mathsf {(MGetPut)}$.     $\diamondsuit$

For pure symmetric lenses, $smlens2span$ does preserve well-behavedness.

Theorem 3.12

If $sl \mathbin {{:}{:}} SMLens \; Id \; C \; A \; B$ is well-behaved, then $smlens2span \; sl$ is also well-behaved, with state space $S$ consisting of the consistent triples of $sl$.     $\diamondsuit$

To summarise: spans of monadic lenses are closed under composition, and correspond to well-behaved symmetric monadic lenses. However, there are well-behaved symmetric monadic lenses that do not map to well-behaved spans. It seems to be an interesting open problem to give a direct axiomatisation of the symmetric monadic lenses that are essentially spans of monadic lenses (and are therefore closed under composition).

4 Equivalence of Spans

Hofmann et al. (2011) introduced a bisimulation-like notion of equivalence for pure symmetric lenses, in order to validate laws such as identity, associativity and congruence of composition. Johnson and Rosebrugh (2014) introduced a definition of equivalence of spans and compared it with symmetric lens equivalence. We have considered equivalences based on isomorphism (Abou-Saleh et al. 2015a) and bisimulation (Abou-Saleh et al. 2015b). In this section we consider and relate these approaches in the context of spans of $M$-lenses.

Definition 4.1

(Isomorphism Equivalence). Two $M$-lens spans $sp _{\mathrm {1}}\mathbin {{:}{:}}$ and are isomorphic ($sp \equiv _{\mathrm {i}} sp'$) if there is an isomorphism $h \mathbin {{:}{:}} S _{1}\rightarrow S _{2}$ on their state spaces such that $h \mathbin {;} sp _{\mathrm {2}}\mathord {.} left \mathrel {=} sp _{\mathrm {1}}\mathord {.} left$ and $h \mathbin {;} sp _{\mathrm {2}}\mathord {.} right \mathrel {=} sp _{\mathrm {1}}\mathord {.} right$.     $\diamondsuit$

Note that any isomorphism $h \mathbin {{:}{:}} S _{1}\rightarrow S _{2}$ can be made into a (monadic) lens; we omit the explicit conversion.

We consider a second definition of equivalence, inspired by Johnson and Rosebrugh (2014), which we call span equivalence:

Definition 4.2

(Span Equivalence). Two $M$-lens spans and are related by $\curvearrowright$ if there is a full lens $h \mathbin {{:}{:}} S _{1}\mathbin {\leadsto } S _{2}$ such that $h \mathbin {;} sp _{\mathrm {2}}\mathord {.} left \mathrel {=} sp _{\mathrm {1}}\mathord {.} left$ and $h \mathbin {;} sp _{\mathrm {2}}\mathord {.} right \mathrel {=} sp _{\mathrm {1}}\mathord {.} right$. The equivalence relation $\equiv _{\mathrm {s}}$ is the least equivalence relation containing $\curvearrowright$.     $\diamondsuit$

One important consideration emphasised by Johnson and Rosebrugh is the need to avoid making all compatible spans equivalent to the “trivial” span . To avoid this problem, they imposed conditions on $h$: its $get$ function must be surjective and split, meaning that there exists a function $c$ such that . We chose instead to require $h$ to be a full lens. This is actually slightly stronger than Johnson and Rosebrugh’s definition, at least from a constructive perspective, because $h$ is equipped with a specific choice of $c \mathrel {=} create$ satisfying , that is, the $\mathsf {(CreateGet)}$ law.

We have defined span equivalence as the reflexive, symmetric, transitive closure of $\curvearrowright$. Interestingly, even though span equivalence allows for an arbitrary sequence of (pure) lenses between the respective state spaces, it suffices to consider only spans of lenses. To prove this, we first state a lemma about the $({\bowtie })$ operation used in composition. Its proof is straightforward equational reasoning.

Lemma 4.3

Suppose $l _{1}\mathbin {{:}{:}} A \mathbin {\leadsto } B$ and $l _{2}\mathbin {{:}{:}} C \mathbin {\leadsto } B$ are pure lenses. Then $( l _{1}\mathbin {\bowtie } l _{2})\mathord {.} left \mathbin {;} l _{1}\mathrel {=}( l _{1}\mathbin {\bowtie } l _{2})\mathord {.} right \mathbin {;} l _{2}$.     $\diamondsuit$

Theorem 4.4

Given and , if $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$ then there exists such that $sp \mathord {.} left \mathbin {;} sp _{\mathrm {1}}\mathord {.} left \mathrel {=} sp \mathord {.} right \mathbin {;} sp _{\mathrm {2}}\mathord {.} left$ and $sp \mathord {.} left \mathbin {;} sp _{\mathrm {1}}\mathord {.} right \mathrel {=} sp \mathord {.} right \mathbin {;} sp _{\mathrm {2}}\mathord {.} right$.     $\diamondsuit$

Proof

Let $sp _{\mathrm {1}}$ and $sp _{\mathrm {2}}$ be given such that $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$. The proof is by induction on the length of the sequence of $\curvearrowright$ or $\curvearrowleft$ steps linking $sp _{\mathrm {1}}$ to $sp _{\mathrm {2}}$.

If $sp _{\mathrm {1}}\mathrel {=} sp _{\mathrm {2}}$ then the result is immediate. If $sp _{\mathrm {1}}\curvearrowright sp _{\mathrm {2}}$ then we can complete a span between $S _{1}$ and $S _{2}$ using the identity lens. For the inductive case, suppose that the result holds for sequences of up to n $\curvearrowright$ or $\curvearrowleft$ steps, and suppose $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$ holds in n $\curvearrowright$ or $\curvearrowleft$ steps. There are two cases, depending on the direction of the first step. If $sp _{\mathrm {1}}\curvearrowleft sp _{\mathrm {3}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$ then by induction we must have a pure span $sp$ between $S _{3}$ and $S _{2}$ and $sp _{\mathrm {1}}\curvearrowleft sp _{\mathrm {3}}$ holds by virtue of a lens $h \mathbin {{:}{:}} S _{3}\rightarrow S _{1}$, so we can simply compose $h$ with $sp \mathord {.} left$ to obtain the required span between $S _{1}$ and $S _{2}$. Otherwise, if $sp _{\mathrm {1}}\curvearrowright sp _{\mathrm {3}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$ then by induction we must have a pure span $sp$ between $S _{3}$ and $S _{2}$ and we must have a lens $h \mathbin {{:}{:}} S _{1}\rightarrow S _{3}$, so we use Lemma 4.3 to form a span and extend $sp _{\mathrm {0}}\mathord {.} right$ with $sp \mathord {.} right$ to form the required span between $S _{1}$ and $S _{3}$.    $\square$

Thus, span equivalence is a doubly appropriate name for $\equiv _{\mathrm {s}}$: it is an equivalence of spans witnessed by a (pure) span.

Finally, we consider a third notion of equivalence, inspired by the natural bisimulation equivalence for coalgebraic bx (Abou-Saleh et al. 2015b):

Definition 4.5

(Base Map). Given $M$-lenses and $l _{2}\mathbin {{:}{:}}$ , we say that $h \mathbin {:} S _{1}\rightarrow S _{2}$ is a base map from $l _{1}$ to $l _{2}$ if

Similarly, given two $M$-lens spans and $sp _{\mathrm {2}}\mathbin {{:}{:}}$ we say that $h \mathbin {{:}{:}} S _{1}\rightarrow S _{2}$ is a base map from $sp _{\mathrm {1}}$ to $sp _{\mathrm {2}}$ if $h$ is a base map from $sp _{\mathrm {1}}\mathord {.} left$ to $sp _{\mathrm {2}}\mathord {.} left$ and from $sp _{\mathrm {1}}\mathord {.} right$ to $sp _{\mathrm {2}}\mathord {.} right$.     $\diamondsuit$

Definition 4.6

(Bisimulation Equivalence). A bisimulation of $M$-lens spans and is a $M$-lens span where $R \subseteq S _{1} \times S _{2}$ and $fst$ is a base map from $sp$ to $sp _{\mathrm {1}}$ and $snd$ is a base map from $sp$ to $sp _{\mathrm {2}}$. We write $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$ when there is a bisimulation of spans $sp _{\mathrm {1}}$ and $sp _{\mathrm {2}}$.     $\diamondsuit$

Figure 2 illustrates the three equivalences diagrammatically.

Fig. 2.

(a) Isomorphism equivalence $(\equiv _{\mathrm {i}})$, (b) span equivalence $(\equiv _{\mathrm {s}})$, and (c) bisimulation $(\equiv _{\mathrm {b}})$ equivalence. In (c), the dotted arrows are base maps; all other arrows are (monadic) lenses.

Proposition 4.7

Each of the relations $\equiv _{\mathrm {i}}$, $\equiv _{\mathrm {s}}$ and $\equiv _{\mathrm {b}}$ are equivalence relations on compatible spans of $M$-lenses and satisfy $\mathsf {(Identity)}$, $\mathsf {(Assoc)}$ and $\mathsf {(Cong)}$.     $\diamondsuit$

Theorem 4.8

 ${sp}_{1}\equiv _\mathrm{i} {sp}_{2}$ implies ${sp}_{1}\equiv _\mathrm{s} {sp}_{2}$, but not the converse.     $\diamondsuit$

Proof

The forward direction is obvious; for the reverse direction, consider

Clearly $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$ by definition and all three structures are well-behaved, but $h$ is not an isomorphism: any $k \mathbin {{:}{:}}()\mathbin {\leadsto } Bool$ must satisfy $k \mathord {.} get \;()\mathrel {=} True$ or $k \mathord {.} get \;()\mathrel {=} False$, so cannot be the identity function.    $\square$

Theorem 4.9

Given , if $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$ then $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$.     $\diamondsuit$

Proof

For the forward direction, it suffices to show that a single $sp _{\mathrm {1}}\curvearrowright sp _{\mathrm {2}}$ step implies $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$, which is straightforward by taking $R$ to be the set of pairs $\{( s _{1}, s _{2})\mid l _{1}\mathord {.} get \; s _{1}\mathrel {=} s _{2}\}$, and constructing an appropriate span . Since bisimulation equivalence is transitive, it follows that $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$ implies $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$ as well.    $\square$

In the pure case, we can also show a converse:

Theorem 4.10

Given , if $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$ then $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$.     $\diamondsuit$

Proof

Given $R$ and a span constituting a bisimulation $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$, it suffices to construct a span satisfying $l \mathbin {;} sp _{\mathrm {1}}\mathord {.} left \mathrel {=} r \mathbin {;} sp _{\mathrm {2}}\mathord {.} left$ and $l \mathbin {;} sp _{\mathrm {1}}\mathord {.} right \mathrel {=} r \mathbin {;} sp _{\mathrm {2}}\mathord {.} right$.    $\square$

This result is surprising because the two equivalences come from rather different perspectives. Johnson and Rosebrugh introduced a form of span equivalence, and showed that it implies bisimulation equivalence. They did not explicitly address the question of whether this implication is strict. However, there are some differences between their presentation and ours; the most important difference is the fact that we assume lenses to be equipped with a create function, while they consider lenses without create functions but sometimes consider spans of lenses to be “pointed”, or equipped with designated initial state values. Likewise, Abou-Saleh et al. (2015b) considered bisimulation equivalence for coalgebraic bx over pointed sets (i.e. sets equipped with designated initial values). It remains to be determined whether Theorem 4.10 transfers to these settings.

We leave it as an open question to determine whether $\equiv _{\mathrm {b}}$ is equivalent to $\equiv _{\mathrm {s}}$ for spans of monadic lenses (we conjecture that they are not), or whether an analogous result to Theorem 4.10 carries over to symmetric lenses (we conjecture that it does).

5 Conclusions

Lenses are a popular and powerful abstraction for bidirectional transformations. Although they are most often studied in their conventional, pure form, practical applications of lenses typically grapple with side-effects, including exceptions, state, and user interaction. Some recent proposals for extending lenses with monadic effects have been made; our proposal for (asymmetric) monadic lenses improves on them because $M$-lenses are closed under composition for any fixed monad $M$. Furthermore, we investigated the symmetric case, and showed that spans of monadic lenses are also closed under composition, while the obvious generalisation of pure symmetric lenses to incorporate monadic effects is not closed under composition. Finally, we presented three notions of equivalence for spans of monadic lenses, related them, and proved a new result: bisimulation and span equivalence coincide for pure spans of lenses. This last result is somewhat surprising, given that Johnson and Rosebrugh introduced (what we call) span equivalence to overcome perceived shortcomings in Hofmann et al.’s bisimulation-based notion of symmetric lens equivalence. Further investigation is necessary to determine whether this result generalises.

These results illustrate the benefits of our formulation of monadic lenses and we hope they will inspire further research and appreciation of bidirectional programming with effects.

Appendices

A Proofs for Sect. 2

Theorem 2.5

If and are well-behaved, then so is $l _{1}\mathbin {;} l _{2}$.

Proof

Suppose $l _{1}$ and $l _{2}$ are well-behaved, and let $l \mathrel {=} l _{1}\mathbin {;} l _{2}$. We reason as follows for $\mathsf {(MGetPut)}$:

For $\mathsf {(MPutGet)}$, the proof is as follows:

   $\square$

B Proofs for Sect. 3

Proposition 3.6

 $setBool \; x$ is well-behaved for $x \in \{ True , False \}$, but $setBool \; True \mathbin {;} setBool \; False$ is not well-behaved.

    $\diamondsuit$

For the first part:

Proof

Let $sl \mathrel {=} setBool \; x$. We consider $\mathsf {(PutRLM)}$, and $\mathsf {(PutLRM)}$ is symmetric.

For the second part, taking $sl \mathrel {=} setBool \; True \mathbin {;} setBool \; False$, we proceed as follows:

However, we cannot simplify this any further. Moreover, it should be clear that the shared state will be $True$ after this operation is performed. Considering the other side of the desired equation:

it should be clear that the shared state will be $False$ after this operation is performed. Therefore, $\mathsf {(PutRLM)}$ is not satisfied by $sl$.    $\square$

Lemma 3.8

If and are well-behaved then so is .

    $\diamondsuit$

Proof

It suffices to consider the two lenses $l _{1}\mathrel {=} MLens \; fst \; put _\mathrm {L}\; create _\mathrm {L}$ and $l _{2}\mathrel {=} MLens \; snd \; put _\mathrm {R}\; create _\mathrm {R}$ in isolation. Moreover, the two cases are completely symmetric, so we only show the first.

For $\mathsf {(MGetPut)}$, we show:

The proof for $\mathsf {(MPutGet)}$ goes as follows. Note that it holds by construction, without appealing to well-behavedness of $ml _{\mathrm {1}}$ or $ml _{\mathrm {2}}$.

The proof for $\mathsf {(MCreateGet)}$ is similar.

Finally, we show that $put _\mathrm {L}\mathbin {{:}{:}}(\sigma _1\mathbin {\!\bowtie \!}\sigma _2)\rightarrow \sigma _1\rightarrow \mu \;(\sigma _1\mathbin {\!\bowtie \!}\sigma _2)$, and in particular, that it maintains the consistency invariant on the state space $\sigma _1\mathbin {\!\bowtie \!}\sigma _2$. Assume that $( s _{1}, s _{2})\mathbin {{:}{:}}\sigma _1\mathbin {\!\bowtie \!}\sigma _2$ and $s _{1}'\mathbin {{:}{:}}\sigma _1$ are given. Thus, $ml _{\mathrm {1}}\mathord {.} mget \; s _{1}\mathrel {=} ml _{\mathrm {2}}\mathord {.} mget \; s _{2}$. We must show that any value returned by $put _\mathrm {L}$ also satisfies this consistency criterion. By definition,

By $\mathsf {(MPutGet)}$, any $s _{2}'$ resulting from $ml _{\mathrm {2}}\mathord {.} mput \; s _{2}\;( ml _{\mathrm {1}}\mathord {.} mget \; s _{1}')$ will satisfy $ml _{\mathrm {2}}\mathord {.} mget \; s _{2}'\mathrel {=} ml _{\mathrm {1}}\mathord {.} mget \; s _{1}'$. The proof that $create _\mathrm {L}\mathbin {{:}{:}}\sigma _1\rightarrow \mu \;(\sigma _1\mathbin {\!\bowtie \!}\sigma _2)$ is similar, but simpler.    $\square$

Theorem 3.10

If is well-behaved, then $span2smlens \; sp$ is also well-behaved.

    $\diamondsuit$

Proof

Let $sl \mathrel {=} span2smlens \; sp$. We need to show that the laws $\mathsf {(PutRLM)}$ and $\mathsf {(PutLRM)}$ hold. We show $\mathsf {(PutRLM)}$, and $\mathsf {(PutLRM)}$ is symmetric.

We need to show that

There are two cases, depending on whether the initial state $mc$ is $Nothing$ or $Just \; c$ for some $c$.

If $mc \mathrel {=} Nothing$ then we reason as follows:

If $mc \mathrel {=} Just \; c$ then we reason as follows:

   $\square$

Theorem 3.12

If $sl \mathbin {{:}{:}} SMLens \; Id \; C \; A \; B$ is well-behaved, then $smlens2span \; sl$ is also well-behaved, with state space $S$ consisting of the consistent triples of $sl$.

    $\diamondsuit$

Proof

First we show that, given a symmetric lens $sl$, the operations of $sp \mathrel {=} smlens2span \; sl$ preserve consistency of the state. Assume $( a , b , c )$ is consistent. To show that $sp \mathord {.} left \mathord {.} mput \;( a , b , c )\; a'$ is consistent for any $a'$, we have to show that $( a' , b' , c' )$ is consistent, where $a'$ is arbitrary and $return \;( b' , c' )\mathrel {=} sl \mathord {.} mput _\mathrm {R}\;( a' , c )$. For one half of consistency, we have:

The proof that $sl \mathord {.} mput _\mathrm {R}\;( a' , c' )\mathrel {=} return \;( b' , c' )$ is symmetric.

as required. The proof that $sp \mathord {.} right \mathord {.} mput \;( a , b , c )\; b'$ is consistent is dual.

We will now show that $sp \mathrel {=} smlens2span \; sl$ is a well-behaved span for any symmetric lens $sl$. For $\mathsf {(MGetPut)}$, we proceed as follows:

For $\mathsf {(MPutGet)}$, we have:

The proof for $\mathsf {(MCreateGet)}$ is similar.

   $\square$

C Proofs for Sect. 4

Lemma 4.3

Suppose $l _{1}\mathbin {{:}{:}} A \mathbin {\leadsto } B$ and $l _{2}\mathbin {{:}{:}} C \mathbin {\leadsto } B$ are pure lenses. Then $( l _{1}\mathbin {\bowtie } l _{2})\mathord {.} left \mathbin {;} l _{1}\mathrel {=}( l _{1}\mathbin {\bowtie } l _{2})\mathord {.} right \mathbin {;} l _{2}$.

    $\diamondsuit$

Proof

Let $( l , r )\mathrel {=} l _{1}\mathbin {\bowtie } l _{2}$. We show that each component of $l \mathbin {;} l _{1}$ equals the corresponding component of $r \mathbin {;} l _{2}$.

For $get$:

For $put$:

Finally, for $create$:

   $\square$

Theorem 4.9

Given , if then .

    $\diamondsuit$

Proof

We give the details for the case $sp _{\mathrm {1}}\curvearrowright sp _{\mathrm {2}}$. First, write $( l _{1}, r _{1})\mathrel {=} sp _{\mathrm {1}}$ and $( l _{2}, r _{2})\mathrel {=} sp _{\mathrm {2}}$, and suppose $l \mathbin {{:}{:}} S _{1}\mathbin {\leadsto } S _{2}$ is a lens satisfying $l _{1}\mathrel {=} l \mathbin {;} l _{2}$ and $r _{1}\mathrel {=} l \mathbin {;} r _{2}$.

We need to define a bisimulation consisting of a set $R \subseteq S _{1} \times S _{2}$ and a span such that $fst$ is a base map from $sp$ to $sp _{\mathrm {1}}$ and $snd$ is a base map from $sp$ to $sp _{\mathrm {2}}$. We take $R \mathrel {=}\{( s _{1}, s _{2})\mid s _{2}\mathrel {=} l \mathord {.} get \;( s _{1})\}$ and proceed as follows:

We must now show that $l _{0}$ and $r _{0}$ are well-behaved (full) lenses, and that the projections $fst$ and $snd$ map $sp \mathrel {=}( l _{0}, r _{0})$ to $sp _{\mathrm {1}}$ and $sp _{\mathrm {2}}$ respectively.

We first show that $l _{0}$ is well-behaved; the reasoning for $r _{0}$ is symmetric. For $\mathsf {(MGetPut)}$ we have:

For $\mathsf {(MPutGet)}$ we have:

Finally, for $\mathsf {(MCreateGet)}$ we have:

Next, we show that $fst$ is a base map from $l _{0}$ to $l _{1}$ and $snd$ is a base map from $l _{0}$ to $l _{2}$. It is easy to show that $fst$ is a base map from $l _{0}$ to $l _{1}$ by unfolding definitions and applying of monad laws. To show that $snd$ is a base map from $l _{0}$ to $l _{2}$, we need to verify the following three equations that show that $snd$ commutes with $mget$, $mput$ and $mcreate$:

For the $mget$ equation:

For the $mput$ equation:

For the $mcreate$ equation:

Similar reasoning suffices to show that $fst$ is a base map from $r _{0}$ to $r _{1}$ and $snd$ is a base map from $r _{0}$ to $r _{2}$, so we can conclude that $R$ and $( l , r )$ constitute a bisimulation between $sp _{\mathrm {1}}$ and $sp _{\mathrm {2}}$, that is, $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$.    $\square$

Theorem 4.10

Given , if $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$ then $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$.

    $\diamondsuit$

Proof

For convenience, we again write $sp _{\mathrm {1}}\mathrel {=}( l _{1}, r _{1})$ and $sp _{\mathrm {2}}\mathrel {=}( l _{2}, r _{2})$. We are given $R$ and a span constituting a bisimulation $sp _{\mathrm {1}}\equiv _{\mathrm {b}} sp _{\mathrm {2}}$. Let $sp _{\mathrm {0}}\mathrel {=}( l _{0}, r _{0})$. For later reference, we list the properties that must hold by virtue of this bisimulation for any $( s _{1}, s _{2})\in R$:

In addition, it follows that:

which also implies the following identities, which we call twists:

It suffices to construct a span satisfying $l \mathbin {;} l _{1}\mathrel {=} r \mathbin {;} l _{2}$ and $l \mathbin {;} r _{1}\mathrel {=} r \mathbin {;} r _{2}$. Define $l$ and $r$ as follows:

Notice that by construction $l \mathbin {{:}{:}} R \mathbin {\leadsto } S _{1}$ and $r \mathbin {{:}{:}} R \mathbin {\leadsto } S _{2}$, that is, since we have used $l _{0}$ and $r _{0}$ to define $l$ and $r$, we do not need to do any more work to check that the pairs produced by $create$ and $put$ remain in $R$. Notice also that $l$ and $r$ only use the lenses $l _{1}$ and $l _{2}$, not $r _{1}$ and $r _{2}$; we will show nevertheless that they satisfy the required properties.

First, to show that $l \mathbin {;} l _{1}\mathrel {=} r \mathbin {;} l _{2}$, we proceed as follows for each operation. For $get$:

For $put$, we have:

Finally, for $create$ we have:

Next, we show that $l \mathbin {;} r _{1}\mathrel {=} r \mathbin {;} r _{2}$. For $get$:

For $put$, we have:

Finally, for $create$ we have:

We must also show that $l$ and $r$ are well-behaved full lenses. To show that $l$ is well-behaved, we proceed as follows. For $\mathsf {(GetPut)}$:

For $\mathsf {(PutGet)}$:

For $\mathsf {(CreateGet)}$:

Finally, notice that $l$ and $r$ are defined symmetrically so essentially the same reasoning shows $r$ is well-behaved.

To conclude, $sp \mathrel {=}( l , r )$ constitutes a span of lenses witnessing that $sp _{\mathrm {1}}\equiv _{\mathrm {s}} sp _{\mathrm {2}}$.    $\square$