Humble lenses

Problem 1

Here's how Lens.humble List.head (::) stacks up against the different laws:

The text statement of the law doesn't really match the lens: "If a set replaces an element, a later get will return the new element." (::) doesn't replace. But if we look at the test, it's clearer what the law actually means. Here's what the test does, shown in the repl:
```
> import Lens.Try3.Lens as Lens
> lens = Lens.humble List.head (::)
> Lens.set lens 3 []
[3] : List number
> Lens.get lens [3]
Just 3 : Maybe number
```
get does indeed "reverse" set, so the law is obeyed.
"If the lens gets a value, then sets it back, the result is equal to the original whole". No:
```
> Lens.get lens [3]
Just 3 : Maybe number
> Lens.set lens 3 [3]
[3,3] : List number
```
Because the lens doesn't actually replace an element, but always adds a new one, no possible set can return the original value.

"The results of one set cannot be detected once another set has been done." No, for the same reason:

> step1 = Lens.set lens "I'll be erased" []
["I'll be erased"] : List String
> Lens.set lens "No, you won't" step1
["No, you won't","I'll be erased"] : List String

"If get returns Nothing, set does not change the whole and get still returns Nothing." Here's the only whole for which get will return Nothing:
```
> Lens.get lens []
Nothing : Maybe a
```
Here's setting that whole:
```
> new = Lens.set lens "something" []
["something"] : List String
```
The whole is changed. (And get will return Just "something".)

Problem 2

Full source

We need to replace (::) with something that only replaces the head of the list (instead of adding a new element). There are two cases: the empty list (in which case there's nothing to replace) and all other lists. That means a case in the code:

lens : Lens.Humble (List val) val
lens =
  let 
    set small big =
      case big of
        [] ->
          big
        _ :: xs -> 
          small :: xs
  in
    Lens.humble List.head set

Problem 3

Full source

In a Classic lens, get always returns a value, so we can just wrap that value in Just. Because a lens can only focus on an existing value, there's no need to worry about the "humble" case where the lens should decline to upsert. That leaves this:

classicToHumble : Classic big small -> Humble big small
classicToHumble (Tagged lens) = 
  humble (lens.get >> Just) lens.set

Because a Classic lens can't return a Nothing, we don't have to worry about the fourth Humble law. The first three laws are the same as the Classic laws, just with the value of get wrapped in a Just. Since that's what the classicToHumble code does, obedience to the Humble laws follows from the converted lens's obedience to the Classic laws.

Upsert and Humble lenses both return a Nothing under the same circumstances, and a Just under the same circumstances. So get doesn't need to be modified.

The difference between Upsert and Humble lies in what they do when get would return a Nothing. The Upsert lens adds a new value (so get will now return a Just), whereas the Humble lens leaves the whole unchanged. That means a case on get:

upsertToHumble : Upsert big small -> Humble big small
upsertToHumble (Tagged lens) =
  let
    set small big =
      case lens.get big of
        Nothing ->
          big
        Just _ ->
          lens.set (Just small) big 
  in
    Lens.humble lens.get set

The first three laws hold because they hold for an Upsert lens. The fourth law holds because the Nothing case does what it requires.

Problem 4

For each of the two lenses, there are two possibilities: get returns Nothing or get returns Just. Let's look at each of the possibilities for the composed lens:

a2b returns Nothing / b2c never used

The composed lens's get returns Nothing. That means the fourth law holds. Its set makes no change. That means the fourth law is obeyed.
a2b returns Just / b2c returns Nothing

The composed lens's get returns Nothing. That means (as above) that its set should make no change. The relevant case contains: a2b.set (b2c.set c b) a. Because b2c.get b would return Nothing, b2c.set c b will leave b unchanged. Therefore, a2b.set will be setting b back to its original value, which leaves the entire structure unchanged.
a2b returns Just / b2c returns Just

The composed lens's get returns what b2c returns.

set requires a little more explanation. Here's the relevant code:
```
set newC a =
   case a2b.get a of
     Just b ->
       a2b.set (b2c.set newC b) a
```
We can throw away the case paraphernalia because we know we're in the case where both lens's gets return a Just. Let's write it like this:
```
let
  Just b = a2b.get a 
in
  a2b.set (b2c.set newC b) a 
```
We can do some reverse substitution, introducing a name for b2c.set newC b:
```
let
  Just b = a2b.get a 
  newB = b2c.set newC b
in
  a2b.set newB a 
```
We now have names for all the intermediate values. That given, let's consider what the first lens law requires:
```
a2c.get (a2c.set newC a)
```
We can replace a2c.get with its definition (for this Just/Just case):
```
a2b.get (a2b.set newB a) |> b2c.get
```
Because a2b obeys the Humble lens laws, we know that the left-hand side of the pipeline can be replaced like this:
```
newB |> b2c.get
```
Replacing newB with the expression that calculates it, we get:
```
b2c.set newC b |> b2c.get
```
Since b2c is law-abiding, the previous expression simplifies to newC. That shows that a2b obeys the first lens law.

Q.E.D.

The second lens law supposes that a2c.get returns a value we'll call Just c. So let's look at setting that value:
```
a2c.set c a
```
We know that activates this code:
```
let 
  Just b = a2b.get a 
  newB = b2c.set newC b
```
But, in this case, newC is the existing value c. Because b2c obeys the lens laws, newB must be equal to b. Which means a2b will be used like this:
```
a2b.set b a
```
By the lens laws, that's the same as a.

Q.E.D.

The third law can be shown in a similar way. Let's start with this scenario:
```
a2c.set newerC (a2c.set newC a)
```
Let's expand the inner a2c.set by substitution and variable-creation:
```
let
  newB = b2c.set newC b
  newA = a2b.set newB a
in 
  a2c.set newerC newA
```
And do the same for the a2c.set on the last line:
```
let
  newB = b2c.set newC b
  newA = a2b.set newB a
  newerB = b2c.set newerC newB
in 
  a2b.set newerB newA
```
Our goal is to show that newC and newB have no effect on the final result. Let's substitute it into the definition of newerB:
```
let
  newB = b2c.set newC b
  newA = a2b.set newB a
  newerB = b2c.set newerC (b2c.set newC b) --- 
in 
  a2b.set newerB newA
```
The newerB line now matches the third law, which means that newC can have no effect. So that line can be simplified:
```
let
  newB = b2c.set newC b
  newA = a2b.set newB a
  newerB = b2c.set newerC               b  --- 
in 
  a2b.set newerB newA
```
Now let's substitute newA's value for its use in the last line:
```
let
  newB = b2c.set newC b
  newA = a2b.set newB a
  newerB = b2c.set newerC b
in 
  a2b.set newerB (a2b.set newB a)  ----
```
We have another match for the third law, which we know a2b obeys. So we can again simplify it:
```
let
  newB = b2c.set newC b
  newA = a2b.set newB a
  newerB = b2c.set newerC b
in 
  a2b.set newerB               a   ----
```
Notice that the name newA is unused and that newB is only used in newA. So they can be removed:
```
let
  newerB = b2c.set newerC b
in 
  a2b.set newerB a
```
Notice that newC is now entirely unused when evaluating the original expression:
```
a2c.set newerC (a2c.set newC a)
```
... which is what the third law requires.

Q.E.D.

Problem 5

We can do the conversion in three steps:

Add link to HumbleAndHumble.png in /images

So we get to reuse functions we already wrote:

upsertAndClassic : Upsert a b -> Classic b c -> Humble a c
upsertAndClassic a2b b2c =
  humbleAndHumble
    (upsertToHumble a2b)
    (classicToHumble b2c)

Problem 6

It is possible to produce an Upsert. The get for both Upsert and Humble lenses returns a Maybe small. There is no problem with set taking a Maybe small and either inserting a new element or deleting one. That's because the change is made at the end of the path (adding or deleting a leaf node in the structure). Or: given that you're setting a Just small, there's no need to "invent" any values as you would if upsertAndClassic returned an Upsert lens:

lens = upsertAndClassic (Dict.lens "key") Tuple2.second  -- suppose this returned an `Upsert` lens
Lens.set lens (Just 5) Dict.empty                        -- What's the value of the tuple's first element

So here's the implementation:

classicAndUpsert : Classic a b -> Upsert b c -> Upsert a c
classicAndUpsert (Tagged a2b) (Tagged b2c) =
  let
    set small big =
      a2b.set (a2b.get big |> b2c.set small) big
  in
    Lens.upsert2 (a2b.get >> b2c.get) set

The body of that function is in fact the same as that of classicAndClassic except that the latter uses Lens.classic instead of Lens.upsert2. Recall how we worked our way to an Upsert lens:

We had Classic get, set, and update behavior.
They worked fine for a Dict lens.
The didn't work when a Dict lens was composed with an Upsert lens. The types aren't compatible, and there's no way to set work sensibly.
So we needed a new Humble lens type that doesn't upsert or delete.
That meant we had to distinguish between Classic and Upsert lenses: without different types, how would we signify that sometimes composing two lenses produces a Humble lens.
But get, set, and update are implemented by the same code in Upsert as in Classic. It's only the types that have to change. (In a way I think of this as like tagged types: division works the same for Hours as for Liters, but the types are used both to constrain the values to divide and also to produce result types that make sense for potential further computations.)
We've now seen that the compose function can also have the same implementation for the two types.

Problem 7

My solution -- and extensions to it -- are described in the book.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Humble lenses

Clone this wiki locally