easy HashMap instantiation

Stream: lean4

[Arthur Paulino]

It's not the first time that I needed something like this so I wrote this function:

def mapFromList {α β : Type} [BEq α] [Hashable α]
    (l : List (α × β)) : Std.HashMap α β :=
  l.foldl (fun m t => m.insert t.fst t.snd) Std.HashMap.empty

It allows us to say:

#eval mapFromList [(1, "one"), (2, "two")] |>.find! 1 -- "one"

Python has dict(...) and Scala has a Map(bla -> ble, ...) and I'm sure JavaScript has something just as practical.

Do you guys think it's worth it having a function like that in mathlib4 or maybe in Std?

[Yakov Pechersky]

As long as you document what happens when the l.map prod.fst is not nodup.

[Arthur Paulino]

Right... eating up a List is a rather rudimentary approach. How could we have a more sophisticated interface in Lean 4? (maybe something that screams in the presence of duplicated keys right away)

[Yakov Pechersky]

I think an Std function that overwrites old values at seen keys with new values is worth it, as long as it documents it. You can have another function that ignores new values too. And then a proof that given nodup (l.map prod.fst) the two are the same.

[Arthur Paulino]

@Yakov Pechersky is there a definition of "nodup" in Lean 4 repo? I can't find it

[Yakov Pechersky]

I don't know, I haven't seen it. In mathlib3, it's written in a particular way so that it doesn't require decidable equality on the type of element. I guess that doesn't matter for a concrete HashMap, but if you want a list.nodup in full generality, you might want that.

[Mauricio Collares]

Haskell people would probably expect the behavior provided by Data.Map.fromList (https://hackage.haskell.org/package/containers-0.4.0.0/docs/src/Data-Map.html#fromList), namely to retain the last value in case of duplicate keys.

[Yakov Pechersky]

(Another nice lemma might be that mapFromList_keepFirst l.reverse = mapFromList_keepLast l)

[Arthur Paulino]

Yakov Pechersky said:

(Another nice lemma might be that mapFromList_keepFirst l.reverse = mapFromList_keepLast l)

Yeah that's exactly what I thought. In fact, I thought about implementing the alternative behavior using the reversed list

[Arthur Paulino]

Another design is having keepLast as a boolean auto parameter set as true

[Arthur Paulino]

Alright, since the discussion seems to be motivated enough, I created this issue:
https://github.com/leanprover/lean4/issues/947

[Arthur Paulino]

@Mauricio Collares I added your suggestion to the issue description :+1:

[Arthur Paulino]

https://github.com/leanprover/lean4/pull/950