Chapter 3

Just enough Lean

Lean 4 is a functional programming language with a very expressive type system. This chapter covers the parts typedb-lean relies on, using small examples you can paste into a file.

Setting up

Install elan, the Lean version manager. It picks the toolchain named in a project's lean-toolchain file. lake is Lean's build tool and package manager:

curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
lake new myapp exe
cd myapp && lake build && lake exe myapp

The VS Code extension for Lean shows types, errors and the results of #eval as you type. Most of learning Lean is reading what the editor tells you.

Definitions and data

def defines a value or function. Types come after a colon, and arguments are written in parentheses:

def greet (name : String) : String := s!"Hello, {name}!"

s!"…" is string interpolation. A structure is a record. Fields can have defaults, and Option α is a value that may be missing (some x or none):

structure Book where
  title : String
  year : Nat
  isbn : Option String := none
  deriving Repr

let b : Book := { title := "Typed Graphs", year := 2026 }   -- isbn is none
b.title                                                    -- "Typed Graphs"

An inductive type lists its constructors, and constructors can carry data. You take it apart with match, or with a function written by cases. The compiler checks that every case is covered:

inductive Format where
  | paperback
  | ebook (drm : Bool)

def describe : Format → String
  | .paperback => "paper"
  | .ebook true => "ebook with DRM"
  | .ebook false => "DRM-free ebook"

def isbnOrDash (b : Book) : String :=
  match b.isbn with
  | some i => i
  | none => "-"

The leading dot in .paperback means "the constructor of the type expected here". You will see it all the time in typedb-lean: .read, .write and .schema are the constructors of TxMode.

Structures can extend other structures. structure Employee extends Person has all of Person's fields plus its own. The ORM maps this to TypeDB's sub.

Type classes and deriving

A type class is an interface that types implement with an instance. The compiler finds instances automatically, by type. This is called instance resolution:

class Pretty (α : Type) where
  pretty : α → String

instance : Pretty Book where
  pretty b := s!"{b.title} ({b.year})"

#eval Pretty.pretty ({ title := "Typed Graphs", year := 2026 } : Book)
-- "Typed Graphs (2026)"

If no instance exists, the program does not compile, and the error names the missing instance. typedb-lean uses this in several places. ToTypeQL α says how to write a value of type α into a query. FromRow α says how to decode a row into an α. Interpolating a value with no ToTypeQL instance is a compile error.

deriving asks the compiler to generate an instance from a type's definition. deriving Repr generates a printer. typedb-lean adds its own deriving handlers, FromRow, Entity, Relation and Polymorphic, which read your structure's fields and generate decoders, queries and schema.

Effects and do-notation

Lean functions are pure. Effects such as printing or talking to a database are values of a monad type, such as IO α: "a program that, when run, does some I/O and returns an α". do blocks sequence them. ← runs an effect and binds its result, and let mut and for work as in an imperative language:

def main : IO Unit := do
  let b : Book := { title := "Typed Graphs", year := 2026 }
  IO.println (Pretty.pretty b)
  let mut total := 0
  for y in [2024, 2025, 2026] do
    total := total + y
  IO.println s!"sum: {total}"

Three monads matter for typedb-lean:

A transaction body in typedb-lean is defined as

def Tx (_m : TxMode) (α : Type) : Type := ReaderT TxCtx (EIO TypeDBError) α

It reads the open transaction (TxCtx), can fail with a TypeDBError, and returns an α. Because it is a monad, transaction bodies are ordinary do blocks with for, try … catch and calls to IO. Because it is a plain reader over EIO, the compiler turns those loops into plain loops.

To use an EIO computation from main : IO Unit, convert it with .toBaseIO and look at the result:

let r ← (someDatabaseWork : EIO TypeDBError Unit).toBaseIO
if let .error e := r then IO.eprintln e

Types that mention values

Look at Tx again. Its first parameter, _m : TxMode, is a value: .read, .write or .schema. So Tx .read Nat and Tx .write Nat are different types, even though m is never used at run time. A type that depends on a value is a dependent type. Here it is used in its simplest form, as a label the compiler tracks. Query need works the same way: a query's type records the weakest transaction that may run it.

The remaining question is how an operation says "I need at least a write transaction". The answer is a type class whose instances are proofs. Here is a self-contained miniature of the idea:

inductive Mode where
  | read
  | write

-- A class in Prop: an instance is evidence, and carries no data at run time.
class CanDo (cur need : Mode) : Prop

instance {m : Mode} : CanDo m .read := ⟨⟩      -- every mode can read
instance : CanDo .write .write := ⟨⟩           -- only write can write

def Action (_m : Mode) : Type := IO Unit

def lookup {m : Mode} [CanDo m .read] : Action m := IO.println "lookup"
def save {m : Mode} [CanDo m .write] : Action m := IO.println "save"

def ok : Action .write := save
def alsoOk : Action .write := lookup
def broken : Action .read := save
error: failed to synthesize instance of type class
  CanDo Mode.read Mode.write

Square brackets mark an instance argument: the caller does not pass it, and the compiler must find it. For broken there is no instance of CanDo .read .write, so the definition is rejected. typedb-lean's TxMode.Allows cur need is exactly this, with three modes and a proof that need ≤ cur. Every query operation asks for it:

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

Curly-brace arguments such as {m : Mode} are implicit: the compiler infers them from the other types. You will see helpers written as {m : TxMode} [TxMode.Allows m .read], which reads "for any mode that can read".

Macros

Lean's syntax is extensible. A macro or elaborator runs at compile time and turns new syntax into ordinary Lean terms. typeql!"…" is one. It reads the query literal, splits out the {…} interpolations, wraps each in a ToTypeQL call, scans the text for keywords such as insert or define, and produces a term of type Query .read, Query .write or Query .schema. You can ask Lean what it built:

#check typeql!"insert $p isa person;"
-- { text := … } : Query TxMode.write
#check typeql!"match $p isa person, has name \"insert\";"
-- { text := … } : Query TxMode.read      (keywords inside strings are ignored)

Because braces mean interpolation inside typeql!, TypeQL's own braces are written \{ and \}.

Where to learn more Lean

To learn more

For dependent types and logic applied to knowledge graphs, see Dependent Types (DTT) & Logic for AI Agent Ready Knowledge Graphs. For the database side, TypeDB for Edge AI Agents. Both are by the author of typedb-lean, on Leanpub.