datalog-dafsa

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:

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

CommandDoes
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)