iteration documentation?

Stream: new members

[JJ]

Hello! Where can I find information on Lean's iteration primitives? I have been working through Functional Programming in Lean, but (unsurprisingly) it doesn't seem to cover this.

I've also been having trouble knowing where to look when trying to understand language features in general... is there a standard place to look besides the FP in Lean / Theorem Proving in Lean books and the Core.lean and Prelude.lean files? I have not had very good luck with the manual. Most of the pages I was hoping to find information in have been empty.

[Mario Carneiro]

lean doesn't really have iteration primitives per se, but if you mean things accepted by the do notation it's basically for, while, and repeat, with the latter two desugared to a form of for

[Mario Carneiro]

the actual primitive from lean's perspective is (tail) recursion

[JJ]

oh yeah that's exactly what i'm looking for - where can i read about how they work?

[Mario Carneiro]

for desugars to an application of the docs#ForIn.forIn typeclass function, so data structures etc can implement that to define what iteration means for them

[JJ]

hmm okay ty

[JJ]

this is a bit dense, do you know if there is any documentation with more examples? i am struggling to follow the types a bit

[JJ]

(also i might as well ask - i'm writing a parser and was hoping to manually manipulate the iterator with something like .next() like in rust. are there existing abstractions for this, or is there a more idiomatic way to manipulate parser state, or is this doable/not doable?)

[Mario Carneiro]

The iteration implemented by ForIn is called "internal iteration", which means it is a higher order function where you give the body of the loop to it and it runs it on the elements yielded by the iterator in order. This is in contrast to "external iteration" in the style of rust, where the iterator has a function returning the next value of the iterator. Lean also has an external iteration typeclass, called docs#Stream, but it is not used as much

[Mario Carneiro]

One reason to prefer internal iteration style is that it is easier to verify termination that way

[Mario Carneiro]

but it is a less flexible model than external iteration, you can't just convert an internal iterator to an external iterator

[JJ]

oh neat ok! i think stream is what i'm looking for. does for while repeat work with it at all?

[Daniel Weber]

They should, thanks to docs#instForInOfStream

[Notification Bot]

JJ has marked this topic as resolved.

[JJ]

i have hit a couple of snags with iteration. reading Stream#instStreamList seems to suggest that List should implement the Stream class. but the following code fails to compile, due to not resolving List.next?:

def main : IO Unit := do
  let hello := "JJ"
  IO.println s!"Hello, {hello}!"
  let data : List Nat := [1, 2, 3, 4]
  for i in data do
    IO.println s!"{i}"
    let _ := data.next?

[Notification Bot]

JJ has marked this topic as unresolved.

[JJ]

also: i've noticed that next? returns Option (value × stream). is there a way to get around needing to shadow stream each time next? is called, perhaps with mutability?

[Mario Carneiro]

Unlike in rust, you can only use dot notation in lean when there is literally a function in the namespace (what you would call an inherent method in rust), not when there is a typeclass function (although in many cases the typeclass function will be defined to equal an inherent method with the expected name, so this can be confusing). To call the typeclass function you should use its name directly and without dot notation, as in Stream.next? data

[JJ]

oh! interesting. can i import the class / every class so i can use dot notation at all / always? (i really like dot notation :grinning:)

[Mario Carneiro]

You need to define List.next? if you want to use dot notation

[Mario Carneiro]

To use a stream with mutable variables, you need the following dance:

  let hello := "JJ"
  IO.println s!"Hello, {hello}!"
  let mut data : List Nat := [1, 2, 3, 4]
  repeat
    let some (i, data') := data.next? | break
    IO.println s!"{i}"
    data := data'

[Mario Carneiro]

in fact, List.next? already exists in Batteries: docs#List.next?

[JJ]

hmm. that's pretty rough. i guess it would be bad to implicitly have a mutable iterator though.

[JJ]

and i guess because mutation isn't first class you can't really define a next? to do that to begin with...

[JJ]

hmmmm. i guess i have some motivation for learning the macro system now :big_smile:

[Mario Carneiro]

You can do something more like first class mutation if you have a function with the type StateT (List A) (Option A)

[Kyle Miller]

Why are you calling next?? You can just do a for loop over the list:

def main : IO Unit := do
  let hello := "JJ"
  IO.println s!"Hello, {hello}!"
  let data : List Nat := [1, 2, 3, 4]
  for i in data do
    IO.println s!"{i}"

#eval main
/-
Hello, JJ!
1
2
3
4
-/

[JJ]

oh, i was calling next to get a sense of how iterators work! that would be a remarkably complicated list iteration haha

[JJ]

but i do actually want to call next explicitly because i'm writing a parser. being able to have an external while loop but skip iterations of it inline with .next() (and have helper functions ex. peek(&mut self): Option<T>, expect(&self, T): Option<Unit>, etc) has been super helpful in rust. the same pattern is maybe seeming more trouble than it's worth with lean's purity though...

[Mario Carneiro]

mutation using let mut is not really first class, do is an elaborate macro that desugars it to state passing

[Mario Carneiro]

I think if you have a state object you want to pass around and modify from several functions, you want to define a monad using StateT

[JJ]

oh yeah, i mean that rust has first class mutation... and its external iterators work well because next has the signature &mut Self -> Option<T>. so it can update the iterator in-place and not need to return a new iterator like Stream does

[JJ]

Mario Carneiro said:

I think if you have a state object you want to pass around and modify from several functions, you want to define a monad using StateT

i might try that once i understand lean a bit better... i think i understand how to (maybe) implement nice sugar for rust-style external iteration with macros, but monads are quite beyond me rn

[Mario Carneiro]

it's easier than writing macros to do the same thing, that's for sure

[Mario Carneiro]

The equivalent of the rust signature &mut Self -> Option<T> is StateM Self (Option T)