Queries and transactions

This chapter covers the everyday API: opening a driver, running transactions, getting answers back in the shape you want, and running several transactions at once.

Connecting

A Driver is one connection to a server, shared by every transaction and thread that uses it. Driver.withDriver opens it, runs your code, and closes it:

import TypeDB
open TypeDB

def main : IO Unit := do
  let r ← (Driver.withDriver { address := "127.0.0.1:1729" } fun d => do
    d.ensureDatabase "pub"
    -- transactions go here
    : EIO TypeDBError Unit).toBaseIO
  if let .error e := r then IO.eprintln e

The Config also takes username, password, tls (.disabled, .system or .rootCA path) and requestTimeoutMs. Databases are managed on the driver with createDatabase, ensureDatabase, databaseExists, deleteDatabase and databases.

Running a transaction

You hand the driver a database name, a mode and a body:

d.runSync "pub" .write body     -- EIO TypeDBError α, on this thread
d.run     "pub" .write body     -- EAsync TypeDBError α, on its own thread

The mode you pass must match the body's type: body : Tx .write α goes with .write. Both functions follow the same steps:

1. Open a transaction of that mode.
2. Run the body.
3. If the body succeeds, commit (write and schema mode) or close (read mode), and return its result.
4. If the body fails, close the transaction without committing and return the error.

There is no way to forget a commit or leak an open transaction: the transaction exists only for the length of the body. TxOptions tunes it:

d.runSync "pub" .read (opts := { timeoutMs := 10000, prefetch := 1024 }) body

Inside a body

A body is an ordinary do block. It can call IO (an IO error becomes TypeDBError.io), raise its own error with Tx.fail, catch errors with try … catch, and call helpers of the same or a weaker mode:

def transferReview (from_ to : String) : Tx .write Unit := do
  let n ← countPeople                    -- a read helper, lifted
  if n == 0 then Tx.fail (.internal "no people")
  exec typeql!"match $r isa review, links (reviewer: $p); $p has email {from_};
    $q isa person, has email {to};
    delete links (reviewer: $p) of $r;
    insert $r links (reviewer: $q);"
  IO.println s!"moved reviews from {from_} to {to}"

Everything in the body is one atomic unit. If the IO.println failed, the reviews would not move. Tx.rollback discards the writes made so far without ending the transaction.

Retrying conflicts

TypeDB detects conflicting writes when a transaction commits. The transaction that commits second fails with TypeDBError.conflict. A retry policy re-runs the whole body when, and only when, the commit loses a conflict:

d.runSync "pub" .write (retry := .conflicts 5 (.exponential 20)) body

The body runs at most six times, waiting 20 ms, 40 ms, 80 ms and so on (capped at 5 s) between attempts. .constant ms and .none are the other backoffs. Any other error is returned immediately. Because the body runs again, any IO it performs runs again too, so keep side effects that must happen once outside the body.

Reading answers

Pick the function by the shape of answer you want:

query builds an array, which is fine for small answers. For large ones, fold or loop. Rows are decoded one batch at a time and the memory used stays the same however many rows there are:

let total ← queryFold (α := Col "y" Int64) typeql!"match $b isa book, has year $y;" 0
  fun s y => s + y.val.toInt

for b in stream (α := Col "t" String) typeql!"match $b isa book, has title $t;" do
  if b.val.startsWith "Typed" then
    IO.println b.val
    break

Values from Lean go into queries through interpolation, with the type checks from chapter 5:

def booksAfter (year : Int64) : Tx .read (Array (Col "t" String)) :=
  query typeql!"match $b isa book, has year $y, has title $t; $y > {year};"

Decoders by hand

deriving FromRow covers most cases. When you want a tuple or a computed shape without declaring a structure, build a RowDecoder from col and colOpt. Decoders are applicative, so <$> and <*> combine them:

def titleYear : RowDecoder (String × Option Int64) :=
  Prod.mk <$> col "title" <*> colOpt "year"

let rows ← queryWith titleYear
  typeql!"match $b isa book, has title $title; try \{ $b has year $year; };"
-- #[("Typed Graphs", some 2026)]

A decoder knows which columns it reads and what it needs from each one: a value, a type label or an IID. That plan is passed to the native layer, which returns exactly those parts for a whole batch of rows in one call. This is where most of the library's speed comes from.

Documents

A fetch query returns JSON documents. Decode them into structures with Lean.FromJson, or keep them as Json with fetchJson:

structure Doc where
  name : String
  deriving Lean.FromJson

let docs ← fetch (α := Doc) typeql!"match $p isa person; fetch \{ \"name\": $p.name };"

Concurrency

Driver.run returns a Std.Async.EAsync TypeDBError α. The C driver blocks the thread it runs on, so each such transaction gets a dedicated thread and the shared task pool stays free. Combine runs with the standard combinators and wait for the result with .block:

let (people, books) ← (Std.Async.EAsync.concurrently
    (d.run "pub" .read (Entity.all (α := Person)))
    (d.run "pub" .read (Entity.count (α := Book)))).block
IO.println s!"{people.size} people, {books} books"

EAsync.concurrentlyAll runs an array of transactions at once, and EAsync.race returns the first result. If any combined transaction fails, the whole computation fails with that transaction's TypeDBError. One driver can serve any number of concurrent transactions; inside a single transaction, the body runs sequentially.

Concurrent writes that touch the same data may conflict. Give each one a retry policy, and the losers will re-run against the winners' committed state.