Type-safe PostgreSQL bindings for Lean 4 via libpq FFI.

Compile-time column verification · Permission-tracked queries · Structural injection prevention

---

lean-pq makes invalid database operations a compile-time error. Column references carry proofs, permissions are tracked in the type system, and user values are structurally separated from SQL — no runtime checks, no overhead.

Compile-time column verification

Column references in queries carry a proof that the column exists in the schema. Reference a column that doesn't exist and the code won't compile.

def users : TableSchema :=
  { name := "users"
    columns := [
      { name := "id",    type := .serial,  nullable := false },
      { name := "name",  type := .text,    nullable := false },
      { name := "email", type := .text,    nullable := false },
      { name := "age",   type := .integer, nullable := true }
    ] }

-- Compiles: "name" exists in the schema
def valid : Expr users.columns := .col "name" (by decide)

-- Won't compile: "phone" is not a column
-- def bad : Expr users.columns := .col "phone" (by decide)

The by decide tactic evaluates the membership check at compile time. No reflection, no runtime cost — the proof is erased after elaboration.

Try it live — uncomment the bad definition to see the compile error.

Permission-tracking monad

PqM perm α tracks the permission level in the type. SELECT operations live in readOnly, INSERT/UPDATE/DELETE in dataAltering, DDL in admin. Lower permissions lift into higher contexts automatically, but the reverse is a type error.

-- Compiles: SELECT lifts into dataAltering context
def migrate : PqM .dataAltering Unit := do
  let rows ← PqM.query (pq! select schema)    -- readOnly, lifts up
  let _ ← PqM.execModify "INSERT INTO ..."     -- dataAltering, matches
  pure ()

-- Won't compile: can't use INSERT in a readOnly context
-- def oops : PqM .readOnly Unit := do
--   let _ ← PqM.execModify "INSERT INTO ..."

Permissions are a compile-time artifact — erased at runtime with zero overhead. The PqM monad is a reader over the connection handle, and MonadLift instances handle the subtyping.

Try it live — uncomment unsafeOp to see the permission violation.

Structural SQL injection prevention

User values never appear in the SQL string. The query AST renders all literals as $1, $2, ... parameters, making SQL injection structurally impossible — not by escaping, but by construction.

-- Malicious input is safely contained in the parameter array
let userInput := "Robert'; DROP TABLE users;--"
let q := pq! select users | name = userInput
let (sql, params) := q.render
-- sql:    "SELECT * FROM users WHERE (name = $1)"
-- params: #["Robert'; DROP TABLE users;--"]

Try it live — run it to see the injection attempt safely contained.

The pq! macro

A SQL-like DSL that expands to the typed Query AST at compile time. Column names are verified against the schema, values become parameters, and the required permission level is inferred.

open LeanPq.Syntax

let products : TableSchema := { name := "products", columns := [
  { name := "id",       type := .serial,                    nullable := false },
  { name := "name",     type := .text,                      nullable := false },
  { name := "price",    type := .numeric (some 10) (some 2), nullable := false },
  { name := "in_stock", type := .boolean,                   nullable := false }
] }

-- SELECT with WHERE, ORDER BY, LIMIT
pq! select products [name, price] | price > "5.00" orderby price desc limit 10
-- → "SELECT name, price FROM products WHERE (price > $1) ORDER BY price DESC LIMIT 10"
--   params: #["5.00"]

-- INSERT
pq! insert products [name, price, in_stock] ["Widget", "9.99", true]
-- → "INSERT INTO products (name, price, in_stock) VALUES ($1, $2, TRUE)"
--   params: #["Widget", "9.99"]

-- UPDATE with WHERE
pq! update products [price := "12.99"] | name = "Widget"
-- → "UPDATE products SET price = $1 WHERE (name = $2)"

-- DELETE, CREATE, DROP
pq! delete products | name = "Widget"
pq! create products
pq! drop_if_exists products

Expressions support =, !=, >, <, >=, <=, &&, ||, !, like, ilike, is_null, is_not_null.

Full CRUD example

import LeanPq

open LeanPq
open LeanPq.Syntax

def main : IO Unit :=
  PqM.withConnectionIO (perm := .admin) "host=localhost dbname=mydb" do
    let schema : TableSchema :=
      { name := "users"
        columns := [
          { name := "id",    type := .serial,  nullable := false },
          { name := "name",  type := .text,    nullable := false },
          { name := "email", type := .text,    nullable := false }
        ] }

    let _ ← PqM.execQuery (pq! drop_if_exists schema)
    let _ ← PqM.execQuery (pq! create schema)

    let _ ← PqM.execQuery (pq! insert schema [name, email] ["Alice", "alice@example.com"])
    let _ ← PqM.execQuery (pq! insert schema [name, email] ["Bob", "bob@example.com"])

    let rows ← PqM.query (pq! select schema [name] | name = "Alice")
    PqM.liftIO (IO.println s!"Found: {rows}")   -- [["Alice"]]

    let _ ← PqM.execQuery (pq! update schema [email := "new@example.com"] | name = "Bob")
    let _ ← PqM.execQuery (pq! delete schema | name = "Bob")
    let _ ← PqM.execQuery (pq! drop_if_exists schema)

Async queries

Each concurrent query runs on its own connection via Lean tasks. No locks, no shared mutable state.

-- Run three queries in parallel, each on a fresh connection
let results ← PqM.concurrent conninfo [
  do let r ← PqM.execSelect "SELECT count(*) FROM orders;";  PqM.fetchAll r,
  do let r ← PqM.execSelect "SELECT count(*) FROM users;";   PqM.fetchAll r,
  do let r ← PqM.execSelect "SELECT count(*) FROM products;"; PqM.fetchAll r
]

-- Spawn a background query and await it later
let task ← PqM.spawnOnNewConn conninfo do
  let r ← PqM.execSelect "SELECT * FROM large_table;"
  PqM.fetchAll r
-- ... do other work on the current connection ...
let rows ← PqM.await task

-- Run two queries concurrently, get both results
let (users, orders) ← PqM.both conninfo
  (do let r ← PqM.execSelect "SELECT * FROM users;"; PqM.fetchAll r)
  (do let r ← PqM.execSelect "SELECT * FROM orders;"; PqM.fetchAll r)

Setup

Prerequisites

• Lean 4 (v4.24.0+)
• libpq — brew install libpq (macOS) or apt install libpq-dev (Ubuntu)
• pkg-config

Add to your project

In your lakefile.lean, add lean-pq as a dependency:

require leanpq from git "https://github.com/user/lean-pq" @ "main"

Build and test

lake build                                       # build library
docker compose -f Tests/docker-compose.yml up -d  # start test database
lake test                                         # run test suite

Architecture

LeanPq/
  Extern.lean    — @[extern] FFI declarations (Handle, PGresult, ~80 libpq bindings)
  extern.c       — C implementations wrapping libpq with Lean external classes
  Error.lean     — LeanPq.Error inductive type
  DataType.lean  — PostgreSQL data type model (Chapter 8)
  Schema.lean    — Column, TableSchema, decidable hasCol
  Monad.lean     — PqM permission-tracking monad
  Query.lean     — SQL AST with schema-indexed expressions, parameterized rendering
  Syntax.lean    — pq! macro DSL
  Async.lean     — PqTask, spawnOnNewConn, concurrent, both

Opaque Handle and PGresult types wrap C pointers with finalizers — the Lean GC calls PQfinish/PQclear automatically. Enum types (ConnStatus, ExecStatus) have constructors ordered to match PostgreSQL's C enum ordinals exactly.