Should this be added to lean 4?

Stream: lean4

[Joseph O]

I would appreciate feedback or confirmation whether this would be useful to add to lean 4

[Arthur Paulino]

A way to know is when you end up needing the same piece of code in 2~3 different contexts.

Example: this is how HashMap.ofList was born:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/easy.20HashMap.20instantiation/near/267786491

[Chris B]

I think it's generally preferable for that kind of thing on ranges to be a stream/iterator and not a concrete list.

[Joseph O]

I have had my need for it. For instance, I don't about everyone else, but I rarely use for loops in lean, and I have had to use Ranges before, piping it into a lot of list methods. I was using List.range n, but recently learned about the range syntax, and needed a use case with stepping, so I was making a toList function, and I assume other people would find it useful too

[Joseph O]

Ranges in my opinion are meant to generate some sort of existing data structure, notably a list

[Joseph O]

HashMap even has a toList to allow easy manipulating.

[Joseph O]

I would prefer some more opinions before I decide.

[Mario Carneiro]

it might help to have actual examples of use

[Mario Carneiro]

Most mathlib additions are done because they are dependencies for some other work that either exists in another PR or will be PR'd soon. What's your application?

[Joseph O]

Mario Carneiro said:

Most mathlib additions are done because they are dependencies for some other work that either exists in another PR or will be PR'd soon. What's your application?

well this isnt for mathlib4 but lean4. Either way, my application is for usefulness

[Mario Carneiro]

that's not an answer

[Joseph O]

What is the point of having ranges, that cant be converted for lists. A use case could be working with mod systems, or primes, and filtering out ranges and numbers, which is what I was doing, and found the need for

[Mario Carneiro]

could you show a concrete example?

[Mario Carneiro]

like a piece of code that you would like to write, that can't be written easily now and would be better with your additions

[Mario Carneiro]

that's what I mean by an application

[Joseph O]

ok, give me a moment

[Joseph O]

very basic example

def foo :=
  [28:1000]
  |>.toList
  |>.map (fun n => [:n] |>.toList |>.filter (n % · = 0))
  |>.filter (·.length = 2)

i am unlikely this will convince you. If you want another better example, let me know

[Joseph O]

I will get an example with the step feature. But can I ask you something: What was the point of ranges when they can only be looped through, explain that to me. My idea may not be "useful", but the current version is even worse! barely any functionality!

[Henrik Böving]

I feel like the for x in [a:b] is an amazing functionality by itself already, sure it could be improved but it's already very useful when you are writing code in a more imperative style

[Joseph O]

Henrik Böving said:

I feel like the for x in [a:b] is an amazing functionality by itself already, sure it could be improved but it's already very useful when you are writing code in a more imperative style

How many people here write in an imperative style? Are we going to exclude functional style for ranges just because we feel like it?

[Joseph O]

You arent really giving good arguments

[Henrik Böving]

I've for example written code with for loops in doc-gen 4, besides I'm not making a point against extending the functionality, I'm merely making a point against "barely any functionality"

[Mario Carneiro]

One reason to prefer the for loop over the list operations, at least in current lean 4, is that the latter uses a lot more memory. For loops actually compile roughly to for loops, while list operations also compile to creating big linked lists and consuming them

[Mario Carneiro]

But that's not to say that we shouldn't have a Range.toList, that seems like a simple addition. I don't think you posted an implementation of this anywhere though

[Joseph O]

I can do that now if you want

[Mario Carneiro]

All of the other functions there exist already, right?

[Mario Carneiro]

You can write a toList function generic over Stream, although I think you can't prove it terminates in general

[Mario Carneiro]

it is a bit easier to translate to an array instead of a list, because you push to the end of an array

[Mario Carneiro]

plus arrays have just as much functional API as lists in lean 4

[Joseph O]

private def List.range' (start stop : Nat) :=
  List.drop start $ List.range stop

private def List.range'' (start stop : Nat) : Nat → List Nat
  | 1 => List.range' start stop
  | step => (List.range' start stop).filter (fun x => (x = 0) || (x % step = 0))

def toList : Range → List Nat
  | { start := m, stop := n, step := o} => List.range'' m n o

#eval [4:1000:5].toList

[Joseph O]

Mario Carneiro said:

All of the other functions there exist already, right?

not really

[Mario Carneiro]

Hm, if your step size is large then that creates a lot of elements. You can leverage the ForIn instance to construct the array for you:

def Std.Range.toArray (r : Std.Range) : Array Nat := Id.run do
  let mut arr := #[]
  for i in r do
    arr := arr.push i
  pure arr

def Std.Range.toList (r : Std.Range) : List Nat := r.toArray.toList

def foo : List (List Nat) :=
  [28:1000]
  |>.toList
  |>.map (fun n => [:n] |>.toList |>.filter (n % · = 0))
  |>.filter (·.length = 2)

[Joseph O]

I guess that makes sense

[Mario Carneiro]

Note that the indirection through arrays is deliberate. Even if you want to construct a list in the end, it's more efficient to construct the array first and tail-recursively convert it to a list at the end

[Joseph O]

I see

[Joseph O]

You might as well make the pr now.

[Mario Carneiro]

Here's another way to write the toArray function:

def Std.Range.toArray (r : Std.Range) : Array Nat :=
  Id.run <| r.forIn #[] fun i arr => ForInStep.yield (arr.push i)

[Mario Carneiro]

it's the same thing but without the do notation sugar

[Mario Carneiro]

This is a collaboration not a competition. This is still your PR, there is still documentation and examples, and maybe there are other streams that could also use toArray or toList functions

[Joseph O]

If you think this is useful to add, you can add it. I am not going to copy someone's code and claim it to be mine

[Mario Carneiro]

You do realize that most of mathlib's files have multiple authors, right?

[Joseph O]

Yes I do, but I didn't author anything here

[Mario Carneiro]

Sure you did, you came up with the idea and wrote a v1 implementation, which makes you first author by mathlib rules

[Mario Carneiro]

and like I said this isn't a PR yet

[Mario Carneiro]

this is a function

[Joseph O]

Hmm. So this will be added to mathlib not lean4?

[Mario Carneiro]

Yes, as you can see it works just as well if it's not in core

[Mario Carneiro]

lean 4 is designed to be extensible from outside the core distribution

[Mario Carneiro]

You also suggested a ToString and a Repr instance above. Can you use the s! macro to write that?

[Joseph O]

Mario Carneiro said:

You also suggested a ToString and a Repr instance above. Can you use the s! macro to write that?

I mean, the instances would have been simple

[Joseph O]

to write

[Mario Carneiro]

okay, then write them

[Mario Carneiro]

you have to start somewhere

[Mario Carneiro]

API design is more than you are giving credit for

[Mario Carneiro]

for instance, is it printed like [1, 3, 5, ..., 17] or [1 : 17 : 2] or [1:17:2]

[Mario Carneiro]

the function is easy to write, but there are bikeshedding issues everywhere you look

[Joseph O]

Mario Carneiro said:

for instance, is it printed like [1, 3, 5, ..., 17] or [1 : 17 : 2] or [1:17:2]

I was thinking [1:17:2]

[Mario Carneiro]

I think you're right. (It should look like the input syntax and have the same style, more or less.) Small PRs like that are generally uncontroversial, and will help you get practice for larger changes

[Joseph O]

Im having trouble with repr. I have a repr instance for my tuple type, and it takes a string, but this isnt workng

instance : Repr Range where
  reprPrec range := "[" ++ reprPrec range.start 0 ++ ":" ++ reprPrec range.stop 0 ++ ":" ++ reprPrec range.step 0 ++ "]"

[Joseph O]

(i tried using the s! macro, but that didnt work)

[Mario Carneiro]

is that a MWE? Because if so you are missing an open

[Joseph O]

Mario Carneiro said:

is that a MWE? Because if so you are missing an open

here is a MWE:

namespace Std

instance : Repr Range where
  reprPrec range := "[" ++ reprPrec range.start 0 ++ ":" ++ reprPrec range.stop 0 ++ ":" ++ reprPrec range.step 0 ++ "]"

end  Std

[Mario Carneiro]

If you write

namespace Std
instance : Repr Range where
  reprPrec range := _

and put your cursor over the _ you will see that it is expecting a Nat -> Format, which means it is expecting another argument

[Joseph O]

Ah, I got it

[Joseph O]

Should the s! macro work now?

[Joseph O]

Let me try

[Mario Carneiro]

the second argument is the precedence under which to display the expression by the way. Since this is a bracketed expression, it looks the same regardless of precedence so you can ignore it

[Joseph O]

Yeah, it does. Ok, it all works

[Mario Carneiro]

also, since it wants a Format and not a String you should use f! instead of s!

[Joseph O]

s! worked though

[Mario Carneiro]

Yaël Dillies said:

That makes a good motto: Code that compiles is not code that works.

[Joseph O]

And is it ok if I do

#eval [:17]

it evaluates that to [0:17:1], or should it just evaluate to [:17]

[Mario Carneiro]

I think it should print as [:17] if possible

[Joseph O]

Do you have an idea for a nice way of doing that. I would prefer some verbal context, as to try it out mainly myself, but I don't mind if you share code yourself.

[Mario Carneiro]

@Joseph O Do a pattern match on range, with cases for <0, stop, 1>, <0, stop, step>, <start, stop, 1>, <start, stop, step>

[Yakov Pechersky]

I think you're right. (It should look like the input syntax and have the same style, more or less.)

Is there a nice way in lean4 to prove that repr roundtrips?

[Joseph O]

Mario Carneiro said:

Joseph O Do a pattern match on range, with cases for <0, stop, 1>, <0, stop, step>, <start, stop, 1>, <start, stop, step>

ok

[Joseph O]

Should I make an auxiliary function to do that?

[Joseph O]

Mario Carneiro said:

Here's another way to write the toArray function:

def Std.Range.toArray (r : Std.Range) : Array Nat :=
  Id.run <| r.forIn #[] fun i arr => ForInStep.yield (arr.push i)

Does doing it this way provide any benefit?

[Joseph O]

Also, is there anywhere I can learn how to use generators like you used here in lean 4?

[Joseph O]

Is it ok to have to Pull requests open at the same time?

[Joseph O]

But are you sure something like this shouldn't be added to lean4 itself? Like, why was Hashmap.ofList deemed good enough to add to the core std, for instance?

[Arthur Paulino]

I don't think it's a matter of something being "good enough" or not. If something isn't good enough, it won't make it to mathlib either.

As I said in the issue, it's standard for programming languages to provide easy interfaces to instantiate their own versions of hash maps out of the box

[Siddhartha Gadgil]

Just a possibility (following scala design) - one can have a typeclass Seq α with a toArray field, with methods like Seq.toListimplemented using this. Also from Seq (α × Nat) we can generate a HashMap. Range should then have a Seq instance. I would be happy to make rough implementations for discussion.

Incidentally I also needed HashMap.fromList and HashMap.fromArray.

[Mac]

Joseph O said:

very basic example

def foo :=
  [28:1000]
  |>.toList
  |>.map (fun n => [:n] |>.toList |>.filter (n % · = 0))
  |>.filter (·.length = 2)

i am unlikely this will convince you. If you want another better example, let me know

You might find my WIP lean4-itertools library to be of interest. I was designed exactly to help do this kind of thing.

[Joseph O]

Arthur Paulino said:

I don't think it's a matter of something being "good enough" or not. If something isn't good enough, it won't make it to mathlib either.

As I said in the HashMap.ofList issue, it's standard for programming languages to provide easy interfaces to instantiate their own versions of hash maps out of the box

Converting ranges to lists are standard in languages as well, in fact, most ranges in langs are lists from the start, just written in shorter notation

[Joseph O]

Siddhartha Gadgil said:

Just a possibility (following scala design) - one can have a typeclass Seq α with a toArray field, with methods like Seq.toListimplemented using this. Also from Seq (α × Nat) we can generate a HashMap. Range should then have a Seq instance. I would be happy to make rough implementations for discussion.

Incidentally I also needed HashMap.fromList and HashMap.fromArray.

Interesting idea. This means that Seq (a x Nat) for example would have a method toArray and generate a hash map?

[Siddhartha Gadgil]

That is what I mean. Indeed one can have an instance of Seq a from an instance of ForIn at least with the correct parameters (I am struggling to understand what ForIn means in general, having only used it in imperative for loops).

[Joseph O]

I guess I should add it to mathlib4 for now and it may be added to the lean 4 std?

[Yakov Pechersky]

A range in python3 is surely not a list by default. Maybe we're talking past each other. Joseph, when you think about and mention lists, are you just referring to any datatype that has indexing, iteration, a length, appending, insertion, mutation at an index; or do you mean some particular implementation like a linked list, doubly linked list, indexed tree?

[Siddhartha Gadgil]

There are probably better ways in lean than the below, but this is what I meant.

universe u
class Iterable (l: Type u → Type u) where
  toArray : l α → Array α

instance : Iterable List :=
  ⟨fun l => l.toArray⟩

instance : Iterable Array :=
  ⟨fun l => l⟩

def mkArray [it : Iterable l] (l: l α): Array α :=
  it.toArray l

def mkList [it : Iterable l] (l: l α): List α :=
  (mkArray l).toList

open Std

def mkHashMap [it : Iterable l][Hashable α][BEq α][BEq β](l: l (α × β)): HashMap α β   :=
  (mkArray l).foldl (fun acc (k, v) => acc.insert k v) HashMap.empty

[Yakov Pechersky]

Probably you want mkList and mkHashMap to be fields in the structure that have default implementations, so that one can override. For example, a List's mkList shouldn't need to go through an Array and then to a List

[Siddhartha Gadgil]

Thanks @Yakov Pechersky I agree and this is something I am learning now.

[Mario Carneiro]

Siddhartha Gadgil said:

That is what I mean. Indeed one can have an instance of Seq a from an instance of ForIn at least with the correct parameters (I am struggling to understand what ForIn means in general, having only used it in imperative for loops).

A ForIn impl is nothing more or less than the natural requirement for desugaring for loops. You give it a monadic function which reports whether to update the state or early-return, and it folds the function over the data structure or iterable or what have you.

[Mario Carneiro]

It's a bit more general than "iterators" such as you would find in e.g. Rust, because it's not just a next function that gets called repeatedly, you get the loop body itself and can do funny business like reuse old state values or apply the function a transfinite number of times

[Yakov Pechersky]

So like a python generator but with more introspection?

[Mario Carneiro]

I don't think imperative languages without a monad abstraction can express this

[Mario Carneiro]

Python generators are generalized along a different axis, what with the yield point stuff

[Mario Carneiro]

I can imagine do notation gaining the ability to desugar yield expressions as well, but generators are not currently supported

[Joseph O]

Siddhartha Gadgil said:

There are probably better ways in lean than the below, but this is what I meant.

universe u
class Iterable (l: Type u → Type u) where
  toArray : l α → Array α

instance : Iterable List :=
  ⟨fun l => l.toArray⟩

instance : Iterable Array :=
  ⟨fun l => l⟩

def mkArray [it : Iterable l] (l: l α): Array α :=
  it.toArray l

def mkList [it : Iterable l] (l: l α): List α :=
  (mkArray l).toList

open Std

def mkHashMap [it : Iterable l][Hashable α][BEq α][BEq β](l: l (α × β)): HashMap α β   :=
  (mkArray l).foldl (fun acc (k, v) => acc.insert k v) HashMap.empty

This is pretty neat.

[Joseph O]

Yeah, and ranges are not usually lists by default. In F#, they are sequences

[Siddhartha Gadgil]

Thanks. But the above does not take care of Range, for which it has to be tweaked.
I'll take a shot at this.

[Mario Carneiro]

You can implement Iterable for anything with a suitable Stream or ForIn implementation

[Sebastian Ullrich]

Mario Carneiro said:

It's a bit more general than "iterators" such as you would find in e.g. Rust, because it's not just a next function that gets called repeatedly, you get the loop body itself and can do funny business like reuse old state values or apply the function a transfinite number of times

This is external vs. internal iteration. Internal iteration like ForM is relatively simple to set up and generate good code for, but limited in other regards - you cannot implement zip on two internal iterators, for example. I'd love to see a robust external iteration library for Lean in the future.

[Mario Carneiro]

Stream is external iteration, is it not?

[Sebastian Ullrich]

Hah yes, I forgot we already have it because it is so barebones and therefore barely used

[Sebastian Ullrich]

We would at least need a new typeclass for bounded streams if we want to make them as useful as ForM

[Joseph O]

Siddhartha Gadgil said:

Thanks. But the above does not take care of Range, for which it has to be tweaked.
I'll take a shot at this.

It shouldn't take to much tweaking

[Joseph O]

At least if I think about it

[Siddhartha Gadgil]

@Mario Carneiro but does Range have a suitable ForIn. A Range is only an Iterable Nat so if the only parameter of an Iterable is the type family I do not see an implementation.

[Sebastian Ullrich]

Mario Carneiro said:

Stream is external iteration, is it not?

There is also an interesting comparison to lazy lists, which have a very similar but simpler interface (which may or may not be a problem for code generation). The big difference is of course that lazy lists are provably finite if not defined coinductively. You can still make them infinite using partial, you just won't be able to prove anything about them.

[Siddhartha Gadgil]

Another take - this is getting more complicated, but includes Range. I am happy to learn how to simplify.

universe u
class Iterable (l: Type u)(α : Type u) where
  toArray : l  → Array α

class IterableFamily (l: Type u → Type u) where
  toArray : l α  → Array α

instance {l: Type u → Type u}[it : IterableFamily l] (α : Type u) : Iterable (l α) α :=
  ⟨fun x => it.toArray x⟩

instance : IterableFamily List    :=
  ⟨fun l => l.toArray⟩

instance : IterableFamily Array   :=
  ⟨fun l => l⟩

def mkArray {l: Type u → Type u}[it : Iterable (l α) α] (l: l α): Array α :=
  it.toArray l

def mkList {l: Type u → Type u}[it : Iterable (l α) α] (l: l α): List α :=
  (mkArray l).toList

def mkHashMap {l: Type u → Type u}{α β : Type u}
  [it : Iterable (l (α × β)) (α × β )][Hashable α][BEq α][BEq β](l: l (α × β)): HashMap α β   :=
    (mkArray l).foldl (fun acc (k, v) => acc.insert k v) HashMap.empty

def ForIn.toArray [ForIn Id l α](x : l): (Array α) := Id.run
  do
    let mut arr := Array.mk []
    for a in x do
      arr := arr.push a
    return arr

instance : Iterable Range Nat :=
  ⟨fun r => ForIn.toArray r⟩

[Joseph O]

interesting

[Joseph O]

Do you mind showing an example of using this to convert a Range to an Array of some sort?

[Arthur Paulino]

One thing I still haven't understood: if you want a list of numbers, why not make a function that creates one directly instead of instantiating a Range and then converting it into a list?

[Arthur Paulino]

The use of Range is too straightforward to me. It supports trivial iterations for for loops.
If you want data to play with, Range is not the shortest path

[Arthur Paulino]

I'm not on my PC, but I think we already have List.range, which might serve as an inspiration if you want something more plastic/generic

[Siddhartha Gadgil]

The above had a problem because of my switching back and forth. The following version of mkArray gives an example:

def mkArray [it : Iterable l α] (x: l): Array α :=
  it.toArray x

instance : Iterable Range Nat :=
  ⟨fun r => ForIn.toArray r⟩

def r : Range := [0:3]
def arr : Array Nat := mkArray r

[Siddhartha Gadgil]

In cleaned up form, here is the code again. @Arthur Paulino I agree that for Range this seems to not make sense. May be useful occasionally though.

universe u
class Iterable (l: Type u)(α : Type u) where
  toArray : l  → Array α

class IterableFamily (l: Type u → Type u) where
  toArray : l α  → Array α

instance {l: Type u → Type u}[it : IterableFamily l] (α : Type u) : Iterable (l α) α :=
  ⟨fun x => it.toArray x⟩

instance : IterableFamily List    :=
  ⟨fun l => l.toArray⟩

instance : IterableFamily Array   :=
  ⟨fun l => l⟩

def mkArray [it : Iterable l α] (x: l): Array α :=
  it.toArray x

def mkList [it : Iterable l α] (x: l): List α :=
  (mkArray x).toList

def mkHashMap
  [it : Iterable l  (α × β )][Hashable α][BEq α][BEq β](x: l ): HashMap α β   :=
    let arr : Array (α × β) := mkArray x
    arr.foldl (fun acc (k, v) => acc.insert k v) HashMap.empty

def ForIn.toArray [ForIn Id l α](x : l): (Array α) := Id.run
  do
    let mut arr := Array.mk []
    for a in x do
      arr := arr.push a
    return arr

instance : Iterable Range Nat :=
  ⟨fun r => ForIn.toArray r⟩

def r : Range := [0:3]
def arr : Array Nat := mkArray r

[Mario Carneiro]

Arthur Paulino said:

One thing I still haven't understood: if you want a list of numbers, why not make a function that creates one directly instead of instantiating a Range and then converting it into a list?

There isn't much overhead to creating a Range, it is just a trivial struct, so I would say that this is just a convenient syntax for calling List.range

[Mario Carneiro]

you would need four versions of the function to get the same behavior with direct list functions

[Joseph O]

I would say 3 actually

[Joseph O]

One for just stop, one for start and stop, and one for start, stop and step

[Arthur Paulino]

I suspect there's a solution with just one function and optional parameters with default values

[Mario Carneiro]

sure, Range's constructor itself has default values like that

[Mario Carneiro]

but Range also has fancy syntax which a custom function wouldn't have

[Joseph O]

yes

[Mario Carneiro]

You can also use @[csimp] lemmas to rewrite calls to [:n].toList to List.range n

[Gabriel Ebner]

Why would List.range be any more efficient than Range.toList? Because of the step size?

[Joseph O]

No customizable start of step

[Mario Carneiro]

Well, List.range as it exists today probably isn't that efficient, since it's not tail recursive IIRC. But if we assume that all the functions are given the most efficient implementations given their spec, it would be advantageous to call List.range when we know at compile time that the step is 1 and the start is 0

[Joseph O]

A lot of conversation, yet im not sure we have made a decision yet

[Mario Carneiro]

Range.toArray and Range.toList are no-brainers (in that the spec is clear and there is no downside to providing the function), everything else is speculative / comes as part of a larger untested infrastructure

[Sebastian Ullrich]

Just to give an idea of what I had in mind, this quick draft already generates pretty good code. The only improvements I can see would be to pass the Range object by value/as separate parameters through the loop (which is a general missing compiler optimization), and to introduce an ExactSizeIterator on top that allows the array to be created with the correct capacity from the beginning.

def Stream.drop [Stream stream value] (n : Nat) (s : stream) : stream :=
  match n with
  | 0 => s
  | n + 1 => drop n s

class BoundedStream (stream : Type u) (value : outParam (Type v)) extends Stream stream value where
  is_bounded : ∀ s, ∃ n, next? (Stream.drop n s) |>.isNone

instance : BoundedStream Std.Range Nat where
  is_bounded := sorry

structure Stream.Map (stream : Type u) (value value' : Type v) (f : value → value') where
  s : stream

instance [BoundedStream stream value] : BoundedStream (Stream.Map stream value value' f) value' where
  next? s := (fun (a, s) => (f a, ⟨s⟩)) <$> Stream.next? s.1
  is_bounded := sorry

def Stream.map [Stream stream value] (f : value → value') (s : stream) : Stream.Map stream value value' f := ⟨s⟩

def BoundedStream.toArray [BoundedStream stream value] (s : stream) : Array value :=
  go s #[]
where
  go s arr := match h : Stream.next? s with
    | none => arr
    | some (a, s') =>
      have : Classical.choose (BoundedStream.is_bounded s') < Classical.choose (BoundedStream.is_bounded s) := by
        sorry
      go s' (arr.push a)
termination_by go _ => Classical.choose (BoundedStream.is_bounded s)

set_option trace.compiler.ir.result true
#eval BoundedStream.toArray [3:5]
#eval BoundedStream.toArray (Stream.map (· + 1) [3:5])

Those sorries? Oh, nothing to worry, especially not that last one...

[Mario Carneiro]

Stream.drop is the identity function

[Mario Carneiro]

probably simpler to define Stream.nth instead of drop

[Joseph O]

Mario Carneiro said:

Range.toArray and Range.toList are no-brainers (in that the spec is clear and there is no downside to providing the function), everything else is speculative / comes as part of a larger untested infrastructure

What do you mean by "everything else"? Did I miss something in the conversation?

[Mario Carneiro]

I mean all the other proposals and ideas on this thread

[Mario Carneiro]

If you are looking for something to PR you can safely ignore them

[Mario Carneiro]

@Sebastian Ullrich Setting aside the sketchy Classical.choose (BoundedStream.is_bounded s) termination measure, I wonder whether it would be advantageous to have something like rust's ExactSizeIterator: make the bound an explicit part of the structure and use it to pre-seed the size of the array

[Mario Carneiro]

Also the bound could depend on the input stream value

[Joseph O]

Mario Carneiro said:

If you are looking for something to PR you can safely ignore them

Question is, where should i PR to. Mathlib4 or lean4?

[Mario Carneiro]

Mario Carneiro said:

My suggestion is to add to mathlib4, for example here -> https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/List/Defs.lean

[Joseph O]

Ah I missed that. I was thinking about adding a file called Range.lean, in Init.Data, wince the toList and toArray methods have to be underst the Std.Range namespace

[Sebastian Ullrich]

Mario Carneiro said:

Sebastian Ullrich Setting aside the sketchy Classical.choose (BoundedStream.is_bounded s) termination measure, I wonder whether it would be advantageous to have something like rust's ExactSizeIterator: make the bound an explicit part of the structure and use it to pre-seed the size of the array

Yes, I mentioned that :) . But it should not be mandatory, you still want toArray to work on filter. Good point with drop though, haha, I'll leave that and fixing the metric as an exercise to the reader.

[Jay Sulzberger]

I do not know what Common Lisp's loop is, but I have heard talk of its mysteries.

[Jay Sulzberger]

I sent above in answer to Mario Carneiro's remark about the power of LEAN's "iterator" 'for in'.

[Mac]

Sebastian Ullrich said:

I'd love to see a robust external iteration library for Lean in the future.

I see that everyone just ignored my post:

Mac said:

You might find my WIP lean4-itertools library to be of interest. I was designed exactly to help do this kind of thing.

It is an external iteration library that is attempting to do much of what is being discussed here. For example:

def foo :=
  range 10
  |> filter (· % 2 == 0)
  |> map (· * 2)
  |> array

I would be really curious what people think of my approach to fill this need and how it could be improved.

[Sebastian Ullrich]

Am I missing something? I only see ForIn methods in your library, which is internal iteration

[Mac]

@Sebastian Ullrich Huh? Does some research. Oh, sorry! I had never heard of the distinction between internal vs external iteration before (at least with those terms). I thought by "external iteration library" you meant an external library (i.e., one outside the Lean core) for iteration. My apologies for the misunderstanding.

[Sebastian Ullrich]

Hah, that indeed was a little ambiguous. I did mention the distinction in the very same comment though... :)

[Sebastian Ullrich]

The mentioned ExactSizeIterator looks like another use case that should be hard to pull off using internal iteration btw

[Sebastian Ullrich]

There is also an interesting blog post about Rust switching from internal to external iteration, and then later adding back internal iteration as an optional optimization of external iterators. Some of the described problems are specific to Rust though. https://medium.com/@veedrac/rust-is-slow-and-i-am-the-cure-32facc0fdcb

[Mac]

@Sebastian Ullrich I would kind of expect that from an imperative low-level language like Rust. As I see it, external iteration is the natural form of iteration in imperative languages (as it is explicitly stateful) whereas internal iteration is the natural form of iteration for functional languages (as it appears stateless). External iteration is still useful in functional languages, it is just more unnatural (and, depending on the language, can be quite cumbersome).

[James Gallicchio]

^ Is there even a good use case for external iterators in Lean? Plenty of functional languages' collections libraries get away with just an internal iterators.

Scala collections, most of the library functions are based on internal iteration but there's a class that all collections implement to expose an external iterator. Might be a valid design for Lean as well to give flexibility when people want it, at the cost of a bit of overhead

[James Gallicchio]

Sebastian Ullrich said:

The mentioned ExactSizeIterator looks like another use case that should be hard to pull off using internal iteration btw

Also RE: this, some Scala collections have a "sizeHint" interface for mutable buffers, which I think would be fine here. Basically just lets you get a buffer given an expected size to be pre-allocated. This could probably be implemented for Lean's native arrays?

[James Gallicchio]

class ExpectedSize (ρ : Type u) where
  expectedSize : ρ → Nat

class ToArray (ρ : Type u) (α : outParam (Type v)) where
  toArray : ρ → Array α

instance [ForIn Id ρ α] [ExpectedSize ρ] : ToArray ρ α where
  toArray r := Id.run do
    let mut a := Array.mkEmpty (ExpectedSize.expectedSize r)
    for x in r do
      a := a.push x
    return a

something simple like this?