Zulip Chat Archive

Hi all. I'm trying out this language again (tried it out for a bit 6 months ago maybe), and it seems very cool and powerful, but there are points of confusion for me. Could someone please clarify whether the List monad is a thing in Lean4? I was surprised the following code didn't work.

I appreciate it.

def addLists (xs: List Nat) (ys: List Nat) : List Nat := do
  let x <- xs
  let y <- ys
  [x + y]

Asei Inoue (Mar 29 2025 at 13:04):

return x + y doesn’t work?

Aaron Liu (Mar 29 2025 at 13:18):

You have to import the list monad first

Aaron Liu (Mar 29 2025 at 13:18):

It lives in file#Data/List/Monad

misterdrgn (Mar 29 2025 at 13:25):

@Aaron Liu Ah ok, that's what I needed. Thanks.

misterdrgn (Mar 30 2025 at 01:26):

@Aaron Liu Actually I have a follow-up question, if you don't mind and you have some experience with monads in Lean. After following your suggestion, the following works for me.

#eval do
  let x <- [1, 2 ,3]
  let y <- [7, 8, 9]
  guard (x > 1)
  return (x, y)

However, the following does not work.

#eval do
  let x <- [1, 2 ,3]
  let y <- [7, 8, 9]
  guard (x > 1)
  [(1,1)]
  return (x, y)

I would _guess_ (I could test it) that that would work in Haskell, and would produce a list where the (x,y) pairs alternate with (1,1). However, I might simply be confused. The reason I think this should work is that in the IO monad, when writing a do statement, you can have lines like stdout.putStrLn ... that don't involve the bind operator--they simply add another line to the IO monad. I'm assuming these lines are combined with mplus from the MonadPlus or Monoid type class. In Lean, maybe this doesn't work because List isn't made an instance of MonadPlus?

Or maybe I'm totally confused.

Kyle Miller (Mar 30 2025 at 01:38):

Maybe it will work if you write discard [(1, 1)].

Matt Diamond (Mar 30 2025 at 01:40):

https://play.haskell.org/saved/6DzZEYhY

Matt Diamond (Mar 30 2025 at 01:44):

in Haskell it just ignores the (1, 1)

Joscha Mennicken (Mar 30 2025 at 01:44):

Isn't a line without <- roughly equivalent to one with _ <-, i.e. discarding the bound variable, and the IO monad can be thought of as a state monad (where printing modifies the state) whereas the list monad has no state?

Joscha Mennicken (Mar 30 2025 at 01:46):

Thus you could write, for example, [0, 0, 0] in a line on its own to repeat each item in the resulting list three times, but if you don't bind it, the values in the list are just ignored.

Joscha Mennicken (Mar 30 2025 at 01:47):

https://play.haskell.org/saved/UMU6jszb

Mario Carneiro (Mar 30 2025 at 01:50):

Joscha Mennicken said:

Isn't a line without <- roughly equivalent to one with _ <-, i.e. discarding the bound variable, and the IO monad can be thought of as a state monad (where printing modifies the state) whereas the list monad has no state?

no, it's more like let () <-

Mario Carneiro (Mar 30 2025 at 01:51):

so it discards but it also enforces the type of the discarded thing is unit

Mario Carneiro (Mar 30 2025 at 01:52):

But if you did _ <- [(1,1)] it wouldn't put (1,1) in the result because it isn't used subsequently. You would need the MonadPlus operation, not bind, to do this

Mario Carneiro (Mar 30 2025 at 01:53):

I think the lean spelling for that operation is <|>

Matt Diamond (Mar 30 2025 at 01:54):

I think there's still a question here of why the code resulted in an error in Lean, even if it wouldn't have accomplished what misterdrgn wanted

Matt Diamond (Mar 30 2025 at 01:56):

but yeah, the result makes total sense when you consider that List bind is just flatMap

Joscha Mennicken (Mar 30 2025 at 01:58):

Mario Carneiro said:

no, it's more like let () <-

The error is that the list elements must be units but are instead tuples, unlike Haskell, where the list elements are just ignored no matter their type.

Matt Diamond (Mar 30 2025 at 01:58):

ah ha

Joscha Mennicken (Mar 30 2025 at 02:04):

For completeness, the lean language reference says this:

A term followed by a sequence of items is translated to a use of bind; in particular, do e1; es is translated to e1 >>= fun () => do es.

misterdrgn (Mar 30 2025 at 02:19):

Thanks everyone and especially @Mario Carneiro. I understand things somewhat better now. The issue with my broken code wasn't that I left out the let something <-. In fact, the following works.

#eval do
  let x <- [1, 2 ,3]
  let y <- [7, 8, 9]
  guard (x > 1)
  [6, 7, 8]
  return (x, y)

Here, [6,7,8] becomes let () <- [6,7,8], which means that those numbers are discarded, but the results are repeated three times, once for each item in that list.

So if that works, why does [(1,1)] fail? I guess I'm still not 100% clear on this...