abstraction for tables

Stream: lean4

[Arthur Paulino]

How to represent query results in Lean 4? Do we have some representation for tables that support columns with different types?

[Kyle Miller]

Is this for your project to make bindings for a database engine like MySQL? (I don't have an answer -- I just figured this context would be helpful.)

I suppose one method is to define an inductive type for the possible column types, but then you have to do dynamic type checking when you want to use one of these values. For example, having accessors for these values like SqlValue.getInt : SqlValue -> Option Int.

[Henrik Böving]

I guess you could work with a typed version of the usual formalization of relational databases here for example:

universe u v
variable (Attribute : Type u)
variable (dom : Attribute → Type v)

So you have a type where each of its values represents a specific attribute name and a domain function that can map an attribute name to the type of its values. And now if you have a QueryResult type you could have a function like:

variable (QueryResult : Type w)
variable (get : QueryResult → (a : Attribute) → dom a)

which one can use like this:

variable (res : QueryResult) (a : Attribute)
#check get res a

But this is just a typified approach of the set theory formalization for relational databases i learned in uni, I would imagine there are ways to represent this easier and more efficient? I would also imagine that this is at least a partially solved issue in the Haskell world so maybe take a look at the libraries they built around databases.

[František Silváši]

The paper A Coq Formalization of the Relational Data Model could be a reasonable starting point - Coq being a theorem prover with DTT (technically CIC), similar to Lean.

[Arthur Paulino]

Is this for your project to make bindings for a database engine like MySQL?

Yeah, exactly

[Henrik Böving]

František Silváši said:

The paper A Coq Formalization of the Relational Data Model could be a reasonable starting point - Coq being a theorem prover with DTT (technically CIC), similar to Lean.

Hey they're using something similar to my domain function \o/, seems like the database theory was useful for something after all :P

[Kyle Miller]

You might also look at how F# does things. I remember it having some interesting ways to interface with databases, and I think it has a mechanism to be able to generate mappings between its internal representation of a query and what we call a structure in Lean. I don't really understand how "type providers" work though. https://fsprojects.github.io/SQLProvider/

[Arthur Paulino]

Thanks for the ideas everyone!

[Chris B]

@Arthur Paulino

Adam Chlipala (of Certified Programming with Dependent Types fame) also did a bunch of stuff with types and SQL for ur/web. He might have written a separate paper on it, but the 'SQL' section of the manual might be of interest.

[Arthur Paulino]

Nice. I'm gonna start with something very rustic and elaborate it gradually after I become more comfortable with the FFI protocol