List Functor

Stream: lean4

[Henrik Böving]

I was writing some code that tried to map on a list haskell style like:

def foo : List Nat := [1,2,3,4,5,6,7]

def bar : List Nat := (λ x => x + 1) <$> foo

and my Lean complains that List has no Functor instance? Is this correct? If so why doesn't it have one it seems like a rather trivial instance to me.

[Mac]

@Henrik Böving The Functor/Applicative/Monad classes in Lean are considered control flow classes for control types like OptionM/ExceptM/etc. Data types (like Option/Except/List) do not implement them (to prevent them two from being confused). This allows for much better type inference and predictable behavior in the do notation.

[Mac]

There is a decent argument, though, that Functor should not be included in this (or there should be a data version), since map is used quote often in pure programming..

[Henrik Böving]

The regular Option type does already seem to implement Functor: https://github.com/leanprover/lean4/blob/master/src/Init/Data/Option/Basic.lean#L43-L44 so I guess it would be valid to just do it for List as well in this case?

[cognivore]

Mac said:

Henrik Böving The Functor/Applicative/Monad classes in Lean are considered control flow classes for control types like OptionM/ExceptM/etc. Data types (like Option/Except/List) do not implement them (to prevent the two from being confused). This allows for much better type inference and predictable behavior in the do notation.

My 2c: List Option is a great model for a continuation-passing-style computation.

One of the bigger "patterns" in ML-style FP is the pattern of describing a computation in one place (and in composable manner) and running it in another. List is a great, albeit a little bit primitive, way to describe computations.

[Leonardo de Moura]

Henrik Böving said:

The regular Option type does already seem to implement Functor: https://github.com/leanprover/lean4/blob/master/src/Init/Data/Option/Basic.lean#L43-L44 so I guess it would be valid to just do it for List as well in this case?

Yes, Option implements Monad at master. OptionM is gone. See discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
Regarding Monad List, it would be great to have more feedback from our user base because Lean is a strict language.

[Leonardo de Moura]

@Henrik Böving Regarding Functor List, please feel free to submit a PR.

[Henrik Böving]

https://github.com/leanprover/lean4/pull/1338/files

[Siddhartha Gadgil]

Leonardo de Moura said:

Henrik Böving said:

The regular Option type does already seem to implement Functor: https://github.com/leanprover/lean4/blob/master/src/Init/Data/Option/Basic.lean#L43-L44 so I guess it would be valid to just do it for List as well in this case?

Yes, Option implements Monad at master. OptionM is gone. See discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
Regarding Monad List, it would be great to have more feedback from our user base because Lean is a strict language.

The one advantage of having Monad List (as with Monad Option) is that this is a familiar type and gives a very good example of Monads for a mathematical audience for whom meta-programming examples may be too complex (and encoding effects may seem artificial).

I am just saying this as an argument in one direction -- arguments the other way may be stronger.

[Mario Carneiro]

The issue with Monad List is not that List isn't a monad / acts as an example monad, but rather that it has completely different strictness behavior than it does in e.g. Haskell which makes it unsuitable for use as a "nondeterminism" monad

[Mario Carneiro]

and giving it a monad structure could result in unexpected results for folks expecting the haskell behavior

[Gabriel Ebner]

rather that it has completely different strictness behavior than it does in e.g. Haskell

I'm not sure I understand this part. The only time the strictness differs is if you only look at, say, the first element (head (do { x <- [1..10^10]; pure (x+1) })). That doesn't work in Lean because the resulting list is evaluated strictly, like every other list in Lean. If you do println do ... then both Haskell and Lean behave the same AFAICT.

[Siddhartha Gadgil]

Mario Carneiro said:

The issue with Monad List is not that List isn't a monad / acts as an example monad, but rather that it has completely different strictness behavior than it does in e.g. Haskell which makes it unsuitable for use as a "nondeterminism" monad

One can safely assume that those who "expect Haskell behaviour" are rather skilled. On the other hand mathematicians knowing not much programming can use a simple example of a Monad.

[Mario Carneiro]

@Gabriel Ebner I think the order of evaluation of the bind functions is also different, although possibly this is not observable since we would only be able to use non-monadic functions in this situation

[Gabriel Ebner]

Okay, that seems plausible. But "does the same pure computations only in an unexpected order" is a rather weak argument against Monad List though.

[Gabriel Ebner]

In my eyes, the only good argument against Monad List and Monad Array is that they have subpar performance (compared to Monad DList and Monad DArray). But that is also true of the Haskell version if you don't have stream fusion.

[Kyle Miller]

One reason for Monad List is that it's the basis for list comprehensions, which many strict languages (like Python) have. Python for example also has generator comprehensions for the lazy version, so it's possible for practitioners to be able to handle strictness issues.

[Sebastian Ullrich]

It uses separate syntax for both cases though. So that's not an argument for List satisfying a generic abstraction.

[Kyle Miller]

That's true, but what I meant is that you could choose to use Monad LazyList when you want a lazy version, which is vaguely similar to choosing to use square brackets or parentheses in Python.

[Kyle Miller]

It'd fair having a separate class for comprehensions (and specialized syntax to go with it) instead of using Monad.

[Sebastian Ullrich]

To move the discussion forward, it would probably help to provide specific use cases where Monad List would be useful

[Joe Hendrix]

Gabriel Ebner said:

If you do println do ... then both Haskell and Lean behave the same AFAICT.

From my experience, it's not exactly out of order evaluation, but rather that intermediate lists will be computed and stored in memory prior to invoking println. I remember at one point naively translating some Haskell List monad code to Lean and immediately hitting out-of-memory issues.

That said, I think Monad List is a good idea in Lean. I don't have a particular use case in mind at the moment, but it's just nice to be able to generate and transform lists using do notation.

[Mario Carneiro]

I have made use of Monad List for unit tests. (Monad Array is essentially the same but I feel like the strict semantics are more expected in that context.) I think that the "unusual" evaluation order may be a paper cut, but I think it's worthwhile to have despite this, and we should just teach people to use LazyList if they want the haskell style nondeterminism monad

[Mario Carneiro]

Stuff like this:

#eval do
  a ← list.range 5,
  b ← list.range 5,
  let a : ℤ := a - 2,
  let b : ℤ := b - 2,
  guard ¬ (a % b < int.nat_abs b),
  pure (a, b)
-- [(0, 0), (1, 0), (2, 0)]

[Mac]

One confusion I have always had with Monad List is that there are actually a variety of monad-like operations (not all of which are lawful) that can be defined on aggregate types like List -- list comprehension is just one of them. So having there be a specific Monad List instance strikes me as off.

[Mac]

For instance, one can define the monad function seq : (fs : List (a -> b)) -> (as : List a) -> List b to be such that bs[i] = fs[i] a[i].

[James Gallicchio]

I think list comprehension is the instance most people want most of the time, which is why it's become a common language feature elsewhere

Also, isn't there a slick way to specify a monad instance at the call site? List comprehension can be the typeclass instance, and I don't think that severely inhibits people using other monad instances on lists

[Mac]

Personally, I have found most list comprehension code I have seen to be completely incomprehensible. The special syntax most languages have for it doesn't help readability (as it tends to aim for conciseness rather intuitiveness). And this coming from someone who likes the functional paradigm (and, in some places, considers it more intuitive than its imperative equivalent), which is already stigmatized in CS as been difficulty to understand.

For instance, it took me a number of re-reads of Mario's example to figure out what it was doing and how it got the answer it got.

[Mac]

However, I guess that is all just matter of taste and not really a relevant objective criticism of Monad List.

[James Gallicchio]

I agree to some extent... scala's for syntax always felt more comprehensible to my brain because it triggered my "iteration is happening" senses :joy:

[Patrick Massot]

I don't know about Haskell or Scala, but list comprehension in python is wonderful and very readable. I'd love to have that in Lean.

[Mac]

Patrick Massot said:

but list comprehension in python is wonderful and very readable.

Sadly, I disagree. I am acclimatized to the CS for were the order is for x in iterable do expression and Python putting the expression first in its list comprehensions always throws me off. However, the ordering in Python is more like math where {x i in S s.t. expression} is the natural order so I can understand why others (especially mathematicians) would find it intuitive.

[Patrick Massot]

I know you disagree, this is why I wrote my message bringing a different perspective.

[Mac]

@Patrick Massot Oh, sorry! How did you know that? I did not mention Python in my original critique?

[Patrick Massot]

I've noticed for a very long time that your programming taste is orthogonal to python and mathematics :wink:

[Mac]

Ah, fair enough. :rofl: That may be a bit extreme though, I did originally find Lean by looking for a theorem prover to try some mathematical proofs. :smile:

[Mac]

Though, I guess that could count as the point/line were the two orthogonal lines/planes cross.

[Patrick Massot]

Right now I'm writing Lean 4 code where I really wish I could use a python list comprehension

[Arthur Paulino]

I believe you can get away with some macro expansion for that

[Kyle Miller]

Indeed you can:

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)]

[Mac]

For example:

syntax "[" term:max " for " term " in " term (" if " term)? "]" : term
macro_rules
| `([$a for $x in $xs]) => `($xs |>.map fun $x => $a)
| `([$a for $x in $xs if $c]) => `($xs |>.filterMap fun $x => if $c then some $a else none)

#eval [(x * 2) for x in List.range 5] -- [0, 2, 4, 6, 8]
#eval [(x - 1) for x in #[1,2,3,4,5] if x % 2 = 0] -- #[1, 3]

[Mac]

@Kyle Miller you literally posted that while I was pasting my example into the comment box. :laughing:

[Kyle Miller]

I learned from yours that if you use term instead of ident that you can do pattern matching in the for clause. That's neat

[Kyle Miller]

For sake of example:

def List.prod (xs : List α) (ys : List β) : List (α × β) := [(x, y) | for x in xs, for y in ys]

#eval [x * y | for (x, y) in List.prod (List.range 3) (List.range 3)]
-- [0, 0, 0, 0, 1, 2, 0, 2, 4]

[Mac]

Or, using the already defined List.zip :smile: :

#eval [(x * y) for (x, y) in List.zip (List.range 3) (List.range 3)]
-- [0, 0, 0, 0, 1, 2, 0, 2, 4]; edit: actually [0, 1, 4]

[Kyle Miller]

I'm getting different output with List.zip:

#eval [x * y | for (x, y) in List.zip (List.range 3) (List.range 3)]
-- [0, 1, 4]

That's using the "diagonal monad" you mentioned earlier.

[Mac]

You are correct, sorry.

[Kyle Miller]

@Mac Still, that got me thinking, why not make list comprehension even more baffling and allow it to do zips too?

For example,

def List.zip' (xs : List α) (ys : List β) : List (α × β) :=
  [(x, y) | Δ for x in xs, for y in ys]
  -- Delta temporarily switches to using the diagonal monad instead of the usual list monad

#eval List.zip' [1,2,3] [4,5,6,7]
-- [(1, 4), (2, 5), (3, 6)]

Code:

declare_syntax_cat compClause
syntax "for " term " in " term : compClause
syntax "if " term : compClause
syntax "Δ" compClause : compClause

syntax "[" term " | " compClause,* "]" : term

def List.diag (xss : List (List α)) : List α :=
  match xss with
  | [] => []
  | []::_ => []
  | (x::_)::xss => x :: List.diag (List.map (· |>.tailD []) xss)
termination_by _ => xss.length

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.diag [[$t | $cs,*] | $c]) -- warning, inefficient
  | `([$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)]

def List.prod (xs : List α) (ys : List β) : List (α × β) :=
  [(x, y) | for x in xs, for y in ys]

#eval [x * y | for (x, y) in List.prod (List.range 3) (List.range 3)]
-- [0, 0, 0, 0, 1, 2, 0, 2, 4]

[Mario Carneiro]

FYI lean will do zips using the notation for x in xs, y in ys do so I guess you could just leave off the second for?

[Mario Carneiro]

it's kind of evil though

[Patrick Massot]

I missed those messages during the night, it's great!

[Juan Pablo Romero]

My 2 cents: when more than one List/Collection is involved, Scala's for-comprehension is much easier to read than Python's:

  for
    x <- List.range(0, 5)
    y <- List.range(0, 5)
    if x + y <= 3
  yield (x, y)

[Patrick Massot]

I still prefer python's version by far.

[Kyle Miller]

Oftentimes it seems like list comprehensions could be more flexible (which is a point against the List monad). Mathematica has Reap and Sow for setting up a comprehension and collecting values. Here's a Lean 4 version of that for collecting an Array:

abbrev CollectM (α : Type _) := StateM (Array α)

def sow (x : α) : CollectM α Unit := modify (· |>.push x)

def reap (m : CollectM α Unit) : Array α := (m.run #[]).2

#eval reap do
  for x in [0:5] do
    for y in [0:5] do
      if x + y <= 3 then
        sow (x, y)
-- #[(0, 0), (0, 1), (0, 2), (0, 3), (1, 0), (1, 1), (1, 2), (2, 0), (2, 1), (3, 0)]

[Sebastian Ullrich]

Is that just an eager special case of iterator generators with yield?

[Kyle Miller]

Yeah, it's basically eager Python/Javascript-style (anonymous) generator functions.

[Kyle Miller]

The Mathematica version of this is wilder since it somehow attaches to the global continuation, so any function can Sow.

[Sebastian Ullrich]

I just hope we don't use these exact names because I would not be able to use them with a straight face without thinking of https://twitter.com/screaminbutcalm/status/1105577845642878976?lang=en

Me sowing: Haha fuck yeah!!! Yes!! Me reaping: Well this fucking sucks. What the fuck.

- The Golden Sir (@screaminbutcalm)

[Mac]

@Sebastian Ullrich That seems like a point in favor of using those terms, no? :stuck_out_tongue_wink:

[François G. Dorais]

I don't have a horse in this race but, if I recall correctly, ListT monad transformer is ill-behaved with strict lists (but the List monad by itself is fine with strictness). It would be unusual if the list monad were significantly different from ListT Id.

[François G. Dorais]

(Of course, this is not a problem if neither ListM nor ListT exist.)

[Chris Lovett]

For another data point on this excellent discussion I also love Python list comprehensions, and I was looking for it the other day, until I found Kyle's awesome implementation here. But I have also thought of these as only useful on very concise list comprehensions and I move to the more powerful "yield pattern" (which I also love in C#) where you can write a huge function to compute what you are yielding and inject yield statements in various places to turn your entire function into an iterator. So I've always thought of the yield iterator as a more powerful version and it's nice to have both. So I like the yield keyword better than sow and with yield in C# you don't need to reap. In fact, you don't want to build that Array in memory since the whole point is to be able to operate on infinite streams efficiently, like pulling transformed rows out of a database and returning them as Json over HTTP, with minimal memory footprint, etc.

[James Gallicchio]

Kyle Miller said:

Oftentimes it seems like list comprehensions could be more flexible (which is a point against the List monad). Mathematica has Reap and Sow for setting up a comprehension and collecting values. Here's a Lean 4 version of that for collecting an Array:

This also can generalize nicely -- my collection library has a generalization for any collection that can be built up one element at a time, so CollectM can be defined over any result collection and a nice syntax could be added.

It seems like python's for comprehensions connect the two (distinct & dual) notions, iterating over a collection vs building one up

We already have a generalization for iterating over a collection (ForIn), so I think it best to add a notion for building one up (Enumerable), add instances for List and Array, and add some pythonic syntax behind an import for those that want it

[Mario Carneiro]

Here's an implementation of the nondeterminism monad which uses continuation passing style to avoid creating lots of intermediate arrays:

def ArrayM (κ α) := (α → Array κ → Array κ) → Array κ → Array κ

instance : Monad (ArrayM κ) where
  pure a k := k a
  bind f g k := f (g · k)

instance : MonadLift List (ArrayM κ) where
  monadLift l k := l.foldl (fun r a => k a r)
instance : MonadLift Array (ArrayM κ) where
  monadLift l k := l.foldl (fun r a => k a r)

def ArrayM.run (x : ArrayM α α) : Array α :=
  x (fun a r => r.push a) #[]

#eval ArrayM.run do
  let a ← [1, 2, 3]
  let b ← #[1, 2, 3]
  return 10 * a + b
-- #[11, 12, 13, 21, 22, 23, 31, 32, 33]

[James Gallicchio]

Is there an application in Lean where you'd want an eager nondeterminism monad implementation?

It would seem reasonable to me to have an explicit Nondet monad with a choose : [ToStream α ρ] -> ρ -> Nondet α operation, and some eliminators for it

[James Gallicchio]

You mentioned you used Monad List in tests, is there a file that has some examples?

[Mario Carneiro]

Using a ToStream instance is a bit weird, since that introduces a dependency between the various nondet branches

[James Gallicchio]

Yeah, I'm not sure what the right class is there. But some class that exposes external iteration.

[James Gallicchio]

(or do you mean a type dependency? I'm not sure I understand what you mean)

[Mario Carneiro]

I mean that the various branches can't be executed independently, you need to hold on to the iterator state

[Chris Lovett]

I ran into this using the Kyle's List Comprehension syntax extension mentioned above:

def vec : List Int := [-4, -2, 0, 2, 4]
-- filter the list to exclude negative numbers
#eval [x | for x in vec, if x >= 0]
-- [0, 2, 4]

which errors:

application type mismatch
  List.map (fun x => if x ≥ 0 then [x] else []) vec
argument
  vec
has type
  List Int : Type
but is expected to have type
  List Nat : Type

To fix it I have to coerce the 0 to an int using #eval [x | for x in vec, if x >= (0: Int)].

So my question, is whether the Lean syntax extensions can improve how type inference happens? I would imagine that since vec is a List Int, then Lean should know that x must be an Int, therefore the 0 must be an Int also ?

[Henrik Böving]

Yes you can do this with a custom elaborator that forces x to be elaborated with a for List a but not just with a simple macro.

[Kyle Miller]

@Chris Lovett This is an elaboration order issue.

If you define

def List.map' (xs : List α) (f : α → β) : List β := List.map f xs

then alter the macro_rules to instead have

  | `([$t:term | for $x in $xs]) => `(List.map' $xs (λ $x => $t))

then your example works without the type ascription.

[Kyle Miller]

My understanding of what is going on is that the elaborator elaborates arguments in order, so while it elaborates the function argument to List.map it doesn't yet know the type of the argument to the function since it hasn't visited the list argument yet. Reversing the order of the arguments to List.map is sufficient in this case.

[Chris Lovett]

wow, thanks!

[Chris Lovett]

Unfortunately it doesn't work:

declare_syntax_cat compClause
syntax "for " term " in " term : compClause
syntax "if " term : compClause

syntax "[" term " | " compClause,* "]" : term

def List.map' (xs : List α) (f : α → β) : List β := List.map f xs

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])

def vec : List Int := [-4, -2, 0, 2, 4]
#eval [x | for x in vec, if x >= 0]

And it also breaks def List.prod (xs : List α) (ys : List β) : List (α × β) := [(x, y) | for x in xs, for y in ys]

[Kyle Miller]

Make sure to change the order of the arguments to List.map' in the macro_rules too

[Chris Lovett]

Doh! thanks.

[Chris Lovett]

So @Kyle Miller I turned your solution into a new Lean sample because I think it's a really great example of Lean syntax extension. See https://github.com/leanprover/lean4-samples/pull/10, let me know there if you have any comments or suggestions, thanks.

[Sebastian Ullrich]

Kyle Miller said:

Chris Lovett This is an elaboration order issue.

If you define

def List.map' (xs : List α) (f : α → β) : List β := List.map f xs

then alter the macro_rules to instead have

  | `([$t:term | for $x in $xs]) => `(List.map' $xs (λ $x => $t))

then your example works without the type ascription.

This has been fixed in https://github.com/leanprover/lean4/commit/d3b0b49c432e9e2ca7c6dd6017fbed074ff1ccb6

[Chris Lovett]

Thanks @Sebastian Ullrich I removed List.map' from the new sample at https://github.com/leanprover/lean4-samples/tree/main/ListComprehension and everything works.