Zulip Chat Archive

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:

  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
  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) $

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