lazy operations for Array/String

Stream: lean4

[eyelash]

I noticed that functions such as Array.take, String.take, Array.map, String.map, Array.filter and many more all return a new Array/String. Unless the compiler is somehow able to optimize this, all of these operations need to allocate new space and copy every element. Have there been any discussions about making these operations lazy to avoid the allocation/copy similar to how Rust does it? In Lean terms this would mean that these functions would return new types that would provide instances of Stream and the functions themselves would need to be redefined to work on Streams in order to allow chaining. Alternatively, functions such as Array.take, String.take, or String.trim could also return a Subarray/Substring.

[Henrik Böving]

We do have support in the runtime for mutating structures that have reference count 1 (which they do if you treat them linearly) in place. In particular something like Array.map will remain in place. filter is currently not implemented in a way to facilitate this, though I think there is a path to making this happen in place in theory.

Array.take and String.take are (or, at least after recent internal discussions will not be) optimized to work in place. I do agree that having API that returns Subarray or Substring is potentially useful but currently both of these have painful API gaps on their own so this wouldn't be a joy to use either.

The more general solution here is likely a general iterator interface that's going to come at some point in the future.

[eyelash]

Will this general iterator interface be similar to Iterator in Rust? I'm assuming this will be a replacement for Stream?

[eyelash]

Are there any plans for unboxed Arrays (as a compiler optimization)? In-place Array.map only works if the element size stays the same.

[Henrik Böving]

eyelash said:

Will this general iterator interface be similar to Iterator in Rust? I'm assuming this will be a replacement for Stream?

Not clear so far

eyelash said:

Are there any plans for unboxed Arrays (as a compiler optimization)? In-place Array.map only works if the element size stays the same.

These are disjoint questions. Unboxed Arrays might happen in the future, note that we have ByteArray and FloatArray for specific purposes already that are unboxed. In place Array.map indeed only works if the lement size stays the same but the elment size of an Array is always sizeof(size_t) so that is not important.

[Notification Bot]

eyelash has marked this topic as resolved.

[Notification Bot]

François G. Dorais has marked this topic as unresolved.

[François G. Dorais]

You can use Substring and Subarray for lazier operations. These also have Stream instances.