HashMap expects a function

Stream: lean4

[Santtu]

New user here. Trying to write a TOML parser as an exercise, but the type definition

import Std.Data.HashMap

--
-- A definition of the kinds of types given in the TOML specification at
-- https://toml.io/en/v1.0.0#objectives.
--
inductive TOMLType where
    | boolean (b : Bool)
    | integer (n : Int)
    | float (n : Float)
    | string (s : String)
    | array (elems : Array TOMLType)
    | table (kvPairs : HashMap String (fun _ => TOMLType))
    -- TODO: add more types like DateTime here.

throws the error

✖ [3/10] Building SantunLeanTOMLParser.TOMLTypes
trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH= /usr/local/lean/v4.14.0/bin/lean ././././SantunLeanTOMLParser/TOMLTypes.lean -R ./././. -o ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.olean -i ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.ilean -c ././.lake/build/ir/SantunLeanTOMLParser/TOMLTypes.c --json
error: ././././SantunLeanTOMLParser/TOMLTypes.lean:13:21: function expected at
  HashMap
term has type
  ?m.21
error: Lean exited with code 1
Some required builds logged failures:
- SantunLeanTOMLParser.TOMLTypes
error: build failed

What am I doing wrong?

[Henrik Böving]

HashMap is scoped, you need to refer to Std.HashMap, the expects a function thing is Lean's auto implicit feature that turns names that are not bound into implicit arguments automatically. You can disable it if you want but you should also be able to tell by the semantic highlighting in your editor.

[Santtu]

So I should import Std.HashMap instead? Also, I'm actually using just Vim with only a simple syntax highlighting file and no fancy LSP features, so I am a bit handicapped in that sense. :D

[Henrik Böving]

No you should write kvPairs : Std.HashMap String ...

I would also not recommend using Lean without an LSP, it's going to be a significantly more difficult experience. There is a great neovim plugin if you want to use that.

[Santtu]

Hmm. Without the import of Std.HashMap I get an error message

trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH= /usr/local/lean/v4.14.0/bin/lean ././././SantunLeanTOMLParser/TOMLTypes.lean -R ./././. -o ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.olean -i ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.ilean -c ././.lake/build/ir/SantunLeanTOMLParser/TOMLTypes.c --json
error: ././././SantunLeanTOMLParser/TOMLTypes.lean:11:24: unknown identifier 'Std.HashMap'
error: Lean exited with code 1
Some required builds logged failures:
- SantunLeanTOMLParser.TOMLTypes
error: build failed

With the import of Std.HashMap in place, I get

✖ [3/10] Building SantunLeanTOMLParser.TOMLTypes
trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH= /usr/local/lean/v4.14.0/bin/lean ././././SantunLeanTOMLParser/TOMLTypes.lean -R ./././. -o ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.olean -i ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.ilean -c ././.lake/build/ir/SantunLeanTOMLParser/TOMLTypes.c --json
error: ././././SantunLeanTOMLParser/TOMLTypes.lean:1:0: object file '/usr/local/lean/v4.14.0/lib/lean/Std/HashMap.olean' of module Std.HashMap does not exist
error: Lean exited with code 1
Some required builds logged failures:
- SantunLeanTOMLParser.TOMLTypes
error: build failed

[Santtu]

Could this be related to my Lean installation? I copied the files from GitHub releases to /usr/local/lean/... and created symbolic links to the binaries in a folder in my path. But when I look at the installation location, I do not see any .olean files.

[Henrik Böving]

No, you need to do both

import Std.Data.HashMap

and type
Std.HashMap String ...

[Henrik Böving]

Santtu said:

Could this be related to my Lean installation? I copied the files from GitHub releases to /usr/local/lean/... and created symbolic links to the binaries in a folder in my path. But when I look at the installation location, I do not see any .olean files.

and regarding this i would highly recommend to use elan if you plan on stickign with lean for any amount of time

[Santtu]

Right. I'll get to know elan, once I get this thing to compile. :D But the problem was that I needed to import Std.Data.HashMap, but when actually declaring the table type, I needed to use Std.HashMap instead. A bit confusing, but I guess that is just a namespace vs module thing? Now I get the error

trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH= /usr/local/lean/v4.14.0/bin/lean ././././SantunLeanTOMLParser/TOMLTypes.lean -R ./././. -o ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.olean -i ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.ilean -c ././.lake/build/ir/SantunLeanTOMLParser/TOMLTypes.c --json
error: ././././SantunLeanTOMLParser/TOMLTypes.lean:13:42: application type mismatch
  @Std.HashMap String fun x => TOMLType
argument
  fun x => TOMLType
has type
  ?m.23 → Type ?u.16 : Sort (max (?u.16 + 2) ?u.22)
but is expected to have type
  Type ?u.20 : Type (?u.20 + 1)
error: Lean exited with code 1
Some required builds logged failures:
- SantunLeanTOMLParser.TOMLTypes
error: build failed

Almost there.

[Santtu]

It seems like the second argument should not be a function at all, but something else. I guess this is related to kinds somehow?

[Henrik Böving]

The second argument should just be TOMLType

[Santtu]

If the value type of the HashMap is changed to TOMLType, we get another error:

trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH= /usr/local/lean/v4.14.0/bin/lean ././././SantunLeanTOMLParser/TOMLTypes.lean -R ./././. -o ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.olean -i ././.lake/build/lib/SantunLeanTOMLParser/TOMLTypes.ilean -c ././.lake/build/ir/SantunLeanTOMLParser/TOMLTypes.c --json
error: ././././SantunLeanTOMLParser/TOMLTypes.lean:7:0: (kernel) arg #1 of '_nested.Std.HashMap_2.mk' contains a non valid occurrence of the datatypes being declared
error: Lean exited with code 1
Some required builds logged failures:
- SantunLeanTOMLParser.TOMLTypes
error: build failed

[Santtu]

Ah, looking at the documentation comment for Std.Data.HashMap we see a probable reason: https://github.com/leanprover/lean4/blob/8a1e50f0b98337f5d0f9a9697f95f10237c4a77c/src/Std/Data/HashMap/Basic.lean#L51-L54

[Santtu]

So I guess standard HashMaps cannot be used in inductive types at all.

[Santtu]

And indeed, changing all instances of HashMap to HashMap.Raw allows the code to compile.

[Santtu]

But I guess this will carry some caveats regarding code safety.