Guide

Install

require ladybug from git "https://github.com/Volland/ladybug-lean" @ "v0.1.0"

Two libraries come with the package:

The first build downloads the LadybugDB release named in lbug.lock for your platform into .lake/lbug/. The shim loads it at runtime from there, so executables need no library path. lake run lbug-update moves the lock to the latest release; LBUG_LIB_DIR builds against a local Ladybug build; LBUG_LIBRARY overrides the library file at runtime. On Windows the C shim needs MinGW-w64 gcc (for example from MSYS2 UCRT64); CC overrides the compiler.

Declaring tables

A table is an ordinary Lean structure. node_table and rel_table check every field's type when the file compiles and generate the rest.

structure Person where
  id   : Int64
  name : String
  age  : Option Int64

structure Company where
  name    : String
  founded : Int32

structure WorksAt where
  since : Int64

structure Knows                      -- a relationship without properties

node_table Person                    -- label "Person", key `id`
node_table Company (key := name) (label := "Org")
rel_table WorksAt (from := Person) (to := Company)
rel_table Knows (from := Person) (to := Person)

def schema : Schema := [.ofNode Person, .ofNode Company, .ofRel WorksAt, .ofRel Knows]

Each command generates encoders and decoders, the table metadata behind ddl Person and applySchema, and two companion structures used in queries:

• Person.Var: a matched person, whose fields are typed expressions, so p.name : Expr String and p.age : Expr (Option Int64);
• Person.OptVar: the same after OPTIONAL MATCH, with every field nullable.

Column types are Bool, every signed and unsigned integer width, Int (INT128), Float, Float32, String, ByteArray, Uuid, Date, Timestamp, Interval, Option α, Array α, Embedding n and structures that derive Ladybug.CypherType. A field of another type, a missing key or an Option key is a compile error naming the field.

structure Bad where
  id : Int64
  f  : Nat → Nat
node_table Bad

node_table Bad: field 'f' has type Nat → Nat, which is not a column type (no Ladybug.CypherType instance)

The query builder

Queries are built in QueryM, a monad that appends clauses and returns typed variables. query turns a builder that ends in return_ into a Query α, whose rows have type α; stmt builds a Statement that returns nothing.

def colleagues : Query (String × String × Int64) := query do
  let p ← match_ (node Person)
  let (w, c) ← match_ (out p WorksAt (node Company))
  where_ (w.since >=. 2020 &&. c.founded <. 2000)
  orderBy p.name
  limit 10
  return_ (p.name, c.name, w.since)

def birthday (pid : Int64) : Statement := stmt do
  let p ← match_ (node Person)
  where_ (p.id ==. lit pid)
  set p.age (p.age +. 1)               -- a NULL age stays NULL

Operators end in a dot: ==. !=. <. <=. >. >=. &&. ||. +. -. *. /. %. ++.. Functions live in Expr: Expr.count, sum, avg, min, max, collect, isIn, startsWith, contains, lower, upper, size and more. Numerals and lit x are literals, and every literal is sent as a query parameter, never as text.

colleagues.print
-- ("MATCH (n0:Person) MATCH (n0)-[r1:WorksAt]->(n2:Org)
--   WHERE (r1.since >= $p0) AND (n2.founded < $p1)
--   RETURN n0.name, n2.name, r1.since ORDER BY n0.name LIMIT $p2",
--  #[("p0", 2020), ("p1", 2000), ("p2", 10)])

NULL and three-valued logic

Nullability is in the types. A property declared Option τ is an Expr (Option τ), every property of an OPTIONAL MATCH variable is nullable, and so are sum, avg, min and max (they are NULL over no rows). Comparisons and connectives have type Expr (Option Bool), where none is Cypher's unknown, and WHERE keeps only the rows that are true.

where_ (p.age >. 30)                      -- unknown for a NULL age: the row is dropped
where_ (p.age >. 30 ||. p.name ==. lit "Ann")   -- unknown OR true is true
return_ (coalesce p.age 0)                -- Expr Int64: no longer nullable
where_ (isTrue (p.age >. 30))             -- unknown becomes false

Decoding never surprises you: a nullable expression decodes to Option τ, and a NULL in a column you declared non-nullable is a .decode error that names the column.

cypher%

Write Cypher directly. The elaborator checks every label and property against your tables and translates each clause into the builder call that expresses it, so the typing and the printed query are exactly the builder's.

def minAge : Int64 := 30

def adults := cypher%
  MATCH (p:Person)-[w:WorksAt]->(c:Org)
  WHERE p.age > $minAge AND c.name STARTS WITH "A"
  RETURN p.name, c.name, w.since ORDER BY w.since DESC LIMIT 5
-- adults : Query (String × String × Int64)

• Clauses: MATCH, OPTIONAL MATCH, WHERE, WITH, RETURN with ORDER BY/SKIP/LIMIT, UNWIND, CREATE, MERGE, SET, DELETE, DETACH DELETE, CALL for vector and text search, UNION / UNION ALL.
• Patterns: (a:A)-[r:R]->(b:B), <-[…]-, -[…]-, ranges *1..3, * SHORTEST 1..5, * ALL SHORTEST 1..5, path variables p = (…); an end node without a label takes the relationship's endpoint.
• Expressions: comparisons, AND/OR/XOR/NOT, IS [NOT] NULL, STARTS WITH, ENDS WITH, CONTAINS, IN, arithmetic, lists, aggregates, coalesce, EXISTS { MATCH … }, COUNT { MATCH … }.
• $x is the Lean local x and $(e) any Lean term, both as parameters.
• Keywords may be upper, lower or capitalized. Strings are Lean string literals, "Ann". Clauses after the first must start at or right of its column, so the query ends where the indentation does.

The repository

For the everyday operations you don't need a query at all. The Repo functions are generic over the backend and typed by your tables; keys have the type of the key field.

Repo.insert (Person.mk 1 "Ann" (some 30))        -- .constraint if the key exists
Repo.upsert { ann with name := "Ann B." }          -- MERGE on the key, overwrite the rest
let ann? ← Repo.get? Person (1 : Int64)            -- Option Person
let seniors ← Repo.findWhere Person fun p => p.age >. 60
Repo.update { ann with age := some 31 }            -- .notFound if there is none
Repo.delete Person (1 : Int64)                     -- .constraint if it still has relationships
Repo.detachDelete Person (1 : Int64)

Repo.link (1 : Int64) (WorksAt.mk 2020) "ACME"     -- endpoints by key, typed by WorksAt
let jobs ← Repo.outgoing WorksAt (1 : Int64)       -- Array (Company × WorksAt)
let staff ← Repo.incoming WorksAt "ACME"           -- Array (Person × WorksAt)
let rels ← Repo.between WorksAt (1 : Int64) "ACME"
Repo.unlink WorksAt (1 : Int64) "ACME"

Repo.insertMany people (batchSize := 1000)         -- one UNWIND query per batch
Repo.upsertMany people
Repo.linkMany #[((1 : Int64), WorksAt.mk 2020, "ACME")]
Repo.copyNodes Person "people.csv"                 -- native: CSV with a header, or Parquet

The repository is deliberately small: no identity map, lazy loading or change tracking. Wrap batches in withTx to make a load atomic.

Paths, subqueries, unions

-- every person within one to three Knows hops, with the paths
let (path, friend) ← matchPaths p Knows (node Person) (max := 3)
return_ (friend.name, pathLength path)          -- path : Expr (Path Person Knows)

let (path, b) ← shortestPath a Knows (node Person) (max := 6)
let (path, b) ← allShortestPaths a Knows (node Person) (max := 6)

where_ (← exists_ (discard (match_ (out p WorksAt (node Company)))))
let reports ← countSub (discard (match_ (inc p Knows (node Person))))

(namesOfPeople.union namesOfCompanies)          -- both must be Query String

Variable-length patterns need an upper bound (max has no default, and Ladybug allows at most 30), so every path query terminates on both backends. A path decodes to Path N R with its nodes, endpoints included, and its relationships.

Vector and text search

structure Doc where
  id   : Int64
  text : String
  emb  : Embedding 384                 -- FLOAT[384]

node_table Doc

runStmt (createVectorIndex Doc "doc_vec" "emb" (metric := .cosine))
runStmt (createFtsIndex Doc "doc_fts" ["text"])

let hits ← runQueryM do
  let (d, dist) ← vectorSearch Doc "doc_vec" queryEmbedding (k := 10)
  where_ (d.id >. 100)                 -- combine with ordinary predicates and patterns
  orderBy dist
  return_ (d.text, dist)

let found ← runQueryM do
  let (d, score) ← ftsSearch Doc "doc_fts" "graph memory"
  orderByDesc score
  return_ d.id

The native backend installs and loads LadybugDB's vector and fts extensions the first time a query needs them. Embedding.ofArray? builds an embedding only from exactly n numbers.

Backends and transactions

Write against [MonadGraph m] and choose the backend when you run:

def onboard {m : Type → Type} [MonadGraph m] (p : Person) : m Unit := withTx do
  Repo.upsert p
  Repo.link p.id (WorksAt.mk 2026) "ACME"

-- LadybugDB
def main : IO Unit := Ladybug.withDatabase "company.lbug" fun db => db.withConnection do
  applySchema schema
  onboard ⟨3, "Cid", none⟩

-- in memory: pure, works in #eval and in tests
#eval (do applySchema schema; onboard ⟨3, "Cid", none⟩; Repo.findAll Person : MemM _).run' {}

• runQuery, runStmt, runQueryM, runStmtM: run a typed query or statement.
• withTx and withReadTx: commit on success, roll back on any error; a nested bracket is a .transaction error.
• applySchema creates missing tables; verifySchema lists the differences between your declarations and the database.
• MemM keeps the database in a pure value and interprets queries with Ladybug's semantics; a differential suite checks it against Ladybug.

Native extras

let rows ← queryAs (String × Int64) "MATCH (p:Person) RETURN p.name, p.age" -- raw Cypher text
exec "CREATE NODE TABLE Tag(name STRING, PRIMARY KEY(name))"
let r ← queryRaw "RETURN $x + 1 AS y" #[param "x" (41 : Int64)]
withTimeout 500 (runQuery heavyQuery)          -- .timeout when exceeded
conn.interrupt                                  -- from another task: .interrupted
loadExtension "algo"

Structures that deriving FromRow decode raw results by column name; tuples and scalars decode by position.

Errors

Every failure is a Ladybug.Error, caught with ordinary try … catch in the monad:

Behaviour to know

• The in-memory backend follows Ladybug where openCypher leaves a choice: NULL sorts as the largest value, x IN [.., NULL] is false, integer / and % truncate toward zero, variable-length patterns may repeat relationships, an undirected pattern matches a self-loop twice, and shortest paths never return to their start.
• Its full-text search uses BM25 and a Porter stemmer: the same documents as Ladybug for ordinary queries, but not the same scores.
• Ladybug has no CALL { … } subqueries, so neither does the typed language.
• A union value's member name is empty when the union has more than one member, because the C API does not report it.
• Timeouts and interrupts take effect between Ladybug's units of work, so one long step can overrun a timeout.