A
Lens is actually a lens family as described in
http://comonad.com/reader/2012/mirrored-lenses/.
With great power comes great responsibility and a
Lens is
subject to the three common sense
Lens laws:
1) You get back what you put in:
view l (set l v s) ≡ v
2) Putting back what you got doesn't change anything:
set l (view l s) s ≡ s
3) Setting twice is the same as setting once:
set l v' (set l v s) ≡ set l v' s
These laws are strong enough that the 4 type parameters of a
Lens cannot vary fully independently. For more on how they
interact, read the "Why is it a Lens Family?" section of
http://comonad.com/reader/2012/mirrored-lenses/.
There are some emergent properties of these laws:
1)
set l s must be injective for every
s This
is a consequence of law #1
2)
set l must be surjective, because of law #2, which
indicates that it is possible to obtain any
v from some
s such that
set s v = s
3) Given just the first two laws you can prove a weaker form of law #3
where the values
v that you are setting match:
set l v (set l v s) ≡ set l v s
Every
Lens can be used directly as a
Setter or
Traversal.
You can also use a
Lens for
Getting as if it were a
Fold or
Getter.
Since every
Lens is a valid
Traversal, the
Traversal laws are required of any
Lens you create:
l pure ≡ pure
fmap (l f) . l g ≡ getCompose . l (Compose . fmap f . g)
type Lens s t a b = forall f. Functor f => LensLike f s t a b