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 Control.Lens.Setter.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