Additive writer monad

Stream: CSLib

[Shreyas Srinivas]

I have started a PR cslib#360 to give us a proper writer monad whose log type is additive. This makes up for the lack of a proper WriterT since Mathlib's version uses a multiplicative log type.

[Shreyas Srinivas]

I'd like to get this PR through so that @Eric Wieser can use it to golf cslib#275 per his preference without introducing an unnecessary dependency on TimeM