Chapter 7

Building an app

The repository's social network example uses every part of the library in one program of about 130 lines. This chapter walks through it and then covers what an application needs beyond it: schema evolution, tests and performance.

The project

The example lives in examples/social/Social.lean. With a server running, run it from the repository:

docker run -d --name typedb -p 1729:1729 typedb/typedb:3.14.0
lake exe social                                   # uses TYPEDB_ADDRESS, default 127.0.0.1:1729

In your own project, add the library to lakefile.lean and define an executable:

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

lean_exe social where
  root := `Social

The first lake build clones TypeDB's driver at the pinned version and builds its C library with cargo, so you need a Rust toolchain and protoc, the protobuf compiler; later builds reuse it.

The types

The domain has people, employees, friendships, endorsements of friendships, posts and authorship. It covers an entity, a subtype, a relation, a relation playing a role, and attributes of several value types:

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

structure Employee extends Person where
  company : String
  salary : Decimal
  deriving Repr, Entity

structure Friendship where
  a : Role "friend" (Ref Person)
  b : Role "friend" (Ref Person)
  since : Std.Time.PlainDate
  deriving Repr, Relation

/-- A relation whose `endorsed` player is itself a relation. -/
structure Endorsement where
  endorsed : Role "endorsed" (Ref Friendship)
  endorser : Role "endorser" (Ref Person)
  note : Option String := none
  deriving Repr, Relation

structure Post where
  id : Key String
  body : String
  tags : Array String := #[]
  postedAt : DatetimeTZ
  deriving Repr, Entity

structure Authorship where
  author : Role "author" (Ref Person)
  post : Role "post" (Ref Post)
  deriving Repr, Relation

def schema : List TypeSpec :=
  [TypeSpec.of Person, TypeSpec.of Employee, TypeSpec.of Friendship, TypeSpec.of Endorsement,
   TypeSpec.of Post, TypeSpec.of Authorship]

Two read-side types complete it. AnyPerson decodes every person as a Person or an Employee, and FriendOf is the row type of a hand-written query:

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

structure FriendOf where
  name : String
  friend : String
  deriving Repr, FromRow

Migrations

A real database outlives any one version of your program, so its schema is changed by migrations rather than by a single define. A migration is a list of versioned steps:

def migrations : List Migration := [
  Migration.define 1 "social 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 := "default nickname", 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;") }
]

Step 1 defines the ORM schema. Step 2 is plain TypeQL with a down step that undoes it. Step 3 is Lean code that backfills data: every person without a nickname gets their name as one.

let report ← d.migrateSync "social" migrations           -- the steps it ran
let report ← d.rollbackSync "social" migrations (to := 1) -- undo down to version 1
let history ← Migrations.history d "social"

The rules:

Versions are unique and increasing. migrate applies, in order, every step newer than the latest applied one.
Each step is atomic. It runs in its own schema transaction together with its history record, stored as typedb-lean-migration entities in the same database. If a step fails, neither its changes nor its record are committed, the earlier steps stay applied, and the error names the version. Since schema transactions can also write data, a step can change the schema and backfill data in one commit.
Applied steps are checksummed. Each step has a checksum of its name and fingerprint. If an applied step's checksum differs from the one in your list, because someone edited a migration that already ran, migrate stops before running anything. Steps written in TypeQL use their text as the fingerprint. Lean code cannot be hashed, so a step written as code must give a fingerprint that you change whenever you change the code.
Rollback runs down steps newest first, each together with the removal of its record. A step marked .irreversible stops the rollback before it.

Writing data

The seed is one write transaction. Each insert returns a typed reference that the next insert uses:

def seed : Tx .write (Ref Post) := do
  let ann ← Entity.insert { email := "ann@example.com", name := "Ann", age := some 34, tags := #["lean", "graphs"] : Person }
  let bob ← Entity.insert { email := "bob@example.com", name := "Bob", company := "Acme", salary := 4200, tags := #["rust"] : Employee }
  discard <| Entity.insert { email := "cy@example.com", name := "Cy \"the quoted\"" : Person }
  let f ← Relation.insert { a := ann, b := bob.up, since := Std.Time.PlainDate.ofYearMonthDayClip 2021 3 14 : Friendship }
  discard <| Relation.insert { endorsed := f, endorser := Ref.key (α := Person) "cy@example.com", note := some "true friends" : Endorsement }
  let at_ := DatetimeTZ.ofLocalFixed (Std.Time.PlainDateTime.ofEpochDay ⟨19000⟩ ⟨⟨9, by decide⟩, ⟨30, by decide⟩, ⟨0, by decide⟩, ⟨0, by decide⟩⟩) 3600
  let post ← Entity.insert { id := "p1", body := "Typed graphs from Lean", tags := #["lean"], postedAt := at_ : Post }
  discard <| Relation.insert { author := ann, post := post : Authorship }
  return post

Note what you do not see: no query strings, no escaping (Cy's name contains quotes), and no conversions for the Decimal salary, the PlainDate or the zoned post time. bob.up turns the Ref Employee into the Ref Person that the friendship expects. The endorsement refers to Cy by key, without looking up an IID. If anything fails, nothing is committed.

Reading it back

The report is a read transaction that mixes the ORM, a typed query and a fold:

def report : Tx .read Unit := do
  IO.println "-- people (polymorphic):"
  for (_, p) in ← Polymorphic.all (α := AnyPerson) do
    match p with
    | .person p => IO.println s!"  person   {p.name} <{p.email}> tags={p.tags}"
    | .employee e => IO.println s!"  employee {e.name} at {e.company}, salary {e.salary}"
  IO.println "-- friendships (typed query):"
  for r in stream (α := FriendOf) typeql!"match $f isa friendship, links (friend: $x, friend: $y);
      $x has name $name; $y has name $friend;" do
    IO.println s!"  {r.name} ↔ {r.friend}"
  let nicknames ← queryFold (α := Col "k" String) typeql!"match $p isa person, has nickname $k;" 0 fun n _ => n + 1
  IO.println s!"-- {nicknames} nicknames, {← Entity.count (α := Person)} people, {← Relation.count (α := Endorsement)} endorsements"

The nickname attribute was added by migration 2, not by a Lean structure. Raw queries can use any part of the schema; only the ORM operations need mapped types.

Putting it together

def main : IO UInt32 := do
  let address := (← IO.getEnv "TYPEDB_ADDRESS").getD "127.0.0.1:1729"
  let result ← (Driver.withDriver { address } fun d => do
    if ← d.databaseExists "social" then d.deleteDatabase "social"
    d.createDatabase "social"
    let applied ← d.migrateSync "social" migrations
    IO.println s!"-- migrations applied: {applied.steps.toList}"
    d.runSync "social" .read (Schema.verify! schema)
    let post ← d.runSync "social" .write seed
    let ann := Ref.key (α := Person) "ann@example.com"
    d.runSync "social" .write (Entity.update ann Person.field.age (some 35))
    d.runSync "social" .read report
    -- Two read transactions at once, on their own threads.
    let (people, posts) ← (Std.Async.EAsync.concurrently
      (d.run "social" .read (Entity.all (α := Person)))
      (d.run "social" .read (Entity.all (α := Post)))).block
    IO.println s!"-- concurrently: {people.size} people, {posts.size} posts"
    if let some p ← d.runSync "social" .read (Entity.get? post) then
      IO.println s!"-- post {p.id}: {p.body} at {render p.postedAt}"
    d.runSync "social" .write (Entity.delete post)
    IO.println s!"-- post deleted: {(← d.runSync "social" .read (Entity.get? post)).isNone}"
    : EIO TypeDBError Unit).toBaseIO
  match result with
  | .ok () => return 0
  | .error e => IO.eprintln s!"error: {e}"; return 1

The order is the one to copy in a real service: migrate, then verify the schema, then serve. After Schema.verify! passes, the structures the program was compiled against match the database it is talking to. Entity.update takes a typed field handle, Person.field.age, so the new value must be an Option Int64.

Testing

The library's own tests show a pattern that works for applications too: unit tests that need no server, and integration tests against a real TypeDB in a container, each with a fresh database.

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 tests whose names contain "orm:"
TYPEDB_ADDRESS=127.0.0.1:1729 lake test     # use a server you already run

The things you would otherwise test for, such as a write in a read transaction or an unescaped value, do not compile, so there is nothing to test. The library pins its compile errors with #guard_msgs in tests/CompileChecks.lean, and you can do the same for invariants of your own API.

Performance

Types cost nothing at run time here. Modes and Allows proofs are erased, and Tx compiles to a plain reader over EIO, so loops in transaction bodies become plain loops. The work that remains is decoding, and it is batched: a decoder's plan tells the native layer which concepts and which parts of them to return, for up to batchSize rows per call. Against the official Rust driver, on the same server and driver version:

Workload	typedb-lean	Rust driver
Scan of 100,000 rows into structures	155,368 rows/s	142,061 rows/s
Point lookup, p50 / p99	1.05 / 1.52 ms	1.03 / 2.39 ms
Bulk insert of 10,000 entities	4.75 s	4.71 s
16 concurrent read transactions	367 ms	607 ms

Some practical advice: stream or fold large answers instead of building arrays; raise prefetch for big scans; run independent reads concurrently with Driver.run; and batch many inserts into one transaction. See the benchmarks page for the method and how to reproduce it.