Writer should use an additive monoid

Stream: mathlib4

[Shreyas Srinivas]

Hi all, Thanks to some downstream discussions in #CSLib I discovered that mathlib's WriterT uses a Monoid instance on its log type. I have made a PR to fix this to AddMonoid. Here is the PR : mathlib4#35578

Arguments in favour of this change:

1. This is the actual intended meaning of the Writer monad. Haskell uses Monoid because it makes no distinction between AddMonoid and Monoid. The writer monad is supposed to act like a log. So for instance it might be collecting a list of log-records, the natural writer monad operation is to concatenate to this list, not take element-wise pairs. It might be counting events, in which case the count needs to be increased additively.
2. This change only affects one other file in mathlib, the ContT monad, which I have naturally fixed in the PR.
3. It would be super useful in cslib#275 to handle cost functions as well as replace the so-called Time monad which is just a writer monad in disguise.

[Shreyas Srinivas]

CC : @Eric Wieser

[Shreyas Srinivas]

I'd be very grateful if we could reach a fast consensus on this, since it would potentially help us kickstart formalizing algorithms in cslib soon.

[Eric Wieser]

Relatedly I wonder if we should remove the duplication for EmptyCollection/Zero, and force users who want to use List X as their log type to use Free(Add)Monoid X instead

[Eric Wieser]

the natural writer monad operation is to concatenate to this list, not take element-wise pairs

Neither * nor + mean concatenate in Lean, so this argument doesn't seem to favor either Monoid or AddMonoid. Unless of course you use Free(Add)Monoid, and then both mean concatenate!

[Shreyas Srinivas]

Yeah, but morally it is an addition operation. The choice of notation ++ is close enough

[Eric Wieser]

The best argument I can see to prefer Monoid is that the log concatenation is typically non-commutative, and in mathematics we prefer to use * instead of + when the operation is non-commutative.

[Shreyas Srinivas]

Yes, but as I pointed out in the PR comment, we actually have a separate class for that AddCommMonoid, which indicates that non-commutative uses of + have already been anticipated

[Eric Wieser]

But I do see the appeal in using + for convenience for CSLib, and in the absence of any other users it seems harmless enough to change it.

[Eric Wieser]

A perhaps more conservative approach would be to define AddWriterT and use to_additive to manage the duplication

[Shreyas Srinivas]

Given that writer is currently hardly used anywhere is Mathlib, I think we should let the default writer be additive and create a MulWriter if necessary

[Christian Merten]

https://ncatlab.org/nlab/show/action+monad uses multiplicative monoids in the first part and switches to additive notation in section 5 when discussing the "logging-effect in computer science".

[Snir Broshi]

Shreyas Srinivas said:

3. It would be super useful in cslib#275 to handle cost functions as well as replace the so-called Time monad which is just a writer monad in disguise.

I don't know the details about either monad, but can't CSLib do TimeM := WriterT <| Multiplicative ℕ? (or TimeM := WriterT <| Multiplicative T after Eric's latest change)

[Shreyas Srinivas]

It’s tedious and and tbh writer monads have a default meaning in CS. They w is additive.

[Snir Broshi]

What, how is a single line more tedious than a monad definition from scratch?

[Shreyas Srinivas]

Every monoid property or theorm has to be applied with toMultiplicative

[Shreyas Srinivas]

And as I point out the moral definition is additive. The change is not huge. This monad is not even being used in mathlib beyond the Cont monad

[Shreyas Srinivas]

I honestly don’t even see why this is controversial. Even ncatlab prefers the name Action monad for the multiplicative version.

[Shreyas Srinivas]

Even the documentation for this module refers to the Haskell definition and there the primary usage is definitely with additive operations.

[Snir Broshi]

Shreyas Srinivas said:

I honestly don’t even see why this is controversial

To be clear: I do not have an opinion on the Mathlib change, I suggested a way to unblock CSLib

[Shreyas Srinivas]

I think merging this PR soon would be a great help in simplifying CSLib. It seems to be practically a neglected leaf node as far as mathlib goes.

[Jovan Gerbscheid]

Why don't we just move the WriterT definition to CSLib altogether, and let them do with it what they want? To me the writer monad seems hardly useful when you can use a state monad instead.

[Shreyas Srinivas]

@Eric Wieser : given the sparse API for writer I am inclined to take this option as a practical route but with a change: I’ll copy WriterT as AddWriterT into a CSLib for now.

[Shreyas Srinivas]

Fwiw I think writerT should still be fixed here and StateT is not a replacement for WriterT. However I need to make progress faster than we can reach consensus here.

[Shreyas Srinivas]

I view this "port" as a stopgap

[Eric Wieser]

I’ll copy WriterT as AddWriterT into a CSLib for now.

I'd be inclined to keep it as TimeM until we need the generality

[Shreyas Srinivas]

I am really keen to avoid the TimeM dependency. Anyway, an additive writer monad is essential CS material. We can have something in Cslib until mathlib's slow process catches up

[Eric Wieser]

Shreyas Srinivas said:

Anyway, an additive writer monad is essential CS material

According to haskell, only the ++/empty version is CS material. I'm not sure where the "CS is +, Math is *" divide is coming from here.

[Shreyas Srinivas]

I am referring to this ncatlab entry on the action monad which Christian cited

[Shreyas Srinivas]

That seems to be some pure math stuff

[Shreyas Srinivas]

https://github.com/leanprover/cslib/pull/360

[Shreyas Srinivas]

Christian Merten said:

https://ncatlab.org/nlab/show/action+monad uses multiplicative monoids in the first part and switches to additive notation in section 5 when discussing the "logging-effect in computer science".

See this

[Shreyas Srinivas]

Anyway this thread should continue to be about WriterT being multiplicative by default, and whether it should be additive by default or whether there's some other way to allow both Monoid and AddMonoid versions.

[Christian Merten]

Eric Wieser said:

A perhaps more conservative approach would be to define AddWriterT and use to_additive to manage the duplication

This seems to be the best solution to me.

[Chris Henson]

Just seeing this thread, thanks for linking from the CSLib PR, Eric. From the discussion above, the to_additive approach seems nice in providing either choice. Regarding this comment:

Shreyas Srinivas said:

We can have something in Cslib until mathlib's slow process catches up

This feels a bit premature for a PR opened just today, and I don't want to leap to duplicating anything downstream. (I also think this could be communicated a bit more graciously)

[Michael Rothgang]

The discussion here could equally be described as deliberate (as opposed to slow). This is not about a week-long delay where this PR is completely unnoticed.

[Shreyas Srinivas]

Okay I accept that I have been hasty. Apologies. But I do think it helps to have some additive version of the writer monad while we discuss mathlib’s API

[Shreyas Srinivas]

Also @Michael Rothgang this is not just about the discussion here. A PR can take several weeks to reach the first page of the review queue

[Michael Rothgang]

Shreyas Srinivas said:

Also Michael Rothgang this is not just about the discussion here. A PR can take several weeks to reach the first page of the review queue

I know (and agree that faster reviews would be great - the mathlib initiative has already made perceptable inroads to me). That said, a lot of this comes down to "are there reviewers for this particular area". It doesn't make sense for e.g. me to review deep category theory or t-computability. Complaining about slow reviews is easy (and still justified to some extent), changing this is harder :-)

[Chris Henson]

Also it is not as if CSLib is immune to this, we just have the luxury of smaller scale for the time being. The areas where I am truly comfortable reviewing are lambda calculi metatheory and metaprogramming. Anything else is me mainly addressing technical issues and pushes at the limits of both my competency and time constraints. I've gratefully accepted help from Eric and others in areas that are on the border between Mathlib and CSLib, and we will have our own growing pains of bootstrapping the expansion of CSLib reviewers/maintainers.

[Shreyas Srinivas]

Accepted. For what it’s worth, I found that the docstring linter is stricter in CSLib than mathlib. Is this something that is expected?

[Chris Henson]

Shreyas Srinivas said:

Accepted. For what it’s worth, I found that the docstring linter is stricter in CSLib than mathlib. Is this something that is expected?

I don't have permission to move messages from here, but we should take discussion to the CSLib channel to keep on topic. But to answer your question, you mean the docBlameenvironment linter? We inherit this from batteries, so it should work the same.

[Jovan Gerbscheid]

Maybe you are talking about the set_option linter.missingDocs true linter? This one is off in mathlib, and on in batteries. This is the syntax linter, not the environment linter. I wonder why there is this discrepancy between mathlib and batteries.

[Shreyas Srinivas]

No idea, but mathlib’s WriterT passes all linters clearly while in cslib#360, I had to add more docstrings. They are nearly identical.

[Michael Rothgang]

What kind of linter errors did you get? Yellow squiggles as you were writing code, or errors when typing #lint/in the "lint cslib" step of CI? (If the later, it's an environment linter.)

[Shreyas Srinivas]

lake lint

[Shreyas Srinivas]

And CI

[Michael Rothgang]

lake lint AFAICT does lake exe runLinter, which runs environment linters.

[Chris Henson]

In CSLib we have lintDriver = "batteries/runLinter" in our lakefile, while in Mathlib lake exe runLinter is run in CI. Is there some difference?

[Chris Henson]

Oh, Mathlib's scripts/nolints.json has several docBlame exceptions for WriterT, pretty sure that's it.