Five bugs the compiler catches for you

Not every check can happen at compile time, and this post is clear about which ones do. Three of the five are compile errors. One is a typed error on the first bad row. One fails once, at start-up, before your program does any work.

The examples use this mapping:

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

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

1. A write inside a read transaction

In a typical driver, the transaction type is an argument you pass at run time, and the query is a string. A helper written for a read transaction picks up an insert during a refactor, and the server rejects it, in production, on the code path nobody tested.

In typedb-lean, a transaction body has type Tx m α, with the mode m (.read, .write or .schema) in the type. typeql! reads the weakest mode a query needs off its text, and every operation demands a proof that the current mode allows it:

def addNickname : 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.write

The other direction is fine. A read helper can run inside a write transaction, and a helper can take the mode as a parameter to work in any mode strong enough:

def findByEmail {m : TxMode} [TxMode.Allows m .read] (email : String) : Tx m (Option PersonRow) :=
  query1? typeql!"match $p isa person, has email {email}, has name $name; try \{ $p has age $age; };"

2. A query built from untrusted text

In a typical driver, TypeDB takes queries as text, with no server-side parameter binding, so values get spliced into the string. One forgotten escape, and a user's input becomes part of the query.

In typedb-lean, every {value} in typeql! goes through the ToTypeQL class, which renders it as a TypeQL literal. Strings are quoted, with quotes, backslashes and control characters escaped. A value can't close the literal and start a new statement:

def email := "x\"; match $p isa person; delete $p;"
#eval IO.println (typeql!"match $p isa person, has email {email};").text

match $p isa person, has email "x\"; match $p isa person; delete $p;";

And a type with no ToTypeQL instance, like a request object you meant to unpack, does not compile at all:

structure UserInput where
  raw : String

def lookup (u : UserInput) : Tx .read (Array PersonRow) :=
  query typeql!"match $p isa person, has email {u}, has name $name; try \{ $p has age $age; };"

error: failed to synthesize instance of type class
  ToTypeQL UserInput

When you really do need to splice text, such as a type label chosen at run time, you say so with Raw.mk, which makes it easy to find in review.

3. A cursor used after its transaction

In a typical driver, a query returns a lazy iterator over the server's answer stream. Return it from the function that opened the transaction, and it fails when someone iterates it later, because the transaction under it has closed.

In typedb-lean, stream q is only a description: a query and a decoder. The one way to iterate it is a for loop inside a transaction body. The cursor is opened when the loop starts and released when it ends, breaks or throws. Smuggle the description out and try to loop outside a transaction, and there's no for to call:

def leak (d : Driver) : EIO TypeDBError Unit := do
  let s ← d.runSync "db" .read (pure (stream (α := PersonRow) typeql!"match $p isa person, has name $name;"))
  for p in s do
    IO.println p.name

error: failed to synthesize instance of type class
  ForIn (EIO TypeDBError) (Tx.RowStream TxMode.read PersonRow) ?α

Move the loop into the body, and it compiles. Memory stays constant however many rows there are:

def printNames : Tx .read Unit := do
  for p in stream (α := PersonRow) typeql!"match $p isa person, has name $name; try \{ $p has age $age; };" do
    IO.println p.name

4. A row decoded into the wrong shape

In a typical driver, you read a column with something like row.get("age").as_integer(). If the query changed and $age is now a string, or missing, you get a null, a cast exception, or a wrong number far from the query.

In typedb-lean, the shape of a row is a type, and rows decode into it directly. The query text is not checked against that type at compile time, though. TypeQL is checked by the server, and what a variable holds depends on the live data. So a mismatch is a run-time error, but a typed one, raised on the first bad row, that names the column:

def ages : Tx .read (Array (Col "name" Int64)) :=
  query typeql!"match $p isa person, has name $name;"

cannot decode column 'name': expected integer, got string attribute

Because it's a value of TypeDBError, not a string, you can match on it:

def safeAges : Tx .read (Array (Col "name" Int64)) := do
  try ages
  catch
    | .decode col expected got => do
        IO.eprintln s!"{col}: expected {expected}, got {got}"
        return #[]
    | e => throw e

Optional columns are explicit too. A field of type Option Int64 reads a column that may be empty, from a try block, as none. A plain Int64 field fails if the column is missing.

5. Code and schema that drifted apart

In a typical driver, the schema lives in the database and the assumptions live in the code. Someone undefines an attribute in a migration, and the first sign is a failed query hours after the deploy.

In typedb-lean, the Lean structures are the expected schema. Schema.verify! compares them with the live database at start-up:

def schema : List TypeSpec := [TypeSpec.of Person]

def start (d : Driver) : EIO TypeDBError Unit := do
  d.runSync "people" .read (Schema.verify! schema)

If the database no longer lets a person own an age, the program stops before doing any work:

schema mismatch:
  - type 'person' does not own 'age'

It also reports missing types, wrong kinds, wrong supertypes, value-type changes, and missing relates and plays. Pair it with migrations, which store their history and checksums in the database, and code and schema change together.

Bonus: the wrong value for a field

The ORM's update takes a typed field handle, so the new value must have the field's type. age is an Option Int64, so a string does not compile:

def birthday (r : Ref Person) : Tx .write Unit :=
  Entity.update r Person.field.age "42"

error: Application type mismatch: The argument
  "42"
has type
  String
but is expected to have type
  ORM.TypeOf fun x => x.age

Entity.update r Person.field.age (some 42) compiles, and Entity.update r Person.field.age none removes the attribute.

The takeaway

None of this needs proofs or tactics. You write ordinary Lean, and the types do the work. The library puts the facts it knows into types: the mode a query needs, which values can be rendered, where a cursor may live, and the shape of a field. The two things it can't know at compile time, the live data and the live schema, it checks once, early, with errors you can match on.

To see these checks in a larger program, read Typed memory for AI agents. For the ideas behind them, chapter 5 of the mini book, Types everywhere, walks through each layer.