Why TypeDB and Lean

Both systems have strong type systems. A typical database client throws both away at the point where they meet. This chapter shows what gets lost there, and what you get by keeping it.

Types die at the boundary

Consider a typical database call in almost any language:

rows = db.query("match $p isa person, has name $n; " + "has age " + age_input + ";")
for row in rows:
    print(row["n"].as_string())

Each line hides a failure that only shows up at run time:

• The query is a string. If age_input comes from a user, it can change the query's structure. That is query injection.
• Nothing says whether this code runs in a read or a write transaction. If someone later adds an insert to the string, the call fails in production with a server error.
• The result is a map from names to dynamically typed values. A misspelled column name, or an attribute that turned from string into integer in the last migration, fails on the first row that hits it.
• The program's idea of what a person is lives in one place, and the database's lives in another. Nothing checks that they agree.

The database knows the schema precisely, and the program's language may have a good type checker. Between them is a string going one way and a bag of values coming back. Every guarantee either side could give is lost at that boundary.

What TypeDB types

TypeDB is a database whose schema is a type system. You declare entity types (things that exist on their own), relation types (things that exist because they connect others through named roles), and attribute types (values with a value type, such as string or datetime). Types form hierarchies with sub, so an employee is a person and every query about people also finds employees.

The schema is enforced. The server rejects an insert that gives a person an attribute it does not own, puts a book into a role it cannot play, or breaks a key or cardinality constraint. TypeQL queries are type-checked against the schema before they run: the server infers the possible types of every variable in a pattern and reports a pattern that can never match.

So the data is typed. What the database cannot see is the program that sends it queries.

What Lean types

Lean 4 is a functional programming language and a proof assistant. As a programming language it has the usual tools: structures, algebraic data types, pattern matching, type classes, monads with do notation. It compiles to C and runs fast.

It also has dependent types: a type can mention a value. That lets the type of a transaction say what kind of transaction it is (Tx .read α or Tx .write α). It lets a query's type carry the weakest transaction that may run it (Query .write), and it lets an operation require evidence that the current transaction is strong enough. The compiler checks all of this, and none of it costs anything at run time.

Lean also has a macro system powerful enough to read a query literal at compile time, and deriving handlers that generate code from a structure's definition. typedb-lean uses both.

Connecting the two

typedb-lean keeps types on both sides of the boundary and connects them. Here is the earlier example again:

structure PersonRow where
  n : String
  deriving FromRow

def adults (age : Int64) : Tx .read (Array PersonRow) :=
  query typeql!"match $p isa person, has name $n, has age $a; $a >= {age};"

• {age} is rendered through the ToTypeQL class as an integer literal. No value can change the query's structure, and a value with no TypeQL form is a compile error.
• typeql! reads the literal and gives it the type Query .read. If the text contained insert, the type would be Query .write, and adults would not compile, because its body is a read transaction.
• Rows are decoded into PersonRow. A missing column or a value of the wrong type becomes a typed decode error that names the column, not a crash on a dynamic cast.

On top of this, the ORM layer makes a Lean structure the single source of truth for a TypeDB type. deriving Entity generates the TypeQL schema, the insert and read queries, and the decoder. Schema.verify! compares the structures with the live schema when the program starts, so any drift between code and database is reported then, as one typed error.

What is still checked at run time

Lean cannot see the database while it compiles your program, so some checks remain at run time:

• Whether a TypeQL pattern is valid for the live schema. The server checks this, and the error comes back as TypeDBError.server with TypeDB's error code.
• Whether a column you decode actually holds the type you asked for. The decoder checks this on every row and fails with TypeDBError.decode.
• Whether the live schema matches your structures. Schema.verify! checks this once, at start-up, and lists every difference.

The library is designed so that each of these happens once, early, and as a typed error you can match on, rather than in the middle of a request.