Make your database speak Lean
Typed schemas, typed queries, typed transactions and typed results, from a single definition.
typedb-lean connects TypeDB 3, the polymorphic graph database, with Lean 4, the language that proves things. Your schema, queries, transactions and results all have types the compiler checks, and it reads data as fast as the official Rust driver.
require «typedb-lean» from git "https://github.com/Volland/typedb-lean" @ "v0.1.0"
@[typedb "person"]
structure Person where
email : Key String -- owns email @key
name : String -- owns name @card(1..1)
age : Option Int64 := none
deriving Entity
structure Friendship where
a : Role "friend" (Ref Person)
b : Role "friend" (Ref Person)
since : Std.Time.PlainDate
deriving Relationdef befriend : Tx .write Unit := do
let ann ← Entity.insert
{ email := "ann@example.com", name := "Ann" : Person }
let bob ← Entity.insert
{ email := "bob@example.com", name := "Bob" : Person }
discard <| Relation.insert
{ a := ann, b := bob,
since := Std.Time.PlainDate.ofYearMonthDayClip 2021 3 14 : Friendship }
-- commits on success, rolls back on any error
d.runSync "social" .write befriendstructure FriendOf where
name : String
friend : String
deriving FromRow
def friendsOf (who : String) : Tx .read (Array FriendOf) :=
query typeql!"match
$x isa person, has name {who}, has name $name;
$f isa friendship, links (friend: $x, friend: $y);
$y has name $friend;"{who} is escaped, so user input can never change the query.def migrations : List Migration := [
Migration.define 1 "social schema"
[TypeSpec.of Person, TypeSpec.of Friendship],
Migration.tql 2 "nicknames"
"define attribute nickname, value string;
person owns nickname;"
(down := some "undefine owns nickname from person; nickname;")
]
let applied ← d.migrateSync "social" migrations
d.runSync "social" .read (Schema.verify! schema)TypeDB types your data. Lean types your program. Most clients throw both away at the boundary. typedb-lean keeps them and connects them.
typeql! queries carry the transaction mode they needToTypeQLderiving FromRowTx .read does not compileDecimal, Duration and Std.Time keep values exactSchema.verify! fails fast at start-up if they differA Lean structure is the single source of truth. It generates the schema, decodes rows, and is verified against the live database.
Small, composable layers over TypeDB's official driver.
Tx .read, Tx .write and Tx .schema are different types. A query that needs more than its transaction allows does not compile.
typeql!"… {value} …" renders every value through ToTypeQL. A value with no rendering is a compile error, never a string concatenation.
Rows decode into structures with deriving FromRow; fetch documents through FromJson. Stream millions of rows in constant memory.
deriving Entity and deriving Relation: inserts, reads, updates, deletes, subtypes, relations that play roles, polymorphic reads.
Versioned up and down steps, with history and checksums kept in the database. One step can change the schema and backfill data atomically.
Migrations →Driver.run returns a Std.Async computation on its own thread. Batched decoding matches the Rust driver on scans and lookups.
Every query carries the weakest transaction mode that may run it, read off its text: define needs schema, insert needs write, match needs read. Every operation asks the compiler for evidence that the current mode allows it.
Read helpers lift into write transactions on their own, and you can write helpers that work in any mode strong enough to run them.
5 bugs the compiler catches →def broken : Tx .read Unit :=
exec typeql!"match $p isa person; insert $p has name \"x\";"error: failed to synthesize instance of type class
TxMode.read.Allows TxMode.writestructure Secret where
x : Nat
example (v : Secret) : Query .read := typeql!"match $p has id {v};"error: failed to synthesize instance of type class
ToTypeQL SecretTypeDB shines where relations have roles, data has subtypes, and correctness matters. Lean makes sure your code agrees.
Observations, beliefs, provenance, time and contradictions as a typed graph instead of a JSON blob. Recall with typed queries, and write atomically from many agent threads.
Read the use case →
N-ary relations, relations that play roles in other relations, and subtype hierarchies map to Lean structures with Role, Ref and extends. Polymorphic reads decode each instance into its own type.
An exact Decimal with 19 fractional digits, durations that keep months and days apart, and a retry policy that re-runs a transfer only when its commit loses a conflict.
Who may do what, through which role, under which grant. Model it as relations, encode the rules in TypeQL functions, and keep the queries that check them injection-safe.
A free, seven-chapter introduction to typed graphs. No prior TypeDB or Lean knowledge needed.
From the PERA model and TypeQL to dependent types, domain modeling, and a complete application with migrations. Every example compiles against the library, and every TypeQL query ran on a real TypeDB 3 server.
Start reading →TypeDB for Edge AI Agents covers TypeDB's model, TypeQL, and using a typed knowledge graph as memory for AI agents.
You need Lean 4 (via elan), a Rust toolchain, protoc and Docker.
The first build compiles TypeDB's C driver; later builds reuse it.
require «typedb-lean» from git
"https://github.com/Volland/typedb-lean" @ "v0.1.0"The default credentials are admin / password.
docker run -d --name typedb \
-p 1729:1729 typedb/typedb:3.14.0Everything returns EIO TypeDBError α.
Driver.withDriver
{ address := "127.0.0.1:1729" } fun d => do
d.ensureDatabase "hello"
d.runSync "hello" .read (query …)Same workloads, same server, same driver version. A decoder knows its columns, so one native call returns hundreds of rows at a time. The full benchmark fails if the scan drops below 80% of Rust's throughput, and CI runs a smaller version with the targets relaxed by 10%.
See the full benchmark →No. Chapter 2 of the mini book teaches entities, relations, attributes, roles and TypeQL from scratch, with queries you can run.
Basic functional programming helps. Chapter 3, Just enough Lean, covers structures, type classes, do notation and the bit of dependent typing the library uses.
TypeDB 3.x. The library builds the official C driver at a pinned version (currently 3.14.0), and its integration tests run against a typedb/typedb container of that version.
Linux x86_64, Linux arm64 and macOS arm64, with Lean v4.35.0. Building needs a Rust toolchain and protoc, or a prebuilt driver library via TYPEDB_DRIVER_LIB.
Yes. Config takes username, password, and tls := .system or .rootCA path.
v0.1.0 is the first release. It has unit tests, compile-time checks and integration tests against a real server in CI on every push, and benchmarks with enforced targets. Try it, and report what you find on GitHub.
Apache-2.0.
Typed schemas, typed queries, typed transactions and typed results, from a single definition.