Typed Graphs: TypeDB and Lean Together

A short book about keeping types intact from the database schema to the code that uses it. It teaches the basics of TypeDB, just enough Lean 4, and how typedb-lean connects the two.

Who it is for

Developers who know at least one of the two systems and want to learn the other. If you have used TypeDB from Python or Rust, the Lean chapters show what a stronger type checker can do with your schema. If you write Lean, the TypeDB chapters introduce a database whose schema is a type system of its own: entities, relations, attributes and roles, with inheritance.

No background in theorem proving is needed. The book uses Lean as a programming language. Dependent types appear only where they do practical work, such as keeping a write out of a read transaction.

Chapters

1. 01
   Why TypeDB and LeanWhere types get lost between a program and its database, and what connecting two type systems gives you.
2. 02
   TypeDB basicsThe entity–relation–attribute model, roles and inheritance, and TypeQL: define, insert, match, fetch, reduce, functions.
3. 03
   Just enough LeanStructures, inductive types, pattern matching, type classes, do-notation, and types that depend on values.
4. 04
   Modeling a domainA small publishing domain, from nouns and verbs to a TypeDB schema to Lean structures that generate it.
5. 05
   Types everywhereEvery layer where typedb-lean keeps a type: schema, values, queries, transaction modes, rows, errors.
6. 06
   Queries and transactionsRunning transactions, commit and rollback, retries, reading rows and documents, and concurrency with Std.Async.
7. 07
   Building an appThe social network example end to end, migrations, testing, performance, and where to read further.

What you need

To run the examples you need Lean 4 (installed with elan), a Rust toolchain and protoc (the first build compiles TypeDB's C driver), and Docker for a local TypeDB server:

docker run -d --name typedb -p 1729:1729 typedb/typedb:3.14.0

Then add the library to your lakefile.lean as described in the guide. Every Lean snippet in this book has been compiled against the library, and every TypeQL query has been run against TypeDB 3.14.0.