Do notation for lists/arrays

Stream: new members

[Matei Adriel]

Coming from other fp languages, this seems like something I should be able to do, but lean tells me my goal (List Nat) is not a monad application. What am I doing wrong? Do I need to import something?

[Wojciech Nawrocki]

I am guessing this is about Lean 4. Could you briefly explain what you are trying to do? Are you trying to use the list monad which joins lists on >>=, or trying to do something with a list inside of a do-block whose type is another monad?

[Henrik Böving]

List is not a monad in lean4 on purpose. There is a thread about this somewhere in #lean4 but the bottom line was that people would expect it to be lazy and the default leean4 isn't

[Jason Rute]

Note there is still a for loop notation in Lean 4 as well as the usual map. But unlike say Scala, neither is not based on list monads (but the for loop notation does require being inside a do block of some monad, such as IO).

[Jason Rute]

I think #lean4 > List Functor might be the discussion.

[Jason Rute]

I’m curious about the lazy comment. Scala’s lists aren’t lazy as far as I can tell, but they have List (and other iterables) as a monad. Indeed for loop notation and do notation are identical (with them using for as the keyword). However, I haven’t read the full conversation to catch the details.

[Matei Adriel]

Henrik Böving said:

List is not a monad in lean4 on purpose. There is a thread about this somewhere in #lean4 but the bottom line was that people would expect it to be lazy and the default leean4 isn't

I for one never expected it to be lazy (I'm primarily coming from Purescript).

Wojciech Nawrocki said:

I am guessing this is about Lean 4. Could you briefly explain what you are trying to do? Are you trying to use the list monad which joins lists on >>=, or trying to do something with a list inside of a do-block whose type is another monad?

I was trying to basically implement List.inter myself (I couldn't find it because I was expecting the name to be List.intersection)

[Wojciech Nawrocki]

Matei Adriel said:

I was trying to basically implement List.inter myself (I couldn't find it because I was expecting the name to be List.intersection)

Okay, could you post the code you tried that gave you this error? It is hard to guess what you are trying without seeing it.

[Klaus Gy]

i stumbled across this as well... whats the most elegant way to do something resembling list comprehension in lean4? using map and implementing some sort of flat or concat?

[Kyle Miller]

@Klaus Gy It was just an experiment, but I once implemented list comprehensions: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/List.20Functor/near/290456697

[Kyle Miller]

It's just nice notation around docs#List.map and docs#List.join (so no need to implement join/flat/concat yourself)

[Kyle Miller]

There's also docs#List.bind, which you can use using notation like xs.bind f or xs |>.bind f

[Klaus Gy]

ah, nice! im a total newbie so i want to learn the basics without macros first :D but List.join is what i was looking for, i only searched for concat and flat, so thanks a lot!