List and monads

Stream: mathlib4

[Wrenna Robson]

I noticed in the Lean 4 documentation that List is no longer a monad. Is that "and can't be made one", or is it "and it isn't inherently but someone could add the monad structure on top"?

[Henrik Böving]

Sure you could make it a monad but the main point against this was that you would usually expect a lazy behaviour from a list based monad and our List is not lazy so the monad might do stuff you are not expecting at times and that's why it is not currently.

[James Gallicchio]

See also: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/List.20Functor

[Wrenna Robson]

Thanks Henrik and James - that's exactly the explanation I was looking for!