Lean SQL initiatives

Stream: lean4

[Arthur Paulino]

Ah, just in case someone's wondering, @Florian Würmseer and I have a plan to deduplicate code. We're both exploring our own ideas to better understand their pros and cons and then we will extract common code to a separated Lean 4 package

[Arthur Paulino]

One difference between Florian's syntax and mine is that the former uses strings and the later uses identifiers. Example:

• Florian's syntax accepts SELECT "c" FROM "t"
• My syntax accepts SELECT c FROM t

What do you guys think? Which one is more appropriate?

[Henrik Böving]

Second

[Sebastian Ullrich]

Note that if you're planning to eventually move on to a statically-typed representation, there is a very good reason for why C# puts from in front of select: it is the correct order for auto completion

[Arthur Paulino]

Do you mean auto completing column names?

[Martin Dvořák]

Extremely minimalistic example:
https://github.com/madvorak/leanq/blob/c0c072ef94f6e8ed827841da158f0729420679e4/Main.lean#L5
If people are interested in LINQ for Lean 4, perhaps I could work on it in my free time.

[Arthur Paulino]

If I were gonna work on this these days, I would implement bindings to DuckDB or Polars. These systems scale remarkably well.

[Max Nowak 🐉]

Just for completeness sake: For a Lean4 intro talk, I showed a simple example involving some SQL. I'd be potentially interested in expanding that into a whole thing.

[Martin Dvořák]

/poll What do you like better?
SQL
LINQ