Why List Monad is in mathlib and not in core ?

Stream: Is there code for X?

[Alfredo Moreira-Rosa]

I was wondering why List don't have an instance of Monad in core.
I'm sure this has already been asked, but i couldn't find an answer in zulip history.
Is it to evoid misunderstanding when using do notation ?

[Henrik Böving]

You're looking for #general > question: why List is nolonger Monad? @ 💬

[Alfredo Moreira-Rosa]

Thanks, so mainly for perf issues with do notation.

[cmlsharp]

I haven’t given it much thought concretely but would it be possible to create an Iterator monad?

[cmlsharp]

Or rather, not just “is it possible” but “would that be desirable”

It feels like the internal iterator state being part of the type might make it not possible though

[Jakub Nowak]

cmlsharp said:

I haven’t given it much thought concretely but would it be possible to create an Iterator monad?

That could be nice. Kinda like generator functions in python or c++.

[cmlsharp]

Yeah exactly, or the list monad in Haskell (iterators are basically just lazy lists)