Pattern matching with arrays

Stream: lean4

[Paul Chisholm]

What is the correct way to pattern match with arrays. It is clear when the arrays are of known length, just use #[], #[a], #[a,b] etc in the pattern. What about when the array length is not known. Playing around I ended up with

def reverse (arr : Array α) : Array α :=
  match arr with
  | ⟨[]⟩    => #[]
  | ⟨a::as⟩ => (reverse ⟨as⟩).push a

but it doesn't seem satisfactory pattern matching on the representation of arrays. Could the explicit reference to the underlying list circumvent the efficient implementation of arrays?

[James Gallicchio]

I believe that would in fact cause the array to be converted to a list first. You could build some array slice/list view types, but nothing like that has been built yet...

[James Gallicchio]

Arrays don't really support any fast modification other than adding/removing at the end

[Marc Huisinga]

James Gallicchio said:

Arrays don't really support any fast modification other than adding/removing at the end

Updating any of the elements is O(1) if the reference count of the array is 1

[James Gallicchio]

(err, sorry, I mean adding/removing elements anywhere other than at the end)

[Paul Chisholm]

Thanks for the response.
Do I understand correctly. In the above function the pattern creates a new list from the non-empty array, then the recursive call creates a new array from the list? So in similar use cases it would be better just using lists directly.

[James Gallicchio]

Yep! It is slightly unfortunate that it is so easy to accidentally turn an array into a list and vice versa, since those operations are not cheap.

[Marc Huisinga]

Arrays don't really lend themselves well for pattern matching, they're best worked with using the functions in the standard library. For programming purposes, I'd personally write reverse as follows:

def reverse (xs : Array α) : Array α := Id.run do
  let mut xs := xs
  for i in [0:xs.size/2] do
    xs := xs.swap! i (xs.size - i - 1)
  return xs