Defining a table type

Stream: new members

[Varun Gandhi]

Hello! I've just started learning Lean, and I'm trying to define a table type. (Apologies if this is the wrong stream to ask!) So far, I have

structure Table (nrows : nat) (schema : list (string × Type)): Type :=
  make :: (data : schema.map (λ (x : (string × Type)) => vector x.2 nrows))

In Haskell-y pseudocode, I'd like to be able to construct tables like so:

t :: Table 3 '["name" :-> String, "age" :-> Int]
t = ["Alice", "Bob", "Charlie"] ::: [10, 12, 11]

However, I run into a type error:

term
  vector x.snd nrows
has type
  Type : Type 1
but is expected to have type
  Prop : Type

Why is the type checker expecting Prop instead of Type? The list.map signature has {α : Type u} {β : Type v} (f : α → β) : list α → list β -- given that v can vary, wouldn't inferring v = 1 solve the issue?

[Kyle Miller]

Here's the error I'm seeing in full:

60:55: invalid lambda expression, ',' or '⟨' expected

60:56: invalid expression

60:56: type mismatch at application
  ⁇ = ⁇ > vector x.snd nrows
term
  vector x.snd nrows
has type
  Type : Type 1
but is expected to have type
  Prop : Type

In Lean 3, the syntax for lambda expressions uses a comma instead of => (that's Lean 4).

[Kyle Miller]

Fixing that, the next problem is to figure out what to do with schema.map (λ (x : (string × Type)), vector x.2 nrows, which has type list Type. That's not a type itself, so Lean has an error that a type is expected for the type of data.

[Kyle Miller]

Here's an attempt at something like the pseudocode:

import data.vector.basic

open vector

inductive Table (nrows : nat) : list (string × Type) → Type 1
| nil : Table []
| cons {name : string} {ty : Type} (data : vector ty nrows) {schema} (t : Table schema) :
  Table ((name,ty)::schema)

def t : Table 3 [("name", string), ("age", int)] :=
  Table.cons ("Alice" ::ᵥ "Bob" ::ᵥ "Charlie" ::ᵥ nil) $
  Table.cons (10 ::ᵥ 12 ::ᵥ 11 ::ᵥ nil) $
  Table.nil

[Arthur Paulino]

Not addressing the question (sorry), but just to mention that some other discussion about tables has happened here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/abstraction.20for.20tables/near/262482596
Maybe it helps

[Varun Gandhi]

@Kyle Miller Thank you, that's very helpful. I probably got confused because I was reading the docs for Lean 4, but editing code for Lean 3. Appreciate the code sample.

[Varun Gandhi]

@Arthur Paulino Thanks for the link. I will probably end up creating an alist version of vector since I want to make the columns unique, and I don't care about real-world use for now, just playing around.

[Pavel Kulko]

Hello! Is this the right forum to ask questions about Z3 theorem prover? I'm particularly interested in its Python version. Thanks

[Mario Carneiro]

Probably not, but you are welcome to try