Introducing typedb-lean

TypeDB is a database with a real type system. Its schema declares entities, relations and attributes, the roles they play, and inheritance between them, and the server rejects data that doesn't fit. Lean 4 is a functional programming language and proof assistant with dependent types.

typedb-lean is a client library that connects them, and it keeps the types on both sides instead of flattening everything into strings at the boundary.

import TypeDB
open TypeDB

@[typedb "person"]
structure Person where
  email : Key String
  name : String
  age : Option Int64 := none
  deriving Entity

structure Friendship where
  a : Role "friend" (Ref Person)
  b : Role "friend" (Ref Person)
  deriving Relation

def main : IO Unit := do
  let r ← (Driver.withDriver { address := "127.0.0.1:1729" } fun d => do
    d.ensureDatabase "social"
    d.runSync "social" .schema (Schema.defineTx [TypeSpec.of Person, TypeSpec.of Friendship])
    d.runSync "social" .write do
      let ann ← Entity.insert { email := "ann@example.com", name := "Ann" : Person }
      let bob ← Entity.insert { email := "bob@example.com", name := "Bob", age := some 41 : Person }
      discard <| Relation.insert { a := ann, b := bob : Friendship }
    d.runSync "social" .read do
      for row in stream (α := Col "n" String) typeql!"match $p isa person, has name $n;" do
        IO.println row.val
    : EIO TypeDBError Unit).toBaseIO
  if let .error e := r then IO.eprintln e

Three ideas

Typed transactions

A transaction body has type Tx .read α, Tx .write α or Tx .schema α. Every query carries the weakest mode that may run it, inferred from its text, so an insert inside a read transaction is a compile error, not a server error. Driver.runSync commits on success, rolls back on any error, and can retry commit conflicts with a policy you choose. Driver.run does the same as a Std.Async computation on its own thread.

Typed queries

typeql!"… {value} …" renders each interpolated value as an escaped TypeQL literal through the ToTypeQL class. A value can't change a query's structure, and a value with no TypeQL form doesn't compile. TypeDB takes queries as text, with no server-side parameter binding, so this is where injection safety has to live.

Typed results

Rows decode straight into Lean structures with deriving FromRow, and fetch documents decode through Lean.FromJson. TypeDB's value types map to exact Lean types: decimal to an exact Decimal, dates and datetimes to Std.Time, duration to a type that keeps months, days and nanoseconds apart. A row of the wrong shape is a typed decode error that names the column.

An ORM and migrations

For everyday work, deriving Entity and deriving Relation give you inserts, reads, updates and deletes. You also get subtypes through extends, relations that play roles in other relations, and polymorphic reads into an inductive type. The same structures generate the TypeQL schema, and Schema.verify! checks them against the live database at start-up.

Migrations are versioned up and down steps. Each one runs in its own schema transaction together with its history record, and checksums stop a changed step from silently running against a database that applied the old one. A step can change the schema and backfill data atomically.

Performance

typedb-lean wraps TypeDB's official C driver, and the question was what the Lean layer costs. lake exe bench runs the same workloads with this library and with the official Rust driver, against one server. On an Apple M-series laptop with TypeDB 3.14.0 in Docker:

Two things make that possible: rows are decoded in batches, many per native call, and the server streams answers ahead of the client. The full benchmark fails if scans fall below 80% of the Rust driver's throughput, or the lookup p50 rises above 1.1×. CI runs a smaller version on pushes to main and on pull requests, with those targets relaxed to 70% and 1.2× for shared runners. The benchmarks page has the workloads, the method and the caveats.

Install

Add the package to your lakefile.lean:

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

The first lake build clones TypeDB's driver at the pinned version (3.14.0) and builds its C library with cargo, so you need a Rust toolchain and protoc, the protobuf compiler:

brew install protobuf                  # macOS
sudo apt-get install protobuf-compiler # Debian, Ubuntu
docker run -d --name typedb -p 1729:1729 typedb/typedb:3.14.0

Supported platforms are Linux x86_64, Linux arm64 and macOS arm64, with Lean v4.35.0.

Learn more

• The docs cover every part of the library.
• The examples are complete programs, from a social network to a bank transfer with conflict retry.
• The mini book is seven short chapters on TypeDB, Lean and how the types connect.
• Typed memory for AI agents is a longer use case built on the library.

What's next

This is the first release, and the best input now is real use. Try it on a model of your own. If something is missing, awkward or wrong, whether an API, a value type, a platform or a confusing error, please open an issue. Pull requests are welcome too. The design decisions and their reasons are recorded in the repository, so you can see why things are the way they are before changing them.