PutPut Setter law redundant?

[tomjaguarpaw]

The documentation says a Setter has two laws

• PutPut: Setting twice is the same as setting once:

  set l v' (set l v s) ≡ set l v' s
  

• Functoriality: Setters must preserve identities and composition:

  over s id ≡ id
  over s f . over s g ≡ over s (f . g)
  

But set o = over o . const so automatically we have

set l v' (set l v s)
≡ (over l . const) v' (set l v s)
≡ over l (const v' (set l v s)
≡ over l v'
≡ over l (const v' s)
≡ (over l . const) v' s
≡ set l v' s

Is the PutPut law actually needed at all?

[phadej]

Note, that for lenses they are equivalent. Lens laws are usually stated in terms of PutPut.

over o f x = set o (f (get o x) x)
==>

over o f (over o g x)
= over o f (set o (g (get o x) x))
= set o (f (get o (set o (g (get o x) x))) (set o (g (get o x) x))  
            ^^^^^^^^^^ GetPut
= set o (f (g (get o x) x) (set o (g (get o x) x))
  ^^^-----------------------^^^ PutPut
= set o (f (g (get o x) x) x)
= over o (f . g) x

Setters are not Lens though.

We could add a note that PutPut is implied by Functoriality but we shouldn't completely remove it: Lens is a Setter + compatible Getter.

Otherwise there would be a question: Why there are no common laws shared by Setter and Lens?

I also have a gut feeling that it's impossible to fulfill PutPut and OverId (over o id = id) but violate OverComp, Can you find a counterexample?

[adamgundry]

Yes, just as we have the "fundamental" and "additional" introduction/elimination forms, we could have the "fundamental" laws of setters be the functor conditions, and explain that PutPut follows from this (and conversely that the functor conditions follow from the lens laws). In general the Haddocks for laws are a bit weak at the moment; I'll try to find an opportunity to improve them soon.