known capacities

Stream: lean4

[Arthur Paulino]

In the same vain of Rust's Vec::new_with_capacity, would it make sense for Lean core to provide Array.mkWithCapacity and ByteArray.mkWithCapacity? I know I can create those locally in C, but I believe this is something more ppl can benefit from (potentially even core itself), as avoiding reallocations+copies when possible is strictly better.

[Sebastian Ullrich]

That's Array.mkEmpty

[Arthur Paulino]

Array.mkEmpty spends time setting data to a value. I would like to avoid that

[Arthur Paulino]

That is, just allocate with junk from memory, but with size=0

[Sebastian Ullrich]

I don't follow, it's a straight call to lean_alloc_array

[Arthur Paulino]

Hm, I will double check. Maybe I'm confused

[Arthur Paulino]

Aha! I was indeed confused. There's mkEmpty and mkArray. Thanks!

[Kyle Miller]

I think it might be nice to include these in the docstring to docs#Array. There's already a discussion of capacities there, so it's natural. (Plus, I tend to forget the name of Array.mkEmpty, so it would be nice to have a quick way to look it up.)

[Kim Morrison]

lean#7430

[Henrik Böving]

I've been wondering whether it would be worth it to break Array.empty just a tiny bit by adding a capacity argument with default value, that way it'd be a bit closer to what we have in Std's containers like HashMap and TreeMap now

[Markus Himmel]

Actually I was thinking of renaming docs#Std.HashMap.empty to something like Std.HashMap.withCapacity or Std.HashMap.emptyWithCapacity so that there is no longer a naming conflict between the empty function and the docs#EmptyCollection notation, which is also called empty in identifiers.

[Arthur Paulino]

Now that you mentioned it, I am extra encouraged to say that I quite like that Rust's APIs have the word "capacity" explicit on related symbols

[Kim Morrison]

emptyWithCapacity everywhere sounds great!

[Arthur Paulino]

I mean, I overlooked mkEmpty for a reason. It would have been a better experience if the LSP had found it for me when I typed "Array.capac"

[Kim Morrison]

lean#7445 does the rename for Array (also ByteArray and FloatArray).

[Kim Morrison]

lean#7446 replaces some .emptys with ∅

[Kim Morrison]

lean#7447 does HashMap/HashSet, which @Markus Himmel will need to review.

(Mostly this was written by Claude, with me just pressing tab. Hopefully we got it right.)

[Jovan Gerbscheid]

(lean4#7445, lean4#7446, lean4#7447)