Using typedb-lean

Everything you need to talk to TypeDB from Lean: from adding the package to typed queries, the ORM and migrations. For the ideas behind it, read the mini book.

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-driver at the version in TYPEDB_VERSION (3.14.0) and builds its C library with cargo, so you need a Rust toolchain and protoc, the protobuf compiler (apt-get install protobuf-compiler or brew install protobuf). That takes about a minute; later builds reuse it. To link a library you built yourself, set TYPEDB_DRIVER_LIB=/path/to/libtypedb_driver_clib.a.

Supported platforms: Linux x86_64, Linux arm64 and macOS arm64. Lean is pinned to v4.35.0.

Run a server

docker run -d --name typedb -p 1729:1729 typedb/typedb:3.14.0

The default credentials are admin / password.

Connect and query

import TypeDB
open TypeDB

def main : IO Unit := do
  let r ← (Driver.withDriver { address := "127.0.0.1:1729" } fun d => do
    d.ensureDatabase "hello"
    d.runSync "hello" .schema (exec typeql!"define attribute name, value string; entity person, owns name;")
    d.runSync "hello" .write (exec typeql!"insert $p isa person, has name {"Ann"};")
    let names ← d.runSync "hello" .read (query (α := Col "n" String) typeql!"match $p isa person, has name $n;")
    IO.println (names.map (·.val))
    : EIO TypeDBError Unit).toBaseIO
  if let .error e := r then IO.eprintln e

Config also takes username, password, tls (.disabled, .system or .rootCA path) and requestTimeoutMs. Everything returns EIO TypeDBError α; inside IO, use .toBaseIO and match on the result.

Database management: createDatabase (fails if it exists), ensureDatabase, databaseExists, deleteDatabase, databases, and schema / typeSchema for the schema as TypeQL text.

Transactions

A transaction body has type Tx m α, where m is .read, .write or .schema. The modes are ordered read ≤ write ≤ schema: a schema transaction may also write data, and a write transaction may read.

Every query carries the weakest mode that may run it, and every operation requires [TxMode.Allows m need]. So this does not compile:

def broken : Tx .read Unit :=
  exec typeql!"match $p isa person; insert $p has name \"x\";"
-- failed to synthesize instance of type class TxMode.read.Allows TxMode.write

Helpers of a weaker mode lift into stronger bodies automatically. To write helpers that work in any sufficient mode, take the mode as a parameter:

def countPeople {m : TxMode} [TxMode.Allows m .read] : Tx m Nat := do
  let n ← queryOne (α := Col "c" Int64) typeql!"match $p isa person; reduce $c = count;"
  return n.val.toInt.toNat

Run a body with:

d.runSync "db" .write body          -- EIO TypeDBError α, on this thread
d.run "db" .write body              -- EAsync TypeDBError α, on its own thread
d.runSync "db" .read (opts := { timeoutMs := 10000, prefetch := 1024 }) body

If the body succeeds, the transaction commits (write and schema) or closes (read). If it fails, it closes without committing and the error is returned. Bodies are ordinary do blocks: they can call IO (an IO error becomes TypeDBError.io), raise errors with Tx.fail, and catch them with try … catch.

Errors and retries

d.runSync "db" .write do
  exec typeql!"insert $p isa person, has name \"a\";"
  try
    discard <| query (α := Col "n" Int64) typeql!"match $p has name $n;"
  catch
    | .decode col expected got => IO.println s!"{col}: expected {expected}, got {got}"
    | e => throw e

TypeDB detects conflicting writes at commit. A retry policy re-runs the whole body when, and only when, the commit loses a conflict. The body below runs at most 6 times; other errors return at once.

d.runSync "db" .write (retry := .conflicts 5 (.exponential 20)) transfer

Typed queries

typeql! builds a Query m. Every {e} is rendered by the ToTypeQL class as a TypeQL value literal, quoted and escaped, so a value can never change a query's structure. A value whose type has no ToTypeQL instance is a compile error.

let name := "Ann \"the\" coder"
let q := typeql!"match $p isa person, has name {name}, has age {(42 : Int64)};"
-- match $p isa person, has name "Ann \"the\" coder", has age 42;

To splice text verbatim, such as a type label, wrap it in Raw. TypeQL braces are written \{ and \}, because {…} is interpolation:

let label := Raw.mk "person"
typeql!"match $x isa {label};"
typeql!"match $p isa person, has name $n; fetch \{ \"name\": $n };"

The mode is read off the query text, ignoring string literals and variables: define, undefine or redefine need a schema transaction; insert, delete, update or put a write transaction; anything else a read transaction. Text built at run time takes an explicit mode: Query.raw .write text.

Decoding results

Derive a decoder for a structure: each field reads the query variable of the same name, and Option fields read optional columns (from a try block).

structure PersonRow where
  name : String
  age : Option Int64
  deriving FromRow

let people ← query (α := PersonRow)
  typeql!"match $p isa person, has name $name; try \{ $p has age $age; };"

Or build one by hand from col and colOpt, applicatively:

let d : RowDecoder (String × Option Int64) := Prod.mk <$> col "name" <*> colOpt "age"
let rows ← queryWith d typeql!"match $p isa person, has name $name; try \{ $p has age $age; };"

Col "v" T decodes a single column, and pairs decode side by side: query (α := Col "n" String × Col "a" Int64) q. For large answers, fold or stream; rows are decoded a batch at a time:

let total ← queryFold (α := Col "a" Int64) typeql!"match $p has age $a;" 0 fun s a => s + a.val.toInt
for p in stream (α := PersonRow) typeql!"match $p isa person, has name $name;" do
  if p.name == "Ann" then break

A stream belongs to its transaction: it is released when the loop ends, breaks or throws, and it cannot be returned out of the body. fetch decodes JSON documents with Lean.FromJson.

Value types

IID, Label (a concept's type label) and Concept decode from instance columns.

The ORM

Map structures to TypeDB types. Key, Role and Attr are transparent markers in field types: a Key String is a String.

@[typedb "person"]                     -- the type label; default: the name in kebab-case
structure Person where
  email : Key String                   -- owns email @key
  name : String                        -- owns name @card(1..1)
  age : Option Int64 := none           -- owns age
  tags : Array String := #[]           -- owns tags @card(0..)
  nick : Attr "nickname" (Option String) := none   -- attribute label override
  deriving Entity

structure Employee extends Person where   -- employee sub person
  company : String
  deriving Entity

structure Friendship where
  a : Role "friend" (Ref Person)       -- relates friend; person plays friendship:friend
  b : Role "friend" (Ref Person)
  since : Int64
  deriving Relation

Ref α points at an instance by key (Ref.key (α := Person) "ann@example.com") or by IID; r.up views a subtype reference as its supertype.

let ann ← Entity.insert ({ email := "ann@x", name := "Ann" } : Person)  -- Ref Person
let p? ← Entity.get? ann                                  -- Option Person
let all ← Entity.all (α := Person)                        -- includes subtype instances
Entity.update ann Person.field.name "Annie"                -- typed field handles
Entity.update ann Person.field.age none                    -- removes the attribute
Entity.delete ann
let n ← Entity.count (α := Person)

Relation.insert, Relation.get? and the rest work the same way. Reads fetch all attributes and role players in two queries, however many instances there are. For polymorphic reads, derive Polymorphic on an inductive whose constructors wrap the subtypes:

inductive AnyPerson where
  | person (p : Person)
  | employee (e : Employee)
  deriving Polymorphic

for (iid, p) in ← Polymorphic.all (α := AnyPerson) do
  match p with
  | .person p => IO.println p.name
  | .employee e => IO.println s!"{e.name} at {e.company}"

Schema

def schema := [TypeSpec.of Person, TypeSpec.of Employee, TypeSpec.of Friendship]

Schema.defineText schema                                  -- the TypeQL define, as text
d.runSync db .schema (Schema.defineTx schema)             -- define it
let issues ← d.runSync db .read (Schema.verify schema)    -- List SchemaIssue
d.runSync db .read (Schema.verify! schema)                -- fails with schemaMismatch

verify reports missing types, wrong kinds, wrong supertypes, attributes that are not owned or have another value type, and missing relates and plays. Run it at start-up and your Lean types and the live database cannot drift apart silently.

Migrations

def migrations : List Migration := [
  Migration.define 1 "schema" schema,
  Migration.tql 2 "nicknames"
    "define attribute nickname, value string; person owns nickname;"
    (down := some "undefine owns nickname from person; nickname;"),
  { version := 3, name := "backfill nicknames", fingerprint := "nickname := name, v1"
    up := exec typeql!"match $p isa person, has name $n; not \{ $p has nickname $k; }; insert $p has nickname == $n;"
    down := .step (exec typeql!"match $p isa person, has nickname $k; delete has $k of $p;") }
]

let report ← d.migrateSync "social" migrations
let report ← d.rollbackSync "social" migrations (to := 1)
let history ← Migrations.history d "social"

• Versions are unique and increasing; migrate applies every step newer than the latest applied one.
• Each step runs in its own schema transaction together with its history record. If it fails, nothing of it is committed and the error names its version.
• Every step has a checksum of its name and fingerprint. If an applied step's checksum changed, migrate stops before running anything. Steps written as Lean code must give a fingerprint that changes when the code does.
• rollback runs down steps newest first; .irreversible stops it.

Async

Driver.run returns a Std.Async.EAsync TypeDBError α on a dedicated thread. Combine runs with the standard combinators:

open Std.Async

def report (d : Driver) : EAsync TypeDBError (Array (Ref Person × Person) × Nat) :=
  EAsync.concurrently
    (d.run "social" .read (Entity.all (α := Person)))
    (d.run "social" .read (Entity.count (α := Post)))

let (people, posts) ← (report d).block

EAsync.concurrentlyAll runs an array of transactions at once, and EAsync.race returns the first result. One driver can be shared by any number of concurrent transactions.

Testing

lake test             # unit tests, then integration tests in a typedb/typedb container
lake test -- --unit   # unit tests only, no Docker needed
lake test -- orm:     # only the tests whose names contain "orm:"
TYPEDB_ADDRESS=127.0.0.1:1729 lake test   # use a server you already run