ladybug : Lean
Typed property graphs for Lean 4. Use the LadybugDB embedded graph database from Lean, with a schema the compiler knows, Cypher it checks, and an in-memory twin of the database for #eval and tests.
The schema is a type
In LadybugDB the schema is the ontology, and the database enforces it when you write. ladybug-lean moves that enforcement to compile time: your node and relationship tables are Lean structures, and every query is checked against them before it runs.
structure Person where
id : Int64
name : String
age : Option Int64 -- nullable column
structure Company where
name : String
structure WorksAt where
since : Int64
node_table Person -- key `id`
node_table Company (key := name)
rel_table WorksAt (from := Person) (to := Company)CREATE NODE TABLE IF NOT EXISTS Person(
id INT64, name STRING, age INT64,
PRIMARY KEY(id))
CREATE NODE TABLE IF NOT EXISTS Company(
name STRING, PRIMARY KEY(name))
CREATE REL TABLE IF NOT EXISTS WorksAt(
FROM Person TO Company, since INT64)Queries that don't fit the schema don't compile
Write Cypher as you know it, or build the same query in a monad. Both produce one typed AST, and both know the result type.
def employees : Query (String × Option String) :=
cypher% MATCH (p:Person) OPTIONAL MATCH (p)-[:WorksAt]->(c:Company)
RETURN p.name, c.name ORDER BY p.name
def seniors : Query String := query do
let p ← match_ (node Person)
where_ (p.age >. 60) -- p.age : Expr (Option Int64)
return_ p.nameA typo, a type mismatch or a pattern the schema forbids is an error at the token that causes it:
example := cypher% MATCH (p:Person) RETURN p.nmaeunknown property 'nmae' of table Person; did you mean 'name'?
example := query do
let c ← match_ (node Company)
let _ ← match_ (out c WorksAt (node Person)) -- WorksAt goes Person → Company
return_ c.namefailed to synthesize instance of type class Matchable (PatOut Company.Var WorksAt (NodeRef Person)) …
What's in the box
Typed Cypher
A monadic builder and a cypher% syntax over one AST. NULL is in the types, with Cypher's three-valued logic. Every Lean value becomes a query parameter, never query text.
Repository
Repo.insert, upsert, get?, update, delete, link, outgoing, batched insertMany and CSV/Parquet import, all typed by your tables.
Graph queries
Variable-length and shortest paths as typed Path values, EXISTS and COUNT subqueries, and UNION of queries with the same result type.
Search
Embedding n columns, vector indexes and nearest-neighbour queries, and full-text indexes, combined with graph patterns in one query.
Two backends
Code written against MonadGraph runs on LadybugDB (LbugM) or on a pure in-memory graph (MemM). The in-memory one works in #eval.
Checked against Ladybug
A differential suite runs generated queries on both backends and shrinks any disagreement, and property tests round-trip every column type.
One program, two backends
def demo {m : Type → Type} [MonadGraph m] : m (Array (String × Option String)) := do
applySchema [.ofNode Person, .ofNode Company, .ofRel WorksAt]
Repo.insert (Person.mk 1 "Ann" (some 41))
Repo.insert (Person.mk 2 "Bob" none)
Repo.insert (Company.mk "ACME")
Repo.link (1 : Int64) (WorksAt.mk 2020) "ACME"
runQuery employees
#eval (demo : MemM _).run' {} -- pure, in the editor
def main : IO Unit := -- on a LadybugDB file
Ladybug.withDatabase "company.lbug" fun db => db.withConnection do
IO.println (← demo)Except.ok #[("Ann", some "ACME"), ("Bob", none)]
Install
require ladybug from git "https://github.com/Volland/ladybug-lean" @ "v0.1.0"The first build downloads the official LadybugDB library for your platform (macOS, Linux, Windows; x86_64 and arm64), and the library is loaded at runtime, so there is no rpath to set. Lean v4.35.0. On Windows the build needs MinGW-w64 gcc.