## Stream: new members

### Topic: Defining a table type

#### Varun Gandhi (Nov 25 2021 at 02:39):

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 (Nov 25 2021 at 02:47):

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 (Nov 25 2021 at 02:51):

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 (Nov 25 2021 at 03:08):

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 (Nov 25 2021 at 03:18):

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 (Nov 25 2021 at 03:37):

@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 (Nov 25 2021 at 04:14):

@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 (Nov 25 2021 at 05:53):

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

#### Mario Carneiro (Nov 25 2021 at 06:14):

Probably not, but you are welcome to try

Last updated: Dec 20 2023 at 11:08 UTC