Haskell-like Lazy Lists?

Stream: new members

[Agnishom Chattopadhyay]

I am trying to create a lazy-list like [1..] in Haskell. But the following does not seem to work:

def startFrom (start : ℕ) : LazyList ℕ :=
  LazyList.cons start  $ Thunk.pure (startFrom (start + 1))

I see that there is an LazyList.iterate function, but it is marked as unsafe. Is there a non-unsafe way to represent lazy lists in Lean?

[Markus Schmaus]

I'm also pretty new to Lean, but this is what I found out so far. There are ways to represent structures similar to lazy lists, but they all have significant drawbacks.

First, there is Stream, which is an efficient representation of infinite lazy lists, but there are barely any functions implemented for it, and it's a type class rather than a type. Second, there is also Stream', which is a type and has many more helper functions and theorems, but it's only a theoretical model for proofing theorems and results in very inefficient computation. There is an open PR which aims at making Stream' more efficient, so I'm hoping this is going to improve the situation significantly. Third, of course there is also LazyList, which you have already seen.

What I've done so far is to use Stream or a custom type very similar to it and implemented the functions I needed myself.

[Kyle Miller]

@Agnishom Chattopadhyay You're getting a "failure to prove termination" error there since the function does not terminate in the strong sense that Lean wants (imagine if it took an eager evaluation strategy and evaluated everything under Thunk.pure ahead of time).

You can get it to work at runtime by using the unsafe modifier:

unsafe def startFrom (start : ℕ) : LazyList ℕ :=
  LazyList.cons start $ Thunk.pure (startFrom (start + 1))

You won't be able to prove anything about the definition, but at least you can use it in programs.

[Kyle Miller]

(You could give it the partial modifier, but I'm under the impression you should only use it if you know the definition generates valid values, but I'm not really sure. Infinite LazyLists are not valid values of the LazyList inductive type.)

[Kyle Miller]

My understanding of the issue is that Lean has inductive types but no coinductive types, which is what you need to properly represent a LazyList. There are ways of simulating LazyLists with inductive types, but LazyList instead uses unsafe to circumvent the assumption that the lists are finite.

[Agnishom Chattopadhyay]

So, there is no official way to represent co-inductive structures like Stream, right?

[Marcus Rossel]

Agnishom Chattopadhyay said:

So, there is no official way to represent co-inductive structures like Stream, right?

I think that's right, but you may find QpfTypes useful.

[Agnishom Chattopadhyay]

Quotients of Polynomial Functors? Do they mean "Final Co-Algebras of Polynomial Functors"?

[Markus Schmaus]

Yes, and quotients of such final Co-Algebras. The thread Stream' is inefficient might be interesting to you. Based on this I don't think the QpfTypes library addresses the computational inefficiency.

[Agnishom Chattopadhyay]

Oh, thanks! I like the quotation I don't think you should be deciding "should lean get coinductive types" by a poll haha