GoKawiilLeanDB: A strongly typed SQL Frontend
Why?
Because in Lean 4 your schema, your queries and your migrations can all be types, and the compiler checks all three.
This post has three jobs. Communicate that a strongly typed SQL frontend can exist. Explain why it might be valuable. Show the first cut so that you can tell me where it is wrong.
Every code example below compiles on Lean 4.33. The ones marked "does not compile" really do not, and I have pasted what the compiler says.
First, why Lean?
Also see my post Why am I betting on Lean 4 for agentic coding? from December last year.
You should think of Lean, and other languages with dependent types, as a class above functional programming languages.
In functional programming languages you can pass around functions, combine functions, have one function as the input of another.
In Lean, your types are first class objects. You can create abstract types, combine types, pass around types, and your types themselves can have inputs and parameters. And the compiler enforces all of that.
... continue reading