Suppose that k is a pure lens, and

s <- extRef r k a0.

The following laws should hold:

• s is a pure reference.
• (k . s) behaves exactly as r.
• The initial value of s is the result of (readRef r >>= setL k a0).

Moreover, (extRef r k a0) should not change the value of r.

The following two operations should be identical:

newRew x

extRef unitLens unitLens x

For examples, see Control.MLens.ExtRef.Pure.Test.

Undo-redo state transformation