How to use Std.HashMap

Stream: new members

[Shubham Kumar 🦀 (he/him)]

I was trying to define HashMap using Std.mkHashMap but it's unable to derive Hashable instance for the type which makes sense because I haven't suggested the type. I am not sure how I should do it.

I know it should be something like the following (from FPIL) just for String

deriving instance BEq, Hashable for Pos
deriving instance BEq, Hashable, Repr for NonEmptyList

But I don't know how to use this knowledge, any help would be great, thanks!

[Shubham Kumar 🦀 (he/him)]

I tried doing deriving instance BEq, Hashable for String it returns an error

failed to synthesize instance
  Hashable (List Char)

[Eric Wieser]

If you provide a #mwe, then it will be easier for others to help you

[Shubham Kumar 🦀 (he/him)]

I'm trying to make a hashmap using eval

#eval Std.mkHashMap

[Shubham Kumar 🦀 (he/him)]

I'm not sure if there is another working example

[Mario Carneiro]

it might help to include relevant imports, did you try writing that in its own file?

[Shubham Kumar 🦀 (he/him)]

yes, the only thing I imported is Std

import Std

def ex := "Game 1: 3 blue, 4 red; 1 red, 2 green, 6 blue; 2 green"

def filterNoise (lst : List String) : List String :=
  let filterChars := fun
    | ';' | ':' | ',' => none
    | ch => some ch
  let filterString (str : String) : String :=
    let charList : List Char := (str.toList).filterMap filterChars
    charList.foldl (init := "") String.push
  lst.map filterString

def parseLine (line : String)  :=
  line.splitOn " " |> filterNoise

#eval Std.mkHashMap

#eval List.map (String.map (fun ch =>
  match ch with
  | ':' => ' '
  | ',' => ' '
  | ';' => ' '
  | _ => ch
)) (ex.splitOn " ")

This is the file I am trying to implement

[Eric Wieser]

(note that #mwe is a link that tells you to, among other things, include relevant imports)

[Shubham Kumar 🦀 (he/him)]

I don't know how to use a HashMap

[Eric Wieser]

What type of map are you trying to create?

[Shubham Kumar 🦀 (he/him)]

String -> String

[Eric Wieser]

Then tell Lean that via (mkHashMap : HashMap String String)

[Shubham Kumar 🦀 (he/him)]

so key is String and value is String

[Eric Wieser]

Or you can pass those as arguments directly to docs#Std.mkHashMap

[Shubham Kumar 🦀 (he/him)]

like this : #eval Std.mkHashMap String String ?

[Shubham Kumar 🦀 (he/him)]

oh ok

[Eric Wieser]

mkHashMap (α := String) (β := String)

[Eric Wieser]

The arguments are implicit (in {}), so you can't write them the usual way and have to pass them by name

[Shubham Kumar 🦀 (he/him)]

Eric Wieser said:

mkHashMap (α := String) (β := String)

Thanks I'm sorry for the stupid question, this makes it clearer

[Eric Wieser]

Eric Wieser said:

Then tell Lean that via (mkHashMap : HashMap String String)

But this spelling is arguably more idiomatic anyway

[Shubham Kumar 🦀 (he/him)]

so when I do #eval Std.mkHashMap (α := String) (β := String) I get the following error

expression
  Std.mkHashMap
has type
  Std.HashMap String String
but instance
  Lean.MetaEval (Std.HashMap String String)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type

[Shubham Kumar 🦀 (he/him)]

and doing this #eval Std.mkHashMap : Std.HashMap String String results in the following error

typeclass instance problem is stuck, it is often due to metavariables
  Hashable ?m.724

[Mauricio Collares]

The first error says Lean doesn't know how to print a hashmap, you'll probably need to iterate over its elements to print it (but the command successfully constructed a hashmap)

[Mauricio Collares]

The second one is probably due to lack of parentheses

[Shubham Kumar 🦀 (he/him)]

Mauricio Collares said:

The first error says Lean doesn't know how to print a hashmap, you'll probably need to iterate over its elements to print it (but the command successfully constructed a hashmap)

ok :thumbs_up:

[Shubham Kumar 🦀 (he/him)]

Mauricio Collares said:

The second one is probably due to lack of parentheses

so I don't where to add the parantheses but thanks! I'll use the first way right now

[Mauricio Collares]

I was thinking of #eval (Std.mkHashMap : Std.HashMap String String)

[Mario Carneiro]

note that the syntax for type ascription is (expr : type), the parentheses are a mandatory part of the syntax

[Shubham Kumar 🦀 (he/him)]

ok so it seems like I am able to make a HashMap and insert elements to it.
Is there a way to generate an equivalent of what a show instance in Haskell for HashMaps in Lean?

[Mario Carneiro]

that's what the error message is suggesting

[Mario Carneiro]

the easiest method is deriving Repr on the type

[Shubham Kumar 🦀 (he/him)]

Mario Carneiro said:

the easiest method is deriving Repr on the type

something like this deriving instance Repr for Std.HashMap String String ?

[Shubham Kumar 🦀 (he/him)]

unrelated but a tiny stupid question : How does one do qualified imports in Lean?

[Yaël Dillies]

This does not exist

[Shubham Kumar 🦀 (he/him)]

oh ok, thanks I did not know that

[Mario Carneiro]

qualified how?

[Shubham Kumar 🦀 (he/him)]

like in haskell I use qualified imports to shorten names : import qualified Data.List as L
so I want to import only HashMap from Std and shorten it to HMap (just an example) how would I do that?

[Shubham Kumar 🦀 (he/him)]

that's kind of what I needed qualified imports for

[Mario Carneiro]

in lean namespaces and imports are not connected

[Mario Carneiro]

you would do that using open instead of import

[Mario Carneiro]

import Std.Data.HashMap.Basic

open Std renaming HashMap → HMap
#check HMap

[Shubham Kumar 🦀 (he/him)]

Oh cool! Thanks!

[Shubham Kumar 🦀 (he/him)]

Shubham Kumar 🦀 (he/him) said:

Mario Carneiro said:

the easiest method is deriving Repr on the type

something like this deriving instance Repr for Std.HashMap String String ?

btw this didn't work

[Mario Carneiro]

this is a bit of abuse of the repr class since it's supposed to be an actual lean expression (more or less), but you can do something like this:

instance [BEq α] [Hashable α] [Repr α] [Repr β] : Repr (Std.HashMap α β) where
  reprPrec m _ := .bracket "{" (.joinSep (m.toList.map fun (a, b) => f!"{repr a} ↦ {repr b}") ", ") "}"

#eval Std.mkHashMap.insert "hi" "there" |>.insert "something" "else"
-- {"something" ↦ "else", "hi" ↦ "there"}