# Applicative lenses

This is written in Literate Haskell.

```
module Applicative.Lenses where
import Control.Applicative
import Control.Monad
import Data.Functor
import Data.Monoid
import Bidirectional.Serialization.Two (Codec(..)) -- 2016-10-13
import Bidirectional.Serialization.Classes
```

I’m trying to figure out a relationship between the abstractions I previously brought up and lenses.

```
data Lens s t a b = Lens
get :: s -> a
{ put :: b -> s -> t
,
}
type Lens' s a = Lens s s a a
idL :: Lens' s s
idL = Lens id const
unitL :: Lens' s ()
unitL = ignorePut
ignorePut :: Lens s s () b
ignorePut = Lens (const ()) (const id)
```

There is a similarity to codecs. We import the definition of `Codec`

from 2016-10-13.

## Straightforward representation

Define the following wrapper types for `get`

and `put`

.

```
type MLensR = (->)
type MLensW s = Const (Endo s)
-- Applicative but not Monad.
lensR :: (s -> a) -> MLensR s a
lensR = id
unMLensR :: MLensR s a -> s -> a
unMLensR = id
lensW :: (s -> s) -> MLensW s a
lensW = Const . Endo
unMLensW :: MLensW s a -> s -> s
unMLensW = appEndo . getConst
type MLens s = Codec (MLensR s) (MLensW s)
```

Then `MLens s a a`

is isomorphic to `Lens' s a`

. The isomorphism can in fact be generalized between `MLens s b a`

and `Lens s s a b`

.

```
fromLens' :: Lens' s a -> MLens s a a
fromLens' = fromLens
toLens' :: MLens s a a -> Lens' s a
toLens' = toLens
fromLens :: Lens s s a b -> MLens s b a
fromLens (Lens get put) = Codec
lensR get)
(lensW . put)
(
toLens :: MLens s b a -> Lens s s a b
toLens (Codec parse produce) = Lens
unMLensR parse)
(unMLensW . produce) (
```

Based on that construction, we now have an `Applicative`

interface for composing lenses “horizontally”, combining their views together.

```
pairP
:: (Profunctor p, Applicative (p (b, b')))
=> p b a -> p b' a' -> p (b, b') (a, a')
pairP p p' = (,)
<$> fst =. p
<*> snd =. p'
pair :: MLens s b a -> MLens s b' a' -> MLens s (b, b') (a, a')
pair = pairP
pairLens :: Lens s s a b -> Lens s s a' b' -> Lens s s (a, a') (b, b')
pairLens l l' = toLens $ pair (fromLens l) (fromLens l')
```

However, their good behavior is not guaranteed.

```
oops :: Lens' s a -> Lens' s (a, a)
oops l = pairLens l l
-- PutGet fails.
oopsFails = get l (put l a s) /= a
where
l = oops idL
a = (True, False)
s = False
```

The problem here is that the lenses *overlap*, so the views may not be modified independently.

Conversely, `pairLens l l'`

is well-behaved if `l :: Lens s a`

and `l' :: Lens s a'`

are well-behaved and **non-overlapping**, i.e., if for all `s`

, `a`

and `a'`

, putting one view does not affect the other:

```
get l (put l' a' s) == get l s
get l' (put l a s) == get l' s
```

We actually only need one equality to hold to ensure the good behavior of `pairLens l l'`

, but determining which one (here, the second) relies on a careful examination of the order of updates in `pair`

.

## Detecting conflicts

Given two lenses `l :: Lens s a`

and `l' :: Lens s a'`

, possibly overlapping, and some source `s`

, we say that a pair `(a, a')`

is a **consistent update** of `s`

through `l`

and `l'`

if:

```
get l (put l' a' s) == get l s
get l' (put l a s) == get l' s
```

Two lenses are non-overlapping if and only if all updates through them are consistent.

For more flexibility, we shall allow ourselves to create partial lenses, which allow updates of overlapping views as long as they are consistent (actually, with a generalized definition of consistency).

We can “record observations” in order to forbid inconsistent modifications as in *Applicative Bidirectional Programming with Lenses*^{1}, using a more elaborate `MLensW2`

type.

```
newtype MLensW2 s a = MLensW2
runMLensW2 :: s -> (s -> Bool) -> Maybe (s, s -> Bool, a)
{
}
instance Functor (MLensW2 s) where
fmap = liftA
instance Applicative (MLensW2 s) where
pure a = MLensW2 $ \s p -> Just (s, p, a)
<*>) = ap
(
instance Monad (MLensW2 s) where
MLensW2 x_ >>= f = MLensW2 $ \s p -> do
s', p', x) <- x_ s p
(s'', p'', y) <- runMLensW2 (f x) s' p'
(return (s'', p'', y)
```

`MLensW2`

is a composition of `State (s, s -> Bool)`

and `Maybe`

.

`sourceW`

fetches the `s`

component of the state.

```
sourceW :: MLensW2 s s
sourceW = MLensW2 $ \s p -> pure (s, p, s)
```

`putW`

updates the source through a partial lens. `putW`

is unsafe to use alone in general, with the risk of defining ill-behaved lenses. However, careful and fine grained use of `putW`

can help optimize composite lenses by avoiding redundant checks.

```
-- PLens' defined below.
putW :: PLens' s a -> a -> MLensW2 s ()
putW l a = MLensW2 $ \s p -> do
s' <- put l a s
pure (s', p, ())
```

`assertW`

checks that the updated source is consistent with previous observations and modifications.

```
assertW :: MLensW2 s ()
assertW = MLensW2 $ \s p ->
guard (p s) $> (s, p, ())
```

`matchW`

adds a another consistency constraint preventing a view of the source to be modified.

```
matchW :: Eq w => (s -> w) -> w -> MLensW2 s ()
matchW get w = MLensW2 $ \s p ->
pure (s, \s' -> p s' && get s' == w, ())
```

We have an isomorphism between `MLens2`

and lenses with a partial `put`

.

```
type MLens2 s = Codec (MLensR s) (MLensW2 s)
type PLens' s a = Lens s (Maybe s) a a
fromLens2 :: Eq a => PLens' s a -> MLens2 s a a
fromLens2 l = Codec
get l)
(a -> putW l a *> assertW *> matchW (get l) a $> a)
(\
toLens2 :: MLens2 s b a -> Lens s (Maybe s) a b
toLens2 (Codec get produce) = Lens get put
where
put b s = fmap fst3 (runMLensW2 (produce b) s (const True))
fst3 :: (a, b, c) -> a
fst3 (s, _, _) = s
```

We can also observe values in the source/state, without writing anything. Modifying a previously observed value is an error.

```
observe :: Eq w => (s -> w) -> MLens2 s () w
observe parse = Codec parse produce
where
produce () = observeW parse
observeW :: Eq w => (s -> w) -> MLensW2 s w
observeW get = do
s <- sourceW
let w = get s
matchW get w
pure w
```

A functor from lenses to functions serves as “vertical” composition.

```
lift :: Lens' s a -> MLens2 z s s -> MLens2 z a a
lift l (Codec parse produce) = Codec
get l . parse)
(a -> do
(\z <- sourceW
let s = parse z
produce (put l a s)
pure a
)
-- A generalized version, though less efficient.
lift_ :: Lens s t a b -> MLens2 z t s -> MLens2 z b a
lift_ l (Codec parse produce) = Codec
get l . parse)
(b -> do
(\z <- sourceW
let s = parse z
s <- produce (put l b s)
pure (get l s)
)
```

*Applicative Bidirectional Programming with Lenses*, K. Matsuda, M. Wang. https://kar.kent.ac.uk/49084↩︎