Types everywhere

This chapter goes through typedb-lean layer by layer and shows, for each one, what the type says, who checks it, and what you see when it is wrong.

The map

Values

Each TypeDB value type has one Lean type that holds it exactly:

The same table drives the schema generator: a salary : Decimal field becomes attribute salary, value decimal. A duration of one month is not 30 days, and a decimal of 0.1 is not 0.1000000000000000055…. Keeping each in its own Lean type keeps those distinctions intact.

Queries know their mode

A Query need is TypeQL text together with the weakest transaction mode that may run it. typeql! computes need at compile time from the literal, ignoring string literals and variable names:

#check typeql!"insert $p isa person;"
-- Query TxMode.write
#check typeql!"match $p isa person, has name \"insert\";"
-- Query TxMode.read
#check typeql!"define entity person;"
-- Query TxMode.schema

define, undefine and redefine need a schema transaction. insert, delete, update and put need a write transaction. Anything else is read. For text you build at run time, you state the mode yourself with Query.raw .write text. Joining two queries with Query.append gives a Query (max m n), the stronger of the two modes.

Transactions know their mode

A transaction body is a Tx m α, and every operation that runs a query asks for evidence that m is strong enough:

def exec [TxMode.Allows m need] (q : Query need) : Tx m Unit
def query [TxMode.Allows m need] [FromRow α] (q : Query need) : Tx m (Array α)

The evidence comes from four instances, one for each allowed pair in read ≤ write ≤ schema:

class Allows (cur need : TxMode) : Prop where
  le : need ≤ cur

instance {m : TxMode} : Allows m .read := ⟨Nat.zero_le _⟩
instance : Allows .write .write := ⟨Nat.le_refl _⟩
instance : Allows .schema .write := ⟨by decide⟩
instance : Allows .schema .schema := ⟨Nat.le_refl _⟩

So an insert in a read transaction does not compile. This is the exact message, which the library's test suite pins:

example : 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 allowed. A schema transaction may write data, and a Tx .read helper can be used inside a write body, because Tx .read lifts into Tx .write and Tx .schema automatically:

def readHelper : Tx .read Nat := pure 1
example : Tx .write Nat := do return (← readHelper) + 1

To write a helper that works in any mode strong enough, make the mode a parameter and require the evidence:

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

Tx is an irreducible definition rather than an abbreviation, so Lean cannot unfold Tx .read α and Tx .write α to the same thing and confuse them. The mode costs nothing at run time: Allows is a Prop, and proofs are erased by the compiler.

Values cannot become syntax

Each {e} in typeql! is rendered by the ToTypeQL instance of its type. A String is quoted with every quote, backslash and control character escaped:

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

Whatever a user types ends up as one string literal, so it cannot change the query's structure. A value whose type has no instance does not compile:

structure NotRenderable where
  x : Nat

example (v : NotRenderable) : Query .read := typeql!"match $p has id {v};"

error: failed to synthesize instance of type class
  ToTypeQL NotRenderable

When you do need to splice text verbatim, such as a type label chosen at run time, you say so with Raw. The unsafe operation is then visible in the code:

def byLabel (label : String) : Query .read :=
  typeql!"match $x isa {Raw.mk label};"

Rows have shapes

A decoder reads named columns of an answer row. deriving FromRow builds one from a structure: each field reads the variable of the same name, and Option fields read columns that a try block may leave empty:

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; };"

Col "v" T decodes a single column, and pairs decode side by side: query (α := Col "n" String × Col "a" Int64) q. If the data does not have the declared shape, the error names the column and both types:

query (α := Col "t" Int64) typeql!"match $b isa book, has title $t;"

TypeDBError.decode "t" "integer" "string value"

It is a value you can match on, raised before your code sees a wrong value.

Streams stay in their transaction

stream q lets a for loop read rows one batch at a time, in constant memory. Its rows can only be pulled while the transaction is open, because the ForIn instance that makes for work exists only in Tx m:

instance [TxMode.Allows m need] : ForIn (Tx m) (RowStream need α) α

You cannot iterate a stream from IO after the transaction has closed, so there is no stale cursor to read from. The stream is released when the loop finishes, breaks or throws.

Errors are typed

Everything returns EIO TypeDBError α, and TypeDBError has one constructor per kind of failure:

Inside a body you can catch some kinds and rethrow the rest:

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

Closing the loop: verification

The one thing the compiler cannot see is the live database. Schema.verify reads the server's schema and compares it with your mappings. It returns a list of SchemaIssues: missing types, wrong kinds, wrong supertypes, attributes that are not owned or have another value type, and missing relates and plays. Schema.verify! fails with TypeDBError.schemaMismatch if the list is not empty:

let issues ← d.runSync db .read (Schema.verify schema)   -- List SchemaIssue
d.runSync db .read (Schema.verify! schema)               -- or fail at start-up

Run it once when your program starts. From then on, the structures you compiled against describe the database you are talking to. If someone changes the schema underneath you, you get a list such as attribute 'year' has value type string, expected integer at start-up rather than a decode error in the middle of a request.