feat: additive writer monad

[Shreyas4991]

This PR adds a writer monad whose log type is additive. This fills a gap in the mathlib API whose writer monad treats the log as multiplicative, which is a mistake as far as computer science is concerned.

Reference

• "As logging-effect in computer science"

[eric-wieser]

which is a mistake as far as computer science is concerned.

Citation needed. Computer science does not make the Monoid/AddMonoid distinction made by mathlib; and in fact haskell's monoid system makes you use Writer (Sum X) and Writer (Product X) to choose between + and * as the accumulation operator (instead of the default of ++)

There is a zulip discussion #mathlib4 > Writer should use an additive monoid @ 💬. If CSLib reviewers have an opinion, I'd propose they leave it there rather than encouraging duplication into cslib.

[Shreyas4991]

Extra reference: https://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf