Modeling a domain

This chapter models a small publishing domain twice, once as a TypeDB schema and once as Lean structures, and then lets the Lean side generate the TypeDB side.

From words to types

Start from how people describe the domain:

People write books. Some people are authors with a pen name. Readers review books and give them a rating. An award goes to an author for a particular book.

Sort the words into TypeDB's three kinds:

Two choices here are worth noticing. "Author" could be a role (someone is an author of something) or a type (someone is an author). It is both: author is a subtype of person because it carries a pen name, and authorship:author is the role any person plays when they write something. The award is the second choice. Giving it to the person loses which book it was for, and giving it to the book loses who won it. The thing that wins is the authorship.

Entities as structures

In typedb-lean, a structure with deriving Entity is an entity type. Fields are attributes it owns, and the field's Lean type decides the cardinality:

import TypeDB
open TypeDB

@[typedb "person"]
structure Person where
  email : Key String
  name : String
  deriving Repr, Entity

structure Book where
  isbn : Key String
  title : String
  year : Option Int64 := none
  genres : Attr "genre" (Array String) := #[]
  deriving Repr, Entity

@[typedb "person"] sets the type label. Without it, the label is the structure name in kebab-case, so Book becomes book. Lean does not accept attributes on structure fields, so the per-field markers Key, Attr and Role are written in the field types instead. They are transparent: a Key String is a String, and you build and read it as one.

Subtypes

Lean's extends becomes TypeDB's sub:

structure Author extends Person where
  penName : Attr "pen-name" (Option String) := none
  deriving Repr, Entity

An Author value has email, name and penName. In the database, an author instance is also a person: it is found by match $p isa person; and can play every role a person plays. A reference to an author converts to a reference to a person with r.up.

Relations and roles

A structure with deriving Relation is a relation type. Fields of type Role "name" (Ref T) are role players, and every other field is an owned attribute:

structure Authorship where
  author : Role "author" (Ref Person)
  work : Role "work" (Ref Book)
  deriving Repr, Relation

structure Review where
  reviewer : Role "reviewer" (Ref Person)
  subject : Role "subject" (Ref Book)
  rating : Int64
  deriving Repr, Relation

Ref T is a typed reference to an instance of T, either by its IID or by its key (Ref.key (α := Person) "ann@example.com"). From Role "author" (Ref Person) the library derives both relates author on the relation and person plays authorship:author. Two fields may share a role name; a friendship has two friend fields, and their players are read back in order.

Relations in roles

The award's winner is a reference to an Authorship, and that is all it takes for a relation to play a role:

structure Award where
  winner : Role "winner" (Ref Authorship)
  prize : String
  deriving Repr, Relation

In a property graph you would need an extra node to stand for the edge, or a second edge from the award to both the author and the book, with nothing to keep the two consistent. In TypeDB the authorship is already an instance, so it can play the role directly.

The generated schema

A schema is a list of TypeSpecs. Schema.defineText returns the TypeQL it generates (or an error, if two mappings give one attribute different value types), and Schema.defineTx runs it in a schema transaction:

def schema : List TypeSpec :=
  [TypeSpec.of Person, TypeSpec.of Author, TypeSpec.of Book,
   TypeSpec.of Authorship, TypeSpec.of Review, TypeSpec.of Award]

#eval match Schema.defineText schema with
  | .ok text => IO.println text
  | .error e => IO.eprintln e

define
  attribute email, value string;
  attribute name, value string;
  attribute pen-name, value string;
  attribute isbn, value string;
  attribute title, value string;
  attribute year, value integer;
  attribute genre, value string;
  attribute rating, value integer;
  attribute prize, value string;
  entity person, owns email @key, owns name @card(1..1);
  entity author, sub person, owns pen-name;
  entity book, owns isbn @key, owns title @card(1..1), owns year, owns genre @card(0..);
  relation authorship, relates author, relates work;
  relation review, relates reviewer, relates subject, owns rating @card(1..1);
  relation award, relates winner, owns prize @card(1..1);
  person plays authorship:author;
  book plays authorship:work;
  person plays review:reviewer;
  book plays review:subject;
  authorship plays award:winner;

Compare it with the hand-written schema in chapter 2. The structure is the same; the value types come from the Lean field types (Int64 is integer, String is string), and every cardinality comes from Option, Array or a plain field. You can still write parts of a schema by hand, such as an abstract supertype or functions. The ORM only needs the types it maps to exist and agree. Schema.verify! checks that (chapter 5).

Using the model

Inserts return typed references, which you pass on to relations:

def seed : Tx .write Unit := do
  let ann ← Entity.insert { email := "ann@example.com", name := "Ann", penName := some "A. Graph" : Author }
  let bob ← Entity.insert { email := "bob@example.com", name := "Bob" : Person }
  let book ← Entity.insert { isbn := "978-1", title := "Typed Graphs", year := some 2026,
                             genres := #["databases", "lean"] : Book }
  let a ← Relation.insert { author := ann.up, work := book : Authorship }
  discard <| Relation.insert { reviewer := bob, subject := book, rating := 5 : Review }
  discard <| Relation.insert { winner := a, prize := "Best Typed Book" : Award }

ann is a Ref Author; the authorship wants a Ref Person, so ann.up converts it. Passing ann directly would be a type error, and passing a Ref Book as the author is a type error too. The mistakes TypeDB would reject at run time are caught when you compile. Reads, updates and deletes use the same references:

let ann := Ref.key (α := Person) "ann@example.com"
Entity.update ann Person.field.name "Annie"      -- typed field handle
let p? ← Entity.get? ann                          -- Option Person
let awards ← Relation.all (α := Award)            -- Array (Ref Award × Award)

Polymorphic reads

Entity.all (α := Person) returns every person, including authors, decoded as Person. When you want each instance as its most specific type, list the cases in an inductive type and derive Polymorphic:

inductive AnyPerson where
  | person (p : Person)
  | author (a : Author)
  deriving Repr, Polymorphic

for (_, p) in ← Polymorphic.all (α := AnyPerson) do
  match p with
  | .person p => IO.println s!"person {p.name}"
  | .author a => IO.println s!"author {a.name} aka {a.penName}"

person Bob
author Ann aka (some (A. Graph))

The first constructor's type is the root that is queried. Each instance decodes into the constructor for its own type, or into the first constructor if its type is not listed. Because the match on p must cover every constructor, adding a subtype to AnyPerson makes the compiler point at every place that needs to handle it.

Guidelines

• Name relations after the fact, roles after the participation. authorship with author and work reads better in queries than writes with from and to.
• Use a subtype when a thing has more facts, a role when it takes part in something. An author has a pen name; a reviewer is just a person in a review.
• Reify when a statement is itself the subject of another statement. Awards, endorsements, provenance and corrections are often about a relation, not about its players.
• Prefer keys for anything users refer to. Ref.key lets you refer to an instance without first looking up its IID.
• Let the cardinality be visible in the Lean type. An Option field reads as "may be missing" everywhere it is used, and the schema says the same.