Strange error

Stream: lean4

[Arthur Paulino]

I'm writing this function:

private def parse (s : String) : Table := do
  if s.length = 0 then
    ⟨[], [], []⟩
  else
    let data : List String := s.splitOn "¨"
    let mut names : List String := []
    let mut types : List Type := []
    let header : String := data.get! 0
    let headerParts : List String := header.splitOn "~"
    for headerPart in headerParts do
      let split : List String := headerPart.splitOn " "
      names := names.concat (split.get! 0)
      types := types.concat (typesMap (split.get! 1))
    ⟨names, types, []⟩

On the line names := names.concat (split.get! 0), it's raising an error:

invalid field notation, type is not of the form (C ...) where C is a constant
  names
has type
  ?m.18868 s

Has anyone seen this?

[Kyle Miller]

In Lean 3 at least, that's usually because at the moment it's trying to resolve the dot notation, it does not know the type of the variable (names in this case). This can be due to the order in which it is elaborating expressions.

You can try doing String.concat names (split.get! 0) instead to help it out.

[Arthur Paulino]

private def parse (s : String) : Table := do
  if s.length = 0 then
    ⟨[], [], []⟩
  else
    let data : List String := s.splitOn "¨"
    let mut names : List String := []
    let mut types : List Type := []
    let header : String := data.get! 0
    let headerParts : List String := header.splitOn "~"
    for headerPart in headerParts do
      let split : List String := headerPart.splitOn " "
      names := List.concat names (split.get! 0)
      types := types.concat (typesMap (split.get! 1))
    ⟨names, types, []⟩

Still a bit weird

application type mismatch
  mk names
argument
  names
has type
  List (?m.19230 s) : Type 1
but is expected to have type
  List String : Type

[Kyle Miller]

Hard to say without a #mwe

[Kyle Miller]

I'm going to guess that it's because the types list is in a different universe than names.

[Arthur Paulino]

https://gist.github.com/arthurpaulino/73fb9d6c4b26b786ce329f84a554d6cc

[Kyle Miller]

You could check this by removing types and seeing if the error goes away, and removing names and doing the same.

[Arthur Paulino]

I removed types and it still doesn't work. Then I removed names and it works smoothly

[Reid Barton]

It's probably because Table is also in a different universe

[Arthur Paulino]

How is this universe change happening? And how can I prevent it from happening?

[Kyle Miller]

List String : Type 0
List Type : Type 1

A way to prevent this from happening is to use the suggestion that's come up to use an inductive type (an enum basically) that represents the specific types that can appear in your database.

inductive DType | DNat | DString | DBool

def DType.toType : DType → Type
| DNat => Nat
| DString => String
| DBool => Bool

def DVal : Type := Σ (t : DType), t.toType

example : DVal := ⟨DType.DString, "hello"⟩

Then List DType : Type 0.

[Reid Barton]

There's nothing you can do with a Type at runtime anyways, so the list Type was kind of useless I think.

[Arthur Paulino]

Hm, I will try that. Thanks!

[Henrik Böving]

Also if you are writing non trivial parsers you might be interested in the Lean.Data.Parsec module which is a partial copy of Haskells parsec

[Arthur Paulino]

It worked! Thanks!
I will improve the parser once I get a first working version