Hand Tatami a pile of JSON with no schema. It finds the tables inside, writes a typed .mli for each one, and a loader to fill them. The data ends up in typed columns, which is what makes queries fast.
Schema inference and code generation, proved in Lean 4
Durwasa · Vimala · Vishakh
Querying JSON Is Slow. Querying Tables Is Fast.
A document has to be walked. A table can be scanned, indexed and joined. Getting from one to the other needs a schema, and the JSON never states one, so we derive it from the documents themselves:
- The types.
msis anint,rateafloat. - The nullability. Which fields can be missing, and which never are.
- The tables. What it shreds into, and the references that hold it together.
An .mli Is a Contract
A signature file sits on a boundary and says exactly what crosses it. That is the right home for an inferred schema, not a JSON-schema document some loader re-interprets at runtime.
// small.json, one job and its steps "jobs": [ { "id": 2, "os": "windows", "steps": [ { "id": 3, "name": "lint", "ms": 4516, "rate": 0.000724, "error": null }, { "id": 4, "name": "checkout", "ms": 2083, "rate": 0.000308, "error": "\"sync-web\" not found" }, { "id": 5, "name": "deploy", "ms": 98950, "rate": 0.000936 } ] } ]
(* step.mli, generated by Lean *) type t type id = int val make : id:int -> job_id:Job.id -> idx:int -> error:string option -> ms:int -> name:string -> rate:float -> t val of_job : Job.id -> t list val error : t -> string option val ms : t -> int val rate : t -> float
Read it and you know the table:
- its columns and their types;
- that
erroris the only column that can be null. It holds a string in one step,nullin another and is missing altogether from a third, so the type isstring option; - that
msisint, notint option, because the data never lacked it; of_job, the foreign key expressed as a function. It comes from the nesting, not from any field in the step;idx, the array position. A JSON array is a list; a SQL table is a set, so the ordering is lost on the way in.ORDER BY idxis what brings it back.
From Documents to Dense Typed Columns
Schemaless JSON
Objects and arrays nested to any depth. No declared shape.
Infer & Prove
Principal type per field; counts of value, null and absence.
Emit Contract
One .mli per table, plus .ml and a loader.
Stream & Shred
A table per nested level, references kept. Postgres via pgx.
Columnar Store
One dense typed array per column. Mask only where option.
Every child row keeps its parent and its array position, so the nesting survives the flattening.
The same loader fills Postgres, which lets the shredding be checked in SQL.
What Knowing Nullability Buys You
One bit per column, and it decides the whole physical layout.
A column that is never missing
- The values sit in one dense array, back to back.
- No mask, and no check before reading a value.
- 8 bytes a row, and a run of rows can be scanned as one block.
A column that can be missing
- The same values, plus a second array saying which ones are real.
- A missing slot still holds something:
0for a number,""for a string, identical to a real zero or a real empty string. - 16 bytes a row, and a check before every value.
That is all the mask is for: telling no value apart from a value that happens to be zero.
When the type says the column is never missing, there is nothing left to tell apart, so the mask is never built.
What an option Costs in Memory
Eight bytes an element against twenty four, and size is the smaller half of it.
The dense array is walked. The boxed one is chased, and the next address is unknown until the current pointer lands.
Both Stores Must Agree
The same questions, asked of three stores that all implement the same signature.
Zero disagreements, on every corpus. If each store answered a question shaped to suit it, the timings would mean nothing.
So the answers are compared first, and only then are the timings believed.
This part is tested, not proved. Lean proves the schema. That the stores answer alike is checked by running them.
Which Queries the Types Make Faster
Five queries, each touching the data a different way.
| Query | In SQL | What it touches |
|---|---|---|
| computed | SELECT sum(ms * rate) FROM step WHERE ms > n | two columns, and arithmetic over both |
| scan | SELECT count(*) FROM step WHERE ms > n | one column out of ten |
| by_status | SELECT status, max(ms) FROM step GROUP BY status | one column, grouped |
| document | SELECT * FROM repo JOIN run JOIN job JOIN step WHERE repo.id = ? | every column of one subtree, joined back together |
| three_hop | SELECT sum(step.ms) FROM step JOIN job JOIN run JOIN repo WHERE org = ? | three joins up the nesting |
Not a faster database. Two go the other way, and that is expected: rebuilding a whole record is what a row store is for.
The claim is narrower. Once the types are known, you can say which queries get faster by reading the schema, before touching a single row.
pipeline_correct, in Five Parts
223 theorems, zero sorrys, composing into one top-level statement.
| Part | What it says |
|---|---|
| Well-formedness | The output is legal OCaml. Nothing is declared twice. |
| Canonicity | Shuffle the documents and you get the same schema. Two runs agree byte for byte. |
| Structure preservation | The tables mirror the nesting exactly. No link lost, none invented, none left unreachable. |
| Principality | Every field gets the tightest type that still fits. Not a decimal for whole numbers, and not an optional column that was never empty. |
| Nullability | A field is optional exactly when some record was missing it. The option is neither absent nor gratuitous. |
It holds for any documents, not just ours. The theorem is written for any list of documents, so nothing in it is tuned to the data we tested on.
Proved, Compiled and Executed
Lean 4 does the inference and the proof. OCaml does everything after. The .mli is the only thing that passes between them, and all three stages read the same one.
- Lean 4 proves it, then writes it. For any data it accepts, the signature it emits is provably a description of that data: the tightest types, the exact nullability, the same nesting. That step carries a theorem, not a test suite.
- The generated code fills the tables. The same signature, compiled. It streams the documents into the tables and pushes the rows into Postgres, with parents and array positions intact.
- The store reads the signature again when it runs. It parses the
.mlifiles as data and picks each column's layout from what they say. Nothing is special-cased by name.
Everywhere else nullability is an input. Here it is an output.
Parquet and Arrow already skip the validity bitmap for a column that cannot be null. But somebody has to assert that flag, by hand or by sampling and guessing, and nothing checks it, even though it decides whether a bitmap exists for every row for the life of the data. We work it out from the documents instead, and prove it exact.
And the exactness survives being computed with.
A cautious analysis decays: maybe null combined with maybe null is maybe null, and a few steps later everything is optional again. Ours start out exact, so a product of two total columns is total as well and needs no mask of its own. That is why the computed query, at 3.34×, beats the plain scan at 3.21× while doing strictly more work per row.