Sophia

Graph Schema

6 min read

design definition

Sources: original to this vault (design and analysis; no single paper); Patterson, Lynch & Fairbanks, Categorical Data Structures for Technical Computing, arXiv:2106.04703; Schultz, Spivak, Vasilakopoulou & Wisnesky, Algebraic Databases, arXiv:1602.03501; code: schema.rs, Store.jl

Theory (CT-ML wiki): Attributed C-Set · Algebraic Database · Data Migration Functor · Provenance Semiring

What the nodes and edges actually are. This is the schema The Original Idea invites anyone to disagree with and migrate away from, so it is written to be replaceable: nothing outside this note and schema should know the concrete labels.

Universal node properties

Every node carries:

PropertyMeaning
hthe 256-bit identity from Hashing and Identity — primary key
kindnode tag (see below), also mixed into h
verhash schema version
payloadkind-specific attributes, canonically encoded

Nodes are immutable and append-only. There is no UPDATE in this system; there are only new nodes and new edges, and names that point somewhere else (Naming and Change Propagation). This is what makes the store re-verifiable without being trusted (Trusted Computing Base).

Node kinds

Core layer — the language of Core Calculus:

  • Term — a core term node (app, lam, pi, let, con, elim, prim, var, …, discriminated in payload)
  • Type — a Term occurring in type position; kept as a separate label purely so type-level queries are cheap
  • Decl — a named, top-level definition: binds a Term to a Type with an effect row
  • Sig — a type signature/interface with no body, for declarations from headers or extern
  • Effect — an effect row or a single effect constructor
  • Universe — a universe level

Surface layer — per-frontend, one sub-schema each:

  • SurfaceNode — a node of a source language’s own AST, before elaboration (lang in payload)
  • Token / Span — lexical provenance, never hashed into the core identity
  • Frontend — the extractor version that produced a surface tree

IR layers:

  • Op — an MLIR Operation: dialect-qualified name, operands, results, attributes, regions
  • Region, Block, Value — MLIR’s nesting structure
  • Instr, BasicBlock, Func, Module — LLVM IR level
  • Target — a target triple + datalayout + CPU features; lowering is only meaningful relative to one

Knowledge layer — nodes that are not compiled:

  • Witness — evidence for an equivalence or a property (Equivalence and Witnesses)
  • Prop — a proposition (a Type in the Prf fragment)
  • Test — an executable test attached to a definition (Tests and Documentation as Nodes)
  • Bench — a benchmark plus recorded results
  • Doc — markdown, a comment, a docstring
  • Name — a human-readable label in a namespace; mutable pointer, the one exception to immutability
  • Author / Signature — provenance for asserted (unproved) claims

Edge kinds

Edges are themselves content-addressed: ℎ(edge)=𝐻(ver‖EDGE‖kind‖ℎ(src)‖ℎ(dst)‖ord‖attrs). This matters because a witness needs to cite edges, and you cannot cite what has no identity.

EdgeFrom → ToNotes
CHILD(i)Term → Termordered structural child; the spine of every AST
HAS_TYPETerm → Type
DEPENDS_ONDecl → Decltransitive closure precomputed and materialised
ELABORATES_TOSurfaceNode → Termthe frontend’s output, one per (node, frontend version)
LOWERS_TOTerm → Op → Instrcarries the Target and pass pipeline in attributes
SPECIALIZESDecl → DeclJulia’s per-signature specialisation, C++ template instantiation
INSTANCE_OFDecl → Sigimplementation of an interface
EQUIV(level, modulo)Term ↔ Termthe load-bearing one; see below
REFINESTerm → Termone-directional: a may be used where b was, not conversely
WITNESSED_BYEQUIV edge → Witnessedges pointing at edges; hence hashed edges
PROVESWitness → Prop
TESTSTest → Decl
DOCUMENTSDoc → any
NAMEDName → anymutable; the only mutable relation
MIGRATES_TOnode@ver1 → node@ver2hash-schema migration (Hashing and Identity)
EMITSModule → artifact blob
SurfaceNodeTermOpInstrDocTypeTerm0ELABORATESTOLOWERSTOHASTYPEEQUIVLOWERSTODOCUMENTSHASTYPEWITNESSEDBY

The EQUIV edge in detail

EQUIV carries two attributes that do all the work:

  • level ∈ {alpha, defeq, rewrite, observational, tested, asserted} — strength, totally ordered
  • modulo ⊆ {alloc, timing, fp_assoc, fp_contract, exception_identity, gc_pressure, ordering} — what the claim ignores

Composition of two EQUIV edges takes the minimum level and the union of moduli. A transitive chain therefore degrades monotonically, which is the honest behaviour; see Equivalence and Witnesses for why union-of-moduli is a real problem and not a formality.

The schema as a category

The node and edge kinds above form an attributed C-set schema: each kind is a table, CHILD(i) is a table with two foreign keys and a position attribute, hashes and payloads are attributes with fixed value types. Read this way, a frontend’s output is an instance, schema migration (MIGRATES_TO) is a data migration functor, e-matching is a conjunctive query, and Catlab’s generic limits, colimits and homomorphism search work on the store without schema-specific code — a cheap way to prototype the schema before committing to a backend.

Mapping onto concrete backends

The schema above is abstract. Three plausible materialisations, matching the candidates in State of the Art - Graph Databases for Code:

Relational (DuckDB / Turso / SQLite) — two wide tables and a name table:

CREATE TABLE node (h BLOB PRIMARY KEY, kind SMALLINT, ver SMALLINT, payload BLOB);
CREATE TABLE edge (h BLOB PRIMARY KEY, src BLOB, dst BLOB, kind SMALLINT,
                   ord INTEGER, attrs BLOB);
CREATE TABLE name (ns TEXT, name TEXT, target BLOB, valid_from BIGINT, valid_to BIGINT);
CREATE INDEX edge_src ON edge(src, kind, ord);
CREATE INDEX edge_dst ON edge(dst, kind);

Structural queries become recursive CTEs. This is unglamorous and probably the right first choice: a columnar engine over two tables with a hash primary key is extremely fast for the “fetch a whole subtree” and “which definitions transitively depend on h” queries that dominate, and it has no server. See Query Cookbook.

Property graph (FalkorDB / Neo4j-compatible) — labels map to node kinds directly, Cypher expresses traversal natively, and variable-length path queries (-[:DEPENDS_ON*]->) are first class. Better ergonomics, worse embeddability.

Typed/deductive (TypeDB, or Datalog over any store) — the schema’s type discipline is enforced by the database, and derived facts (transitive dependency, equivalence closure, dead-code reachability) are rules rather than materialised tables. Architecturally the closest fit to Compilation as Query, and the closest relative of egglog.

The recommendation is to implement a backend trait and start with DuckDB, because the schema is simple enough that the graph-specific features earn their keep only later.

Scale estimate

A 100k-line Julia package elaborates to roughly 106–107 core Term nodes. Lowering to MLIR multiplies by ~3–10; LLVM IR by another ~2–5. So a mid-sized package is 107–108 nodes if all IR layers are persisted for one target. That is large but not exotic for a columnar store — and it is the main argument for making IR-layer persistence optional and cache-like rather than mandatory. See Open Problems and Risks.

Garbage collection

Append-only stores grow. Reachability is from the Name table (the roots) plus pinned hashes; anything unreachable and older than a retention window is collectable. Note that deleting a node is safe precisely because identity is content-derived: if it is ever needed again it can be regenerated with the same hash.

Graph View

Backlinks