Type-level dhashmap["name"]'h doesn't reduce to value

Stream: new members

[aron]

I'm trying to emulate record types with dynamic field names and types using a DHashMap.

import Std.Data.HashMap
open Std

def fieldTypesList : List (String × Type) := [("age", Nat), ("name", String)]
def fieldTypes : HashMap String Type := HashMap.ofList fieldTypesList

def RecordType := DHashMap String (fun field => (h : field ∈ fieldTypes) → fieldTypes[field]'h)

def myRecord : RecordType :=
  DHashMap.empty
  |>.insert "age" (fun h => 0)
  |>.insert "name" (fun h => "myName")

But I get these errors:

failed to synthesize
  OfNat fieldTypes["age"] 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  fieldTypes["age"]
due to the absence of the instance above

type mismatch
  "myName"
has type
  String : Type
but is expected to have type
  fieldTypes["name"] : Type

For some reason Lean can't figure out that fieldTypes["age"]'h reduces to Nat and that fieldTypes["name"]'h reduces to String. Am I doing something wrong here?

[Kyle Miller]

I don't know what you should do instead, but I'm not surprised to see that fieldTypes["name"]'h doesn't reduce to String.

Maybe it's complex enough that it needs some custom elaborator?

[Markus Himmel]

Std.HashMap wasn't designed for kernel computations. Have you seen https://youtu.be/pao0UQKoKO0?si=jmHdpPeMIOKA7wbv ? The library described there might be a better fit for your use case.

[Robin Arnez]

This works a bit better:

def fieldTypes (s : String) : Type :=
  if s = "age" then Nat
  else if s = "name" then String
  else Empty

def RecordType := DHashMap String fieldTypes

def myRecord : RecordType :=
  (∅ : DHashMap _ _)
  |>.insert "age" (0 : Nat)
  |>.insert "name" "myName"

[aron]

Markus Himmel said:

Std.HashMap wasn't designed for kernel computations. Have you seen https://youtu.be/pao0UQKoKO0?si=jmHdpPeMIOKA7wbv ? The library described there might be a better fit for your use case.

Mm that looks interesting. I'm about 10m into the video but he hasn't mentioned the name of the library yet and it's not in the description either. Do you have a link to the library?

Looks like it's this https://github.com/jrr6/lean-tables

[aron]

@Robin Arnez yeah but the point of this is to be able to make the fields a bit more dynamic. If I could hardcode all the field names in an if expression ahead of time I wouldn't be trying to do this in the first place

[aron]

I thought this would just work tbh, I don't see why maps would work any differently if they are at the type level vs if they are values.

Are there any resources that would explain why this doesn't "just work" as I was expecting it to? Is it that Lean has a limit on how much computation it does at the type level and inserting things into a DHashMap crosses that limit so it stops evaluation the type expression?

[Robin Arnez]

well, kernel "evaluation" is unlike normal evaluation in that it has more limits and in particular recursive functions don't always work well

[Robin Arnez]

not sure what it is this time but you can quickly get "defeq blockers" from e.g. irreducible definitions or well-founded recursion

[Robin Arnez]

oh I found the culprit: protected opaque String.hash : String → UInt64 (yeah, opaque is another case of a blocker)

[Robin Arnez]

maybe it's worth trying TreeMap? although this table library might be a better fit

[Robin Arnez]

yup, seems to work:

import Std.Data.HashMap
import Std.Data.TreeMap

open Std

def fieldTypesList : List (String × Type) := [("age", Nat), ("name", String)]
def fieldTypes : TreeMap String Type := TreeMap.ofList fieldTypesList

def RecordType := DHashMap String (fun field => fieldTypes.getD field Empty)

def myRecord : RecordType :=
  (∅ : DHashMap _ _)
  |>.insert "age" (0 : Nat)
  |>.insert "name" "myName"

[aron]

Ahh amazing!! yeah that works :fire: thanks so much @Robin Arnez