Match vs. Let Pattern

Stream: lean4

[Marcus Rossel]

In the implementation of HashMap I noticed that sometimes structures are destructured using a match and sometimes a let-pattern. E.g. in HashMap.contains:

def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
  match m with
  | ⟨_, buckets⟩ =>
    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
    (buckets.val.uget i h).contains a

Is there a particular reason to use the match-expression here, instead of just using a let-pattern? So something like:

def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
  let ⟨_, buckets⟩ := m
  let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
  (buckets.val.uget i h).contains a

[Arthur Paulino]

According to git blame that function is at least 1 year old. And the match m with line is 2 years old. I don't know when the let-pattern syntax was introduced so maybe it didn't exist yet

[Marcus Rossel]

Arthur Paulino said:

According to git blame that function is at least 1 year old. And the match m with line is 2 years old. I don't know when the let-pattern syntax was introduced so maybe it didn't exist yet

I was considering the same explanation. But there's also this implementation of HashMap.find?:

@[inline] def find? (m : HashMap α β) (a : α) : Option β :=
  match m with
  | ⟨ m, _ ⟩ => m.find? a

... which I guess could always have been written as:

@[inline] def find? (m : HashMap α β) (a : α) : Option β :=
  m.val.find? a

So I feel like there's more to it :D

[Leonardo de Moura]

@Marcus Rossel There is nothing. This is an old file that was created using a Lean 3 variant. When we started Lean 4, we first tried to simplify Lean 3 as much as possible to make the bootstrapping process simpler. We had to use many workarounds until we managed to compile Lean 4 using itself. We have removed most of these workarounds, but some are still there. Here is the original file: https://github.com/leanprover/lean4/blob/5a560b6d4379698aa5a87d1b9e4cede3c8c19909/library/init/data/hashmap/basic.lean

[Marcus Rossel]

@Leonardo de Moura Ok, thanks for resolving the mystery :D
Are PRs cleaning up these kinds of things welcome?

[Leonardo de Moura]

Thanks for asking. We are currently a bit overwhelmed. Let's wait until Mathilb has been ported to Lean 4. We are trying to prioritize missing features and bugs.