Zulip Chat Archive

Stream: mathlib4

Topic: List and monads


Wrenna Robson (Oct 26 2022 at 16:10):

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 (Oct 26 2022 at 16:27):

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 (Oct 26 2022 at 22:17):

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

Wrenna Robson (Oct 27 2022 at 09:16):

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


Last updated: Dec 20 2023 at 11:08 UTC