Slowness in converting an array of pairs to a HashMap

Stream: lean4

[Anand Rao Tadipatri]

I have some code for converting an array of pairs into a HashMap that seems unreasonably slow to me. Here is an #mwe:

import Lean

def generateCache {α β} [BEq α] [Hashable α] (results : Array (α × β)) (capacity := 8) : Std.HashMap α (Array β) :=
  results.foldl (init := Std.HashMap.empty (capacity := capacity)) fun map ⟨fst, snd⟩ ↦
    match map[fst]? with
    | some arr =>
      let map := map.erase fst
      map.insert fst (arr.push snd)
    | none => map.insert fst #[snd]

def dummyData (n : Nat) : Array (String × String) := Id.run do
  let mut arr := #[]
  for i in [0:n] do
    for j in [0:n] do
      arr := arr.push (s!"Key{i}", s!"Value{j}")
  return arr

-- slower than expected
/-
122511589|Starting ...
122511589|Generated data ...
122516170|Generated cache of size 750 ...
-/
#eval show IO _ from do
  IO.println s!"{← IO.monoMsNow}|Starting ..."
  let data := dummyData 750
  IO.println s!"{← IO.monoMsNow}|Generated data ..."
  let cache := generateCache (capacity := 2048) data
  IO.println s!"{← IO.monoMsNow}|Generated cache of size {cache.size} ..."

Is this kind of slowdown to be expected while converting between the datastructures? I'd appreciate any feedback in optimizing this code to reduce its runtime.

[Henrik Böving]

There's no need to do map.erase and then map.insert for the same value, only do map.insert

[Henrik Böving]

But the operation that you actually want to use here is modify which doesn't exist yet unfortunately

[Henrik Böving]

(which is my fault)

[Anand Rao Tadipatri]

Okay, thanks for the clarification.