Typed Projects (dlp)
dlp (“dl-project”) is a typed, project-based
workflow layered on top of the engine. Instead of loading untyped
facts and rules directly, you define a database schema in Dhall,
load data validated against it, and write Datalog rules whose relations are
typechecked against the schema before they compile. This
turns silent type errors into clear, early diagnostics.
dlp is a separate binary from the low-level dl CLI.
It links the engine together with the dhall-c
interpreter in-process, so the schema is typechecked and normalized without
any on-disk intermediate. The gcc core build is untouched — dlp
is opt-in via make dlp DHALLC=<path-to-dhall-c>.
Why typed schemas?
Every engine value is a u32 — either a raw integer or an interned
symbol id. Without column types, an int column and a symbol column are
indistinguishable, and a rule can silently mix them (a real correctness trap).
The typed workflow closes that gap:
- Closed world — every relation is declared in
schema.dhall; using an undeclared relation is an error that points at the schema. - Per-column types — eight built-in types spanning flat scalars (Natural, Text, Bool, Char, Date, Timestamp, Signed) and parameterized (List, Optional, Enum), checked on both data and rules.
- Rule typechecking — every rule is checked for
occurrence consistency (a variable can’t be Natural in one
atom and Text in another), with
file:line:coldiagnostics. - Typed data loading — CSV/JSON rows are validated and coerced per column before they enter the store.
For example, the rule tc(A, W) :- weight(A, W). is rejected:
W is Natural in weight.w but
Text in tc.dst — a bug the untyped engine would
silently mis-evaluate.
Project layout
A database project is a directory with a few conventional subdirectories:
mydb/
schema.dhall # the typed schema (the contract)
data/ # EDB CSV/JSON inputs, file stem = relation name
rules/ # .datalog rule files (concatenated, sorted)
.build/ # dlp-owned: build snapshot, schema.json echo
The schema DSL
The schema is Dhall-as-data: self-contained lets
with a final : Schema annotation. Each relation declares its
name, arity, and per-column type. The column-type union spans flat
scalars (all raw u32: Natural, Text /
interned symbol, Bool, Char, Date
=yyyymmdd, Timestamp =epoch seconds, Signed =i32
zigzag) and parameterized types (List /
Optional of a flat element type, and Enum with a
fixed value set). The column-type union uses an empty-record payload
to tag a flat type, and a payload record to carry a parameterized type’s
element type / value set:
let Elem = < Natural : {=} | Text : {=} | Bool : {=} | Char : {=} |
Date : {=} | Timestamp : {=} | Signed : {=} >
let ColumnType = < Natural : {=} | Text : {=} | Bool : {=} | Char : {=} |
Date : {=} | Timestamp : {=} | Signed : {=} |
List : { elem : Elem } | Optional : { elem : Elem } |
Enum : { values : List Text } >
let Column = { name : Text, type : ColumnType }
let Relation = { name : Text, columns : List Column }
let Schema = { relations : List Relation }
in { relations =
[ { name = "node", columns = [ { name = "id", type = < Text = {=} > },
{ name = "tags", type = < List = { elem = < Text = {=} > } > },
{ name = "nick", type = < Optional = { elem = < Text = {=} > } > },
{ name = "color", type = < Enum = { values = [ "red", "green" ] } > } ] } ]
} : Schema
Coercion is per-type on load: Text/Enum interned,
Natural ^[0-9]+$ ≤ 4294967295, Bool
true/false/0/1 (CSV) or a JSON boolean, Char one
Unicode codepoint, Date yyyy-mm-dd,
Timestamp unix-seconds integer, Signed signed i32,
List a JSON array or a bracketed quoted CSV cell
[a,b,c], Optional JSON null or an empty
CSV cell.
Arity is the length of columns (1–8, enforced by the tool).
Relations that appear as rule heads are IDB (derived); loading data
into them is an error.
Commands
| Command | Does |
|---|---|
dlp init [dir] | Scaffold a project directory with an example schema. |
dlp schema [dir] | Dhall-typecheck + normalize schema.dhall and print the typed relations. |
dlp check [dir] | Validate schema + typecheck rules + dry-run data. No writes — the CI command. |
dlp build [dir] | Check, then build a snapshot under .build/ (declare EDB, load data, compile, publish). |
dlp query [dir] 'goal' | Build in-process and evaluate a goal, e.g. 'tc(alice, X)'. |
Data files are matched to schema columns by name (any order):
CSV headers map to columns; JSON is an array of objects. CSV is text-typed
(Text takes any cell verbatim; Natural requires
^[0-9]+$ ≤ 4294967295). JSON is strict (number →
Natural, string → Text).
Catching the bug
A mixed-type rule fails dlp check and dlp build with
a precise diagnostic (here <input> is the rule file):
$ dlp check .
rules/reach.datalog: <input>:1:19: variable W is Natural here (weight) but Text at <input>:1:6 (tc)
Data validation reports the exact row and column, e.g.
weight.csv:3:2: column 'w' expects Natural, got "heavy".
Building dlp
dlp is an opt-in cosmocc build (the default gcc make /
make test never touch it or dhall-c). With dhall-c as a sibling
repo:
make dlp DHALLC=../dhall-c # builds dlp/dlp
make dlp-golden # end-to-end golden test (check/build/query)