Regarding map and extract for Byte/FloatArrays

Stream: lean4

[Number Eighteen]

Hi all;

I notice that ByteArray and FloatArray lack map, and FloatArray also lacks extract. Is there a performance reason for this, or just that these operations were not needed for these types?

I would like to understand how compiler optimizations are applied to these two types in order to avoid doing something bad. Say I write an extract function for FloatArray as follows (NOT compatible with the current API):

@[inline]
def FloatArray.extractAux (A C : FloatArray)
    (start size : Nat) : FloatArray :=
  match size with
  | 0 => C
  | k + 1 => FloatArray.extractAux A
        (C.push <| A.get! start) start.succ k

@[inline]
def FloatArray.extract (A : FloatArray)
    (start size : Nat) : FloatArray :=
  if start + size > A.size then
    ⟨#[]⟩
  else
    FloatArray.extractAux A
       (FloatArray.mkEmpty size) start size

Is there something bad happening here? If so, what are the tools if any to test performance pitfalls in the above code?

A similar question applies to map: would the obvious implementation of map create performance problems?

[François G. Dorais]

Note that ByteArray and FloatArray are scalar arrays, which are implemented differently from Array. The issue with map is that in-place optimization is not possible for ByteArray except for maps UInt8 -> UInt8. (Similarly for FloatArray.) So there is no major advantage over a plain for loop.

The reason ByteArray.extract exists is that it is a common special case of ByteArray.copySlice, which is basically Lean's wrapper around C's memcpy. There is no similar low-level function for FloatArray implemented in Lean core, so there is currently no FloatArray.copySlice nor FloatArray.extract. I think that's an omission.

I think Lean core would currently accept these only if they come with efficient low-level implementations. That said, all of these would be welcome additions to Batteries, even if implemented as for loops.

[François G. Dorais]

See batteries#902