Monad List

Stream: mathlib4

[Reid Barton]

mathlib4#966 added a global Monad List instance. I think that's fine for now, and certainly won't cause any problems for the port, but given that the core library intentionally removed this instance, maybe we want to consider whether we should do something less "opinionated", such as making it a scoped instance.

[Yaël Dillies]

Why did core remove it, exactly?

[Henrik Böving]

There are two discussions about this in #lean4, the baseline is that a Lean 4 List is not lazy so it can have unexpected computational consequences. There are people who believe this is bad, others who believe this is just right etc.

[Reid Barton]

I think the reasoning was that for programming purposes, List is not a very good implementation of a nondeterminism monad (though in my opinion, it's still useful in sufficiently trivial situations).

[Yaël Dillies]

Ah I see. So this is irrelevant for most of mathlib.

[Johan Commelin]

I suggest we make a clear issue about this, and return to it after the port is done.

[Reid Barton]

Hypothetically, if we go along with core's decision, it seems easy enough to make it scoped to MonadList or something, and opt in to it explicitly in the few places in mathlib where we use it or prove theorems about it

[Johan Commelin]

Until then, I don't expect too many projects that will depend on a half-ported mathlib and be bitten by this issue. If you do fall in that category: I'm sorry and tough luck.

[Arien Malec]

When I looked at MList in the past it was only used for tactics FWIW.

[Mario Carneiro]

I think it makes sense to just add the instance in mathlib4 in this case. Mathlib4 needs backward compatibility, std doesn't

[Mario Carneiro]

I think it's also reasonable to add it to core, despite the performance pitfalls

[Mario Carneiro]

It's just a bit jarring to see it missing if you are coming from e.g. haskell