{'fraction_non_alphanumeric': 0.039769019966070726, 'fraction_numerical': 0.012723476445256426, 'mean_word_length': 4.29412780656304, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Reflections on Monadic Lenses

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.


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. (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 f · g with a centred dot, and use a lowered dot for field lookup x .f , in contrast to Haskell's notation f x . Throughout the paper, we introduce a number of different repre-sentations 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 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.

Asymmetric monadic lenses
Recall that a lens (Foster et al., 2007(Foster et al., , 2012) is a pair of functions, usually called get and put: data α β = Lens {get :: α → β, put :: α → β → α} satisfying (at least) the following well-behavedness laws: The idea is that a lens of type A 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 data α β = Lens {get :: α → β, put :: α → β → α, create :: β → α} 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.

A naive approach
As a first attempt, consider simply adding a monadic effect µ 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 l :: 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 (MGetPut 0 ) law appears to sharply constrain mget: indeed, if mget a has an irreversible side-effect then (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 µ. In order to show (MGetPut 0 ) for the composition l 1 ; l 2 , it seems necessary to be able to commute l 2 .mget with l 1 .mget and we also need to know that doing l 1 .mget twice is the same as doing it just once. Likewise, to show (MPutGet 0 ) we need to commute l 2 .mget with l 1 .mput.

Monadic put-lenses
Pacheco et al. (2014) proposed a variant of lenses called monadic putbackoriented 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 µ has a monad membership operation (∈) :: α → µ α → Bool satisfying the following two laws: Then the laws for M Lens 1 (adapted from Pacheco et al. (2014, Prop. 3, p49)) 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 ∈ operation.
Many interesting monads do have a sensible ∈ operation (e.g. Maybe, [ ]). Pacheco et al. suggest that ∈ can be defined for any monad as x ∈ m ≡ (∃h : where h is what they call a "(polymorphic) algebra for the monad at hand, essentially, a of type m a → 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 (∈-ID) law can never hold in this case. It is not clear that we can define a useful ∈ operation directly for IO either: given that m :: IO a could ultimately return any a-value, it seems safe, if perhaps overly conservative, to define x ∈ m = True for any x and m. This satisfies the ∈ 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 :: IO a to find out what its eventual return value is. But then the precondition of the (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.

Monadic lenses
We propose the following definition of monadic lenses for any monad M : Note that in (MPutGet), we use a continuation k :: α → β → µ γ to quantify over all possible subsequent computations in which a and l .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 = λa b → return (a, b), so in the sequel when we prove (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 µ = Id ; the laws then specialise to the standard equational laws. Monadic lenses where µ = 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: 3. If l :: Lens α β is well-behaved, then so is lens2mlens l . Many more examples of pure lenses are to be found in the literature (Foster et al., 2007(Foster et al., , 2012, all of which lift to well-behaved monadic lenses. ♦ 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 (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 α argument optional (using Maybe), to allow for initialisation when only a β 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 (MPutGet), this property follows from the special case k = λx y → return (x , y), and we will use this fact freely. This approach, in our view, helps keep the (GetPut) and (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 µ. 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).

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 R turns an α into a β, modifying a complement γ as it goes, and symmetrically for put 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 sl ; sl and of sl differ, so it is not even type-correct to ask whether id 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.2 (Symmetric lens equivalence). Two symmetric lenses sl 1 :: Hofmann et al.show that ≡ sl is an equivalence relation; moreover it is sufficiently strong to validate identity, associativity and congruence laws: ←→ Z are well-behaved, then so is sl 1 ; sl 2 . In addition, composition satisfies the laws:

Naive monadic symmetric lenses
We now consider an obvious monadic generalisation of symmetric lenses, in which the put L and put 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: 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 Section 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: (PutRLM) fails for setBool True; setBool False because setBool True and setBool False share a single Bool state value. ♦ Proposition 3.6. setBool b is well-behaved for b ∈ {True, False }, but setBool True; setBool False is not well-behaved. ♦ 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.

Entangled state monads
The types of the mput R and mput L operations of symmetric lenses can be seen (modulo mild reordering) as stateful operations in the state monad State γ α = γ → (α, γ), where the state γ = 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 Section 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 µ = StateT σ ν for some ν, where StateT is the state monad transformer (Liang et al., 1995), i.e. StateT σ ν α = σ → ν (α, σ). We formulated the definition of monadic lenses given earlier in this paper in the process of exploring this design space.

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. ♦ 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 [A S 1 B ] M and [B S 2 C ] M 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 Composing spans of lenses from some common state type S to the state types S 1 and S 2 , and composing with the outer legs. (See Figure 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 S 2 for the type of consistent state pairs {(s 1 , s 2 ) ∈ S 1 × S 2 | l 1 .mget (s 1 ) = l 2 .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. S 2 ] µ . ♦ Note that (MPutGet) and (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: The well-behavedness of the composition of two well-behaved spans is immediate because and preserve well-behavedness of their arguments: However, smlens2span may not preserve well-behavedness even for simple monads such as Maybe, as the following counterexample illustrates. For pure symmetric lenses, smlens2span does preserve well-behavedness.
Theorem 3.12. If sl :: 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 . ♦ To summarise: spans of monadic lenses are closed under composition, and correspond to well-behaved symmetric monadic lenses. However, there are wellbehaved 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).  Note that any isomorphism h :: S 1 → 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: 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 h.get ·c = id . 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 = create satisfying h.get · c = id , that is, the (CreateGet) law.

Equivalence of spans
We have defined span equivalence as the reflexive, symmetric, transitive closure of . 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 ( ) operation used in composition. Its proof is straightforward equational reasoning. Proof. Let sp 1 and sp 2 be given such that sp 1 ≡ s sp 2 . The proof is by induction on the length of the sequence of or steps linking sp 1 to sp 2 . If sp 1 = sp 2 then the result is immediate. If sp 1 sp 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 or steps, and suppose sp 1 ≡ s sp 2 holds in n or steps. There are two cases, depending on the direction of the first step. If sp 1 sp 3 ≡ s sp 2 then by induction we must have a pure span sp between S 3 and S 2 and sp 1 sp 3 holds by virtue of a lens h :: S 3 → S 1 , so we can simply compose h with sp.left to obtain the required span between S 1 and S 2 . Otherwise, if sp 1 sp 3 ≡ s sp 2 then by induction we must have a pure span sp between S 3 and S 2 and we must have a lens h :: S 1 → S 3 , so we use Lemma 4.3 to form a span sp 0 :: S 1 (S 1 S 3 ) S 3 and extend sp 0 .right with sp.right to form the required span between S 1 and S 3 .
Thus, span equivalence is a doubly appropriate name for ≡ 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):    Proof. The forward direction is obvious; for the reverse direction, consider Clearly sp 1 ≡ s sp 2 by definition and all three structures are well-behaved, but h is not an isomorphism: any k :: () Bool must satisfy k .get () = True or k .get () = False, so (h ; k ).get = k .get · h.get cannot be the identity function. Proof. For the forward direction, it suffices to show that a single sp 1 sp 2 step implies sp 1 ≡ b sp 2 , which is straightforward by taking R to be the set of pairs {(s 1 , s 2 ) | l 1 .get s 1 = s 2 }, and constructing an appropriate span sp : A R B . Since bisimulation equivalence is transitive, it follows that sp 1 ≡ s sp 2 implies sp 1 ≡ b sp 2 as well.
In the pure case, we can also show a converse: 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 ≡ b is equivalent to ≡ 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).

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.

B Proofs for Section 3
Proposition 3.6. setBool x is well-behaved for x ∈ {True, False }, but setBool True; setBool False is not well-behaved. ♦ For the first part: Proof. Let sl = setBool x . We consider (PutRLM), and (PutLRM) is symmetric.
We will now show that sp = smlens2span sl is a well-behaved span for any symmetric lens sl . For (MGetPut), we proceed as follows: For (MPutGet), we have:  Finally, for create: Proof. We give the details for the case sp 1 sp 2 . First, write (l 1 , r 1 ) = sp 1 and (l 2 , r 2 ) = sp 2 , and suppose l :: S 1 S 2 is a lens satisfying l 1 = l ; l 2 and r 1 = l ; r 2 .
We need to define a bisimulation consisting of a set R ⊆ S 1 × S 2 and a span sp = (l 0 , r 0 ) :: [A R B ] M such that fst is a base map from sp to sp 1 and snd is a base map from sp to sp 2 . We take R = {(s 1 , s 2 ) | s 2 = l .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 = (l 0 , r 0 ) to sp 1 and sp 2 respectively. We first show that l 0 is well-behaved; the reasoning for r 0 is symmetric. For (MGetPut) 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: 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 1 and sp 2 , that is, sp 1 ≡ b sp 2 .
First, to show that l ; l 1 = r ; l 2 , we proceed as follows for each operation. For get: 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 (GetPut): Finally, notice that l and r are defined symmetrically so essentially the same reasoning shows r is well-behaved.
To conclude, sp = (l , r ) constitutes a span of lenses witnessing that sp 1 ≡ s sp 2 .