[2pEXgD0fZ5cF]

Does Lean have something similar to Haskell's List comprehension [1] or some kind of set builder notation for functional programming purposes?

[1]: Example: `[x*2 | x <- [1..10]]`

[eric-wieser]

It has the following which means the same as what you wrote:

    do let x ← List.range' 1 10; return x^2

The syntax is flexible enough that you could build your own:

    macro "[" r:term "|" preamble:doElem "]" : term => `(do 
    $preamble; return $r)

    #eval [x^2 | let x ← List.range' 1 10]

[kmill]

Here's an extensible one I wrote a while back for just List, but I haven't tested it in a while:

    declare_syntax_cat compClause
    syntax "for " term " in " term : compClause
    syntax "if " term : compClause
    
    syntax "[" term " | " compClause,* "]" : term
    
    macro_rules
      | `([$t:term |]) => `([$t])
      | `([$t:term | for $x in $xs]) => `(List.map (λ $x => $t) $xs)
      | `([$t:term | if $x]) => `(if $x then [$t] else [])
      | `([$t:term | $c, $cs,*]) => `(List.join [[$t | $cs,*] | $c])
    
    #eval [x+1| for x in [1,2,3]]
    -- [2, 3, 4]
    #eval [4 | if 1 < 0]
    -- []
    #eval [4 | if 1 < 3]
    -- [4]
    #eval [(x, y) | for x in List.range 5, for y in List.range 5, if x + y <= 3]
    -- [(0, 0), (0, 1), (0, 2), (0, 3), (1, 0), (1, 1), (1, 2), (2, 0), (2, 1), (3, 0)]

(Your doElem idea is a good one though)

[2pEXgD0fZ5cF]

Huh that is really cool! Thanks for the example!

[ykonstant]

Surely you can define such notation, but why? The following is just as clear and concise, and does not rely on any extensions:

    (. * 2) <$> [1,2,3]

For example:

    def byTwo (inputList : List Nat) :=
      (. * 2) <$> inputList

    #eval byTwo [1, 2, 3]
    -- [2, 4, 6]

[2pEXgD0fZ5cF]

> but why?

Why not? I was curious, Haskell is the functional language I know. Lean is the language I do not know.

Since Lean leans even heavier towards mathematics, set builder style notation seems like a natural fit. Now whether or not such notation is actually needed or worth it, that is a whole different question.

[kmill]

That's not exactly clear to mathematicians, who tend to complain about the "ascii art operators".

I think you'll usually see

    def byTwo (inputList : List.Nat) := inputList.map (. \* 2)

rather than using `<$>`. There's also `inputList |>.map (. * 2)`, but I haven't seen it in any mathlib theory code yet, just Lean core or in metaprogramming.

[skavi]

never understood the appeal of this syntax over standard do notation or just fmap.

[nequo]

List comprehensions read like math which we know from school. Do notation reads like Haskell which is fine but less accessible to non-Haskellers. Fmap is somewhat less convenient for slightly more complex examples such as

  [x*y | x <- [1..10], y <- [2,3,5]]

[sullyj3]

For that you'd use Applicative

  (*) <$> [1..10] <*> [2,3,5]
  -- or
  liftA2 (*) [1..10] [2,3,5]

Admittedly also not accessible to non-haskellers. But on the other hand, if you're going to learn a language, you ought to learn its idioms at some point.

[ykonstant]

That being said, nequo's request is not unreasonable; given Lean's advanced metaprogramming facilities, their request should be easy to implement.

The nice thing nequo's example illustrates is rank polymorphism: list comprehensions work with lists, products of two, three, four,... lists with the same easy notation : `[n-ary function | x_1 <- List_1, ..., x_n <- List_n]`. It is quite nice to have this, especially for complex numerical operations.

Note also that unlike Lean 3, in Lean 4 `List` does not inherently implement `Applicative` or `Monad`, so your code cannot work as is.

[eric-wieser]

Mathlib4 provides a `Monad List` instance, which you can see at https://leanprover-community.github.io/mathlib4_docs/Mathlib...

[aseipp]

Haskell has always been a language where there are many ways to skin any particular cat, for reasons from ergonomics to expressiveness to theoretical niceness or practicality. "Learn the idioms" has nothing to do with it. Why didn't you just use do-notation instead, for example, than write some applicative mess where it isn't needed?

It's not rocket science why someone would ask this. I don't always use list comprehensions. But sometimes I do. They have open arity and the syntax doesn't as often require things like parenthesis to handle fixity conflicts between other (non-applicative) operators. They are asking about list comprehensions, just because they think it's nice. It is a very simple question and talking about applicative is irrelevant.

[kmill]

That's perfectly fine Haskell, but I wouldn't say that using Applicative is much of a Lean idiom. Especially in the mathlib, people prefer using custom notation that looks like math notation or using the underlying functions directly rather than by using generic point-free notations. For example, you'll see `⨆ i, s i` for a supremum across the values of `s`, vs a point-free version.