LeanDB: A Strongly Typed SQL Frontend

The Core Motivation: Why LeanDB?

The fundamental premise of LeanDB is that in Lean 4, your database schemas, queries, and migrations aren't just configuration files—they are types. This allows the compiler to verify the correctness of all three before a single line of code runs.

Note: This is an initial iteration. Feedback on where the implementation fails is welcome. Some examples below are explicitly marked as "does not compile" to demonstrate the compiler's protective power.

For more context, see the author's discussion on Why am I betting on Lean 4 for agentic coding?

---

A "Class Above" Functional Programming

To understand Lean, you must view languages with dependent types as a tier above standard functional programming (FP).

• In standard FP: You can treat functions as first-class citizens (passing them as arguments, combining them, etc.).
• In Lean: You can do all that, plus treat types as first-class citizens. Types can have their own inputs and parameters.

Example: Refinement Types

Consider a type for Age where the value must be less than 150. In LaTeX terms: $\text{Age} = \{ n : \mathbb{N} \mid n < 150 \}$

def Age := { n : Nat // n < 150 } 
def me : Age := ⟨34, by decide⟩ -- 'by decide' provides the proof

Attempting to bypass the rule:

• def nobody : Age := ⟨200, by decide⟩ $\rightarrow$ FAILED

Compiler Error: Tactic decide proved that the proposition 200 < 150 is false

The "Receipt" Pattern

Some validations can't happen at compile time (e.g., checking if a string is an email). Lean handles this by creating a "receipt" of validation.

def Email := { s : String // s.contains '@' } 

def Email.parse (s : String) : Option Email := 
  if h : s.contains '@' then some ⟨s, h⟩ else none 

Here, h is the proof. Once a value is typed as Email, any downstream function is guaranteed to receive a string containing an @ symbol. Validation happens once; the type carries the proof.

---

Combining and Parameterizing Types

Standard Type Composition

Lean handles structures similarly to Rust or TypeScript.

When pattern matching on a Payment, the compiler enforces exhaustiveness. If you handle .wire and .card but forget .credit, the code will not compile.

Dependent Types: The Real Power

The true leap occurs when types take other types as parameters. In LeanDB, a database row takes the schema as an input.

1. Defining the Mapping

First, we map database types to Lean types:

inductive Ty where 
  | int | text | bool 

abbrev Ty.denote : Ty → Type 
  | .int = Int 
  | .text = String 
  | .bool = Bool 

2. The Row Type

The Row is defined as a function: Row : Schema → Type.

abbrev Schema := List (String × Ty) 

inductive Row : Schema → Type where 
  | nil : Row [] 
  | cons {n : String} {t : Ty} {s : Schema} : t.denote → Row s → Row ((n, t) :: s)

Practical Application:

abbrev users : Schema := [("id", .int), ("email", .text), ("active", .bool)] 
def alice : Row users := .cons 1 (.cons "alice@example.com" (.cons true .nil))

Preventing Data Corruption

The compiler blocks invalid data entry:

1. Wrong Type: def bob : Row users := .cons "bob" ...

   Error: Argument "bob" has type String but is expected to have type Ty.int.denote

2. Missing Column: def carol : Row users := .cons 3 (.cons "carol@example.com" .nil)

   Error: Row.nil has type Row [] but is expected to have type Row [("active", Ty.bool)]

---

Proof-Based Validation vs. Agentic Errors

Consider a banking operation where you cannot withdraw more than the current balance.

structure Account where 
  id : Nat 
  balance : Nat 

def withdraw (a : Account) (amt : Nat) (_ : amt ≤ a.balance) : Account := 
  { a with balance := a.balance - amt }

The third argument is a proof. You cannot simply call withdraw; you must prove the balance is sufficient.

• Invalid Call: def overdraw (a : Account) : Account := withdraw a 1000000

  Error: Type mismatch... expected Account but got (1000000 ≤ a.balance → Account)

The Solution:

def safeWithdraw (a : Account) (amt : Nat) : Option Account := 
  if h : amt ≤ a.balance then some (withdraw a amt h) else none

Why this matters for AI: AI agents often introduce bugs where they maintain the logic but accidentally delete the validation check. With dependent types, the check isn't a "best practice"—it is a compiler requirement.

---

Advanced Queries and Schema Joins

To make this useful, we need to prove a column exists within a schema.

inductive HasCol : Schema → String → Ty → Type where 
  | here {s : Schema} {n : String} {t : Ty} : HasCol ((n, t) :: s) n t 
  | there {s : Schema} {n n' : String} {t t' : Ty} : HasCol s n t → HasCol ((n', t') :: s) n t 

Using this, we can implement a type-safe get method:

def Row.get {s : Schema} {n : String} {t : Ty} : Row s → HasCol s n t → t.denote 
  | .cons v _, .here = v 
  | .cons _ r, .there h = r.get h 

def Row.col {s : Schema} (r : Row s) (n : String) {t : Ty} (h : HasCol s n t := by repeat constructor) : t.denote := 
  r.get h

The Result:

• #eval alice.col "email" $\rightarrow$ returns a String.
• #eval alice.col "active" $\rightarrow$ returns a Bool.
• #eval alice.col "emial" $\rightarrow$ Does not compile (The compiler searches the schema, finds nothing, and throws an error).

Joining Schemas

We can compute the resulting schema of a join at the type level:

def Row.append {a b : Schema} : Row a → Row b → Row (a ++ b) 
  | .nil, r = r 
  | .cons v l, r = .cons v (l.append r)

abbrev orders : Schema := [("order_id", .int), ("total", .int)] 
def joined : Row (users ++ orders) := alice.append (.cons 17 (.cons 4200 .nil)) 

#eval joined.col "total" -- 4200