How to use a hashmap?

Stream: new members

[Jafar Tanoukhi]

I am trying to use the hashmap implementation provided by Lean core but I can't figure out the syntax, can someone write me a simple function that shows how to use a hashmap in general, how do you make an "instance" of it and then fill it with key-value pairs and then use these value pairs when needed?

[Damiano Testa]

import Lean
/-!
A very quick tutorial for using `HashMap`s
-/

open Lean

/-- using `HashMap.empty` and `HashMap.insert` -/
def myHM : HashMap Nat String := HashMap.empty
  |>.insert 1 "one"
  |>.insert 2 "two"
  |>.insert 3 "three"

--  the above is just for "clean" formatting: you could also write
--  `def myHM1 : HashMap Nat String := ((HashMap.empty.insert 1 "one").insert 2 "two").insert 3 "three"`

-- Now also `HashMap.find?` and `HashMap.contains`
#eval myHM.find? 1  -- `some "one"`
#eval myHM.find? 4  -- `none`
#eval myHM.contains 1  -- `true`
#eval myHM.contains 4  -- `false`

-- to print a HashMap, convert it to a `List` or an `Array`
#eval IO.println myHM.toArray -- #[(1, one), (2, two), (3, three)]
#eval IO.println myHM.toList  -- [(3, three), (2, two), (1, one)]

[Jafar Tanoukhi]

hi, thanks for replying, i did a lot of trial and error after asking the question and eventually got my answer, but i still have some questions, in the documentation there's HashMapImp, HashMap, HashMapBucket. I don't understand the difference especially between HashMap and HashMapImp.

Also I am interested in understanding this syntax, how does it work ?

def myHM : HashMap Nat String := HashMap.empty
  |>.insert 1 "one"
  |>.insert 2 "two"
  |>.insert 3 "three"

[Damiano Testa]

I personally view everything in the HashMap file that comes before the definition of HashMap as an implementation detail: I have never used neither ...imp, nor ...Bucket.

Regarding the final syntax, it is more an optical illusion than anything else: |> essentially means "close here a parenthesis that has been opened as far left as possible". (There is an analogous symbol <| for going right.) After that, you are leveraging dot-notation for the term appearing in the previous line. The inlined, commented code above is "exactly the same", but without the visual effect.

[Damiano Testa]

So, in effect, you are starting from the empty HashMap and you are adding key-value pairs to it one at a time, except that you are well-spacing them and making each addition on a new line and nicely justified.

[Jafar Tanoukhi]

Ok so from what i understand |> closes the "last unclosed bracket".
Is this like a special notation cooked into lean or is this symbol actually defined somewhere to do this?

[Damiano Testa]

Hovering over <| should give you some information. Maybe docs#«term_<|_» also works?

[Damiano Testa]

That did not work, but maybe this does: https://leanprover-community.github.io/mathlib4_docs/Init/Notation.html#%C2%ABterm_%3C|_%C2%BB

[Jafar Tanoukhi]

Oh ok thanks alot

[Mario Carneiro]

Damiano Testa said:

I personally view everything in the HashMap file that comes before the definition of HashMap as an implementation detail: I have never used neither ...imp, nor ...Bucket.

Note that the Imp in HashMapImp stands for "implementation (detail)" (although normally this is abbreviated Impl...) so your view is the correct one. You should basically never use these functions directly