### Undo does not imply PutPut

I have to conclude that my brain does very weird things at night while I sleep. The evidence I have consists of

(a) my math/programming productivity drops off rapidly if I get sleep-deprived

(b) I often wake up early in the morning with (not always correct, but potential) solutions to last night's problems almost fully formed

Sometimes they are solutions to problems I wasn't even particularly trying to solve.

For instance, I woke up this morning with my head full of thoughts about lenses for some reason. I hadn't really thought about them for months, but I went through the exercise of seeing that lenses with the GetPut and PutGet nicely form a category, but then tragically (and I think this is coming from some flashback to overhearing the tail end of an advisor meeting between Aaron Bohannon and Benjamin Pierce) that category is not obviously cartesian closed. I tried to think if there was any way of thinking about some sort of magic special pair type that would provide a monoidal closed structure together with lens-functions being the lolli, but I didn't get anywhere.

What did spool itself out of my brain after that point was an example located somewhere in the "Lens Bestiary" on slide 70 of the slides I linked above, that shows there's a property that is a slight (and strict!) weakening of the "forgetful" lenses. I did some searching later and found that other people have called this property "Undo", for example on page 10 of Algebra of bidirectional model synchronization.

A recap of basic lens stuff: a lens from A to B is a pair of functions

get : A → B

put : A x B → A

such that

get(put(a, b)) = b ("PutGet")

put(a, get(a)) = a ("GetPut")

A lens is a way of "viewing" a piece of data of type A as instead being type B --- this view being the "get" function --- that is sort of reversible, in that you can change the "view" and have those changes reflected back into the original data --- what you do is take your original data a, and the new b that you want, and give them to "put". The "PutGet" axiom says that if you put b in, you'll get b out, and "GetPut" says that if you put the unchanged view of a back in, it won't change anything.

"Forgetfulness" in the slides above (elsewhere called I think "PutPut"), is a further property that says if you do two puts, only the last one matters.

put(put(a, b1), b2) = put(a, b2) ("PutPut")

The weakening I had in mind was saying that if you do a put of some foreign data, and then a put of the original view B-data, you get back your original A-data:

put(put(a, b), get(a)) = a ("Undo")

A counterexample to show that this notion of "Undo" is actually strictly weaker than "forgetful" is as follows:

What's going on here? put's job is to force the new a to have the desired remainder mod 3. If it's already the same as b, leave it alone. If b is one more than a mod 3, we bump a up by one. If b is one less than a mod 3, we bump a down by one.

I imagine the natural number a to be like bead on a helical wire, spiraling up (and down!) to infinity, and b ∈ {0,1,2} is like a huge tall skinny magnet that I can move around the outside of the helix, pulling the bead towards it. If I just move the magnet back and forth, the bead will just move back to where it started, but if I move the magnet all the way around in one or more full revolutions around the helix, I can make the bead make progress up or down the wire.

For example I have:

put(put(put(0,1),2),0) = 3

but

put(put(0,1),0) = 0

So two puts aren't always the same as one put, (it fails PutPut) but a put immediately followed by a put of the original get does have no effect. (it has Undo)

(a) my math/programming productivity drops off rapidly if I get sleep-deprived

(b) I often wake up early in the morning with (not always correct, but potential) solutions to last night's problems almost fully formed

Sometimes they are solutions to problems I wasn't even particularly trying to solve.

For instance, I woke up this morning with my head full of thoughts about lenses for some reason. I hadn't really thought about them for months, but I went through the exercise of seeing that lenses with the GetPut and PutGet nicely form a category, but then tragically (and I think this is coming from some flashback to overhearing the tail end of an advisor meeting between Aaron Bohannon and Benjamin Pierce) that category is not obviously cartesian closed. I tried to think if there was any way of thinking about some sort of magic special pair type that would provide a monoidal closed structure together with lens-functions being the lolli, but I didn't get anywhere.

What did spool itself out of my brain after that point was an example located somewhere in the "Lens Bestiary" on slide 70 of the slides I linked above, that shows there's a property that is a slight (and strict!) weakening of the "forgetful" lenses. I did some searching later and found that other people have called this property "Undo", for example on page 10 of Algebra of bidirectional model synchronization.

A recap of basic lens stuff: a lens from A to B is a pair of functions

get : A → B

put : A x B → A

such that

get(put(a, b)) = b ("PutGet")

put(a, get(a)) = a ("GetPut")

A lens is a way of "viewing" a piece of data of type A as instead being type B --- this view being the "get" function --- that is sort of reversible, in that you can change the "view" and have those changes reflected back into the original data --- what you do is take your original data a, and the new b that you want, and give them to "put". The "PutGet" axiom says that if you put b in, you'll get b out, and "GetPut" says that if you put the unchanged view of a back in, it won't change anything.

"Forgetfulness" in the slides above (elsewhere called I think "PutPut"), is a further property that says if you do two puts, only the last one matters.

put(put(a, b1), b2) = put(a, b2) ("PutPut")

The weakening I had in mind was saying that if you do a put of some foreign data, and then a put of the original view B-data, you get back your original A-data:

put(put(a, b), get(a)) = a ("Undo")

A counterexample to show that this notion of "Undo" is actually strictly weaker than "forgetful" is as follows:

A = nat B = {0,1,2} get(a) = a mod 3 put(a, b) = case (b - a) mod 3 of 0 => a | 1 => a + 1 | 2 => a - 1

What's going on here? put's job is to force the new a to have the desired remainder mod 3. If it's already the same as b, leave it alone. If b is one more than a mod 3, we bump a up by one. If b is one less than a mod 3, we bump a down by one.

I imagine the natural number a to be like bead on a helical wire, spiraling up (and down!) to infinity, and b ∈ {0,1,2} is like a huge tall skinny magnet that I can move around the outside of the helix, pulling the bead towards it. If I just move the magnet back and forth, the bead will just move back to where it started, but if I move the magnet all the way around in one or more full revolutions around the helix, I can make the bead make progress up or down the wire.

put(put(put(0,1),2),0) = 3

but

put(put(0,1),0) = 0

So two puts aren't always the same as one put, (it fails PutPut) but a put immediately followed by a put of the original get does have no effect. (it has Undo)