# DKE Python — Tutorial

**Version:** 1.1.2, changed in rev 151 · alpha · API 1.3 · rev 159\
**Status:** Published tutorial for DKE Python.\
**Audience:** Programmers who know Python and are writing DKE Python for the
first time.\
**This document as Markdown:** [dke-python-tutorial.md](/tutorial/dke/python/dke-python-tutorial.md) — the same text
this page is rendered from, for readers and tools that would rather have
the source than the page.

This tutorial teaches DKE Python by example; the
[Python Reference](/ref/dke/python/) is the exhaustive entry-per-construct
companion, and the [MCP Reference](/ref/dke/mcp/) specifies the transport
that carries a program to the service.

This tutorial **assumes you know Python.** It does not re-teach `def`, `for`,
`match`, or string building — you have those already. It teaches what those
familiar shapes *do in DKE*, the vocabulary that has no Python equivalent, and the
handful of places DKE deliberately departs from Python. The syntax is Python's;
the semantics are a deterministic reasoning engine's.

Every complete example below runs exactly as shown: each is a program body that
defines a procedure you can compile and run. The shorter fenced snippets are
fragments shown for illustration only.

---

## Chapter 1 — Coming from Python

DKE Python is a small language for **recording facts and reading them back** — you
tell the DKE service to *remember* a claim, then ask for it later with its
provenance and its type intact. It talks to the DKE service at `dke.langsyn.net`.

The one shift to make up front is *where your data lives*. A Python program keeps
state in variables and objects that vanish when the function returns; **a DKE
Python program keeps state in the store, as claims.** A *claim* is a value at an
addressed cell, stamped with the source that asserted it — and claims persist,
carry their own type, remember their history, and can be *reasoned over* long
after your program has finished. Local variables still exist, but they only hold
what you are about to write or have just read. The durable state is always the
store.

Here is the Python you already know, translated into DKE habits:

| In Python you… | In DKE Python you… |
|---|---|
| keep state in variables and objects | record **claims** in the store — persistent, typed, and stamped with a source |
| mutate a value in place | *supersede* it — the prior value stays as history you can walk |
| `return` a value from a function | the same — a `def` returns it, and the caller binds the result |
| loop with `while`, recursion, or an unbounded `for` | iterate a **finite collection** with `for … in` — every program is guaranteed to terminate |
| take a fractional power of an `int` with a computed exponent (`2 ** n`) | write it as a literal (`2 ** -1` is `0.5`) or make the base a `real` — a *runtime*-negative exponent refuses, because the type is fixed before the value is known |
| catch a `ZeroDivisionError` | a divide-by-zero **refuses** — a catchable outcome, not an exception |
| format with `.format` or `%` | the same, or an f-string — `f"{x:.2f}"`, Python's own |
| pass `key=lambda w: w[-1]` | name a short `def` and pass the name, `key=last_letter` — no value holds a function, so there is no `lambda` |
| `match` on structural patterns | the same, on values and on the shape of a list or a dict — and also on a read result's kind, a value's class, or an instance's class |

Keep that table in the corner of your eye; the chapters ahead earn every row —
and **when you get one of them wrong, you get told what to write instead.** A
compile that fails refuses the whole submission (nothing is stored) and answers
with the line, the column, and the DKE Python form that belongs there. Write
`while` and it says there is no `while` and hands you `for <var> in <finite
collection>:`. So a first draft written on Python reflexes is usually one edit
from compiling rather than a rewrite, and the fastest way to learn this table is
to get a row wrong on purpose and read the answer.

Here are three of those rows broken on purpose, and what comes back. The first
is refused when you **compile**; the other two compile and refuse when they
**run** — a distinction the table's wording is careful about, and one worth
having in hand before Chapter 2.

Unbounded iteration is refused at compile time, so nothing is stored at all:

```dpy
def tally(k: string):
    while True:                  # rejected: DKE Python has no `while`
        print(k)
```

A computed negative exponent compiles — the type is fixed before the value is
known — and refuses when it runs:

```dpy
# negative-exponent.dpy — a computed negative exponent on an int base refuses.
def shrink():
    n = 0 - 1
    print(2 ** n)
```

```
error: script shrink() failed — line 4: a negative exponent needs a real base — write the base as a real (e.g. `2.0 ** -1`), or write the exponent as a literal
```

Take either way out it offers and it runs: `2.0 ** n` makes the base a real, and
`2 ** -1` is a literal exponent, which is `0.5`.

A divide by zero refuses the same way. A refusal is an outcome your caller can
read, not an exception that unwinds:

```dpy
# divide-by-zero.dpy — a divide by zero refuses at run time.
def ratio():
    print(1 // 0)
```

```
error: script ratio() failed — line 3: integer division or modulo by zero
```

If you are driving the service from a program rather than by hand, that
correction arrives as its own field — `fix`, beside the human-readable
`message` — so a client can apply it without parsing prose. The [MCP Reference §6.1](/ref/dke/mcp/#the-repair-loop-a-rejected-submission-its-fix-and-the-resubmit) works an example end to end.

And one capability has no Python row at all: **the engine reasons.** You can declare
facts the engine *derives and maintains on its own* — recompute-on-change fields,
standing rules, and what-if hypotheses. That is where DKE Python stops resembling
a scripting language and starts resembling a deterministic reasoning engine you program. It is
Chapter 8, and it is the reason the language exists.

### Your first program

A DKE Python source file is the **program body**: it begins with your first
declaration or statement, and its keywords are English.

A **procedure**, introduced with `def`, records and reads facts and prints lines
with `print`. Here is a complete first program, a single procedure:

```dpy
# hello-store.dpy — record one fact, read it straight back.
def hello_store():
    remember(Greeting.hello.text, "world", "op1")
    cur = current(Greeting.hello.text)
    match cur:
        case active_claim:
            print("greeting = " + str(cur.value) + " (per " + str(cur.source) + ")")
        case empty:
            print("nothing recorded yet")
```

Three things are happening, and only one of them looks like Python:

- `remember(Greeting.hello.text, "world", "op1")` **records a claim**: at the
  *cell* named `Greeting.hello.text` (a kind `Greeting`, a subject `hello`, an
  attribute `text`), the value `"world"`, attributed to the source `"op1"`. No
  Python assignment does this — the fact goes into the store, not into a variable.
- `current(Greeting.hello.text)` **reads back** the live claim at that cell.
- `match cur:` inspects the result. Reading a cell gives you either an
  `active_claim` or `empty`, and a `match` must handle both. Here the `match`
  dispatches on the result's *kind*, and the `case` syntax is the one you know;
  Chapter 9 gathers everything else a `match` can test. Inside the `active_claim`
  arm, `cur.value` and `cur.source` are available.

### Compiling and running

A DKE Python program runs at the DKE service in two wire steps ([MCP Reference §4](/ref/dke/mcp/#the-two-compute-verbs)). First you
**compile** the source as a module, here named `hello` — the service typechecks it
and stores each procedure the module defines ([MCP Reference §4.1](/ref/dke/mcp/#compile-validate-and-store-a-module)):

```
compile(name = "hello", source = "<source>")
```

Then you **run** instructions that import the module and call the procedure by
its module-qualified name — the module, a dot, the procedure ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

```
run(source = "import hello\nhello.hello_store()")
```

The service runs them and returns a transcript — a header with a verdict tallying
what the run did, then the lines the program printed and the facts it recorded, in
execution order:

```
OK program: 1 claim written, 1 print
  remember Greeting.hello.text = "world"
  print greeting = world (per op1)
```

`run` keeps nothing: the instructions execute once, the data they write lands in
the store, and the source itself leaves no trace. That is also why it takes
instructions and never definitions — a `def`, a `class` or a standing `@rule` in a
run's source is refused, because a definition made there would take effect
nowhere ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)). So: `compile` is for *keeping* a program, so later
instructions can call it and its rules can stand; `run` is for *trying*
instructions and for calling what you kept.

That is the whole shape of the language — the rest of this tutorial fills in the
values you can record, the questions you can ask, the reasoning the engine can do
on your behalf, and the control flow that ties it all together.

---

## Chapter 2 — Claims, cells, and provenance

Chapter 1 recorded a claim with `remember` and read it back with `current`. Those
two verbs are the heart of DKE programming, so before anything else, meet the
model they work over and the fuller cast around them.

Every fact in the store is a **claim**: a value at a **cell**, from a **source**.
A cell is addressed by a three-part path `K.s.a` — a *kind* `K`, a *subject* `s`,
and an *attribute* `a` (`Greeting.hello.text`, `Cat.felix.color`). You never
declare a kind or a subject up front; naming a cell brings it into being. Where a
Python object has fields you assign, a DKE subject has attributes you *claim* —
and the difference that matters is the third argument every write carries.

### Writing

- `remember(K.s.a, v, src)` — record a value from a source. A *different* value
  from a *different* source stands alongside as a co-active alternative; to revise
  a value from the *same* source, use `update`.
- `update(K.s.a, v, src)` — revise the value from that source, superseding its
  prior one (and establishing a value on an empty cell). A value from another
  source stands beside it; restating what the source already holds changes
  nothing.
- `qualifiers={…}` on either — facts the writer states about the claim it is
  writing, such as how the value was measured or how sure the writer is:
  `remember(Reading.r1.temp, 21, "lab", qualifiers={"method": "observed"})`. A
  read gives them back as `c.qualifiers`. They belong to that one claim, and the
  store keeps them without acting on them.
- `forget(K.s.a)` / `forget(K.s)` — **permanently** remove data (path-scoped).
  This is a hard erase: every value ever recorded at the cell is reclaimed, not
  just the current one, and `forget(K.s)` removes the whole subject and its
  kind. Nothing is kept in history that a read can reach, and nothing in this
  language puts it back. One qualifier lives outside the language: while a
  checkpoint stands, a removed value is copied to an archive no read path joins,
  so the `restore` tool of the [**MCP Reference**](/ref/dke/mcp/) can
  bring it back, given a `read-write-delete` key: a value that was in force
  returns as a new claim, and an older version goes back into the history where
  it stood. That is a re-assertion and not a rewind — the removal still happened. Removal
  cascades into facts derived from the target instead of refusing while they
  exist, and needs a `read-write-delete` key.
- `forget(K.s.a, datetime("…"))` — remove only what was **true at that instant**, leaving
  the rest of the cell's history standing. Reach for this when you want to shed a
  period rather than a cell: you name a moment, and the values whose validity
  window covers it go. An instant nothing covers removes nothing and is not an
  error. The [Python Reference](/ref/dke/python/) has the full form list, including removing one named
  claim, by its value and source, by the claim a read returned, or by that
  claim's `.claim_id` (below).
- `forget(K.s.a, recorded_before=datetime("…"))` — trim **history**: remove the older
  versions written before that instant, keeping whatever is in force now.
  Unlike every other form above, a range can never empty a cell — the value in
  force always survives one. `valid_before=` asks the other question, removing
  the older versions that stopped being *true* before the instant, and both
  have an `at_or_before` spelling for the boundary. There is no `after` form on
  purpose: it would reach the current value, which is a different operation
  with its own spelling.

  A range is also the one form that takes **more than a cell**: `forget(K.s,
  <range>)` trims every cell of a subject and `forget(K, <range>)` trims the
  whole kind. That is what it is for — a year of history is not something you
  can drop one cell at a time. The safety property holds at every width, so
  even the kind-wide form cannot empty anything. A bare `forget(K)` with no
  range is refused: emptying a kind is not a thing to reach by leaving a path
  short.
- `would_forget(K.s.a, recorded_before=datetime("…"))` — how many versions that same
  range **would** remove, removing none. It takes the same three widths, so
  every removal you can write has a preview you can write. It is a read, so a
  read-only key can ask, and a removal you have counted first is one you
  meant — at `K.s` and `K`, count first.
- `assert(K.s.a, src)` — record an **absence** — that there is deliberately no
  value — with no value argument. A rule can tell a recorded absence from a
  value nobody wrote, and conclude one itself (`known_absent`, Chapter 8).
- `pin(K.s.a)` — protect a cell that holds a value: while it is pinned,
  `forget` refuses there, until `unpin(K.s.a)` lifts it. `list_pinned()` lists
  what is pinned. Pinning a cell with no value, or one already pinned, refuses.

Every write takes a **source** as its last argument: provenance is not
optional. A claim always knows where it came from. This is the habit with no
Python equivalent — you do not just store `"final"`, you store *that `op1` said
`"final"`* — and it is what makes a store auditable rather than merely stateful.

This example revises a value, marks a cell, removes another, and records a
deliberate absence:

```dpy
# revise-remove-mark.dpy — supersede, pin, forget, and assert absence.
def revise_remove_mark():
    remember(Widget.w1.state, "draft", "op1")
    update(Widget.w1.state, "final", "op1")     # revise (same source supersedes)
    pin(Widget.w1.state)                          # mark the cell
    remember(Widget.w1.note, "temp", "op1")
    forget(Widget.w1.note)                        # drop that cell's claims
    assert(Widget.w1.price, "op1")               # record a deliberate absence
    print("revised, marked, removed, and asserted")
```

Notice that `update` supersedes rather than overwrites: the prior value stays as
history you can walk. Removal is the deliberate exception — `forget` reclaims
every value at the path it names, and what it removes does not come back.

### Reading

- `current(K.s.a)` gives the live `active_claim` (or `empty`).
- `get(K.s.a)` gives the full **history** as a `claim_list` you can iterate.

Recording twice and reading the history shows how claims accumulate:

```dpy
# history-walk.dpy — record, supersede, then walk the history.
def history_walk():
    remember(Cat.felix.color, "grey", "op1")
    update(Cat.felix.color, "orange", "op1")     # same source supersedes
    cur = current(Cat.felix.color)
    match cur:
        case active_claim:
            print("current colour = " + str(cur.value) + " (per " + str(cur.source) + ")")
        case empty:
            print("no colour")
    hist = get(Cat.felix.color)
    print("history depth = " + str(hist.length))
```

### Fields on a claim

An `active_claim` exposes typed fields: `.value` (the typed value),
`.source` (who recorded it), `.created_at` (when, as an RFC 3339 UTC string), and
`.trust`. A `claim_list` and any collection answer `.length`, and any value or
discriminator answers `.kind`. Only ever read `.value`/`.source` on a claim you
know is active — inside a `case active_claim:` arm, or right after a write. This
is why reads come back as a `match`-able result rather than a bare value: there is
no `None` to trip over, because `empty` is a case you are made to handle.

A claim also has a name of its own. `.claim_id` is its cell path, a `#` and a
code of twelve hexadecimal digits — `Cat.felix.color#3f09c1a27b44` — and a claim
carries the same id on every read. Writing, revising or removing some other claim
leaves it unchanged, so an id you read today names the same claim tomorrow, in
this program or a later one. A revision is a new claim, and has an id of its own:

```dpy
# claim-id.dpy — a claim keeps its name while other claims change around it.
def claim_id():
    remember(Cat.felix.color, "orange", "op1")
    first = current(Cat.felix.color)
    remember(Cat.felix.age, 3, "op1")            # a write somewhere else
    again = current(Cat.felix.color)
    print("same claim: " + str(first.claim_id == again.claim_id))
    update(Cat.felix.color, "grey", "op1")       # a revision is a new claim
    revised = current(Cat.felix.color)
    print("after the revision: " + str(first.claim_id == revised.claim_id))
```

```
OK script claim_id(): 3 claims written, 2 prints
  remember Cat.felix.color = "orange"
  remember Cat.felix.age = 3
  print same claim: True
  update Cat.felix.color = "grey"
  print after the revision: False
```

Keep the id wherever you would keep a pointer to the claim — in a variable, in a
list, or recorded as a string value. Chapter 11 hands it to the verbs that trace
a claim and to `forget`.

The other fields each answer one question, and the chapter that asks it
introduces the field: `.valid_from` and `.valid_to`, the window a claim was
recorded for (Chapter 4); `.preferred`, whether it is the one you said you go by,
and `.written_by`, the store key that wrote it (Chapter 5); `.derived_by` and
`.rule_kind`, what concluded it (Chapter 12). One more is worth knowing before
you reach rules. `.maintained` is `False` on a value a rule concluded and cannot
keep current: the value is the last one the rule produced, and the data behind
it has moved on. Every read still serves such a value, so where it matters,
check the flag beside the value:

```
c = current(Totals.all.sum)
match c:
    case active_claim:
        if not c.maintained:
            print("this total is not being kept current")
    case empty:
        pass
```

The flag is decided when you read, so read it with the value it describes rather
than keeping it from an earlier read. The [Python Reference](/ref/dke/python/)
lists every field a claim has.

### `empty` is one answer to two different questions

A cell you never wrote reads `empty`. So does a cell you DID write, whose value
carries a validity window that does not cover the moment you asked about
(Chapter 4 records values across time and shows how a window is written).
The read cannot tell you which, and it does not try — it answers about the
instant you asked about, and at that instant there is nothing.

Both hold in a kind the store knows: one it holds something under now, or one a
class declares (Chapter 7). A read that names a kind the store knows nothing about
is not `empty` — it refuses with `no such kind`, because a kind nothing was ever
written to is far likelier to be a misspelling than a question. So the program
below writes one sensor before it reads another. Declaring the class is the other
way to read a kind while it holds nothing.

`why_not` tells you which:

```dpy
# out-of-force.dpy — the same empty read, explained.
def explain_empty():
    remember(Sensor.hall.temp, 19.5, "ops")
    reading = current(Sensor.room.temp)
    match reading:
        case active_claim:
            print(str(reading.value))
        case empty:
            reason = why_not(Sensor.room.temp)
            print(reason)
```

For a cell that was never written it says no rule concludes it. For one that is
recorded but out of force it says so **and names the value it holds** — a fact
you already have, not one to go and find. Reach for it the first time an empty
answer surprises you. When a whole QUERY comes back empty rather than one cell,
the store-wide version of the same question is the `checkup` tool on the wire
([MCP Reference §9.6](/ref/dke/mcp/#checkup-does-your-store-meet-the-reasoning-over-it)) — it is a tool and not a language verb, so it is something you call
instead of a program, not something you write inside one.

---

## Chapter 3 — Typed values

A recorded value **carries its own type**, and you get that exact type back when
you read it. DKE Python has nine value classes: you can *write* eight of
them as values, and the ninth, `null`, you *detect* on read.

### Writing typed values

The write literals are:

- **string** — `"orange"`, with the escapes `\\ \" \n \t \r \a \b \f \v`, a
  character by number (`\xNN`, `\uNNNN`, `\UNNNNNNNN`) or by its Unicode name
  (`\N{BULLET}`). Raw, triple-quoted and formatted strings close this chapter.
- **int** — `42`, and also `0xDE_AD`, `0o17`, `0b1010`, `1_000_000`.
- **bool** — `True` or `False`.
- **datetime** — `datetime("2026-01-02T03:04:05Z")`, an RFC 3339 UTC instant; the `Z` is
  required and 1–9 fractional-second digits are allowed.
- **duration** — `duration("PT1H30M")`, an ISO 8601 span (`P[nD][T[nH][nM][nS]]`, no
  calendar years or months). The lowest term may carry up to nine fractional
  digits, so spans are exact to the nanosecond — `duration("PT0.5S")`.
- **real** — `3.5`, a fractional number (a digit on each side of the point; `_`
  separators allowed, `3` alone stays an int).
- **blob** — `blob("48656C6C6F")`, an opaque byte string as an even count of hex
  digits — or the same bytes as base64, `blob_b64("SGVsbG8=")` (both read back as
  canonical hex).
- **scientific** — `scientific("6.022e23")`, a number that keeps its significant
  figures (a mantissa and a required exponent).
  `scientific("6.022e23")` and `scientific("6.0220e23")` are the same magnitude
  but distinct values — the trailing zero counts.
- **complex** — `3 + 4j`, a number with a real part and an imaginary part. `4j`
  is the imaginary literal, a number followed by `j`, and the sum is how you
  write one with a real part, as in Python. It prints the way Python prints it,
  `(3+4j)`. `complex(3, 4)` builds the same number from its two parts, and
  `complex("3+4j")` reads it from text. A complex is also what a negative
  number under a fractional power is: `(-8) ** 0.5`, or `complex(x) ** 0.5`
  for a number held in `x`.

The type is chosen by the literal you write — `42` records an int, `"42"` records
a string, and the two never collide on read:

```dpy
# values-write.dpy — three cells, three different value classes.
def values_write():
    remember(Widget.w1.size, 42, "op1")          # int
    remember(Widget.w1.ready, True, "op1")        # bool
    remember(Widget.w1.label, "42", "op1")        # string (not the int 42)
    n = current(Widget.w1.size)
    match n:
        case active_claim:
            print("size = " + str(n.value))
        case empty:
            print("no size")
```

`datetime` and `duration` read back in a canonical form — `duration("PT90M")` comes back
as `PT1H30M`, and a datetime keeps its instant:

```dpy
# datetime-round-trip.dpy — a datetime value keeps its type across write/read.
def datetime_round_trip():
    remember(Event.launch.at, datetime("2026-01-02T03:04:05Z"), "ops")
    cur = current(Event.launch.at)
    match cur.value:
        case datetime as d:
            print("launch at " + str(d))
        case default:
            print("not a datetime")
```

```dpy
# duration-round-trip.dpy — a duration keeps its type and reads back canonical.
def duration_round_trip():
    remember(Task.build.budget, duration("PT90M"), "ops")
    cur = current(Task.build.budget)
    match cur.value:
        case duration as u:
            print("budget = " + str(u))               # prints PT1H30M
        case default:
            print("not a duration")
```

`real` and `blob` round-trip the same way. A real reads back in a canonical
decimal form (`3.50` comes back as `3.5`), and a blob reads back as canonical
uppercase hex:

```dpy
# real-blob-round-trip.dpy — a real and a blob keep their types across write/read.
def real_blob_round_trip():
    remember(Sensor.a.reading, 3.5, "ops")
    remember(Doc.d1.payload, blob("48656C6C6F"), "ops")
    r = current(Sensor.a.reading)
    match r.value:
        case real as rv:
            print("reading = " + str(rv))             # prints 3.5
        case default:
            print("not a real")
    b = current(Doc.d1.payload)
    match b.value:
        case blob as bv:
            print("payload = " + str(bv))             # prints 48656C6C6F
        case default:
            print("not a blob")
```

### The `value` union

When you read a claim's `.value`, its type is one of these classes:

```
value = int | bool | string | datetime | duration | real | null | blob | scientific | complex
```

You discriminate them with a `match` over `.value`. The writable classes can
**bind** the typed value with `as`; the one detect-only class, `null`, is matched
**bare** — it is never a value you store (an absent value is asserted with the
`assert` verb, Chapter 2, and the one place you write the word `null` is the open
end of a validity window, Chapter 4), but you can still recognise it on read:

```dpy
# value-classes.dpy — every value class discriminated on read.
def value_classes():
    remember(Sensor.room.count, 41, "op1")
    c = current(Sensor.room.count)
    match c.value:
        case bool as b:     print("flag = " + str(b))
        case int as n:      print("next = " + str((n + 1)))     # n : int, arithmetic OK
        case string as s:   print("text = " + str(s))
        case datetime as d: print("time = " + str(d))
        case duration as u: print("span = " + str(u))
        case real as r:     print("half = " + str((r / 2)))      # r : real, arithmetic OK
        case blob as b2:    print("bytes = " + str(b2))          # b2 : blob
        case scientific as s: print("sci = " + str(s))          # s : scientific
        case complex as z:  print("size = " + str(abs(z)))      # z : complex, arithmetic OK
        case null:          print("an absent value")        # detect-only, no binding
```

A `match` over `.value` must either name every class or end with a
catch-all, `case default:` or `case _:`, which mean the same. Because the
recorded value here is an int, the `int` arm runs — and because every arm is
type-checked, `case int as n:` can safely do integer arithmetic on `n`.

When several classes take the same action, one arm can name them all, separated
by `|`:

```
match c.value:
    case int | real | scientific:  print("a number")
    case default:                  print("not a number")
```

That is the same program as three separate arms with the same body — a shorter
spelling, not a different rule. An arm written this way takes no `as` binding,
because the alternatives would each bind a different type and the name would
have no single one; when you need the value, write the arms out separately.

The same `|` joins *values* when you match a plain `int`, `real`, `string` or
`bool` rather than a `.value`: there `case 1 | 2:` compares, as Python's `match`
does. Those value patterns are taught in Chapter 9.

An arm can also ask a question about the value it matched, with `if`:

```
match c.value:
    case int as n if n > 100:  print("big")
    case int as n if n > 0:    print("positive")
    case int:                  print("zero or negative")
    case default:              print("not an int")
```

The arms are tried top to bottom and the first one that both matches the class
and passes its `if` runs. `n` is bound before the `if` is asked, which is what
lets the condition talk about the value.

One rule is worth learning early, because it is where a guarded `match` usually
first refuses to compile: **a guarded arm does not count as covering its class.**
Its `if` might be false, so the language cannot treat it as handling every int.
Write a plain `case int:` below the guarded ones — as above — or end with
`case default:`. That is also why `case default:` may not itself carry an `if`:
it is the arm that always runs, and a guard on it would leave nothing that does.

`match` has one more shape to it. Everything above dispatches on the *class* of a
stored value; you can also match on the *shape* of a list or a dict:

```
match parts:
    case []:              print("nothing")
    case [only]:          print("just " + only)
    case [first, *rest]:  print(first + ", plus " + str(rest.length) + " more")
    case default:         print("unreachable")
```

A plain name in the brackets binds whatever is in that slot, so `only` and
`first` are yours to use in the arm. `*rest` scoops up everything left over and
has to come last. Writing a literal instead of a name turns that slot into a
test: `case [1, b]:` matches only lists that start with `1`.

Dicts work the same way, by naming keys:

```
match record:
    case {"id": i, "kind": "sensor"}:  print("sensor " + i)
    case default:                      print("not a sensor")
```

The arm is taken when all the keys it names are there — other keys are simply
ignored, so this asks "does it have these?" rather than "is it exactly this?".

As in Python, you can match on any expression, and no arm has to be taken: when no
pattern fits, none runs and the program carries on below the `match`. Numbers **compute** with `+ - * / // ** %` and the
ordered comparisons `< > <= >=`, over `int` and `real` alike, matching Python 3:
`/` is **true division** (`7 / 2` is `3.5`), `//` is **floor division** (`7 // 2`
is `3`, `-7 // 2` is `-4`), `%` is **floor modulo** at either operand class (the
sign follows the divisor, so `-7 % 2` is `1` and `-7.5 % 2` is `0.5`), and `**`
is **power** (right-associative). One DKE specific is worth pinning now: `2 ** -1`
is `0.5` as you would expect, but an `int` base with an exponent that only turns
out negative at run time (`2 ** n`) **refuses** — a written literal can be typed,
a computed value cannot, and the refusal names the fix. And where Python raises,
DKE **refuses**: dividing by zero, an integer overflow, or a result out of range
is a catchable refuse rather than a garbage number or an exception.

### The type system at a glance

The value classes above are what you *store*. They are part of a larger, closed
vocabulary of built-in types; the only types you add to it are the classes you
declare (Chapter 7). Most built-in types you never write down; you meet them as
the shapes verbs hand back. They fall into a few families:

| Family | Types | You meet them as |
|--------|-------|------------------|
| Primitives | `string`, `int`, `bool` | literals, `.length`, comparison results |
| Value | `value`, `datetime`, `duration`, `real`, `blob`, `scientific`, `complex` | a claim's `.value` union and its named value-class types (`null` is a further *class* of the union, not a standalone type) |
| Discriminators | `active_claim` (with its `empty` case), `verify_result` | results of `current` and `verify` — destructured with `match` |
| Finite collections | `claim_list`, `proof_tree`, `diagnosis`, `subject_set`, `string_list`, `result_type_set` | results of `get`, `why`, `why_not`, `subjects`, and the `list_*` verbs — iterated with `for … in` |
| Handler bindings | `refuse_info`, `engine_error_info` | what `except refuse as e` and `except engine_error as e` bind (Chapter 9) |

That is the whole built-in vocabulary; the table in
[Python Reference §4.1](/ref/dke/python/#the-base-types) lists every entry.

Two accessors work across every family: `.length` gives an `int` for any string or
collection, and `.kind` gives the type's name as a `string` for any discriminator
or a `proof_tree`. You meet each of these types as the tutorial goes — the
collections in Chapters 5 and 11 and the discriminators throughout.

### Working with strings

Strings are more than something to concatenate with `+`. You can read one
character with `s[i]`, take a substring by **slicing** with `s[a:b]`, search
with `s.find(sub)`, count with `s.count(sub)`, test the ends with
`s.startswith(prefix)` / `s.endswith(suffix)`, rewrite with `s.replace(old,
new)`, change case with `s.upper()` / `s.lower()`, and trim the ends with
`s.strip()` / `s.lstrip()` / `s.rstrip()`. Positions count characters, and
`.length` is the character count. Slicing and every string method are *total* —
they never fail: an out-of-range slice bound is clamped, `find` returns `-1`
when the substring is absent, and case mapping is character-for-character (so a
string keeps its length).

A common shape is cleaning up a value, then splitting it on a separator — trim
it, test it, find the separator, and slice around it:

```dpy
# strings-tutorial.dpy — trim, test, search, slice, and change case.
def strings_tutorial():
    email = "  Merlin@Langsyn.org  ".strip()
    at = email.find("@")
    print("user = " + str(email[:at]).lower())     # everything before the @
    print("host = " + str(email[at + 1:]))         # everything after
    print("length = " + str(email.length))         # character count
    print("is org = " + str(email.endswith(".org")))
    print("dots = " + str(email.count(".")))
    print("has at = " + str(("@" in email)))        # substring membership
    print("shown = " + str(email.upper()))
```

To test whether one string appears inside another, use `in` (and `not in`) —
the same operator Python uses: `"@" in address` is `True` when the address
contains an `@`. It tests substring containment, so it is string-only; the `in`
in a `for` loop is a different thing (the loop keyword, iterating a finite
collection).

Both bounds of a slice are optional (`s[a:]`, `s[:b]`, `s[:]`), and a slice can
take a third **step** value — `s[a:b:step]` — that picks every `step`-th
character. A negative step goes backwards, so `s[::-1]` reverses a string and
`s[::2]` takes every other character. **Negative positions count from the end**,
the same as Python: `s[-1]` is the last character, `s[-3:]` the last three, and
`s[:-1]` everything but the last. The strip family also takes an optional set
of characters to trim instead of whitespace (`s.strip("*_ ")`). The string
methods introduced here are `find`, `count`, `startswith`, `endswith`,
`replace`, `upper`, `lower`, and `strip`/`lstrip`/`rstrip` — enough for the work
in this chapter. The method set is **closed**: there is no open namespace to
extend, and the [Python Reference](/ref/dke/python/) lists every member. It is
also larger than this chapter needs — the methods that bridge text and
collections (`split`, `join`, `partition`, `splitlines`) arrive with lists in
Chapter 14 and tuples in Chapter 15, once there is something for them to
return. Until then, reach for slicing and these methods, composed with `+` and
`.length`.

### Writing a string literal

A string literal takes Python's forms, not only the plain `"…"`:

- A **raw** string, `r"…"`, keeps every backslash as an ordinary character, so a
  path or a pattern is written the way it looks.
- A **triple-quoted** string, `"""…"""`, runs to the next `"""`, so it can span
  lines and hold a lone `"` without an escape.
- Two literals with only whitespace between them **join** into one, with no
  `+` — inside parentheses they may sit on separate lines, which is how a long
  constant is split.
- The **escapes** are Python's: `\\ \" \' \n \t \r \a \b \f \v`, a character
  by number (`\xNN`, `\uNNNN`, `\UNNNNNNNN` for one past `U+FFFF`, and one to three
  octal digits), and a character by its Unicode name (`\N{BULLET}`).

```dpy
# string-literals.dpy — raw, escaped, triple-quoted and joined strings.
def string_literals():
    path = r"C:\temp\new"
    print(path)
    print("\N{BULLET} by name, \u00e9 by number, \U0001D11E past U+FFFF")
    note = """first line
second line"""
    print(note)
    title = ("a long title "
             "written across two lines")
    print(title)
```

```
OK script string_literals(): 4 prints
  print C:\temp\new
  print • by name, é by number, 𝄞 past U+FFFF
  print first line
second line
  print a long title written across two lines
```

That is what Python prints for the same lines. A backslash before anything else
stays in the value with the backslash, as in Python, so `"C:\path"` is the same
string as `r"C:\path"` and `"C:\\path"`. One place differs on purpose: no escape may
produce the NUL character, so `"\0"` is refused: a string never holds one.

### Putting values into text — f-strings

`+` joins two strings and nothing else, which is why the examples so far wrap
every number in `str(…)`. An **f-string** does that work in one literal: put an
`f` before the quote, and each `{…}` inside holds an expression whose value is
written in place. `f"{name} has {count} sensors"` is the same string as
`name + " has " + str(count) + " sensors"`. After a colon a field takes
Python's format spec — `{share:.2f}` for two decimals, `{count:>4}` to pad to
four places, `{name:*^8}` to centre — `{name!r}` writes the value's `repr`,
`{count * 2=}` writes the expression followed by its value, and `{{` and `}}`
are literal braces. A list, tuple, dict, set, dict view or slice takes no spec at all: write `f"{xs}"`, never `f"{xs:>6}"`, which is refused:

```dpy
# f-strings.dpy — values written straight into text, with and without a format spec.
def f_strings():
    name = "hall"
    count = 7
    share = 2 / 3
    print(f"{name} has {count} sensors")
    print(f"share {share:.2f}, padded [{count:>4}], centred [{name:*^8}]")
    print(f"{name!r} is quoted, {{braces}} are doubled, and {count * 2=}")
    remember(Sensor.hall.reading, 21.5, "ops")
    r = current(Sensor.hall.reading)
    match r:
        case active_claim:
            print(f"reading {r.value} per {r.source}")
        case empty:
            print("no reading")
```

```
OK script f_strings(): 1 claim written, 4 prints
  print hall has 7 sensors
  print share 0.67, padded [   7], centred [**hall**]
  print 'hall' is quoted, {braces} are doubled, and count * 2=14
  remember Sensor.hall.reading = 21.5
  print reading 21.5 per ops
```

A field holds a name, arithmetic, a method call, an element or a slice such as
`xs[0]` or `s[1:]`, or a field of a claim you already hold, like `{r.value}`
above. A store read goes into a name first, exactly as with `+`. An f-string
joins its neighbours like any literal, which is how you write a long one across
lines; it cannot itself be triple-quoted, and `r` and `f` combine as `rf"…"`.
The full list of what a field accepts is in the
[Python Reference](/ref/dke/python/).

Python's two older ways to format are here too. `"{:.2f}".format(x)` and
`"%.2f" % x` each give what `f"{x:.2f}"` gives. What the f-string holds is checked as
the program compiles, and a mistake in the other two refuses as it runs, in Python's
words.

### Mathematics with `math` and `cmath`

Python's `math` and `cmath` are here, with the functions a numeric program
reaches for most. Import them as you would in Python. Neither lives in your
store, so the `import` reads nothing from it.

```dpy
# triangle.dpy — a right triangle's long side and angle, the angle again from
# its sine, the same triangle as a complex number, and a logarithm outside its
# domain caught as a refusal.
import math
import cmath

def triangle():
    a = 3.0
    b = 4.0
    c = math.hypot(a, b)
    print("hypotenuse " + str(c))
    print("angle " + str(round(math.degrees(math.atan2(b, a)), 2)) + " degrees")
    print("from its sine " + str(round(math.degrees(math.asin(b / c)), 2)) + " degrees")
    z = complex(a, b)
    print("as a point " + str(cmath.polar(z)))
    print("same angle: " + str(math.isclose(cmath.phase(z), math.atan2(b, a))))
    try:
        x = math.log(-1)
    except refuse as e:
        print("refused (" + e.discriminator + "): " + e.reason)
```

```
OK script triangle(): 6 prints
  print hypotenuse 5.0
  print angle 53.13 degrees
  print from its sine 53.13 degrees
  print as a point (5.0, 0.9272952180016122)
  print same angle: True
  print refused (value_error): math domain error
```

`math` has the square root, the exponential and logarithm, the trigonometric
functions and their inverses, the distance `hypot`, conversion between degrees
and radians, logarithms to base 10 and 2 and to any base, the error function
`erf` and `erfc`, `gamma` and `lgamma`, `isclose`, `floor`, `ceil` and the constants; `cmath` has the
complex exponential and square root, phase and polar form. Every answer is correctly rounded at each step, so it is the same
wherever your program runs. Where Python raises, as `math.log(-1)` does above,
the call refuses with Python's message, and you catch it as any refusal. The
whole list, with what each function takes, is in the
[Python Reference](/ref/dke/python/).

### Applying a matrix with `vector`

A list of 2ⁿ numbers can be read as a table with n axes of two places each,
where bit a of an element's index is its place on axis a. `vector.apply` applies
a matrix along the axes you name, in one call, so a step that would otherwise be
a loop over pairs of elements is one line. `vector` is DKE's own rather than
Python's, and you import it as you import `math`.

```dpy
# totals.dpy — running totals of a 2 × 2 table of readings, taken along one
# axis and then the other, and an axis the list does not have, caught as a
# refusal.
import vector

def totals():
    running = [[1, 0], [1, 1]]
    xs = [4, 2, 1, 3]
    xs = vector.apply(xs, running, [0])
    print("along axis 0 " + str(xs))
    xs = vector.apply(xs, running, [1])
    print("along both " + str(xs))
    try:
        xs = vector.apply(xs, running, [2])
    except refuse as e:
        print("refused (" + e.discriminator + "): " + e.reason)
```

```
OK script totals(): 3 prints
  print along axis 0 [4, 6, 1, 4]
  print along both [4, 6, 5, 10]
  print refused (value_error): vector.apply(): axis 2 is out of range for a vector of 4 elements
```

The second argument is the matrix, and the third names the axes it acts on.
Along axis 0, `running` leaves the element at 0 as it is and adds it into the
element at 1, and does the same for 2 and 3; along axis 1 it pairs 0 with 2 and
1 with 3. Along both, each element holds the total of the readings at or before
it on both axes, so the last is the sum of all four. A matrix along two axes is
4 × 4, and the first axis named is the high bit of its rows. A call is one operation however long the list is, and each
element keeps the class its arithmetic gives, as it would in Python. The
[Python Reference](/ref/dke/python/) states exactly what a call computes.

`vector.sumsq` adds along the same axes. It squares the real and the imaginary
part of every element and answers one total for each place on the axes you name,
as a list of reals, in one call, so the squared size of each half of a list is one
line and not a loop over its elements. Each total is `math.fsum`'s, rounded once
whatever the order the squares are added in.

```dpy
# weights.dpy — the squared size of four readings, added over everything, along
# axis 0 and along axis 1, and an axis the list does not have, caught as a
# refusal.
import vector

def weights():
    xs = [3, 4, 12, 5]
    print("all " + str(vector.sumsq(xs, [])))
    print("along axis 0 " + str(vector.sumsq(xs, [0])))
    print("along axis 1 " + str(vector.sumsq(xs, [1])))
    try:
        print(vector.sumsq(xs, [2]))
    except refuse as e:
        print("refused (" + e.discriminator + "): " + e.reason)
```

```
OK script weights(): 4 prints
  print all [194.0]
  print along axis 0 [153.0, 41.0]
  print along axis 1 [25.0, 169.0]
  print refused (value_error): vector.sumsq(): axis 2 is out of range for a vector of 4 elements
```

Along axis 0 the readings at 0 and 2 make one total, `9 + 144`, and those at 1 and
3 the other, `16 + 25`; along axis 1 it is 0 and 1 against 2 and 3. Naming no axis
makes one total of everything. The first axis named is the high bit of the place
the totals are listed in, as it is for the rows of a matrix. A call is one
operation however long the list is, and what it builds is the totals alone.

### Keeping numbers as one blob with `struct`

A list is not a value a field can hold, so a list kept in the store is kept as
something that is: a blob holding its numbers. `struct` is Python's module for
that, and you import it as you import `math`. `struct.pack` lays numbers out as
bytes by a format, and `struct.unpack` reads them back, bit for bit.

```dpy
# keep_points.dpy — two points on a plane, written as their four coordinates,
# kept in the store as one blob, read back and unpacked to the same numbers; a
# blob of the wrong length is caught as a refusal.
import struct

class Kept:
    data: blob

def keep_points():
    points = [1.5, 2.0, -0.0, 0.25]
    k = Kept("route")
    remember(k.data, struct.pack(f"<{len(points)}d", *points), "tutorial")
    c = k.data
    match c:
        case active_claim:
            match c.value:
                case blob as b:
                    back = list(struct.unpack(f"<{len(b) // 8}d", b))
                    print(f"kept {len(b)} bytes, back {back}")
                case default:
                    print("not a blob")
        case empty:
            print("nothing kept")
    try:
        one = struct.unpack("<d", blob("00"))
        print(one)
    except refuse as e:
        print("refused (" + e.discriminator + "): " + e.reason)
```

```
OK script keep_points(): 1 claim written, 2 prints
  remember Kept.route.data = blob("000000000000F83F00000000000000400000000000000080000000000000D03F")
  print kept 32 bytes, back [1.5, 2.0, -0.0, 0.25]
  print refused (value_error): unpack requires a buffer of 8 bytes
```

The format `<4d` says little-endian, then four reals of eight bytes each, and an
f-string writes the count from the list's length. The `*` spreads
the list into `pack`'s arguments, and `len` of a blob is its count of bytes, so
the read side works out the count again. A field read is a claim, so the blob
is matched out of it as any value is. Packing and unpacking are one operation
each, however long the list. The [Python Reference](/ref/dke/python/) lists
every format code.

A blob is cut and joined as Python's `bytes` are. `data[a:b]` is the blob of the
bytes from `a` up to `b`, `data[i]` is the byte at `i` as a number from 0 to 255,
and `+` joins two blobs, each one operation however long the blob is.

```dpy
# halves.dpy — a blob cut into its two halves and joined back the other way
# round, a byte read as a number, and a position past the end caught as a refusal.
def halves():
    data = blob("0A0B0C0D")
    half = len(data) // 2
    first = data[:half]
    second = data[half:]
    print("first " + str(first) + ", second " + str(second))
    print("swapped " + str(second + first))
    print("byte 2 is " + str(data[2]))
    try:
        print(data[4])
    except refuse as e:
        print("refused (" + e.discriminator + "): " + e.reason)
```

```
OK script halves(): 4 prints
  print first 0A0B, second 0C0D
  print swapped 0C0D0A0B
  print byte 2 is 12
  print refused (index_out_of_bounds): index out of range
```

A negative position or bound counts from the end, so `data[-1]` is the last byte
and `data[::-1]` the blob reversed. The [Python Reference](/ref/dke/python/) gives
the rules.

---

## Chapter 4 — Recording and reading across time

The claims in Chapter 2 were all about *now*. But knowledge in DKE is not only
current — it is **dated**. A write may carry a **validity window**: a from- and a
to-datetime bracketing the span the value was true. A read may carry an
**as-of** datetime, asking for the value that was in force *at that moment*
rather than now. Together they let one cell hold a value that changed over time, and let
you read it at any instant — a history of when each value was true, without
bookkeeping of your own.

Two windows model a rate that changed, and two as-of reads select the value in
force at each date. Here each period has its own source. One source can record
both just as well, as long as its windows do not overlap — and both bounds count,
so two windows that share an end instant overlap at it. Writing into its own
overlap, a source is refused by `remember`, and with `update` the newer window
replaces the older:

```dpy
# reading-across-time.dpy — a value that changed over time, read as of a past date.
def reading_across_time():
    remember(Rate.usd.pct, "3.0", "y2019", datetime("2019-01-01T00:00:00Z"), datetime("2021-01-01T00:00:00Z"))
    remember(Rate.usd.pct, "5.0", "y2021", datetime("2021-01-01T00:00:00Z"), datetime("2023-01-01T00:00:00Z"))
    early = current(Rate.usd.pct, datetime("2020-06-01T00:00:00Z"))
    print("rate as of 2020 = " + str(early.value))       # 3.0 — inside the first window
    later = current(Rate.usd.pct, datetime("2022-06-01T00:00:00Z"))
    print("rate as of 2022 = " + str(later.value))        # 5.0 — inside the second
```

The write signature is `remember(K.s.a, v, src, datetime("from"), datetime("to"))` and the timed
read is `current(K.s.a, datetime("as-of"))`; both time arguments are optional — omit the
window to record a value with no stated end, and omit the as-of time to read the
present. `get` takes an as-of time the same way. A datetime is an RFC 3339 UTC
instant with the required `Z` suffix.

Either bound may be `null` instead, which leaves that side of the window open.
`remember(Plan.p1.tier, "pro", "billing", datetime("2024-01-01T00:00:00Z"), null)`
is valid from the start of 2024 onward, with no end; `null` first and a datetime
second is valid up to that instant, with no start. This is the one place you
write `null`, and one of the two bounds must still be a datetime.

A claim gives its window back as `.valid_from` and `.valid_to`. Each is a
`value`: a `datetime`, or `null` for an open side — and for both sides of a claim
written with no window at all. So read them the way Chapter 3 read `.value`,
with a `match`, rather than by comparing against some far-off date:

```dpy
# open-window.dpy — a window open at one end, read back from the claim.
def open_window():
    remember(Plan.p1.tier, "pro", "billing", datetime("2024-01-01T00:00:00Z"), null)
    c = current(Plan.p1.tier)
    print("from " + str(c.valid_from))          # from 2024-01-01T00:00:00Z
    match c.valid_to:
        case datetime as end:
            print("until " + str(end))
        case null:
            print("no end")                     # this arm runs
        case default:
            print("not a window bound")
```

### One source, one period at a time

The opening example gave each period its own source. Just as often one source
tells the whole story — a finance act that sets this year's rate and next
year's — and the verb for that is `update`. A windowed `update` replaces only
its own source's claims whose windows overlap the new one, so each period you
write leaves the others standing, and writing a period again revises it:

```dpy
# rate-by-period.dpy — one source records a changing rate, one period at a time.
def rate_by_period():
    update(Rate.vat.pct, 25, "finance act", datetime("2024-01-01T00:00:00Z"), datetime("2024-12-31T23:59:59Z"))
    update(Rate.vat.pct, 27, "finance act", datetime("2025-01-01T00:00:00Z"), null)
    mid2024 = datetime("2024-06-01T00:00:00Z")
    mid2025 = datetime("2025-06-01T00:00:00Z")
    a = current(Rate.vat.pct, mid2024)
    b = current(Rate.vat.pct, mid2025)
    print("2024: " + str(a.value) + ", 2025: " + str(b.value))
    update(Rate.vat.pct, 26, "finance act", datetime("2025-01-01T00:00:00Z"), null)   # revise 2025 onward
    a2 = current(Rate.vat.pct, mid2024)
    b2 = current(Rate.vat.pct, mid2025)
    print("2024: " + str(a2.value) + ", 2025: " + str(b2.value))
```

```
OK script rate_by_period(): 3 claims written, 2 prints
  update Rate.vat.pct = 25 valid_from=datetime("2024-01-01T00:00:00Z") valid_to=datetime("2024-12-31T23:59:59Z")
  update Rate.vat.pct = 27 valid_from=datetime("2025-01-01T00:00:00Z")
  print 2024: 25, 2025: 27
  update Rate.vat.pct = 26 valid_from=datetime("2025-01-01T00:00:00Z")
  print 2024: 25, 2025: 26
```

The revision overlapped the claim for 2025 onward and replaced it. The claim for
2024 lies outside the new window, so it stands. What an overlap replaces, it
replaces whole: a claim is superseded, never trimmed to the part the new window
leaves uncovered. Had the revision started in 2026 instead, it would still have
overlapped the claim for 2025 onward, and mid-2025 would then read nothing. So
revise a period with the window you wrote it with. Because `update` also works
on a cell that holds nothing yet, a loader that re-runs over every period can
use it for all of them.

### The window may be in the future

Nothing about a validity window says it has to be over. A release date, a rate
change agreed for next quarter, a contract that starts in January — these are
facts you know now and that become true later, and a window is how you say so.

The consequence is worth being deliberate about: **a fact whose window has not
opened yet is not part of the present**, so a read at the present will not report
it. That is correct — it is not true yet — but it means the as-of time is not a
convenience for historical questions. It is how you read a commitment back at
all.

```dpy
# scheduled-commitment.dpy — a fact recorded now, valid later.
def scheduled_commitment():
    remember(Release.v2.ships, "2027-03-01", "roadmap",
             datetime("2027-01-01T00:00:00Z"), datetime("2027-12-31T00:00:00Z"))
    now = current(Release.v2.ships)
    match now:
        case active_claim:
            print("ships " + str(now.value))
        case empty:
            print("nothing ships today")     # correct — the window has not opened
    then = current(Release.v2.ships, datetime("2027-06-01T00:00:00Z"))
    print("as of mid-2027: " + str(then.value))     # 2027-03-01
```

The enumeration verbs you meet in the next chapter take the same argument, for
the same reason.

### What the store knew, and when

The as-of time asks when a value was **true**. There is a second question, and
it has a different answer: when the store was **told**. A rate that held in 2020
and was entered today was true in 2020, but nobody reading the store in 2020
could have seen it. `known_at=` asks the second question. It takes a datetime
and answers over what the store had been told by then:

```dpy
# known-then.dpy — true at a time, and known at a time, are two questions.
def known_then():
    remember(Rate.eur.pct, "4.0", "ecb", datetime("2019-01-01T00:00:00Z"), datetime("2021-01-01T00:00:00Z"))
    mid2020 = datetime("2020-06-01T00:00:00Z")
    true_then = current(Rate.eur.pct, mid2020)
    print("in force in 2020: " + str(true_then.value))           # 4.0
    told_then = get(Rate.eur.pct, mid2020, known_at=mid2020)
    print("known in 2020: " + str(len(told_then)) + " claims")   # 0 claims — entered today
```

The two times are independent, and a read may carry either, both or neither.
`current`, `get`, `why` and the three enumerations all take `known_at=`. A
value that was later revised is still in the answer as it stood, so a read at a
moment before an `update` sees what the store said before it, and a
conclusion is what the rules, as they read then, concluded then. What it will
not tell you is anything later forgotten — `forget` erases, so a forgotten fact
was never known, as far as any read can tell — or how a rule changed since used
to read, so a read that rests on one refuses.

---

## Chapter 5 — Asking questions

Beyond reading a single cell, you can ask the store questions.

`verify` checks whether a cell holds a particular value and gives you a
`verify_result` with a `.match` boolean:

```dpy
# confirm-value.dpy — verify a cell against an expected value.
def confirm_value():
    remember(Cat.felix.color, "orange", "op1")
    v = verify(Cat.felix.color, "orange")
    if v.match:
        print("confirmed: colour is orange")
    else:
        print("mismatch: expected orange, got " + str(v.actual))
```

Reading with `verify` gets subtle when two sources disagree. On a **contradicted**
cell — one holding co-active claims from different sources — `verify` asks "is this
value present here?", not "is this the settled value?". So it reports a match for
*each* of the competing values:

```dpy
# verify-contradicted.dpy — verify a cell two sources disagree on.
def verify_contradicted():
    remember(Cat.felix.color, "orange", "op1")
    remember(Cat.felix.color, "grey", "op2")     # a second source disagrees
    orange = verify(Cat.felix.color, "orange")
    grey = verify(Cat.felix.color, "grey")
    print("orange matches? " + str(orange.match))        # True
    print("grey matches? " + str(grey.match))            # True — both are co-active
```

Invoking it, both checks pass — the cell genuinely holds both values at once:

```
OK script verify_contradicted(): 2 claims written, 2 prints
  remember Cat.felix.color = "orange"
  remember Cat.felix.color = "grey"
  print orange matches? True
  print grey matches? True
```

Two different values both answering `true` is itself the sign that a cell is
contradicted — `verify` never hides the disagreement by picking a winner. The two
verbs that inspect disagreement directly, `caveats` and `conflicts`, appear later
in this chapter.

The result also says so outright. `.conflicted` is `True` when the cell holds
competing values, and `.actual` — the value that stands — is then empty, because
no single value does. `.actual` is empty on a cell nobody wrote, too, so
`.conflicted` is what tells those two apart. A `verify` scoped to one source,
`verify(K.s.a, v, src)`, asks about that source's claim alone and is never marked
conflicted. `.expected` hands back the value you asked about, so code that
reports on a result later can still say what was expected:

```dpy
# verify-fields.dpy — what a verify result says about the cell it checked.
def verify_fields():
    remember(Cat.felix.color, "orange", "op1")
    remember(Cat.felix.color, "grey", "op2")      # a second source disagrees
    both = verify(Cat.felix.color, "orange")
    print("conflicted " + str(both.conflicted) + ", actual '" + both.actual + "'")
    mine = verify(Cat.felix.color, "orange", "op1")
    print("per op1: conflicted " + str(mine.conflicted) + ", actual '" + mine.actual + "'")
    remember(Cat.tom.color, "black", "op1")
    other = verify(Cat.tom.color, "orange")
    print("expected " + other.expected + ", got " + other.actual)
```

```
OK script verify_fields(): 3 claims written, 3 prints
  remember Cat.felix.color = "orange"
  remember Cat.felix.color = "grey"
  print conflicted True, actual ''
  print per op1: conflicted False, actual 'orange'
  remember Cat.tom.color = "black"
  print expected orange, got black
```

`agreement` turns that into a **count**: how many distinct sources back a given
value. It is `verify`'s quantitative sibling — where `verify` asks *"is this value
present?"*, `agreement` asks *"how many sources say it?"*:

```dpy
# count-sources.dpy — how many distinct sources back each value.
def count_sources():
    remember(Cat.felix.color, "orange", "op1")
    remember(Cat.felix.color, "orange", "op2")   # a second source agrees
    remember(Cat.felix.color, "red", "op3")       # a third source disagrees
    orange = agreement(Cat.felix.color, "orange")
    red = agreement(Cat.felix.color, "red")
    print("orange sources = " + str(orange))             # 2
    print("red sources = " + str(red))                   # 1
```

Invoking it counts the distinct sources behind each value:

```
OK script count_sources(): 3 claims written, 2 prints
  remember Cat.felix.color = "orange"
  remember Cat.felix.color = "orange"
  remember Cat.felix.color = "red"
  print orange sources = 2
  print red sources = 1
```

A count is **evidence, not a verdict**. Two sources backing a value does not make
it true, and the store does not treat those sources as independent witnesses — it
simply reports how many recorded the value. Which sources to trust is your
judgment; read them by name with `get`, and record the judgment with `prefer`,
later in this chapter. (`agreement` counts every source, so it takes no source
argument.)

A source is what a claim **cites**. Who **wrote** it is a separate fact, and
`writers(K.s.a, v)` counts that one: how many distinct store keys wrote the
value. The two counts can differ either way, and the difference tells you
something. Three sources cited under one key is corroboration one party
assembled; one source written under three keys is three parties recording the
same thing:

```
a = agreement(Cat.felix.color, "orange")   # 2 — two sources cited
w = writers(Cat.felix.color, "orange")     # 1 — one key wrote both
```

Each claim names its key in `.written_by`. The writer chooses the source, but not
this: the key is observed from the call, never stated in it. A claim written
without an authenticated call, or concluded by a rule, has no key — `writers`
does not count it, and its `.written_by` is empty. Like `agreement`, `writers`
takes no source argument.

`subjects` finds every subject of a kind whose attribute holds a given value, and
returns a `subject_set` you can size or iterate. It is **type-discriminating** — searching for the int `42` never matches the string `"42"`:

```dpy
# find-subjects.dpy — which cats are orange?
def find_subjects():
    remember(Cat.felix.color, "orange", "op1")
    remember(Cat.tom.color, "orange", "op1")
    remember(Cat.mittens.color, "black", "op1")
    orange_cats = subjects(Cat.color, "orange")
    print("orange cats = " + str(orange_cats.length))
```

The `list_*` family enumerates structure — attributes of a kind, subjects, values
at an attribute, and more:

```dpy
# list-structure.dpy — enumerate what a kind knows.
def list_structure():
    remember(Cat.felix.color, "orange", "op1")
    remember(Cat.felix.age, 3, "op1")
    attrs = list_attributes(Cat)
    print("Cat has " + str(attrs.length) + " attribute(s)")
```

These `list_*` heads (`list_attributes`, `list_values`, `list_subjects`, …) are
soft keywords — recognised as verbs only right before `(`, so the same words are
free to be ordinary identifiers elsewhere. The full enumeration family
walks a kind's subjects, values, and categories:

```dpy
# enumerate-store.dpy — walk the store's structure.
def enumerate_store():
    remember(Cat.felix.color, "orange", "op1")
    remember(Cat.tom.color, "grey", "op1")
    every = list_subjects(Cat)          # subject_set — every subject of the kind
    subs = list_subjects(Cat.color)     # subject_set — only those with a colour
    vals = list_values(Cat.color)       # claim_list — the values recorded there
    cats = list_categories()            # string_list — the kinds in the store
    print("every = " + str(every.length) + ", coloured = " + str(subs.length) + ", values = " + str(vals.length) + ", kinds = " + str(cats.length))
```

`list_subjects`, `list_values` and `list_attributes(K.s)` take the same optional
as-of datetime as `current` and `get` (Chapter 4), and it matters more here.
A cell read you can always reach by naming the cell; an enumeration is how you
find something you do **not** already know the name of. Without a time, they
enumerate the present, so the scheduled commitment from Chapter 4 is reachable
only by someone who already knows the subject, the attribute *and* a date inside
the window — which is to say, by someone who already has the answer.

```dpy
# walk-as-of.dpy — find a commitment recorded for later.
def walk_as_of():
    remember(Release.v2.ships, "2027-03-01", "roadmap",
             datetime("2027-01-01T00:00:00Z"), datetime("2027-12-31T00:00:00Z"))
    when = datetime("2027-06-01T00:00:00Z")
    here = list_subjects(Release)
    print("subjects now: " + str(here.length))                            # 0
    subs = list_subjects(Release, when)
    print("subjects then: " + str(subs.length))                           # 1
    attrs = list_attributes(Release.v2, when)
    vals = list_values(Release.ships, when)
    print("attrs = " + str(attrs.length) + ", values = " + str(vals.length))
```

Two of the family take no as-of time: `list_categories()` and the one-argument
`list_attributes(K)`. Those report the kinds and attribute names the store has
recorded — its shape rather than its state — so they already cover every time,
and there is nothing for an anchor to select. Note that `list_attributes`
therefore takes a time in its `K.s` form and not in its `K` form: one reads a
subject's claims, the other a kind's vocabulary.

Two verbs inspect **disagreement**. `caveats(K.s)` returns the cautionary claims
on a subject, and `conflicts()` returns the claims that stand in disagreement —
the co-active alternatives from different sources you met in Chapter 2:

```dpy
# inspect-disagreement.dpy — caveats on a subject, conflicts across the store.
def inspect_disagreement():
    remember(Cat.felix.color, "orange", "op1")
    remember(Cat.felix.color, "grey", "op2")   # a second source disagrees
    cv = caveats(Cat.felix)
    cf = conflicts()
    print("caveats = " + str(cv.length) + ", conflicting claims = " + str(cf.length))
```

Finding a disagreement is half the job; the other half is deciding which source
you go by. `prefer(K.s.a, src)` records that judgment at a cell where sources
disagree, and discards nothing: every claim stays, and so does the disagreement.
What changes is a mark — each claim `get` returns carries `.preferred`, `True` on
the one you chose. `unprefer(K.s.a)` withdraws the judgment and leaves the claims
as they were:

```dpy
# prefer-source.dpy — say which source you go by, and keep both claims.
def prefer_source():
    remember(Cat.felix.color, "orange", "op1")
    remember(Cat.felix.color, "grey", "op2")      # a second source disagrees
    prefer(Cat.felix.color, "op2")                # you go by op2
    claims = get(Cat.felix.color)
    for c in claims:
        print(c.source + " says " + str(c.value) + ", preferred " + str(c.preferred))
    cf = conflicts()
    print("claims in disagreement: " + str(cf.length))
    unprefer(Cat.felix.color)                     # withdraw the judgment
```

```
OK script prefer_source(): 2 claims written, 2 preference changes, 3 prints
  remember Cat.felix.color = "orange"
  remember Cat.felix.color = "grey"
  prefer Cat.felix.color = "op2"
  print op1 says orange, preferred False
  print op2 says grey, preferred True
  print claims in disagreement: 2
  unprefer Cat.felix.color
```

A preference is a mark, not a verdict. `conflicts()` still reports the cell,
`current` still refuses there because two values stand, and no standing rule
concludes anything differently. Read the claims with `get` and act on the one
marked. Naming another source replaces the judgment, and preferring a source that
recorded nothing at the cell refuses.

The store also keeps a small **registry** you can read back — the pins you have
set, the result types the language can produce, and the names of the scripts you
have stored:

```dpy
# read-registry.dpy — enumerate pins, result types, and scripts.
def helper():
    remember(Cat.felix.color, "orange", "op1")

def read_registry():
    remember(Cat.felix.color, "orange", "op1")
    pin(Cat.felix.color)
    pins = list_pinned()            # string_list — pinned cell paths
    rts  = list_result_types()      # result_type_set — the types verbs can return
    scr  = list_scripts()           # string_list — stored script names
    print("pinned = " + str(pins.length))
    print("result types = " + str(rts.length) + ", scripts = " + str(scr.length))
```

### Summary statistics over an attribute

Beyond reading single cells, you can summarise a whole **attribute** — the values of
one attribute across every subject of a kind. An **aggregate query** folds an
attribute into one summary `value`. It is read-only: it never changes the
store.

```dpy
# summary-stats.dpy — read-only summary statistics over an attribute.
def summary_stats():
    remember(Reading.r1.value, 10, "sensor")
    remember(Reading.r2.value, 20, "sensor")
    remember(Reading.r3.value, 30, "sensor")
    n = count(Reading.value)
    mean = avg(Reading.value)
    hi = max(Reading.value)
    print("readings = " + str(n) + ", mean = " + str(mean) + ", max = " + str(hi))   # readings = 3, mean = 20, max = 30
```

The single-attribute folds include `count`, `sum`, `avg`, `min`, `max`, `median`,
`variance`, and `stdev`; two-attribute folds relate two attributes of one kind —
`slope(Point.x, Point.y)`, `correlation(Point.x, Point.y)`. Each returns a `value`
whose class follows the attribute (a numeric attribute yields a number), so bind it and
render or `match` it.

`variance` and `stdev` are the **population** figures: they divide by the number
of values. That is not what CPython's `statistics.stdev` gives you — there it is
the *sample* figure, and `statistics.pstdev` is the population one. Over the
eight values 2, 4, 4, 4, 5, 5, 7 and 9, `stdev` here answers `2.0` where
`statistics.stdev` answers `2.138…`, and `variance` answers `4` where
`statistics.variance` answers `4.571…`. Both are right for their own definition,
which is why the name alone does not tell you which you have.

Those folds are a few of a larger family: more over one attribute (`product`,
`mode`, `span`, `iqr`, `geomean`, `skewness`, …); folds about identity and
position — `distinct` counts the different values, `argmin` and `argmax` name the
subject holding the least and the greatest, `first` and `last` give the earliest-
and latest-recorded value; a ranked fold, `percentile(Reading.value, 90)`; and
more over two attributes (`covariance`, `intercept`, `rsquared`). The
[Python Reference](/ref/dke/python/) lists them all, with the definition each
name denotes.

Two rules matter. First, **bind an aggregate to a name on its own line**, then use
that name — an aggregate may not be written as a bare argument to another call
(`n = count(Reading.value)` then `print("readings = " + str(n))`, never `print("readings = "
+ str(count(Reading.value)))`). Second, a numeric fold **refuses** rather than guess: an aggregate over an attribute with no data refuses, and so does a numeric
fold (`sum`, `avg`, `min`, `max`, `stdev`, …) over an attribute whose values are not
numbers — it declines rather than treating a non-number as zero. Aggregate over
numeric data you know exists, or guard the call. (`count` counts any class, and
`mode`, `distinct`, `first`, `last` and `entropy` never compare values as numbers,
so they fold text too.)
The fold names are soft keywords, recognised as an aggregate only right before `(`,
so `count`, `sum`, and the rest stay ordinary identifiers elsewhere.

One thing an aggregate query does *not* do: answer per subject. `avg(Reading.value)`
is the mean of every reading in the store, one number, however many sensors wrote
them. For a mean *per sensor* — one answer each — the fold goes in a standing
rule's conclusion instead, which Chapter 8 covers under "Concluding a count".
There the refusal rule works differently, because a standing rule has no caller
to refuse to: when a value it cannot fold arrives, the rule keeps the last value
it computed, and every read serves that value with `.maintained` set to `False`
(Chapter 2).

For reference, here is every verb this tutorial uses — its result type and where
it appears. The [Python Reference](/ref/dke/python/) lists them all,
including the ones this tutorial does not reach.

| Verb | Result | Chapter |
|------|--------|---------|
| `remember` / `update` / `forget` / `assert` / `pin` / `unpin` | (void) | 1, 2 |
| `current` | `active_claim` | 1 |
| `get` | `claim_list` | 2 |
| `would_forget` | `int` | 2 |
| `verify` | `verify_result` | 5 |
| `agreement` / `writers` | `int` | 5 |
| `subjects` / `list_subjects` | `subject_set` | 5 |
| `list_attributes` / `list_categories` / `list_pinned` / `list_scripts` | `string_list` | 5 |
| `list_values` / `caveats` / `conflicts` | `claim_list` | 5 |
| `list_result_types` | `result_type_set` | 5 |
| `prefer` / `unprefer` | (void) | 5 |
| `suppose` | `value` | 8 |
| `suppose_absent` | `active_claim` | 8 |
| `create_world` / `merge_world` / `discard_world` | (statement) | 10 |
| `compare_worlds` | `claim_list` | 10 |
| `list_worlds` | `string_list` | 10 |
| `dependents` | `claim_list` | 11 |
| `why` | `proof_tree` | 12 |
| `premises` | `claim_list` | 12 |
| `why_not` / `what_needs` | `diagnosis` | 2, 12 |

---

## Chapter 6 — Procedures

Every program so far has been a single `def`. A source file may declare several,
and within one file this is how you structure a program: procedures that share
their work through the store. (Splitting work across *files*
is what modules are for — Chapter 17.)

A procedure may **call another**, above or below it in the file, and name a class
declared below it: the unit compiles a callee before its caller, which is
*compile-before-call*. A call is expanded inline
at compile time, so there is no recursion and calls may never form a cycle: the same
termination guarantee that governs loops governs calls.

In-language, you call a procedure as you call a Python function, `name(args)`.
From a `run`, the same call reaches a compiled module's script
once you have imported it: `import <module>` then `<module>.<name>(...)` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

```dpy
# compose-scripts.dpy — two procedures; the second calls the first.
def seed_colour():
    remember(Cat.felix.color, "orange", "op1")

def audit_colour():
    seed_colour()                        # calls the earlier declaration
    cur = current(Cat.felix.color)
    match cur:
        case active_claim:
            print("audited colour = " + str(cur.value))
        case empty:
            print("no colour to audit")
```

Nothing in the file runs by itself. You compile it as a module and call the
procedure you want by name: compiled as `colours`, a run of `import colours` and
then `colours.audit_colour()` calls `audit_colour`, which calls `seed_colour` in
turn. Here is the departure a Python programmer feels most: these two procedures
**share their work through the store**. `seed_colour` records a claim and
`audit_colour` reads it back, and what one of them records, any later program can
read. A procedure can still return a value when that is what you want —
`return` the value, and the caller binds it, as the helpers at the end
of this chapter do.

Procedures may also take typed parameters (`def name(room: string):`), supplied
by position or by keyword when called. A parameter may be any value type the
engine stores — the primitives `string`, `int`, `bool` and the value-class scalars `datetime`,
`duration`, `real`, `blob`, `scientific`, `complex` — plus the read-result types (`claim_list`,
`active_claim`, …) for calls between procedures, and a class you declare, which
Chapter 7 introduces. A value-class scalar is passed as its canonical
text: `"2026-01-02T03:04:05Z"` for a `datetime`, `"3.5"` for a
`real`, `"PT1H30M"` for a `duration`, hex for a `blob`. (`null` is absence and is
never a parameter type.)

A parameter or return type may also be a **collection** — `list<int>`,
`dict<string, int>`, `set<string>`, `tuple<int, string>`, nested as deep as you
like — so a collection can be handed to a helper and handed back:

```dpy
def total(xs: list<int>) -> int:
    return sum(xs)

def doubled(xs: list<int>) -> list<int>:
    return [x * 2 for x in xs]
```

`total([1, 2, 3])` is `6`, `doubled([4, 5])` is `[8, 10]`. (These pass the list
**between procedures**; a collection argument is not written on the wire — such
helpers are called from other DKE Python code.)

The rest of Python's calling forms work as they do in Python. A parameter may
carry a **default**, and a call may then leave it out; an argument may be passed
**by keyword**, after the positional ones; and a final `*name: T` parameter is
**variadic**, collecting the extra positional arguments into a tuple you can
read by position, measure and loop over:

```dpy
# call-options.dpy — a default, a keyword argument, and a variadic parameter.
def greet(name: string, greeting: string = "Hello") -> string:
    return greeting + ", " + name

def total(label: string, *nums: int) -> string:
    return label + " = " + str(sum(nums)) + " over " + str(len(nums))

def call_options():
    print(greet("Ada"))
    print(greet("Bo", greeting="Hi"))
    print(total("sum", 1, 2, 3))
    print(total("none"))
```

```
OK script call_options(): 4 prints
  print Hello, Ada
  print Hi, Bo
  print sum = 6 over 3
  print none = 0 over 0
```

A defaulted parameter comes after the required ones, as in Python. The variadic
names its element type, takes no default and cannot be passed by keyword, and
whatever follows it, or follows a bare `*`, is passed by name; whatever stands
before a `/` is passed by position. One form is missing on purpose — there is no `**kwargs`. A signature
names every keyword a call may pass, so a misspelt keyword is refused where you
wrote it instead of being quietly collected. When you want an open set of named
options, take a `dict` parameter.

---

## Chapter 7 — Classes

A **class** groups typed fields and the methods that operate on them. Think
of it as a convenient, Python-shaped way to organise the same stored facts you
have worked with all along: the cells simply get names grouped by class. Nothing
new happens underneath — a field read still yields a claim, and a field write
still records a value together with its source.

A class declaration is `class Name:` with typed fields and `def` methods. A **void method** (`def m(self, …):`) is called as a statement; a
**value method** (`def m(self, …) -> T:` ending in `return`) is called in an
expression:

```dpy
# classes.dpy — a class with a typed field, a void method, and a value
# method; a def binds an instance and calls both.
class Sensor:
    temp: string
    def record(self, v: string, src: string):
        remember(self.temp, v, src)    # field write
    def label(self) -> string:
        return "sensor"                # value method

def demo():
    s = Sensor("room-a")               # instance binding
    s.record("21", "op1")              # void method call
    name = s.label()                   # value method call
    reading = s.temp                   # field read
    match reading:
        case active_claim:
            print(name + " = " + str(reading.value) + " per " + str(reading.source))
        case empty:
            print(name + ": no reading")
```

Note the field write `remember(self.temp, v, src)` — a value *and* its source, exactly
like `remember`. Provenance does not disappear because you wrapped the cell in a
class. A never-written field reads back as `empty`.

Two things from Python classes are missing on purpose. There is **no
constructor**: `Sensor("room-a")` takes the subject and nothing else, and runs no
code, so a field gets its value from `remember` once the instance exists — as
`record` does above — or from an ordinary method you call then. And there are no
**special methods**: a method named `__init__`, `__str__`, `__eq__` or any other
double-underscore name is refused at its name, because nothing would ever call
it, and the refusal tells you what to write instead. An instance already prints,
as its class and subject: `print(Sensor("room-a"))` shows `<Sensor 'room-a'>`.

You can dispatch on an instance's class with a class `match`. A `case` matches its
class or any subclass, the first match wins, and the arm is chosen from the class
the instance actually has when the program runs — so an instance held as a base
class takes its own subclass's arm. Written with no `()`, as here, the arms must cover
every class the instance could be, or end in `case default:` or `case _:`. Written as
Python writes them, `case Sensor():`, they are tests, and none need run:

```dpy
# class-match.dpy — dispatch on an instance's class.
class Sensor:
    temp: string
class Actuator:
    state: string

def configure():
    s = Sensor("room-a")
    match s:
        case Sensor:
            remember(s.temp, "21", "op1")
            print("configured a sensor")
        case Actuator:
            remember(s.state, "on", "op1")
            print("configured an actuator")
```

### Inheritance — one class extends another

A class can **extend** another, inheriting its fields and methods. Write the base
class in parentheses after the name. A subclass gets everything the base has, adds
its own, may **override** a method with its own version, and can reach the base's
version with `super()`:

```dpy
# inheritance.dpy — a Dog is an Animal with more: it inherits Animal's fields
# and methods, adds its own, overrides one, and calls the base with super.
class Animal:
    sound: string
    def speak(self):
        remember(self.sound, "generic", "op1")
    def describe(self) -> string:
        return "an animal"

class Dog(Animal):
    breed: string
    def describe(self) -> string:            # override — Dog's own version
        return "a dog"
    def speak(self):
        super().speak()                      # run Animal's speak first...
        remember(self.breed, "collie", "op1")   # ...then extend it

class Cat(Animal):
    def describe(self) -> string:
        return "a cat"

def label(a: Animal):                        # takes any Animal — subclasses too
    print(a.describe())                      # runs the actual class's describe

def demo():
    animals = [Dog("d1"), Cat("c1")]
    for a in animals:
        label(a)                             # "a dog", then "a cat" — polymorphism
    d = Dog("d2")
    if isinstance(d, Animal):                # a Dog is an Animal
        d.speak()
    match d:                                 # class match across the hierarchy
        case Dog: print("it is a dog")
        case Cat: print("it is a cat")
        case default: print("unknown")
```

The reason inheritance matters is `label`: written once, for an `Animal`, it works
for a `Dog` and a `Cat` alike — each runs its *own* `describe`. A base-typed
parameter (or list element) accepts any subclass, and the call resolves to the
instance's actual class. That is **polymorphism**. Two companions go with it:
`isinstance(x, C)` asks whether `x` is a `C` or a subclass of one — a `Dog` is an
`Animal`, a plain `Animal` is not a `Dog` — and a class `match` works across a
hierarchy, where `case Dog:` matches a `Dog` or any of its subclasses. A class
extends at most one base.

A class name is a type wherever a type is written: a parameter (`a: Animal`, as
in `label`), a binding (`pet: Animal = Dog("d3")`), a return
(`def adopt() -> Animal:`), and a collection's element type (`list<Animal>`). A
subclass instance fits wherever its base is named. A list you write with several
subclasses in it takes their nearest common base, so `animals` above is a list
of `Animal`, and that is why each element can be handed to `label`.

Through a base-typed name you may use only what the base declares: `a.breed` on
an `Animal` does not compile, because not every animal has a breed.
`isinstance` is how you get past that — it also **narrows**. Inside
`if isinstance(a, Dog):` the name `a` is a `Dog`, so `a.breed` is there to read
and write. The narrowing lasts to the end of that branch, and it happens only
when the `isinstance` call is the whole condition. `super()` works in a value
method as well as a void one: there `super().describe()` is the value the base's
version returns, and the override can build on it:

```dpy
# narrowing.dpy — a subclass's own field behind isinstance, and super() in a
# value method.
class Animal:
    sound: string
    def describe(self) -> string:
        return "an animal"

class Dog(Animal):
    breed: string
    def describe(self) -> string:
        return "a dog, which is " + super().describe()

class Cat(Animal):
    def describe(self) -> string:
        return "a cat"

def narrowing():
    pets = [Dog("rex"), Cat("tom")]
    for a in pets:
        if isinstance(a, Dog):
            remember(a.breed, "collie", "op1")
        print(f"{a}: {a.describe()}")
```

```
OK script narrowing(): 1 claim written, 2 prints
  remember Dog.rex.breed = "collie"
  print <Dog 'rex'>: a dog, which is an animal
  print <Cat 'tom'>: a cat
```

The second argument of `isinstance` may also be a value type instead of a class
— `isinstance(x, int)`, a tuple such as `isinstance(x, (int, real))`, or a union,
`isinstance(x, int | real)` — and then it asks what `x` holds when the program
runs. Python's own spellings `str` and `float` are accepted for `string` and
`real`. A test on a value type narrows a name that holds a `value`: inside
`if isinstance(x, int):` the name reads as an `int`, and in the `else` as the
classes it can still be. To use a value at its type without a test, `match` on
its class, as Chapter 3 does.

A class field can also be **computed** — derived and kept current by the engine
rather than written by you. That is the first form of the engine's reasoning, and
it opens the next chapter.

---

## Chapter 8 — The engine reasons

This is the chapter with no Python analogue. Until now you have *recorded* facts
and *read* them back. Now you declare facts the **engine derives and maintains for
you** — you state a relationship once, and the engine keeps the conclusion current
as its inputs change, on its own, forever after. It comes in three escalating
forms: a field derived within one class, a named rule that ranges over the whole
store, and a hypothesis that reasons without committing anything. Beside them
stands the one declaration that derives nothing: a constraint, which watches the
store for a condition you say must never hold.

### Computed fields — derivation within a class

A class field may be **computed**: declared with an initializer the engine derives
from the class's other fields and keeps current as they change. You write
only the inputs; the derived field is maintained automatically and reads back with
a `derived` provenance in place of a source:

```dpy
# computed-fields.dpy — fields the engine derives and maintains.
class Invoice:
    rate: int
    hours: int
    total: int = rate * hours        # a computed value
    large: bool = total > 1000        # a computed flag, built on the one above

def computed_fields():
    remember(Invoice.i1.rate, 150, "billing")
    remember(Invoice.i1.hours, 8, "billing")
    t = current(Invoice.i1.total)
    print("total = " + str(t.value))                    # 1200 (derived: rate × hours)
    big = current(Invoice.i1.large)
    print("large = " + str(big.value))                  # True  (derived: total > 1000)
```

An `int` field is an arithmetic expression (`+ - * %`) over earlier fields; a
`real` field may also use `/`, and its `%` may take real operands; a `complex`
field takes `+ - * /` over earlier fields, numbers and imaginary literals, so
`shifted: complex = gain * 1j` turns each gain a quarter turn; a `bool`
field is one ordered comparison of an earlier field. Every reference points at a field **declared earlier**, so a
class's computed fields never form a cycle — and writing an input re-derives every
field built on it. You will see the derivation itself in Chapter 12, where `why`
over a computed field lists the inputs it was built from.

A computed field is never written. A `remember` or `update` at
`Invoice.i1.total`, or a supposition there (later in this chapter), is refused,
and the refusal names the inputs to write instead — here, *write `rate` or
`hours` instead*. `current` goes on reading the derived value, and a `forget`
there is never refused. The same holds from the other side: compiling a class
whose computed field already holds values someone recorded is refused, and the
refusal names them — forget them, or give the computed field a name of its own.

### Standing rules — derivation across the store

A computed field derives one field of one class from that class's own fields. A
**standing rule** is the same idea made standalone and named: it states a
condition over the stored data and a conclusion to record whenever that condition
holds. Once defined, the conclusion **always reflects the current data** — it is
in force exactly while its condition holds, so a derived fact is never stale.

A rule is a `def` marked with the `@rule` decorator and given a name nothing
else in the unit uses — no script, constraint, class or other rule — then a
`for` clause naming the subjects it ranges over, an `if` clause of one or more
premises joined by `and`, and an indented conclusion. The two premises to start
with are a **comparison** of a field against a number (`o.total > 1000`) and an
**absence** — `absent(o.shipment)`, which holds when the subject has no value
recorded for that field. (It has two relatives, `not_asserted` and
`known_absent`, which you meet later in this chapter.) A premise may also test
a field for equality (`o.lic == "MIT"`), or relate two subjects to each other, which the next two sections
are about:

```dpy
# standing-rule.dpy — a named rule the engine keeps current on its own.
@rule
def needs_review():
    for o in Order:
        if o.total > 1000 and absent(o.shipment):
            o.review = True

def standing_rule():
    remember(Order.o1.total, 1500, "sales")
    r = current(Order.o1.review)
    print("review before shipment = " + str(r.value))       # True — the rule fired
    remember(Order.o1.shipment, "sent", "logistics")
    after = current(Order.o1.review)
    match after:
        case active_claim:
            print("review after shipment = " + str(after.value))
        case empty:
            print("review withdrawn after shipment")     # this arm runs
```

Running it shows the rule's conclusion in force while the order is unshipped,
then no longer in force once a shipment is recorded (the `absent(o.shipment)`
premise stops holding):

```
OK script standing_rule(): 2 claims written, 2 prints
  remember Order.o1.total = 1500
  print review before shipment = True
  remember Order.o1.shipment = "sent"
  print review withdrawn after shipment
```

The derived `review` field reads back like any other field, with a `derived`
provenance; its value always reflects the rules currently in force. When you
need to know for certain whether a claim was concluded rather than recorded,
read its `trust` — `asserted` or `derived` — rather than its source: a source
is a string the writer chose and could be the word "derived" itself, while
`trust` is the engine's own account and cannot be written. The `for`/`if`
here look like the control flow of Chapter 9, but read them declaratively: a rule
does not *loop*, it *holds*. Two things keep a rule usable, each checked when you
define it: a rule must name **which subjects** it applies to — every name it
binds needs a premise that is not an absence test — and its outcome must **settle**, so
a rule set that would cancel itself out is rejected. A rule ranges over finitely many subjects and
its premises are tested, not iterated, so the termination guarantee of Chapter 13
still holds.

A rule's conclusion belongs to the rule, as a computed field belongs to its
class. Write `Order.o1.review` yourself and the write is refused, naming the
field to write instead — here `total` — and the other way out: *a rule that
should give way to a recorded value says so with `not_asserted`*, which is what
the rule in *Copying a value* below does. Compiling a rule whose field already
holds values someone recorded is refused too, naming them: forget them, or
conclude at another field.

Once you have defined a few rules, `list(target = "rules")` at the wire surface names the ones
you have — names only, so keep your own source for what each rule does. To
remove one, pass a name that listing prints to the `forget_rule` tool. It
withdraws what that one rule concluded and leaves the rest of its module in
place; the facts the rule read are untouched, and a conclusion another rule
still supports stays. Both are tools you call, not verbs you write in a program,
and the [MCP Reference](/ref/dke/mcp/) describes them.

**A `class` does not fence a rule in.** If you met `class` in Chapter 7 you may
expect it to constrain what a rule can conclude, and it does not: a rule may
conclude about a kind no `class` declares, into a field its class does not
declare, and with a value whose type is not the declared one — a rule concluding
`s.mean = avg(r.v)` over whole-number readings records `1.5` into a field
declared `int`, and nothing objects.

That is not an inconsistency with Chapter 7, where reading an undeclared field
off an instance is an error. The two are the same rule from opposite sides. When
you write `s = Sensor(room)` you have an **instance**, and a class is a closed
schema for instances — that is what makes `s.typo` catchable. When a rule writes
`for s in Sensor`, it has a **path**, and paths are the store's open surface:
anyone may record anything anywhere, which is the property the whole store rests
on. A class is a schema where you construct one, and a vocabulary where you
reason.

The practical reading: declare a field when you want the instance surface to
check your spelling, and do not expect the declaration to validate what a rule
derives. If a derived value must be of a certain shape, the rule that produces
it is where that is decided.

### Rules over more than one subject — relating them

`needs_review` looks at one order at a time. Many questions are about a
*relationship* instead — this function calls that one, this order belongs to that
customer — and a rule can bind more than one subject and relate them. Separate
the bindings with commas, and relate them with a premise whose right side is
another of those **names** rather than a value:

```
@rule
def taint_propagates():
    for f in Fn, c in Call, g in Fn:
        if f.tainted == True and c.caller == f and c.callee == g:
            g.tainted = True
```

Read it plainly: whenever a tainted function `f` is the caller of some call `c`,
and `c`'s callee is `g`, then `g` is tainted too. `c.caller == f` reads the field
as a *reference* — it holds when `caller` names the subject `f` — so two of the
three names are found rather than compared: `c` and `g` are reached through `f`.
That is what lets a single rule follow a chain. The bindings are commas rather
than nested `for` blocks on purpose: a rule does not walk the store, it states a
condition over it, and nesting would suggest an order that is not there.

Because the conclusion writes the same field the first premise reads, the rule
applies to its own results — the taint reaches everything the call graph
connects, not a fixed number of steps out.

### Concluding a count — a fold grouped by its subject

Every conclusion so far has recorded a value you wrote into the rule:
`g.tainted = True`. A conclusion can instead **fold the subjects the rule ranged
over**. That is how a rule counts.

```dpy
# regular-customers.dpy — count each customer's orders, then flag on the count.
class Customer:
    name: string
    order_count: int
    regular: bool

class Order:
    customer: string

@rule
def count_orders():
    for c in Customer, o in Order:
        if o.customer == c:
            c.order_count = count(o)

@rule
def regulars():
    for c in Customer:
        if c.order_count > 3:
            c.regular = True

def show():
    remember(Customer.c1.name, "Ada", "sales")
    remember(Customer.c2.name, "Bo", "sales")
    remember(Order.o1.customer, "c1", "sales")
    remember(Order.o2.customer, "c1", "sales")
    remember(Order.o3.customer, "c1", "sales")
    remember(Order.o4.customer, "c1", "sales")
    remember(Order.o5.customer, "c2", "sales")
    ada = current(Customer.c1.order_count)
    bo = current(Customer.c2.order_count)
    print("Ada orders = " + str(ada.value))
    print("Bo orders = " + str(bo.value))
```

```
OK script show(): 7 claims written, 2 prints
  remember Customer.c1.name = "Ada"
  remember Customer.c2.name = "Bo"
  remember Order.o1.customer = "c1"
  remember Order.o2.customer = "c1"
  remember Order.o3.customer = "c1"
  remember Order.o4.customer = "c1"
  remember Order.o5.customer = "c2"
  print Ada orders = 4
  print Bo orders = 1
```

Read it plainly. The `for` clause ranges over customer–order pairs, the premise
keeps the pairs that belong together, and the conclusion names `c` — so the fold
is taken over the *other* name, once for each customer. Ada gets `4` and Bo gets
`1`; nobody gets the store's total.

**That per-subject answer is the whole difference from the aggregate query of
Chapter 5.** `count(Order.customer)` folds one attribute across every subject of
the kind and yields a single number — how many orders exist, which here is five.
`count(o)` in a conclusion yields one number *per subject* — how many are this
customer's. Reaching for the Chapter 5 form to ask "how many orders does each
customer have" answers five, for everybody, and looks right until you check the
second customer.

Two shapes, told apart by what is folded. `count(o)` folds the orders themselves —
a bare subject name. `sum(o.amount)` folds one field of those orders, and naming a
field makes its presence a premise, so an order with no amount contributes
nothing to the sum while still counting as an order. The single-operand folds you
already know — `count`, `sum`, `avg`, `min`, `max`, `median`, `stdev`,
`argmax`, `distinct` — all work here. The ones that take a second argument
(`percentile`, `slope`) do not: a conclusion has nowhere to put it. A condition
on the folded field chooses which of its values are folded: with
`o.amount > 10`, an amount recorded as `5` by one source and `15` by another
adds `15`.

**A fold ranges over matches, not over subjects.** Chapter 5 taught you that
several sources can back one value — that is what `agreement` counts. When they
do, the location holds that value more than once *in force*, and the order matches
once per value. An order two sources agree on is therefore folded twice.

```dpy
# corroborated-count.dpy — one fold counts records, the other counts orders.
class Customer:
    name: string
    records: int
    orders: int

class Order:
    customer: string

@rule
def count_records():
    for c in Customer, o in Order:
        if o.customer == c:
            c.records = count(o)

@rule
def count_orders():
    for c in Customer, o in Order:
        if o.customer == c:
            c.orders = distinct(o)

def show():
    remember(Customer.c1.name, "Ada", "sales")
    remember(Order.o1.customer, "c1", "sales")
    remember(Order.o2.customer, "c1", "sales")
    remember(Order.o2.customer, "c1", "audit")
    remember(Order.o3.customer, "c1", "sales")
    remember(Order.o4.customer, "c1", "sales")
    records = current(Customer.c1.records)
    orders = current(Customer.c1.orders)
    print("records = " + str(records.value))
    print("orders = " + str(orders.value))
```

```
OK script show(): 6 claims written, 2 prints
  remember Customer.c1.name = "Ada"
  remember Order.o1.customer = "c1"
  remember Order.o2.customer = "c1"
  remember Order.o2.customer = "c1"
  remember Order.o3.customer = "c1"
  remember Order.o4.customer = "c1"
  print records = 5
  print orders = 4
```

Ada has four orders and the store holds five records of them, because `o2`'s
customer was written by `sales` and again by `audit` — the same `remember` line
twice in the transcript. Both numbers are right, for different questions:
`count(o)` answers *how many records*, `distinct(o)` answers *how many orders*.

So `regular-customers.dpy` above answers `4` only because nothing in its store
is corroborated. Reach for `distinct(o)` when the question is about the things
themselves and the store may hold more than one source per fact; reach for
`count(o)` when the question really is about the records.

**A derived field is an ordinary premise**, which is why "count, then flag" is
two rules rather than one. `regulars` reads `c.order_count` exactly as it would
read a field somebody recorded by hand, and so can any later rule or query. Each
rule states one thing, and the engine works out that the second needs the first.

### Comparing two fields, and `!=`

The comparisons so far set a field against a value you wrote into the rule. A
premise can set a field against **another field** instead, and it can ask for a
value **other than** the one you name:

```dpy
# budgets.dpy — compare two fields, and test for a different value.
class Project:
    budget: int
    spent: int
    status: string
    over: bool
    unfinished: bool

@rule
def over_budget():
    for p in Project:
        if p.spent > p.budget:
            p.over = True

@rule
def still_running():
    for p in Project:
        if p.status != "closed":
            p.unfinished = True

def budgets():
    remember(Project.roof.budget, 100, "plan")
    remember(Project.roof.spent, 120, "books")
    remember(Project.roof.status, "closed", "plan")
    remember(Project.porch.budget, 50, "plan")
    remember(Project.porch.spent, 40, "books")
    remember(Project.porch.status, "active", "plan")
    remember(Project.shed.spent, 30, "books")        # no budget, no status
    over = subjects(Project.over, True)
    for p in over:
        print("over budget: " + p)
    running = subjects(Project.unfinished, True)
    for p in running:
        print("unfinished: " + p)
```

```
OK script budgets(): 7 claims written, 2 prints
  remember Project.roof.budget = 100
  remember Project.roof.spent = 120
  remember Project.roof.status = "closed"
  remember Project.porch.budget = 50
  remember Project.porch.spent = 40
  remember Project.porch.status = "active"
  remember Project.shed.spent = 30
  print over budget: roof
  print unfinished: porch
```

`roof` spent 120 against a budget of 100, so it is over. `shed` has spent 30
and has no budget, so it has nothing to be over and the rule says nothing about
it: **both fields must hold a value**. Numbers compare as numbers, instants in
time order — `o.delivered > o.deadline` is how a late delivery is written — and
texts alphabetically; a number and a text stand in no order at all. The two
fields may belong to one subject, as here, or to two subjects the same `for`
binds (`c.amount > l.cap`). One token tells this apart from a join: a bare name
on the right (`c.caller == f`) is a join, and a name followed by a field
(`p.spent > p.budget`) compares two values.

`!=` holds when the field holds some **recorded** value other than the one you
name. `porch` is `"active"`, so it is unfinished; `roof` is `"closed"`, so it is
not; and `shed` has no status at all. A field with no value holds neither `==`
nor `!=` — comparing against nothing is not a comparison — so to ask about a
field with no value, reach for `absent`.

### When none of them does — `none(...)`

`absent` asks about one cell of one subject. Some conditions are about a whole
set instead: *an order is complete when none of its lines is still open*.
`none(<name> in <Kind>: <premises>)` holds when no subject of that kind
satisfies every premise inside it:

```dpy
# complete-orders.dpy — an order is complete when none of its lines is still open.
class Order:
    placed: bool
    complete: bool

class Line:
    order: string
    shipped: bool

@rule
def order_complete():
    for o in Order:
        if none(l in Line: l.order == o and l.shipped == False):
            o.complete = True

def complete_orders():
    remember(Order.o1.placed, True, "shop")
    remember(Order.o2.placed, True, "shop")
    remember(Order.o3.placed, True, "shop")
    remember(Line.a.order, "o1", "shop")
    remember(Line.a.shipped, True, "depot")
    remember(Line.b.order, "o2", "shop")
    remember(Line.b.shipped, True, "depot")
    remember(Line.c.order, "o2", "shop")
    remember(Line.c.shipped, False, "depot")
    done = subjects(Order.complete, True)
    for o in done:
        print("complete: " + o)
```

```
OK script complete_orders(): 9 claims written, 2 prints
  remember Order.o1.placed = True
  remember Order.o2.placed = True
  remember Order.o3.placed = True
  remember Line.a.order = "o1"
  remember Line.a.shipped = True
  remember Line.b.order = "o2"
  remember Line.b.shipped = True
  remember Line.c.order = "o2"
  remember Line.c.shipped = False
  print complete: o1
  print complete: o3
```

The premises inside are the ordinary kind, and they may name one of the rule's
own subjects: `l.order == o` is what ties the set of lines to the order being
concluded about. `o2` has a line not yet shipped, so it is not complete. `o3`
has no lines at all, and it *is* complete — none of its lines is open, because
it has none. `none(...)` holds **vacuously** for a subject the set never
mentions, so add a premise of your own if an order with no lines should not
count. That is also why `none(...)` is enough on its own to say which subjects a
rule is about, where `absent` is not.

The rule records a helper field named after the rule —
`Order.order_complete__none1` here — holding `True` for the orders the
`none(...)` excluded. It shows in `list_attributes` and reads like any derived field, which
makes it a way to see what the quantifier found. A `none(...)` cannot sit inside
another one: conclude the inner condition into a field with a rule of its own,
and write the outer `none(...)` over that field.

### Copying a value — a conclusion that carries what it read

A conclusion can also record a value the rule **read**. Write a field of a bound
subject on the right, and the value found there is what the rule records:

```dpy
# sensor-labels.dpy — a sensor is labelled with its name unless someone labels it.
class Sensor:
    name: string
    label: string

@rule
def label_default():
    for s in Sensor:
        if not_asserted(s.label):
            s.label = s.name

def labels():
    remember(Sensor.a.name, "north door", "install")
    remember(Sensor.b.name, "south door", "install")
    remember(Sensor.b.label, "loading bay", "ops")
    la = current(Sensor.a.label)
    lb = current(Sensor.b.label)
    print("a: " + str(la.value))
    print("b: " + str(lb.value))
```

```
OK script labels(): 3 claims written, 2 prints
  remember Sensor.a.name = "north door"
  remember Sensor.b.name = "south door"
  remember Sensor.b.label = "loading bay"
  print a: north door
  print b: loading bay
```

`a` has no label recorded, so the rule gives it its name. `b` has one, and the
condition is `not_asserted(s.label)`, so the label someone recorded wins and the
rule stops concluding for `b`. This is a default that copies rather than one
that invents a value, and it needs no comparison: reading `s.name` is enough to
say which sensors the rule is about.

That same condition is what lets the program write `Sensor.b.label` at all.
`label` is the rule's conclusion, and a write at a rule's conclusion is refused
unless the rule **yields** — unless its condition has `not_asserted` on the very
field it concludes, as this one does. Without the `not_asserted`, the `remember`
of `b`'s label would be refused, naming `name` as the field to write instead.

A copy works across a join as well: `d.owner_name = p.name`, with `d.owner == p`
in the condition, records the owner's name on the device. It copies **every**
value the field holds, so when two sources disagree about a name the copy
records both, one from each, and the disagreement shows in the copied field
exactly as it stands in the original. A condition on the copied field chooses
which values pass: `if r.t > 30: r.hot = r.t` copies only the readings above
`30`.

### Writing a sentence — a conclusion that writes a text

A conclusion can write a text from the values the rule read, with an f-string.
Each field between braces is one of the rule's fields, as a copy's right side
is, and the words around them are yours:

```dpy
# sensor-summary.dpy — a sentence about each live sensor, written from its facts.
class Sensor:
    name: string
    temp: int
    status: string
    summary: string

@rule
def summary_line():
    for s in Sensor:
        if s.status == "live":
            s.summary = f"{s.name} reads {s.temp} degrees."

def summaries():
    remember(Sensor.a.status, "live", "install")
    remember(Sensor.a.name, "North door", "install")
    remember(Sensor.a.temp, 21, "probe")
    first = current(Sensor.a.summary)
    print(str(first.value))
    update(Sensor.a.temp, 24, "probe")
    second = current(Sensor.a.summary)
    print(str(second.value))
    steps = why(Sensor.a.summary)
    for step in steps:
        print(str(step.value) + " (" + step.trust + ")")
```

```
OK script summaries(): 4 claims written, 6 prints
  remember Sensor.a.status = "live"
  remember Sensor.a.name = "North door"
  remember Sensor.a.temp = 21
  print North door reads 21 degrees.
  update Sensor.a.temp = 24
  print North door reads 24 degrees.
  print North door reads 24 degrees. (derived)
  print live (asserted)
  print North door (asserted)
  print 24 (asserted)
```

Nothing rewrote the sentence. The program revised the temperature, and the
sentence the store holds is the one written from the temperature now in force.
It is a conclusion, so `why` explains it: the sentence, then the three recorded
values it rests on. A sensor with no temperature recorded has no sentence,
because reading a field makes its presence a premise, as it does for a copy.

Three things to know. The text is a `string` whatever it reads as, so
`f"{s.temp}"` records the text `"24"` where the copy `s.shown = s.temp` records
the number. A field holds a `string` or an `int`; over a field holding anything
else, a `real` or a `bool` say, no sentence is drawn for that subject, and
`why_not(Sensor.a.summary)` names the field and the value it holds. And a field
is written plain: `{s.temp + 1}`, `{s.temp:>5}` and `{s.name!r}` are refused
when you define the rule. A value that needs working out goes into a field of
its own, and the sentence names that field.

### Where a value came from — `source` and `trust`

A premise can ask where a value came from as well as what it is.
`source(r.temp) == "lab"` holds for the value the lab recorded, and the right
side may instead be a subject the rule binds, which relates a value to what
the store says about whoever recorded it:

```dpy
# readings.dpy — the lab's readings, and the ones an accredited station vouches for.
class Reading:
    temp: int
    lab_temp: int
    vetted: int

class Station:
    accredited: bool

@rule
def lab_temp():
    for r in Reading:
        if source(r.temp) == "lab":
            r.lab_temp = r.temp

@rule
def vetted():
    for r in Reading, s in Station:
        if source(r.temp) == s and s.accredited == True:
            r.vetted = r.temp

def readings():
    remember(Reading.r1.temp, 21, "lab")
    remember(Reading.r1.temp, 24, "north")
    remember(Reading.r1.temp, 26, "south")
    remember(Station.north.accredited, True, "registry")
    lt = get(Reading.r1.lab_temp)
    vt = get(Reading.r1.vetted)
    for c in lt:
        print("lab: " + str(c.value))
    for c in vt:
        print("vetted: " + str(c.value))
```

```
OK script readings(): 4 claims written, 2 prints
  remember Reading.r1.temp = 21
  remember Reading.r1.temp = 24
  remember Reading.r1.temp = 26
  remember Station.north.accredited = True
  print lab: 21
  print vetted: 24
```

Three sources disagree about `r1.temp`, and each rule picks out the value it
asked for. `lab_temp` copies the lab's `21` and nothing else, because the copy
and the source test read one value. `vetted` copies `24`, since `north` is a
station the store holds as accredited. `south` is not, and the lab is not a
station at all. Forget the accreditation and `vetted` is withdrawn.
`source(r.temp) != "lab"` would hold through `24` and `26`.

`trust(...)` asks the other half: whether a person recorded the value
(`"asserted"`) or a rule concluded it (`"derived"`). Beside the sensor default
above, `if trust(s.label) == "derived": s.defaulted = True` marks the sensors
that are showing their name because nobody labelled them.

### A known absence — `known_absent`, and concluding one

Chapter 2's `assert(K.s.a, src)` records an **absence**: not that nobody knows
the value, but that a source looked and there is none. The vet scanned the dog
and found no chip. That is information, and a rule can tell it apart from a lack
of information. A field has three states a premise can ask about:

- `absent(p.chip)` — the field has **no value at all**: nobody wrote one, no rule
  concluded one, and nobody recorded an absence.
- `not_asserted(p.chip)` — **nobody recorded** anything there, whatever a rule
  concluded.
- `known_absent(p.chip)` — a source **recorded that there is none**.

A recorded absence is a claim, so `absent` does not hold over it, and a person
recorded it, so `not_asserted` does not either. Only `known_absent` holds. It
reads a claim, which also makes it enough on its own to say which subjects a rule
is about, where `absent` and `not_asserted` are not.

A rule can **conclude** an absence too. Write `assert(<cell>)` as the
conclusion, with no source — the rule is the source:

```dpy
# chip-scan.dpy — a recorded absence is a fact; a missing value is not.
class Pet:
    born_here: bool
    chip: string
    to_chip: bool

@rule
def born_here_unchipped():
    for p in Pet:
        if p.born_here == True and not_asserted(p.chip):
            assert(p.chip)

@rule
def needs_chip():
    for p in Pet:
        if known_absent(p.chip):
            p.to_chip = True

def chip_scan():
    remember(Pet.rex.chip, "985112003", "vet")        # scanned: a chip
    assert(Pet.bella.chip, "vet")                     # scanned: no chip
    remember(Pet.milo.born_here, True, "shelter")     # born here, never scanned
    remember(Pet.luna.born_here, False, "shelter")    # came in, not scanned yet
    todo = subjects(Pet.to_chip, True)
    for p in todo:
        print("to chip: " + p)
    remember(Pet.milo.chip, "985112004", "vet")       # milo is chipped
    later = subjects(Pet.to_chip, True)
    for p in later:
        print("still to chip: " + p)
```

```
OK script chip_scan(): 4 claims written, 1 absence assertion, 3 prints
  remember Pet.rex.chip = "985112003"
  assert Pet.bella.chip absent
  remember Pet.milo.born_here = True
  remember Pet.luna.born_here = False
  print to chip: bella
  print to chip: milo
  remember Pet.milo.chip = "985112004"
  print still to chip: bella
```

`bella`'s absence the vet recorded. `milo`'s the rule concluded, because he was
born here and nobody had recorded a chip for him. Over the rule's conclusion
`known_absent` holds, `absent` does not — the field holds a claim — and
`not_asserted` does, since no person recorded it. `luna` is not on the list:
nothing is recorded about her chip, so her field is `absent`, but nobody has said
she has none. Read with `current`, a recorded absence is a claim whose value is
`null` (Chapter 3), so a rule cannot copy or fold a field it tests with
`known_absent` — there is no value to carry.

Like any conclusion, a concluded absence goes when its condition stops holding.
Once the vet records `milo`'s chip, `not_asserted(p.chip)` fails, the absence is
withdrawn, and `milo` drops off the list. That `remember` is allowed because
`born_here_unchipped` yields: its condition has `not_asserted` on the field it
concludes.

### Facts about a pair

`g.tainted` is a fact about one subject. A fact about a **pair** — `a` reaches
`b` — is written with the same three-segment path you use everywhere else,
except that its last two segments are bound names:

```dpy
# reaches.dpy — a rule that reads what it writes, so one step becomes every step.
class Fn:
    cyclic: bool

class Call:
    caller: string
    callee: string

class Reach:
    placeholder: bool

@rule
def reaches_direct():
    for c in Call, x in Fn, y in Fn:
        if c.caller == x and c.callee == y:
            Reach.x.y = True

@rule
def reaches_further():
    for c in Call, x in Fn, y in Fn, z in Fn:
        if Reach.x.y == True and c.caller == y and c.callee == z:
            Reach.x.z = True

def reaches():
    remember(Call.c1.caller, "main", "src")
    remember(Call.c1.callee, "parse", "src")
    remember(Call.c2.caller, "parse", "src")
    remember(Call.c2.callee, "lex", "src")
    one = current(Reach.main.parse)
    two = current(Reach.main.lex)
    print("main reaches parse = " + str(one.value))
    print("main reaches lex   = " + str(two.value))
```

```
OK script reaches(): 4 claims written, 2 prints
  remember Call.c1.caller = "main"
  remember Call.c1.callee = "parse"
  remember Call.c2.caller = "parse"
  remember Call.c2.callee = "lex"
  print main reaches parse = True
  print main reaches lex   = True
```

Nothing recorded that `main` reaches `lex`. The calls say only `main → parse` and
`parse → lex`; the second rule reads a reach already derived, joins it to a
further edge, and records the longer one — so it applies to its own conclusions
until nothing new follows. Reading a relation with a bound name in the field
position asks for **every** cell of that subject, which is why `Reach.x.y` in a
premise finds each `y` that `x` reaches instead of needing one supplied.

A name used twice in one cell **agrees with itself**, so asking which subjects
are in a cycle needs nothing further — a subject that reaches itself is in one:

```
@rule
def in_cycle():
    for x in Fn:
        if Reach.x.x == True:
            x.cyclic = True
```

Every name in a rule is one its `for` binds, and a relation premise decides which
subjects both of its names stand for. So a pair reads backwards as easily as
forwards: the name in the field position may be the subject of a conclusion.

```
@rule
def reached_by():
    for x in Fn, y in Fn:
        if Reach.x.y == True:
            Back.y.x = True
```

Beside the two rules above, this records `Back.lex.main` as `True` once
`reaches()` has run: `lex` is reached from `main`, which no call said directly.

A conclusion can copy the value a pair holds, as it copies a field's. With
`r.origin == x and r.dest == y` in the condition, `r.km = Dist.x.y` records on
each route the distance recorded for its two towns; both names in the pair must
be bound, as they are in a relation premise.

A pair can be missing as a field can. `absent(Reach.x.y)` holds where nothing is
recorded for that pair, and `not_asserted(...)` and `known_absent(...)` take a
pair the same way. An absence says which pairs a rule does *not* apply to, never
which ones it does, so another premise must name both subjects — here the reach
the other way round:

```
@rule
def one_way():
    for x in Fn, y in Fn:
        if Reach.y.x == True and absent(Reach.x.y):
            OneWay.x.y = True
```

Beside the rules above, this records `OneWay.parse.main`, `OneWay.lex.parse` and
`OneWay.lex.main`: each is reached, and none reaches back. A later call from
`lex` to `main` closes a loop in which each function reaches every other, and all
three withdraw. A rule may
not test `absent(Reach.x.y)` and conclude into `Reach` itself, since the field
`y` names could be the one it records; `not_asserted(Reach.x.y)` is the form
that yields to a recorded value instead.

**A relation is as large as the pairs it holds.** A rule like `reaches_further`
records a fact for every pair one subject reaches, and each of those is a stored
claim you can read, question and withdraw like any other. That is the right shape
for a module import graph, a service dependency map, or a workflow of a few
hundred subjects. For a graph of thousands, ask the narrower question — the
number of steps you actually need — rather than deriving every pair.

### Standing constraints — an invariant you are told about

A rule concludes something. Sometimes what you want is the opposite: a condition
that should never hold, and a report when it does. That is a **standing
constraint**. It reads like a rule, with `@constraint` for `@rule` and `violated`
where the conclusion would be:

```dpy
# stock-watch.dpy — an invariant the store is watched against.
class Product:
    stock: int

@constraint
def stock_never_negative():
    for p in Product:
        if p.stock < 0:
            violated

def stock_watch():
    remember(Product.bolt.stock, 40, "warehouse")
    remember(Product.nut.stock, -3, "warehouse")
    n = current(Product.nut.stock)
    print("nut stock = " + str(n.value))       # -3
```

The `-3` is recorded. A constraint is **never checked on write**: a store in the
middle of an edit is routinely inconsistent, and a write that failed on somebody
else's invariant would be a worse failure than a report saying so. A constraint
concludes nothing and writes nothing, either, so no later rule can pick a breach
up as a fact — which is the whole difference from a rule that concludes
`p.invalid = True`.

You ask for the report with the `checkup` tool. It gives one line per constraint
that does not hold, naming how many subjects breach it and up to five of them.
With this program compiled as the module `shop`, it reads
`violated shop.stock_never_negative 1 nut`. To stop watching, pass that name to
the `forget_constraint` tool. It reclaims nothing — the constraint concluded
nothing — so the data it watched stays, the `-3` included: stopping the watch is
not fixing the breach. Both are tools you call, described in the
[MCP Reference](/ref/dke/mcp/).

A constraint binds **exactly one** subject, and its premises are comparisons
against a literal (`p.stock < 0`, `p.tier == "gold"`) or absences
(`absent(o.customer)`), joined by `and`. A comparison may order text as well as numbers: a premise that orders a string field against a quoted bound (`<`, `<=`, `>`, `>=`) is judged by codepoint order, and the constraint is reported violated exactly when a rule with the same premise would conclude. To watch something beyond that, conclude
it into a field with a rule, and write the constraint over that field. A
constraint shares the unit's one name space with scripts, rules and classes, and
`list(target = "rules")` does not list it, since it derives nothing.

### Hypotheses — reasoning without committing

A **hypothesis** reads what a value *would be* under supposed facts, changing
nothing. `suppose(<field>, <value>, …, <field>)` sets each named field to the
value beside it, lets your rules and computed fields run as if those were true,
reads the last field, and then discards the suppositions — the store is left
exactly as it was:

```dpy
# what-if.dpy — read a value under a supposed fact, committing nothing.
class Order:
    total: int
    review: bool

@rule
def needs_review():
    for o in Order:
        if o.total > 1000:
            o.review = True

def what_if():
    would = suppose(Order.o1.total, 2000, Order.o1.review)
    print("if total were 2000, review would be = " + str(would))   # True
    after = current(Order.o1.review)
    match after:
        case active_claim:
            print("persisted?! " + str(after.value))
        case empty:
            print("nothing persisted")                          # this arm runs
```

```
OK script what_if(): 2 prints
  print if total were 2000, review would be = True
  print nothing persisted
```

The result is a `value` — bind it and read it, or concatenate it into a `print` (it
renders `true` here). If the read field has no value under the supposition,
`suppose` produces no value — a catchable refuse (guard it with `try` /
`except`, Chapter 9, or read a field a rule is known to derive). Because nothing
it touches persists, a hypothesis is safe for preview, comparison, and what-if
exploration.

### Supposing more than one fact

Real scenarios rarely turn on a single fact. A rule that needs two conditions at
once cannot be probed by supposing one of them — so give as many `<field>,
<value>` pairs as the question takes. The field to read is always the last
argument, alone:

```dpy
# what-if-two.dpy — a rule that needs two facts, asked about both at once.
@rule
def needs_review():
    for o in Order:
        if o.total > 1000 and o.shipment == "sent":
            o.review = True

def what_if_two():
    remember(Order.o1.total, 500, "sales")
    remember(Order.o1.shipment, "held", "ops")

    both = suppose(Order.o1.total, 2000,
                   Order.o1.shipment, "sent",
                   Order.o1.review)
    print("under both = " + str(both))                  # True

    after = current(Order.o1.review)
    match after:
        case active_claim:
            print("persisted?! " + str(after.value))
        case empty:
            print("still nothing persisted")            # this arm runs
```

Supposing only the total here would answer nothing at all: the order still has
not shipped, so the rule does not fire and there is no value to read. Both facts
have to be true at the same time, which is exactly what the scenario says.

Two things worth knowing. Suppositions apply **left to right**, so if two of
them name the same field the later one stands — the same rule an ordinary
sequence of writes follows. And a hypothesis takes at most **16**; that is a
cost bound, not a limit on what you can ask, and going over it is a compile
error that says the number. A scenario written by hand does not come close.

`suppose_absent` takes as many fields as you like the same way, and its read is
also the last argument — `suppose_absent(a, b, c)` supposes away `a` and `b` and
reads `c`. One hypothesis supposes facts into place or away, though, never
both.

### Asking what you would lose

There is a second hypothesis, and it is the one to reach for before you delete
anything. `suppose_absent(<field>, <field>)` asks what the second field would say
if the first field's fact **were not there**:

```
r = suppose_absent(Order.o1.total, Order.o1.review)
match r:
    case active_claim:
        print("review would still say", r.value)
    case empty:
        print("review would disappear")
```

`forget` (Chapter 2) is permanent — only the `restore` tool, while a checkpoint
stands, brings anything back — and `dependents` (Chapter 11) only tells you what
*points at* a fact, not what your answers become without it. This tells you
that, while the fact is still there to keep.

Note what comes back: an **active claim that may be empty**, matched exactly
like `current`. That differs from `suppose` on purpose. `suppose` asks what a
value *would be*, so having no answer is unusual and arrives as a refuse you
catch. `suppose_absent` asks what would *survive* — and "nothing" is usually
exactly what you were checking for, so you read it rather than catch it.

---

## Chapter 9 — Control flow as constraints

You have been using DKE Python's control flow all along — `match` since Chapter 1,
`if` since Chapter 5, `for … in` inside rules in Chapter 8. It is the control flow
you already know from Python: `if`/`else`, `for … in`, `match`, and `try`/`except`. What earns a chapter is not what these constructs *do* — you have that —
but what DKE deliberately takes **away**.

There is no `while`, no recursion, and no unbounded loop; `for … in` ranges only
over a **finite collection** — one the store hands back, or one your program
built, such as a list or a `range(n)` — never an open-ended counter.
That is not a limitation to work around — it is the mechanism by which **every DKE
Python program is guaranteed to terminate**, bought by refusing the shapes
that could loop forever. The rest of this chapter is the specific guardrails.

### `if` / `else`

The condition can be any value that **has a truth value** — DKE Python uses
Python's **truthiness**. `if xs:` is true when the list is non-empty, `if s:` when
the string is non-empty, `if n:` when the number is non-zero; `False`, `0`, `0.0`,
`""` and the empty collections you build are falsy. You saw a plain boolean
condition in `if v.match:` in Chapter 5, but you can branch on emptiness directly
too. Two more Python idioms follow from this: `and` / `or` **return an operand**
(not a coerced bool), so `name or "anonymous"` is `name` when it is non-empty and
`"anonymous"` otherwise, and `x > 0 and label` is `label` when `x > 0`; and `not x`
gives the boolean opposite of `x`'s truthiness.

What the store hands back is the exception. A read result — an `active_claim`, a
`claim_list`, a `proof_tree`, a `subject_set` and the rest — has **no** truth value,
and using one as a condition is refused. An empty read and a read that found
nothing to tell you are different answers, and a single `False` would say both, so
ask for `.length` when you mean emptiness, and walk the result with `for … in`.

### `for … in`

You may only iterate a **finite** source — a `claim_list`, `string_list`,
`subject_set`, `result_type_set`, or `proof_tree`; a constructed `list` / `set` /
`dict`, `range(n)` among them; a dict's `.keys()`, `.values()` or `.items()`; a
tuple whose elements all have one type; or a
`string`, which binds each **character** in turn (a one-character string), by
Unicode character. The source is snapshotted when the loop begins:

```dpy
# iterate-history.dpy — walk every claim in a cell's history.
def iterate_history():
    remember(Cat.felix.color, "grey", "op1")
    remember(Cat.felix.color, "orange", "op2")     # co-active alternative
    hist = get(Cat.felix.color)
    print("walking " + str(hist.length) + " claim(s)")
    for c in hist:
        print("  recorded by " + str(c.source))
```

A `for` header can also name several targets and unpack each element into them,
as in `for k, v in d.items():` — Chapter 15 shows it with tuples and dicts.

### `match`

`match` dispatches over a read result (`active_claim` vs `empty`, as in Chapter 1),
over a `.value`'s class and over the shape of a list or a dict (both in Chapter 3),
and over an instance's class (Chapter 7). It also **compares**, as Python's does:
over an `int`, a `real`, a `string` or a `bool`, a `case` label is a value pattern —
a literal, literals joined by `|`, or a name that captures the value — and `case _:`
takes whatever is left:

```
n = 2
match n:
    case 0:        print("none")
    case 1 | 2:    print("a couple")
    case _:        print("several")
```

A `match` over any value Python has needs no catch-all: when no arm matches, none
runs, exactly as in Python. `case int():` tests a class, and `case int(n):` also binds
the value. A `match` over a `value` that names a class, and one naming a class with no
`()`, must be exhaustive, or end in `case _:` or `case default:`.

### `try` / `except`

A recoverable failure is a **refuse**; a fault from the service layer is an
`engine_error`. You catch each with its own handler, binding the details. The
handlers may come in either order, and the first one naming what was raised is the
one that runs:

```dpy
# guard-try.dpy — catch a refuse and an engine error.
def guard_try():
    try:
        remember(Cat.felix.color, "orange", "op1")
        print("write succeeded")
    except refuse as r:
        print("refused: " + str(r.reason))
    except engine_error as e:
        print("engine error: " + str(e.reason))
```

Both handlers are optional, and so is each handler's `as <name>`: write a bare
`except refuse:` when the body does not need the refuse details. `except engine_error` takes any run-time failure the run would report as `engine_error`; a spent budget, a stopped run and an add-only refusal remain uncatchable.

`r.reason` is written for a person, and it is what a program should report. When
a program must act differently depending on *which* refusal it met, it branches
on `r.discriminator`, a short tag. For a refusal the store raises, the tag is the
`refuse_reason` code the [MCP Reference](/ref/dke/mcp/) publishes, such as
`conflicting_write`, `pinned_address` or `invalid_value`; for one your own program
raises, it is the exception name you wrote (Chapter 13). `r.teaching_hint` says
how to correct the call, and is `""` when there is no suggestion — show it to a
person, never branch on it. An `engine_error` carries its tag as `e.code`.

```dpy
# refusal-tags.dpy — branch on which refusal it was, not on its wording.
def refusal_tags():
    remember(Door.front.state, "shut", "op1")
    pin(Door.front.state)
    try:
        forget(Door.front.state)
    except refuse as r:
        if r.discriminator == "pinned_address":
            print("pinned, so it stays")
        else:
            print("refused: " + r.reason)
        if r.teaching_hint != "":
            print("to change it: " + r.teaching_hint)
```

```
OK script refusal_tags(): 1 claim written, 1 pin, 2 prints
  remember Door.front.state = "shut"
  pin Door.front.state
  print pinned, so it stays
  print to change it: lift the pin with `unpin` on the same address, then remove it
```

Only those two kinds of tag are promised — the published codes and your own
exception names — so branch on the ones you have seen and keep an `else` for the
rest.

### The rest of Python's control flow

These work as they do in Python, so they get one example rather than a section
each: `elif`; `break` and `continue`; an `else` on a `for`, which runs when no
`break` left the loop; `else` and `finally` on a `try`; `pass`; a bare `return`
to leave a procedure early; the conditional expression `a if c else b`; chained
assignment `a = b = 0`; and a binding with a type annotation,
`limit: int = 50`. `raise` and the `assert` statement are here too — Chapter 13
shows them.

```dpy
# python-flow.dpy — the rest of Python's control flow works as it does there.
def check(reading: int):
    if reading < 0:
        print("a level cannot be negative")
        return
    try:
        remember(Tank.t1.level, reading, "gauge")
    except refuse as r:
        print("refused: " + r.reason)
    else:
        print(f"recorded {reading}")
    finally:
        print("checked")

def python_flow():
    limit: int = 50
    under = skipped = 0
    for n in [12, 0, 48, 73, 90]:
        if n == 0:
            skipped += 1
            continue
        elif n > limit:
            print(f"first over the limit: {n}")
            break
        under += 1
    else:
        print("nothing over the limit")
    size = "large" if under > 1 else "small"
    print(f"{under} under, {skipped} skipped, a {size} batch")
    check(-5)
    check(30)
```

```
OK script python_flow(): 1 claim written, 5 prints
  print first over the limit: 73
  print 2 under, 1 skipped, a large batch
  print a level cannot be negative
  remember Tank.t1.level = 30
  print recorded 30
  print checked
```

A closing note: comparisons **chain** as in Python — `a < b < c` means
`(a < b) and (b < c)`, each adjacent pair compared — so range checks read
naturally.

---

## Chapter 10 — Transactions

Ordinary invocation is **not** transactional: if a later write fails, earlier
writes still stand. When you need all-or-nothing, open a **branch**:

```dpy
# try-paint.dpy — an experimental write, committed only if it holds.
def try_paint():
    with branch("experiment"):
        try:
            remember(Cat.felix.color, "tigret", "audit")
            after = current(Cat.felix.color)
            if after.value == "tigret":
                commit
            else:
                rollback
        except refuse as r:
            print("paint refused: " + str(r.reason))
            rollback
```

A `branch` runs its suite and **commits on normal completion**; an uncaught
failure rolls it back and re-raises. Inside a branch, `commit` and `rollback`
finish it explicitly. Branches do not nest, and only the store is rolled
back — your variable bindings are never undone. This is the one place the
store behaves transactionally: a rolled-back branch leaves no trace, where an
ordinary sequence of writes leaves each write as history.

### Worlds — alternatives you keep

A branch is settled when its block ends. When you want an alternative that
outlasts the program — a scenario you build up over several runs, read later,
and weigh against another — create a **world**:

```dpy
# scenarios.dpy — two forecasts, kept side by side.
def scenarios():
    create_world("wet")
    create_world("dry")
    with world("wet"):
        remember(Field.north.rain_mm, 180, "forecast")
    with world("dry"):
        remember(Field.north.rain_mm, 40, "forecast")
    d = compare_worlds("wet", "dry")
    for c in d:
        print(c.path, c.value)
```

Inside `with world(...)`, a program reads everything the store holds and what
the world holds, and every write lands in the world; the store never sees it.
The world stays when the program ends, and a later program enters it again with
`with world("wet"):`. `compare_worlds(a, b)` lists the claims `a` holds that `b`
does not, rule conclusions included, so you see how the scenarios' consequences
differ as well as their facts. When one proves right, `merge_world("wet")` makes
its writes the store's own, and `discard_world("dry")` drops the other. A world
adds to the store and never changes what the store held before it, and worlds do
not nest.

A later program need not remember what an earlier one created. `list_worlds()`
names the worlds that exist, in name order, and it answers inside a
`with world(...)` block as well as outside one. After `scenarios.dpy` this
prints `world: dry`, then `world: wet`:

```
names = list_worlds()
for w in names:
    print("world: " + w)
```

---

## Chapter 11 — Tracing what a claim caused

Given a **claim**, you can ask what other claims the engine derived from it —
the forward direction of provenance, complementing `why` in the next chapter:

```dpy
# track-changes.dpy — read a claim, then see what was derived from it.
def track_changes():
    remember(Cat.felix.color, "orange", "op1")
    update(Cat.felix.color, "grey", "op1")   # a later edit supersedes it
    cur = current(Cat.felix.color)           # the current claim at this cell
    deps = dependents(cur)                   # claims derived from this claim
    print("dependents = " + str(deps.length))
    hist = get(Cat.felix.color)              # every claim at the cell, in order
    print("history depth = " + str(hist.length))
```

- `dependents(<claim>)` → `claim_list` — the claims the engine derived from a
  claim (read the claim from `get`/`current` first). A base fact with no rules
  firing on it has none.
- `dependents(<claim>, transitive=True)` → `claim_list` — everything resting on
  the claim, however far down: what it concluded, what those concluded, and so
  on, each claim once.
- `get(K.s.a)` → `claim_list` — every claim ever recorded at the cell, so a
  supersession chain is readable as history without any bookmark to compare
  against.

`dependents` takes a claim's `.claim_id` (Chapter 2) in place of the claim, and
so do `premises` (Chapter 12), `forget` and `would_forget`. The id names the
claim whatever is written after you read it, so you can keep it and come back
to the claim later — further down the procedure, or in a later program
altogether:

```dpy
# trace-by-id.dpy — keep a claim's id, then trace and remove the claim by it.
class Order:
    price: int
    qty: int
    total: int = price * qty

def trace_by_id():
    remember(Order.o1.price, 300, "sales")
    remember(Order.o1.qty, 5, "sales")
    p = current(Order.o1.price)
    kept = p.claim_id                          # a string that names this claim
    update(Order.o1.qty, 6, "sales")           # later writes leave the id alone
    below = dependents(kept)
    print("the price feeds " + str(below.length) + " claim(s)")   # the price feeds 1 claim(s)
    n = would_forget(kept)
    print("forgetting it removes " + str(n))                      # forgetting it removes 1
    forget(kept)
    t = current(Order.o1.total)
    match t:
        case active_claim:
            print("total = " + str(t.value))
        case empty:
            print("no price, so no total")                        # this arm runs
```

`forget(kept)` removes that one claim — and, as every removal does, what was
derived from it, which is why the total goes too. An id that names no claim the
store holds is refused, and the refusal says why that can happen: the claim may
have been removed, or concluded again, or brought back by the `restore` tool as
a value in force — and the last two each record a new claim, with an id of its
own.

> **A note on where undo lives.** The language has no restore point and no
> rewind; undo lives outside it, in two tools. The service's `checkpoint`,
> `diff` and `restore` tools mark a position under a name, show what changed
> since it, and bring back values and whole modules removed after it — at the
> store's current position, never overwriting what you wrote since
> ([MCP Reference §9.7](/ref/dke/mcp/#change-what-happened-since-a-mark)). They
> reach only removals made while a mark was standing, so take one before
> anything uncertain. A **store snapshot**, taken and restored from your
> account dashboard, is the broader undo: restoring replaces the whole store
> with the snapshot and keeps an automatic backup of what it replaced, so the
> undo is itself undoable.

---

## Chapter 12 — Provenance with `why`

Every claim knows where it came from, and `why` shows you the whole derivation
that produced a value. It returns a `proof_tree` — a finite, **iterable**
collection of the claims that participated, with `.length`, indexing, `for … in`,
and a `.root` (the claim you asked about):

```dpy
# show-why.dpy — inspect the provenance of a recorded value.
def show_why():
    remember(Cat.felix.color, "orange", "op1")
    pt = why(Cat.felix.color)
    print("proof has " + str(pt.length) + " claim(s)")
    r = pt.root
    print("root recorded per " + str(r.source))
    for c in pt:
        print("  participating claim per " + str(c.source))
```

Handed straight to `print`, a `proof_tree` shows only its size — `proof_tree(2)` —
so read a claim's fields — `.path`, `.value`, `.source` — or build a string from
them with `+`, as above, to see what it holds. The `proof_tree` is the derivation alone, the conclusion and then the claims it rests on: a cell's earlier, superseded values are no longer elements of it, and `get` lists them.

When the value you ask about is **derived** — a computed field or a fact a standing
rule recorded (Chapter 8, where the engine derives facts) — `why` shows the claims it was built from,
not just the value itself. This is where the engine's reasoning becomes auditable:
a derived fact carries the inputs that justify it:

```dpy
# why-derived.dpy — why over a derived value lists the claims it was built from.
class Order:
    price: int
    qty: int
    total: int = price * qty

def why_derived():
    remember(Order.o1.price, 300, "sales")
    remember(Order.o1.qty, 5, "sales")
    pt = why(Order.o1.total)                       # total is derived: price × qty
    print("proof has " + str(pt.length) + " claim(s)")     # 3 — the value and its two inputs
    root = pt.root
    print("derived value = " + str(root.value))            # 1500
```

### Which rule, and what it read

A derived claim names what concluded it in `.derived_by`: a rule by its name, a
computed field by its class and field. A claim someone recorded reads the empty
string there. `premises(c)` goes one step up from a conclusion, to the claims it
was drawn from — the mirror of `dependents` in Chapter 11, which goes one step
down:

```dpy
# why-premises.dpy — name what concluded a value, then read what it rested on.
class Order:
    price: int
    qty: int
    total: int = price * qty

def why_premises():
    remember(Order.o1.price, 300, "sales")
    remember(Order.o1.qty, 5, "sales")
    t = current(Order.o1.total)
    print("concluded by " + t.derived_by)          # Order.total
    ps = premises(t)
    for p in ps:
        print("  from " + p.path + " = " + str(p.value))
```

The premises come back in name order — here `Order.o1.price`, then
`Order.o1.qty` — and a claim someone recorded has none. Walking `premises` from
each claim you reach traces a derivation to the facts it rests on, one step at a
time.

A rule can also say what kind of relation it states: `@rule(kind="causal")`, or
`"definition"`, `"empirical"`, `"policy"` or `"heuristic"`. A conclusion reads
it back as `.rule_kind`, so whoever reads an answer can tell one resting on a rule
of thumb from one resting on a definition. The kind changes nothing the rule
concludes; it is there for the reader.

### Why the answer changed

A derivation rests on claims, and claims carry validity windows (Chapter 4). So
a conclusion can hold at one moment and not another, without anybody rewriting
a rule — the premise simply moved out of force, or a different one moved in.

`why` takes the same as-of datetime `current` and `get` take, and it answers
with the derivation **as it stood then**:

```dpy
# why-changed.dpy — the same question, asked at two moments.
@rule
def needs_review():
    for o in Order:
        if o.total >= 1000:
            o.review = True

def why_changed():
    remember(Order.o1.total, 900, "sales",           # first half of 2024
             datetime("2024-01-01T00:00:00Z"),
             datetime("2024-05-31T00:00:00Z"))
    remember(Order.o1.total, 1500, "sales",          # second half
             datetime("2024-06-01T00:00:00Z"),
             datetime("2024-12-31T00:00:00Z"))

    early = why(Order.o1.review, datetime("2024-03-01T00:00:00Z"))
    late  = why(Order.o1.review, datetime("2024-09-01T00:00:00Z"))

    print("in March: " + str(early))          # <empty> — the rule had not fired
    print("in September: " + str(late))       # a proof_tree
    for c in late:
        print("  rested on " + str(c.value) + " per " + str(c.source))
```

In March the order totalled 900 and the rule did not fire, so there is no
derivation to show. In September it totalled 1500 and the rule concluded, so the
proof carries the premise that made it true. The difference between the two
answers is the account of what changed.

Note what the March call returns. There being **no derivation** is not a
zero-length proof — it is `empty`, the same absence sentinel a never-written
`current` gives you (Chapter 4). So reach for `.length` or `for … in` only on an
answer you know is a proof; a `str()` tells the two apart, and `match` is the
thorough way. Its arms are the two answers `why` can give — `case proof_tree:`
for a derivation, `case empty:` for none — and inside the first you can read the
proof safely. Continuing the program above:

```dpy
    match early:
        case proof_tree:
            print("March rested on " + str(early.length) + " claims")
        case empty:
            print("March: nothing was derivable")
    match late:
        case proof_tree:
            if late.truncated:
                print("September: part of the derivation")
            else:
                print("September: the whole derivation, " + str(late.length) + " claims")
        case empty:
            print("September: nothing was derivable")
```

The March arm that runs is `case empty:`, and September prints `the whole
derivation, 2 claims`. `.truncated` is the one field worth checking before you
treat a proof as complete: a derivation can run deeper than a proof shows, and a
proof cut short otherwise reads exactly like a whole one. It is `True` when the
answer stops short of the whole derivation, and `False` when what you have is
all of it.

An empty proof is a finding, not a failure: it means no conclusion was derivable
at that instant. That is a different thing from a conclusion that is derivable
and false, which is the next section's question.

Omit the datetime and you get the derivation as of now.

### When the answer is not there

`why` needs a claim to explain. The harder moment is the other one: you ask for
a conclusion and get nothing back, and the store cannot tell you anything —
because there is no claim to point at.

`why_not` answers that. It names the condition that blocked the conclusion, at
the cell you can act on. What makes it worth having is a distinction you cannot
otherwise make: an empty read looks exactly the same whether a condition was
never recorded, or was recorded and fails its test. Those need opposite fixes.

```dpy
# why-not.dpy — the two empties that need opposite fixes.
@rule
def device_is_online():
    for d in Device:
        if d.power > 0 and d.checks > 0:
            d.online = True

def show_why_not():
    remember(Device.b.power, 5, "s1")           # b: checks never recorded
    remember(Device.c.power, 5, "s1")
    remember(Device.c.checks, 0, "s1")          # c: recorded, and it fails > 0
    remember(Device.w.power, 5, "s1")
    remember(Device.w.checks, 2, "s1",          # w: recorded, passes the test,
             datetime("2024-01-01T00:00:00Z"),  #    and its window has closed
             datetime("2024-12-31T00:00:00Z"))

    why_b = why_not(Device.b.online)
    why_c = why_not(Device.c.online)
    why_w = why_not(Device.w.online)
    print(why_b) # rule `device_is_online` needs Device[b].checks > 0,
               # and nothing is recorded there
    print(why_c) # rule `device_is_online` needs Device[c].checks > 0,
               # and Device[c].checks is 0 (int)
    print(why_w) # rule `device_is_online` needs Device[w].checks > 0,
               # and Device[w].checks is recorded as 2 but not in force
               # at the time asked about
```

`w` is the one worth pausing on. Its `checks` is recorded and its value passes
the rule. What it lacks is force at the moment you asked: the window you gave
the write closed before then. The move is a wider window or an as-of inside the
one you have — not another write, which is what "nothing is recorded there"
would have sent you to do.

`c` carries the other detail worth reading: the `(int)` after its value. A
failing condition tells you the value it read **and what type that value is**,
because those are two different reasons a condition can fail. `0` is an `int`
and genuinely is not `> 0`. Had `checks` held the string `"0"`, the line would
read `is "0" (string)` — and a string is not compared with a number at all, so
the condition would not fail on the comparison so much as never reach it. The
two print the same value, and the type is what tells them apart. When a
condition fails and the value looks like it should have passed, read the type
first.

The same thing is true of the cell you ask about directly. `why_not(Device.w.checks)`
— the windowed cell itself, not the conclusion it feeds — tells you it is
recorded and out of force, rather than leaving you to infer it from an empty
`get`. You do not need a rule in the picture to get that answer.

Two more answers are worth recognising. If no standing rule concludes the cell
at all, you are told exactly that — your model has no path to the conclusion,
which is a different problem from an unmet condition. And if the sources at a
condition disagree, you are told that too — when the disagreement is the reason
nothing concluded. A rule reads every value standing at a location and derives
from each one that satisfies its condition. Every condition on that field must
hold of the same value, so `r.t > 30 and r.t < 40` is not met by a `50` and a
`20` together. A disagreement where one side
would satisfy the rule gives you a conclusion from that side; you hear about the
disagreement when no side satisfies it. Either way the store decides nothing:
`conflicts()` still names the location, and `why` on a conclusion shows the
claim it came from.

`what_needs` asks the same situation forward. Where `why_not` says what is
blocking, `what_needs` says what would unblock it — walking through conditions
your own rules can derive and stopping at the facts only you can supply.

```dpy
    need_b = what_needs(Device.b.online)
    print(need_b) # via rule `device_is_online`:
               #   have Device[b].power
               #   need Device[b].checks > 0 (record this)
    need_w = what_needs(Device.w.online)
    print(need_w) # via rule `device_is_online`:
               #   have Device[w].power
               #   need Device[w].checks > 0 (recorded, but not in force
               #     at the time asked about)
```

The `w` line is the same distinction reaching the forward question. A list of
things to do is only useful if every line is a thing you have not done, so a
condition you already recorded says so rather than asking for it again.

A rule that looks across subjects can meet one more kind of empty. Each of its
conditions can be recorded, and met, and still nothing is concluded, because no
one subject meets them all:

```dpy
# why-not-together.dpy — each condition met, but not by the same plant.
@rule
def open_valve():
    for p in Plant, b in Bed:
        if p.thirsty == True and p.bed == b:
            b.water_on = True

def show_not_together():
    remember(Plant.fern.thirsty, True, "s1")    # fern: thirsty, in the north bed
    remember(Plant.fern.bed, "north", "s1")
    remember(Plant.cactus.thirsty, False, "s1") # cactus: in the south bed,
    remember(Plant.cactus.bed, "south", "s1")   #   and not thirsty

    why_south = why_not(Bed.south.water_on)
    print(why_south) # rule `open_valve` needs Plant[`p`].thirsty == True
               # and Plant[`p`].bed == "south" together: each is met on its
               # own, but no one `p` meets all of the rule's conditions at once
    need_south = what_needs(Bed.south.water_on)
    print(need_south[0]) # via rule `open_valve`:
    print(need_south[1]) #   need Plant[`p`].thirsty == True (met on its own,
               #     but not together with the rule's other conditions)
    print(need_south[2]) #   need Plant[`p`].bed == "south" (met on its own,
               #     but not together with the rule's other conditions)
```

`` Plant[`p`] `` is the rule's own `p`, a plant the rule has not fixed, and not
a plant called `p`. Both conditions are recorded, and both are met: fern is
thirsty, and cactus is in the south bed. Nothing is missing, so writing another
fact would be the wrong move. They are met by different plants, and the fix is
on one plant. The answer names no plant, since any plant could be the one, and
it gives the same answer whichever order you write the `and` in.

Both are reads: asking why something is missing never changes whether it is.
Both return a `diagnosis` — print it for the whole answer, or iterate it a line
at a time.

---

## Chapter 13 — Errors and guarantees

Four things can go wrong, each with a distinct class:

- **`parse_error`** — the source is not well-formed (a syntax slip).
  Caught at compile time.
- **`type_error`** — the source parses but is not well-typed (a read result used
  as an `if` condition, a `for … in` over a tuple whose positions differ in type,
  an `as` binding on a detect-only value class).
  Also caught at compile time.
- **`refuse`** — a runtime request the service declines (for example `rollback`
  outside a branch, an aggregate over an attribute with no data, or a hypothesis whose
  supposed read has no value), or one your own program raises (below). Refuses
  are **control flow** — you catch them with `except refuse`. Where Python would
  raise, DKE hands you a refuse.
- **`engine_error`** — a fault from the service layer, caught with
  `except engine_error`. Its `.code` names which fault it was, the way a
  refuse's `.discriminator` does (Chapter 9).

Because a refuse is ordinary control flow, you can turn a declined request into a
printed line rather than a crash:

```dpy
# catch-refuse.dpy — a refuse is control flow, not a crash.
def catch_refuse():
    try:
        rollback                        # refuses: there is no branch here
        print("this line is skipped")
    except refuse as r:
        print("caught a refuse: " + str(r.reason))
```

Your own program can refuse, too, with Python's two statements for it.
`raise ValueError("…")` refuses with that message as `r.reason` and the
exception name as `r.discriminator`; any of Python's built-in exception names
works (`ValueError`, `KeyError`, `TypeError`, `RuntimeError`, …), and they all
behave the same — there are no exception classes to declare. `assert cond, msg`
refuses as an `AssertionError` when `cond` is false, and does nothing when it is
true:

```dpy
# raise-and-assert.dpy — refusals you raise yourself, and how to tell them apart.
def deposit(amount: int):
    assert amount != 0, "a deposit of nothing records nothing"
    if amount < 0:
        raise ValueError("a deposit cannot be negative")
    remember(Account.main.pending, amount, "teller")

def raise_and_assert():
    for amount in [25, -5, 0]:
        try:
            deposit(amount)
            print(f"deposited {amount}")
        except refuse as r:
            print(f"{r.discriminator}: {r.reason}")
```

```
OK script raise_and_assert(): 1 claim written, 3 prints
  remember Account.main.pending = 25
  print deposited 25
  print ValueError: a deposit cannot be negative
  print AssertionError: a deposit of nothing records nothing
```

Python prints the same three lines. A `raise` never falls through, so a branch
ending in one needs no `return` in a procedure that returns a value. Inside an
`except`, `raise` alone sends the same exception on, and `raise e` does too.

The `assert` **statement** is not the `assert(K.s.a, src)` **verb** of Chapter 2,
which records that a value is known to be absent. The parenthesis straight after
the word is what tells them apart: `assert amount > 0` is the statement, and
`assert(Pet.rex.chip, "vet")` is the verb. So do not wrap the condition in
parentheses as Python allows — `assert (amount > 0), "…"` is read as the verb,
and refused.

Two guarantees hold for **every** DKE Python program, and they are the
deepest departure from Python — not a feature you invoke but a property you cannot
opt out of:

- **Termination.** With no recursion and only bounded iteration over finite
  collections, every program finishes. There is no infinite loop to write.
- **Determinism.** The same program over the same store produces the same result
  shape every time.

Python gives you the freedom to loop forever and to depend on run-to-run
variation; DKE trades both away on purpose, and gets provable termination and
reproducibility in return.

---

## Chapter 14 — Lists and comprehensions

Everything so far has read collections *out of the store* — a `get` gives a
`claim_list`, `subjects` a `subject_set`. DKE Python also lets you **build** your
own lists, with the syntax you already know from Python, and transform them
without writing anything to the store.

A list literal is written `[…]`. You can index it, slice it, ask its `.length`,
and test membership with `in`, exactly as in Python. A **comprehension**
(`[expr for x in xs if cond]`) filters or maps one list into another. And two
string methods bridge text and lists: `split` cuts a string into a `list<string>`,
and `join` stitches one back into a string.

```
# lists-tutorial.dpy — build a list, read it, filter with a comprehension,
# and bridge to and from text with split and join.
def lists_tutorial():
    scores = [90, 55, 72, 40, 88]
    print("all = " + str(scores))
    print("how many = " + str(scores.length))
    print("top = " + str(scores[0]))
    print("worst = " + str(scores[-1]))
    passing = [s for s in scores if s >= 60]
    print("passing = " + str(passing))
    csv = "ada,grace,alan"
    names = csv.split(",")
    print("names = " + str(names))
    shouted = [n.upper() for n in names]
    print("shouted = " + str(", ".join(shouted)))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

A list you build prints as Python prints it — `[90, 55, 72, 40, 88]` — while a
collection the store hands back prints as a counted preview, `2 entries […]`; a
comprehension keeps only the elements its `if` admits; `split` and `join` are inverses across a
separator:

```
OK script lists_tutorial(): 7 prints
  print all = [90, 55, 72, 40, 88]
  print how many = 5
  print top = 90
  print worst = 88
  print passing = [90, 72, 88]
  print names = ['ada', 'grace', 'alan']
  print shouted = ADA, GRACE, ALAN
```

These lists are **shared** and **bounded**. `xs.append(v)` changes the list `xs`
holds in place, as `xs += [v]` does, so every name holding that list sees the
change — `b = xs` holds the same list, not a copy, exactly as in Python ([Python Reference §7.17](/ref/dke/python/#changing-a-collection)). When you want a copy, take one: `ys = xs.copy()` is a new list
holding the same elements, and appending to it leaves `xs` as it was. To ask
whether two names hold one list, use `is`: after `b = xs`, `b is xs` is `True`
and `xs is xs.copy()` is `False`, and `is not` says the opposite. It asks the
same of a set or a dict. Over a number or a string `is` is refused, with a
message naming `==`: Python leaves it to the implementation whether two equal
numbers or strings are one object, so there is no answer to match. Every
comprehension ranges over a finite source, and a `for`
never runs more steps than its list had when it began, so — like every other DKE
Python construct — a program over lists is guaranteed to terminate (Chapter 13).
A constructed list exists only while the program runs; it is never stored.

### Changing a list in place

A list changes the way it does in Python. Write one element with `xs[i] = v`, or
replace a whole slice with `xs[a:b] = […]`, which may be longer or shorter than
the slice it replaces. Remove with `del xs[i]` or `del xs[a:b]`. `xs.pop()` removes
the last element and hands it back (`xs.pop(i)` the one at `i`), so it can stand
wherever a value can. A write reaches inside a list of lists too: `grid[1][0] = 7`
changes the inner list in place.

```
# change-list.dpy — write an element and a slice, delete, pop, and write
# inside a nested list.
def change_list():
    xs = [1, 2, 3, 4, 5]
    xs[0] = 10
    xs[1:3] = [20]
    print("written = " + str(xs))
    del xs[-1]
    print("deleted = " + str(xs))
    last = xs.pop()
    print("popped = " + str(last) + ", left = " + str(xs))
    grid = [[0, 0], [0, 0]]
    grid[1][0] = 7
    print("grid = " + str(grid))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

The slice `[2, 3]` became the one element `20`, so the list got shorter, and `pop`
answered the `4` it removed:

```
OK script change_list(): 4 prints
  print written = [10, 20, 4, 5]
  print deleted = [10, 20, 4]
  print popped = 4, left = [10, 20]
  print grid = [[0, 0], [7, 0]]
```

An index past either end refuses at run time, as Python's `IndexError` does, and
you can catch it with `try` (Chapter 13).

The rest of Python's list methods work too, each changing the list in place:
`xs.sort()` (which takes `sorted`'s `key=` and `reverse=`, Chapter 15),
`xs.reverse()`, `xs.extend(ys)`, `xs.insert(i, v)`, `xs.remove(v)`, which removes
the first element equal to `v`, and `xs.clear()`. Each is a statement that answers
nothing, so `ys = xs.sort()` is refused where Python would bind `None`; `pop` is
the one that also answers a value.

```dpy
# list-methods.dpy — sort, reverse, grow, and shrink a list in place.
def list_methods():
    xs = [3, 1, 2]
    xs.sort()
    print("sorted = " + str(xs))
    xs.reverse()
    print("reversed = " + str(xs))
    xs.extend([4, 5])
    xs.insert(0, 9)
    print("grown = " + str(xs))
    xs.remove(2)
    print("without 2 = " + str(xs))
    same = xs
    print("same list = " + str(same is xs) + ", copy = " + str(xs is xs.copy()))
    xs.clear()
    print("cleared = " + str(same))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

`same` holds the list `xs` holds, so clearing `xs` empties it too:

```
OK script list_methods(): 6 prints
  print sorted = [1, 2, 3]
  print reversed = [3, 2, 1]
  print grown = [9, 3, 2, 1, 4, 5]
  print without 2 = [9, 3, 1, 4, 5]
  print same list = True, copy = False
  print cleared = []
```

Removing a value the list does not hold refuses in Python's words,
`list.remove(x): x not in list`.

### Counting, converting, and repeating

`range` gives a counting loop its numbers, in its three Python forms:
`range(stop)`, `range(start, stop)` and `range(start, stop, step)`, where a
negative `step` counts down. What it hands back is an ordinary list, so it prints
as one: `print(range(4))` prints `[0, 1, 2, 3]`, where CPython prints
`range(0, 4)`. `reversed(xs)` is not: like CPython's, it hands back an
iterator, which `list(...)` reads into a list and `"".join(...)` into a string
(more on iterators under *Pairing collections*, below).

The everyday Python builtins work as they do in Python. `int(…)` and `float(…)`
convert a string or a number; `round`, `abs` and `divmod` do arithmetic, and
`round` rounds half to even, as Python's does; `ord` and `chr` cross between a
character and its codepoint; `repr` gives a value's repr text. `*` repeats a
string, a list or a tuple: `"-" * 20` draws a rule and `[0] * n` makes a list of
`n` zeros.

```dpy
# builtins-demo.dpy — count with range, convert, round, and repeat.
def builtins_demo():
    print("range = " + str(range(4)) + " " + str(range(2, 7)) + " " + str(range(10, 0, -3)))
    print("converted = " + str(int("42") + 1) + ", " + str(float("2.5")))
    print("rounded = " + str(round(2.5)) + ", " + str(round(3.14159, 2)) + ", " + str(abs(-7)))
    print("divmod = " + str(divmod(17, 5)))
    print("codes = " + str(ord("A")) + ", " + chr(97) + ", " + repr("hi"))
    print("backwards = " + str(list(reversed([1, 2, 3]))))
    print("-" * 12)
    print("zeros = " + str([0] * 3))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

Every line but the first prints what CPython prints; that one prints lists
where CPython prints `range` objects:

```
OK script builtins_demo(): 8 prints
  print range = [0, 1, 2, 3] [2, 3, 4, 5, 6] [10, 7, 4, 1]
  print converted = 43, 2.5
  print rounded = 2, 3.14, 7
  print divmod = (3, 2)
  print codes = 65, a, 'hi'
  print backwards = [3, 2, 1]
  print ------------
  print zeros = [0, 0, 0]
```

A string that is not a number, as in `int("abc")`, refuses at run time the way
Python's `ValueError` does. The [Python Reference](/ref/dke/python/) gives each
of these with its full rules in §6.3, and `range` in §6.12.

### Generator expressions

A comprehension written in a call's parentheses instead of brackets,
`sum(n * n for n in nums)`, is a **generator expression**. DKE Python accepts one
as the whole argument of a call that reads every element before it returns:
`sum`, `min`, `max`, `any`, `all`, `sorted`, `list`, `tuple`, `set`, `dict`, a
string's `join`, and the set methods of Chapter 15. There it means the bracketed
comprehension, except that `any` and `all` stop at the element that decides, as
Python's do. Beside another argument, give it its own parentheses.

```dpy
# generator-demo.dpy — reduce a list without building one first.
def generator_demo():
    nums = [3, 1, 4, 1, 5]
    print("sum of squares = " + str(sum(n * n for n in nums)))
    print("any above 4 = " + str(any(n > 4 for n in nums)))
    print("all positive = " + str(all(n > 0 for n in nums)))
    words = ["ada", "grace", "alan"]
    print("longest = " + str(max(len(w) for w in words)))
    print("shouted = " + ", ".join(w.upper() for w in words))
    print("by remainder = " + str(sorted((n % 3 for n in nums), reverse=True)))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

Each line prints what CPython prints for the same program:

```
OK script generator_demo(): 6 prints
  print sum of squares = 52
  print any above 4 = True
  print all positive = True
  print longest = 5
  print shouted = ADA, GRACE, ALAN
  print by remainder = [2, 1, 1, 1, 0]
```

Anywhere else a generator expression would be a generator object, and DKE Python
has none: bound to a name, returned, printed, or passed to `len`, `zip` or a
script, it is refused, and the message tells you to build a list with
`[… for … in …]` instead.

---

## Chapter 15 — Tuples, dicts, and sets

Chapter 14 built **lists**. DKE Python gives you three more collections you already
know from Python — **tuples**, **dicts**, and **sets** — and, like a list, each
exists only while the program runs: bounded and never stored. A tuple never
changes; a dict and a set are shared and change in place, as a list does. You
build them, read them, and transform them without writing to the store.

### Tuples — a fixed group of mixed-type values

A **tuple** `(a, b, c)` is a fixed-length group whose positions may each hold a
different type. A comma is what makes it a tuple: `(x)` just groups an expression,
`(x,)` is a one-element tuple, and `()` is empty. Because the positions can differ
in type, you index a tuple with a **constant** number — `t[0]`, `t[1]`, `t[-1]` —
and each read has a definite type. A tuple has a `.length` and compares with `==`,
and you can walk it with `for … in` when its positions share one type. A tuple of an
`int` and a `string` you index by position instead, since a loop variable holds one
type. You search a tuple as in Python: `t.index(v)` answers the first position
holding `v`, and refuses when none does, and `t.count(v)` answers how many
positions hold it.

```
# tuples-demo.dpy — build tuples, index them, and compare them.
def tuples_demo():
    point = (3, 4)
    print("point = " + str(point))
    print("x = " + str(point[0]))
    print("y = " + str(point[1]))
    print("dims = " + str(point.length))
    print("last = " + str(point[-1]))
    mixed = (1, "ada", True)
    print("mixed = " + str(mixed))
    print("name = " + str(mixed[1]))
    nested = ((1, 2), 3)
    print("nested = " + str(nested))
    single = (7,)
    print("single = " + str(single))
    print("same = " + str((3, 4) == point))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

A tuple renders as `(…)`, a one-element tuple keeps its trailing comma, and two
tuples of the same shape compare equal position by position:

```
OK script tuples_demo(): 10 prints
  print point = (3, 4)
  print x = 3
  print y = 4
  print dims = 2
  print last = 4
  print mixed = (1, 'ada', True)
  print name = ada
  print nested = ((1, 2), 3)
  print single = (7,)
  print same = True
```

### Dicts — a mapping kept in insertion order

A **dict** `{key: value, …}` maps keys to values. A key is hashable — a scalar (a
string, an int, a datetime, …) or a tuple of hashables — and keys are kept in the
order you wrote them — DKE Python dicts are
**insertion-ordered**, matching modern Python. Look a value up with `d[k]` (or
safely, with a fallback, `d.get(k, default)` — which returns `default` when the
key is absent instead of refusing; a default is required, since DKE Python has no
`None`), test a key with `k in d`, count entries with `.length`, walk the **keys**
with `for k in d`, and look at the parts through `.keys()`, `.values()`, and
`.items()` (the last gives `(key, value)` tuples). Each is a **view** of the dict,
as in Python: it follows the dict as the dict changes, so after
`names = ages.keys()` and `ages["dee"] = 19`, `names` holds `"dee"`. A view has a
length and takes `in`, but has no position — `list(ages.keys())[0]` reads the
first key. Writing a key twice keeps its first
position but takes the last value. The empty dict is `{}`. Two dicts compare
**order-independently** with `==` / `!=` — equal when they hold the same
key→value mapping, regardless of the order you wrote them in.

```
# dicts-demo.dpy — build a dict, read it by key, and project its parts.
def dicts_demo():
    ages = {"ana": 30, "bo": 25, "cy": 41}
    print("ages = " + str(ages))
    print("count = " + str(ages.length))
    print("ana = " + str(ages["ana"]))
    print("has bo = " + str(("bo" in ages)))
    print("has zz = " + str(("zz" in ages)))
    print("same = " + str((ages == {"cy": 41, "bo": 25, "ana": 30})))
    print("names = " + str(ages.keys()))
    print("years = " + str(ages.values()))
    print("pairs = " + str(ages.items()))
    for who in ages:
        print("key = " + str(who))
    dup = {"x": 1, "x": 9}
    print("dup = " + str(dup))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

The dict renders in insertion order; `.keys()` / `.values()` / `.items()` print
as the views they are, as Python prints them; and the duplicate key `"x"` keeps
its place but takes the later value `9`:

```
OK script dicts_demo(): 13 prints
  print ages = {'ana': 30, 'bo': 25, 'cy': 41}
  print count = 3
  print ana = 30
  print has bo = True
  print has zz = False
  print same = True
  print names = dict_keys(['ana', 'bo', 'cy'])
  print years = dict_values([30, 25, 41])
  print pairs = dict_items([('ana', 30), ('bo', 25), ('cy', 41)])
  print key = ana
  print key = bo
  print key = cy
  print dup = {'x': 9}
```

Looking up a **missing** key is a refuse, not a silent default — catch it with a
`try` (Chapter 13) or guard with `k in d` first.

### Changing a dict — counting and grouping

A dict fills the way it does in Python: `d[k] = v` writes a key, `d[k] += 1`
updates one, and `del d[k]` removes one. Three methods change the dict and hand
back a value. `d.pop(k)` removes a key and answers its value.
`d.setdefault(k, default)` answers the value at `k`, writing `default` there
first if the key is absent. `d.popitem()` removes the last entry and answers it as
a `(key, value)` tuple. `d.pop(k, default)` answers `default` when `k` is absent,
where `d.pop(k)` refuses. Two more change the dict and answer nothing:
`d.update(e)` writes every entry of another dict, or of a list of `(key, value)`
pairs, and `d.clear()` empties it. You can start from an empty `{}`. What you
first put in it, or add to what you read from it, gives it its key and value
types, so the counting loop you would write in Python is the one you write here.

```
# word-count.dpy — count words two ways, group them, and pop one out.
def word_count():
    words = "the cat and the hat".split(" ")
    counts = {}
    for w in words:
        if w in counts:
            counts[w] += 1
        else:
            counts[w] = 1
    print("counts = " + str(counts))
    tally = {}
    for w in words:
        tally[w] = tally.get(w, 0) + 1
    print("same = " + str(tally == counts))
    by_first = {}
    for w in words:
        by_first.setdefault(w[0], []).append(w)
    print("by first letter = " + str(by_first))
    gone = counts.pop("and")
    print("popped and = " + str(gone) + ", left = " + str(counts))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

Both loops count the same. `setdefault` hands back the list at each letter,
making it the first time, so `append` fills it in place:

```
OK script word_count(): 4 prints
  print counts = {'the': 2, 'cat': 1, 'and': 1, 'hat': 1}
  print same = True
  print by first letter = {'t': ['the', 'the'], 'c': ['cat'], 'a': ['and'], 'h': ['hat']}
  print popped and = 1, left = {'the': 2, 'cat': 1, 'hat': 1}
```

If nothing gives an empty dict a type before you read from it, as in
`v = d["a"]` right after `d = {}`, the compile is refused. The message names the
annotation that settles it: `d: dict<string, int> = {}`.

### Sets — unique elements, presented sorted

A **set** `{a, b, c}` (no colons — a colon makes it a dict) holds **unique**
elements: duplicates are dropped on the way in. DKE Python presents a set in a
**deterministic sorted order**, so a run is reproducible (Python leaves set order
unspecified; sorting it is a defined refinement). Test membership with `x in s`,
count with `.length`, walk it with `for x in s`, and combine sets with `.union`,
`.intersection`, `.difference`, and `.symmetric_difference`. Because `{}` is the
empty dict, the empty set has no literal: write `set()`. A set has no positions,
so `s[0]` is refused before it runs, as Python refuses it
(`'set' object is not subscriptable`). Read a set's elements with `for`, or
test one with `in`.

```
# sets-demo.dpy — dedupe, test membership, and combine sets.
def sets_demo():
    tags = {"red", "green", "red", "blue"}
    print("tags = " + str(tags))
    print("size = " + str(tags.length))
    print("has red = " + str(("red" in tags)))
    warm = {"red", "orange"}
    print("union = " + str(tags.union(warm)))
    print("shared = " + str(tags.intersection(warm)))
    print("only tags = " + str(tags.difference(warm)))
    print("either only = " + str(tags.symmetric_difference(warm)))
    nums = {3, 1, 2, 3, 1}
    print("nums = " + str(nums))
    for n in nums:
        print("n = " + str(n))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

The four repeated `"red"` and duplicate `3`/`1` collapse to one each, and every
set — literal, combined, or walked — comes out sorted:

```
OK script sets_demo(): 11 prints
  print tags = {'blue', 'green', 'red'}
  print size = 3
  print has red = True
  print union = {'blue', 'green', 'orange', 'red'}
  print shared = {'red'}
  print only tags = {'blue', 'green'}
  print either only = {'blue', 'green', 'orange'}
  print nums = {1, 2, 3}
  print n = 1
  print n = 2
  print n = 3
```

Python's set operators work as well: `s | t` (union), `s & t` (intersection),
`s - t` (difference) and `s ^ t` (symmetric difference), each a new sorted set.
On two integers `|`, `&` and `^` are bitwise instead, as in Python. Two
sets compare **by inclusion**: `s <= t` when every element of `s` is in `t`, and
`s < t` when `t` holds more besides; `>=` and `>` ask it the other way, and the
methods `s.issubset(t)`, `s.issuperset(t)` and `s.isdisjoint(t)` ask it of any
collection. A set changes in place, as a list does: `s.add(x)`, `s.discard(x)`,
`s.remove(x)`, which refuses when `x` is absent, `s.update(t)`, `s.clear()`, and
`s |= t` with its siblings `&=`, `-=` and `^=`. `s.pop()` removes and answers the
first element in the set's sorted order.

```dpy
# set-operators.dpy — combine and compare sets with operators, and change one.
def set_operators():
    tags = {"red", "green", "blue"}
    warm = {"red", "orange"}
    print("either = " + str(tags | warm))
    print("both = " + str(tags & warm))
    print("tags only = " + str(tags - warm))
    print("one only = " + str(tags ^ warm))
    print("inside = " + str({"red"} <= warm) + ", proper = " + str(warm < warm))
    print("apart = " + str(warm.isdisjoint({"blue", "gray"})))
    seen = set()
    seen |= warm
    seen.add("teal")
    seen.discard("red")
    print("seen = " + str(seen))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

The operators give the four sets the methods above gave. `{"red"}` is included in
`warm`, but no set is a proper subset of itself, and the empty `seen` took its
element type from `warm`:

```
OK script set_operators(): 7 prints
  print either = {'blue', 'green', 'orange', 'red'}
  print both = {'red'}
  print tags only = {'blue', 'green'}
  print one only = {'blue', 'green', 'orange'}
  print inside = True, proper = False
  print apart = True
  print seen = {'orange', 'teal'}
```

### Dict and set comprehensions

Chapter 14's comprehension built a list. The same shape, in braces, builds a set
or a dict. `{expr for x in xs}` is a **set comprehension** (deduped and sorted);
`{key: value for x in xs}` is a **dict comprehension** (insertion-ordered). Both
may carry an `if` filter, and both range over a finite source, so — like every DKE
Python construct — they terminate.

```
# comprehend-demo.dpy — build a dict and a set by bounded iteration.
def comprehend_demo():
    nums = [1, 2, 3, 4, 5]
    squares = {n: n * n for n in nums}
    print("squares = " + str(squares))
    evens = {n for n in nums if n % 2 == 0}
    print("evens = " + str(evens))
    parity = {n % 2 for n in nums}
    print("parity = " + str(parity))
    words = "ada,grace,alan".split(",")
    lengths = {w: w.length for w in words}
    print("lengths = " + str(lengths))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

The dict comprehension keeps insertion order; the set comprehension dedupes `n %
2` down to `{0, 1}` and sorts:

```
OK script comprehend_demo(): 4 prints
  print squares = {1: 1, 2: 4, 3: 9, 4: 16, 5: 25}
  print evens = {2, 4}
  print parity = {0, 1}
  print lengths = {'ada': 3, 'grace': 5, 'alan': 4}
```

### Pairing collections: zip, enumerate, and partition

Two builtins pair collections into **tuples**. `zip(a, b)` pairs elements
position by position (stopping at the shorter input); `enumerate(xs)` numbers each
element from `0`, or from a start you give it, `enumerate(xs, 1)`. Both hand back
an **iterator**, as Python's do: it gives each pair once. Walk it and unpack each
pair into two names, `for name, score in zip(names, scores):` (more on unpacking
below), or read it into a list with `list(...)` when you want to index the pairs
or read them twice. Reading an iterator uses it up, so a second read finds it
empty, and it has no `len` and no `[i]` of its own. And on
the string side, `partition` and `rpartition` split a string **once** — at the
first or last separator — into a three-part tuple, while `splitlines` breaks a
string into a list of its lines.

Three more reduce a collection to one value: `sum(xs)` adds numeric elements
(`0` for an empty list), starting from a value you give it with `sum(xs, start)` or
`sum(xs, start=…)` (`sum([1, 2], 10)` is `13`, and a list start joins lists: `sum([[1], [2]], [])`
is `[1, 2]`), and `min(xs)` / `max(xs)` return the smallest / largest —
`min`/`max` also take the values directly, `min(3, 7, 2)`. These read an in-memory
list; they are distinct from the same-named **store aggregates** `sum(K.attr)` /
`max(K.attr)` (Chapter 5), which fold one attribute across every subject of a
kind — the argument tells them apart (a bare `Kind.attribute` path folds the
store; anything else reduces the list in hand). `min`/`max` of an empty list refuses, like Python's `ValueError`.

A few more round out the set. `sorted(xs)` returns a new list in order
(`sorted(xs, reverse=True)` descending, and `key=` orders it by a key, below);
`any(xs)` / `all(xs)` fold truthiness to a `bool` (`all([])` is `True`); `bool(x)`
gives any value's truthiness; and `tuple(xs)` makes an immutable, runtime-length
tuple from a list. You can index it
(`t[i]`), size it (`len(t)`) and unpack it (`a, b = tuple(xs)`). Because its length
is known only when the program runs, an unpack that does not fit refuses then,
as Python's `ValueError` does.

```
# pairing-demo.dpy — pair lists, number them, and split strings.
def pairing_demo():
    names = ["ada", "grace", "alan"]
    scores = [90, 85, 70]
    paired = zip(names, scores)
    print("paired = " + str(paired))
    pairs = list(paired)
    print("pairs = " + str(pairs))
    print("first pair = " + str(pairs[0]))
    print("again = " + str(list(paired)))
    ranked = list(enumerate(names))
    print("ranked = " + str(ranked))
    for name, score in zip(names, scores):
        print(name + " scored " + str(score))
    parts = "user@example.com".partition("@")
    print("parts = " + str(parts))
    print("local = " + str(parts[0]))
    print("domain = " + str(parts[2]))
    tail = "a.b.c".rpartition(".")
    print("tail = " + str(tail))
    lines = "one\ntwo\nthree".splitlines()
    print("lines = " + str(lines))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

`zip` prints as the iterator it is. `list(...)` reads its pairs into a list you
can index, and leaves the iterator used up, so reading it again gives `[]`;
`partition` splits at the **first** `@` and `rpartition` at the **last** `.`:

```
OK script pairing_demo(): 13 prints
  print paired = <zip object>
  print pairs = [('ada', 90), ('grace', 85), ('alan', 70)]
  print first pair = ('ada', 90)
  print again = []
  print ranked = [(0, 'ada'), (1, 'grace'), (2, 'alan')]
  print ada scored 90
  print grace scored 85
  print alan scored 70
  print parts = ('user', '@', 'example.com')
  print local = user
  print domain = example.com
  print tail = ('a.b', '.', 'c')
  print lines = ['one', 'two', 'three']
```

### Unpacking into several names

Names separated by commas, on the left of `=` or after `for`, form a **target
list**, and it unpacks a tuple or a list into those names at once, as in Python.
`for k, v in d.items():` walks a dict's entries,
`for n, name in enumerate(names, 1):` numbers a list, and
`key, value = line.split("=")` takes a string apart. The whole right side is
worked out before any name is bound, so `a, b = b, a` swaps
two values, and `xs[i], xs[j] = xs[j], xs[i]` swaps two elements. A target may
itself be a list in parentheses, `(x, y), z = ((1, 2), 3)`, and one target may be
starred, `first, *rest = xs`, to take whatever is left over as a list.

```dpy
# unpack-demo.dpy — unpack tuples, swap, and walk pairs.
def unpack_demo():
    ages = {"ana": 30, "bo": 25}
    for name, age in ages.items():
        print(name + " is " + str(age))
    for n, name in enumerate(["ada", "grace"], 1):
        print(str(n) + ". " + name)
    key, value = "colour=red".split("=")
    print(key + " -> " + value)
    a, b = 1, 2
    a, b = b, a
    print("a = " + str(a) + ", b = " + str(b))
    (x, y), z = ((1, 2), 3)
    print("x, y, z = " + str(x) + ", " + str(y) + ", " + str(z))
    first, *rest = [10, 20, 30]
    print("first = " + str(first) + ", rest = " + str(rest))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

Each line prints what CPython prints for the same program:

```
OK script unpack_demo(): 8 prints
  print ana is 30
  print bo is 25
  print 1. ada
  print 2. grace
  print colour -> red
  print a = 2, b = 1
  print x, y, z = 1, 2, 3
  print first = 10, rest = [20, 30]
```

A comprehension takes a target list too, `[k for k, v in ages.items() if v > 26]`,
and after `return` or on the right of `=` a tuple may drop its parentheses:
`return 1, 2` returns `(1, 2)`, and `x = 1,` binds `(1,)`. A tuple must hold
exactly as many values as there are names, and a compile checks that. A list's
length is known only when the program runs, so a list that does not fit refuses
then, in CPython's words: `key, value = "colour".split("=")` refuses with
`not enough values to unpack (expected 2, got 1)`, which you can catch with `try`
(Chapter 13).

### Sorting and picking by a key

`sorted`, `min` and `max`, and a list's `sort`, take `key=` as in Python: each
element is compared by what the named function answers for it.
`sorted(words, key=len)` puts the shortest word first and `max(words, key=len)`
picks the longest. The key is a **name** — a builtin that takes one argument, such as `len`,
`abs`, `ord` or `str`, or a script of your own, declared in the same unit or
imported. Equal keys keep their order, because the sort is stable.

```dpy
# sort-by-key.dpy — sort and pick by a key: a builtin's, or your own script's.
def last_letter(w: string) -> string:
    return w[-1]

def sort_by_key():
    words = ["pear", "fig", "banana", "kiwi"]
    print("by length = " + str(sorted(words, key=len)))
    print("longest = " + max(words, key=len))
    print("shortest = " + min(words, key=len))
    print("by last letter = " + str(sorted(words, key=last_letter)))
    print("longest first = " + str(sorted(words, key=len, reverse=True)))
```

Run it with `run` ([MCP Reference §4.2](/ref/dke/mcp/#run-execute)):

`pear` and `kiwi` are the same length, so they keep the order they came in,
whichever way the list is sorted. Each line prints what CPython prints:

```
OK script sort_by_key(): 5 prints
  print by length = ['fig', 'pear', 'kiwi', 'banana']
  print longest = banana
  print shortest = fig
  print by last letter = ['banana', 'fig', 'kiwi', 'pear']
  print longest first = ['banana', 'pear', 'kiwi', 'fig']
```

There is no `lambda`. A lambda is a function held as a value, and no DKE Python
type holds a function, so where Python would write `key=lambda w: w[-1]` you write
a short `def` and name it, as `last_letter` does here. The compiler's answer to a
`lambda` says the same.

Every collection here — tuple, dict, and set — is bounded, exactly like a list,
and each exists only while the program runs and is never stored. A tuple
never changes. A dict and a set are shared like a list: change one through any
name and every name holding it sees the change ([Python Reference §7.17](/ref/dke/python/#changing-a-collection)). Each
copies the way a list does — `s.copy()`, `d.copy()`, or `dict(d)`.

---

## Chapter 16 — Loading many facts at once

Everything so far wrote one claim per statement. That is the right shape for a
handful of facts and the wrong one for ten thousand: a program that says
`remember` ten thousand times is ten thousand lines to generate, to send, and to
read back.

You do not need a different verb. Put the claims in **data** and write the
`remember` once. A path segment that names a variable in scope resolves to that
variable's *value*, so the subject can come from the row:

```
# survey-load.dpy — many claims from one written `remember`.
def survey_load():
    rows = [("kitchen", 21), ("hallway", 18), ("cellar", 9)]
    for r in rows:
        room = r[0]
        remember(Sensor.room.temp, r[1], "survey")
```

Three claims, one written `remember`. The rows can be as long as you like — the
loop does not grow.

Only the **subject** needs a name of its own (`room = r[0]`), because a path
segment has to be an identifier. The value and the source take the row's fields
directly, which is what lets each claim carry its own provenance:

```
# survey-sources.dpy — each claim carries the source its own row named.
def survey_sources():
    rows = [("attic", 14, "survey-a"), ("porch", 11, "survey-b")]
    for r in rows:
        room = r[0]
        remember(Sensor.room.temp, r[1], r[2])
```

Each cell now records the source that particular reading came from, exactly as
if you had written the two `remember` calls out by hand.

### When a row is bad

A subject arriving from data is data, and data has bad rows. A value that is not
a name — one holding a space, or a `.`, or leading with a digit — is refused,
and the refusal names **the value**, not just the line:

```
that subject is not a usable name: `room` held "back porch" — a name starts
with a letter or `_` and continues with letters, digits, `_` or `-`, so it
cannot hold a space or a `.`
```

A source taken from a row is not held to that rule, because a source is not a
name. It is a label: any text naming where the reading came from, so
`"2026 survey"`, `"Statistics Norway"` and a URL are all sources exactly as
written. What a source cannot be is empty, and data has blank cells too, so a
row whose source is blank is refused, naming where in the row it sat:

```
that source is empty: `r[2]` held "" — a source is any non-empty text naming
where the content came from
```

A source also may not hold one of a few reserved characters, and that refusal
names the character by its code point.

That matters here more than anywhere else. The loop is one line, so the line
number tells you nothing about which of ten thousand rows was wrong; what the
refusal names is what you have to go on.

Because it is a refuse and not an error, you can take it per row — skip what
will not load, keep what will, and report the rest. A bad subject and a bad
source raise the same kind of refusal, so one handler takes both:

```
# survey-skip.dpy — skip the rows that will not load, keep the rest.
def survey_skip():
    rows = [("larder", 6, "survey"), ("back porch", 19, "survey"),
            ("study", 20, ""), ("attic", 14, "2026 survey")]
    kept = 0
    skipped = 0
    for r in rows:
        room = r[0]
        try:
            remember(Sensor.room.temp, r[1], r[2])
            kept = kept + 1
        except refuse as e:
            skipped = skipped + 1
            print(e.reason)
    print("kept " + str(kept) + ", skipped " + str(skipped))
```

If you would rather have all-or-nothing, wrap the loop in a transaction
(Chapter 10) and a bad row takes the whole load back with it:

```
# survey-atomic.dpy — a bad row takes the whole load back with it.
def survey_atomic():
    rows = [("landing", 17), ("scullery", 12)]
    with branch("survey"):
        for r in rows:
            room = r[0]
            remember(Sensor.room.temp, r[1], "survey")
```

### What it costs

The same as writing the claims out one at a time. Each claim you ask for is one
operation whether it came from a statement you typed or a row in a list, so the
compact form is cheaper to write and to read back, never cheaper to buy. Choose
the shape that says what you mean.

---

## Chapter 17 — Modules

Everything you have compiled so far was a **module**, whether or not you thought
of it that way. A `.dpy` file *is* a module: it is the unit you submit, the unit
that gets stored under a name, and the unit another program can `import`.

A module's top level is its **body**, read top to bottom. It may hold
declarations (`def`, `class`, a `@rule`-marked `def`), ordinary statements, and
— this is the part with no Python equivalent — **data declarations**: writes
that sit at module scope rather than inside a procedure.

```dpy
# rates.dpy — a module that ships a fact and a procedure that reads it.
remember(Rate.vat.pct, 25, "finance-act-2026")

def show_vat():
    r = current(Rate.vat.pct)
    match r:
        case active_claim:
            print("vat = " + str(r.value) + "%")
        case empty:
            print("no rate recorded")
```

Compiling that stores the `def` **and performs the write**, because compiling a
module runs its body. The write is not a side effect to be careful of; it is how
a module ships the facts its procedures need.

### Importing

`import <module>` loads a module already stored under that name — it runs the
module's body once and brings its names into scope:

```dpy
import rates

def quote():
    rates.show_vat()
```

Because loading runs the body, anything the imported module prints or writes
belongs to *your* run: it joins your transcript at the point of the `import`,
and counts in your verdict. An `import` cycle — a module that imports itself,
directly or through another — is rejected when the module is loaded.

If your store holds no module by that name, the `import` fails with
`no module named rates`. When the program also calls into the module, as
`quote` does, it is refused before it runs, at the `import` and in those same
words. Check the spelling, or compile `rates` into this store first: each store
holds only what was compiled into it.

### Re-submitting is reconciliation, not duplication

This is the place DKE departs hardest from Python's `import`. A Python module
body runs once per process. A DKE module is **durable store state**, so
compiling it again — or importing it again — re-runs the body, and the re-run
**reconciles**:

- a data declaration whose value changed replaces the value it recorded
  before, and leaves a value any other source holds at that cell where it is;
- a data declaration whose value is unchanged leaves the cell alone — an
  identical write is not recorded again;
- a `class` or rule install is a no-op when nothing changed;
- a `def`, rule, computed field or constraint that an earlier compile installed
  and the text you submit does not declare is removed, and the answer names each
  thing it removed. Removing a rule or a computed field withdraws what it
  concluded. Removing takes a `read-write-delete` key: under a `read-write` key
  the compile is refused, names what it would remove, and changes nothing.

For the same reason a module's top level states each value once: writing one cell
twice from one source there is refused, because the second write would be
replayed, and the cell revised again, on every import.

So editing `rates.dpy` and compiling it again moves exactly the cells whose
values you changed, and nothing else. Re-submitting is safe to repeat, which is
what lets you treat a module as the current statement of what is true. The way
to stop using one of a module's rules is to delete it from your copy of the file
and compile again, and the way to bring it back is to restore the line and
compile again.

Two things a re-import leaves where they are. **Data is never removed by one**:
delete the line that wrote a fact and compile again, and the fact stays, still
readable. Removing facts takes a verb that says so — `forget`, or `forget_module`
for the whole module. And a re-import reaches the module, **not what was compiled
against it**: a script of yours compiled earlier that calls one of the module's
scripts keeps the body it was compiled with. The import's answer names each such
script, and compiling it again moves it onto the module as it stands.

### Namespaces, and who wins

A module is a namespace. A kind or script it declares is addressed under the
module name — `code.Function`, `code.impact_of` — so two modules may each
declare a `Function` without ever touching each other's cells.

Importing brings the imported module's kinds into scope *unqualified* in a path,
so after `import code` a bare `Call` in a path means `code.Call`. Building an
instance is the exception: a module's class is constructed only through its
module, so you write `code.Function("f1")`, and a bare `Function("f1")` is refused,
just as a bare name is not in scope after `import code` in Python. When a bare
name in a path could be ambiguous, the
rule is: **your own declaration wins**; failing that, the one imported module
that declares the name; and if two imported modules declare it and you declare
none, the program is refused rather than resolved by import order. The qualified
form always works and is always unambiguous, so it is the fix.

What `code.Function("f1")` builds is an instance, as a construction of your own
class is (Chapter 7). Bind it, and you read and write its fields through it:

```dpy
import code

def survey():
    f = code.Function("parse")
    remember(f.lines, 120, "survey")
    n = f.lines
    print(str(f) + " has " + str(n.value) + " lines")
```

Invoking `survey` writes the one fact and prints
`<code.Function 'parse'> has 120 lines`: an instance prints as its
module-qualified class and its subject. The instance goes wherever one of your
own would. Call a method its class declares on it, pass it to a parameter of
yours annotated `code.Function` (as `def size_of(f: code.Function):`), and test
it with `isinstance(f, code.Function)`, which is `True` here.

The same qualified name calls an imported module's scripts:

```dpy
import code

def review(fn: string):
    who = code.callers_of(fn)
    print(str(who.length) + " caller(s)")
```

`from <module> import <name>, …` loads the module exactly as `import` does, and
binds the scripts and classes you name, so you call them without the module
name. This one is a program you `run`:

```dpy
from code import callers_of, impact_of

who = callers_of("parse")
reach = impact_of("parse")
print(str(who.length) + " caller(s), " + str(reach.length) + " reached")
```

It binds only the names you list, as in Python: `code.hubs()` needs an
`import code` of its own, and a name the module does not declare is refused at
the `from` line. An `as` binds another name, as in Python: `from code import
callers_of as callers`. `from code import *` and a relative import are refused,
and each message names the form to write instead.

### Modules somebody else wrote

We publish **reasoning modules** — ordinary `.dpy` files with the classes, rules
and queries for one domain already written. You download the file and `compile`
it into your store, once, and `import` it from then on. A published name like
`code` is a default, never a reserved word: your store holds whatever you
compiled under that name.

Once compiled it is yours, without qualification. You can read every line before
you run it, remove a rule you do not want with `forget_rule`, or edit the file and
compile again. Nothing puts a removed rule back but a compile of your own — your
store holds what you put in it.

You manage modules at the wire surface, with tools rather than statements.
`list_modules` lists the modules in your store, and `info_module` reports one:
the scripts it defines, the classes, rules and constraints it declares, and when
it last changed. `list` gives every script with its signature, and
`list(target = "rules")` the names of your rules. `info` gives one script's compile
provenance, and `forget` removes one script; both name it `module.script`.
`forget_rule` removes one rule and withdraws what it concluded, leaving the rest
of the module in place. `forget_module` removes a whole module with its scripts,
rules, kinds and data. It needs `confirm = true`, and it refuses while another
stored module still refers to it. The [MCP Reference](/ref/dke/mcp/) gives
each tool's arguments and answers.

The published modules are part of the DKE Library, which has its own tutorial
and reference — the [Library Tutorial](/tutorial/dke/library/) and the
[Library Reference](/ref/dke/library/) — starting with `code`,
which reasons about call graphs, complexity and dependencies.

---

## Chapter 18 — Where to go next

The language teaches itself, too. Any source can carry a single option-verb line
to print a lesson — bare `--help` for an index, or `--help <topic>` for a specific
area:

```dpy
--help types
```

From here:

- The [Python Reference](/ref/dke/python/) is the exhaustive companion,
  organised by construct: every verb, type, operator, statement and class rule
  with a worked example. Its §15, *The knowledge model*, maps each distinction
  DKE keeps, such as unknown against false or disagreement against uncertainty,
  to the verbs that make it.
- The [MCP Reference](/ref/dke/mcp/) is the transport: the tool surface,
  the response envelope, the error model, and billing.
- The [MCP Tutorial](/tutorial/dke/mcp/) walks the connection itself — key,
  endpoint, first `compile`, first `run`.
- The [Library Tutorial](/tutorial/dke/library/) covers the modules we
  publish, which you compile into your store instead of writing the same declarations
  again.

Your Python tools work on DKE Python too. A standard Python parser reads a `.dpy`
file, so black, ruff and language servers work on it as it stands. A type checker
such as pyright or mypy also wants every name in scope, so DKE ships a stub,
`dke.pyi`, that declares the builtin surface: the verbs, the value factories, the
type names, `@rule` and `branch`. Check a copy that opens with the line
`from dke import *`, and submit the original, because the service refuses that line
as it refuses every `from … import *`. Two DKE constructs mean something different to a
Python checker — building an instance from a subject, `Sensor(room)`, and the
`case <type> as <var>:` type match — so relax the checks they trigger. The stub's
header lists the settings, the [Python Reference §14](/ref/dke/python/#python-tooling-and-type-checking) says the rest, and the
service stays the authority on types.

Everything you record is a claim, at a cell, with a source and a type you get back
unchanged; the engine will reason over those claims on your behalf; and `why` will
always show you how a value came to be. That — not the Python-shaped syntax — is
the whole of DKE Python.

## Revision history

Newest first. The revision is the surface's — one number stated by every
published document, the web pages and the service wire, moving whenever any
document changes. This list records the revisions at which this document
changed and what changed in it; a revision absent here left this document as it
was. The Version line at the top states this document's
version, the revision it last changed in and the current revision; from rev
148 each entry opens with the version that revision gave this document. The history
starts at rev 1. What a revision promises is stated in the
[Python Specification](/spec/dke/python/), its section 11.1.

- **1.1.2** · **rev 151** (2026-11-13) — The Version line states API 1.3: a rule premise may test part of a text, as `r.path.startswith("/srv/")`, `t.name.endswith(".test")` and `"admin" in a.role` ([Specification §14.2](/spec/dke/python/#premises)), and an addition moves the API's MINOR.
- **1.1.1** · **rev 150** (2026-11-13) — The Version line states API 1.2: calls made with keys that may only read run on one store together, where every call on a store ran alone ([MCP §9.8](/ref/dke/mcp/#stop-end-the-call-running-on-your-store)), and an addition moves the API's MINOR. Nothing else changed.
- **1.1.0** · **rev 149** (2026-11-13) — Chapter 8 gains *Writing a sentence — a conclusion that writes a text*: a rule's conclusion may be an f-string whose fields are the rule's own, `s.summary = f"{s.name} reads {s.temp} degrees."`, so the store holds a sentence that follows the facts it was written from and that `why` explains. The Version line states API 1.1.
- **1.0.0** · **rev 148** (2026-11-12) — This document states a version of its own, 1.0.0, first on the Version line and followed by the revision it last changed in, and from this revision each entry here opens with the version it made (Python Specification §11.1). Nothing else changed.
- **rev 147** (2026-11-12) — The Version line states API 1.0: the API version is `MAJOR.MINOR` (Python Specification §11.1). Nothing else changed.
- **rev 130** (2026-11-10) — Chapter 3: an f-string field takes no spec on a list, tuple, dict, set, dict view or slice. Chapter 8: a constraint premise may order text against a quoted bound by codepoint, and the constraint is reported violated exactly when a rule with the same premise would conclude. Chapter 9: `except engine_error` takes any run-time failure the run would report as `engine_error`. Chapter 12: a `proof_tree` is the derivation alone, and `get` lists a cell's earlier values.
- **rev 122** (2026-11-08) — Mathematics with `math` and `cmath`: the list of what `math` has names the logarithms to base 10, 2 and any base, `erf` and `erfc`, and `gamma` and `lgamma`.
- **rev 120** (2026-11-08) — Mathematics with `math` and `cmath`: the triangle program finds its long side with `math.hypot` and its angle in degrees with `math.degrees`, and finds the angle again from its sine with `math.asin`.
- **rev 112** (2026-11-06) — Structs and blobs: a blob is cut, joined and read a byte at a time, with a program that halves, swaps and reads one.
- **rev 111** (2026-11-06) — Applying a matrix with `vector`: `vector.sumsq` adds the squares of a list along axes, with a program that totals four readings over everything, along axis 0 and along axis 1.
- **rev 69** (2026-11-02) — Classes: a test on a value type narrows a name holding a `value`, in the branch it takes and, at the classes left to it, in its `else`.
- **rev 66** (2026-11-02) — Patterns, Instances, Coming from Python: a `match` needs no catch-all over a value Python has, reads any expression, and tests a class with `case int():`.
- **rev 65** (2026-11-02) — Coming from Python, Procedures: a `return` of a value needs no annotation.
- **rev 62** (2026-11-01) — Procedures: a procedure may name a class declared below it.
- **rev 61** (2026-11-01) — Procedures: a procedure may call another above or below it in the file. Sorting by a key: the script a `key=` names may stand anywhere in the unit.
- **rev 57** (2026-11-01) — A string's `.format` and `%` are here, as Python's are.
- **rev 41** (2026-10-31) — Calling a script: whatever follows a variadic or a bare `*` is passed by name, and whatever stands before a `/` by position. Raising: `raise` alone and `raise e` send on what an `except` caught.
- **rev 40** (2026-10-31) — Writing a string literal: the escapes are Python's, and a
  backslash before anything else stays in the value. Chapter 17: `as` binds another
  name.
- **rev 37** (2026-10-29) — Writing typed values: a scientific value is written
  as `scientific("…")`. A written blob and a written window are printed back as
  their factory calls. A refusal's code is snake_case: a program compares
  `r.discriminator` with `"pinned_address"`.
- **rev 33** (2026-10-23) — The first program: a source file is the program
  body, and its keywords are English. A scientific value has an accepted shorter
  prefix spelling. The built-in types point to the
  [Python Reference §4.1](/ref/dke/python/) for every entry. A plain call is
  written as a Python function call, and a class declaration is `class Name:`.
  A list, a tuple, a dict and a set the program builds exist only while it runs
  and are never stored.
- **rev 32** (2026-10-21) — "Facts about a pair" shows an absence over a pair, in
  a rule that finds the functions reached one way only.
- **rev 31** (2026-10-19) — Chapters 17 and 18 name the Library Tutorial and the
  Library Reference, the DKE Library's documents, at their new addresses.
- **rev 29** (2026-10-17) — The chapter on modules says that removing what a
  recompile no longer declares takes a `read-write-delete` key, and that under a
  `read-write` key the compile is refused and changes nothing.
- **rev 26** (2026-10-17) — The header states Version, Status, Audience and the
  Markdown copy, one field to a line, and the introduction follows it.
  Cross-references name the MCP Reference and the Python Reference and link to
  the section they cite. `written_by` names the store key that wrote a claim,
  and `writers` counts store keys, the name the key has in every other document.
  DKE is a deterministic reasoning engine, the words the landing uses. The links
  to the published modules name the Modules Tutorial and the Modules Reference.
- **rev 21** (2026-10-14) — This section records revisions 14 to 20 as one
  entry. Nothing else changed.
- **rev 14 to rev 20** (2026-10-13 to 2026-10-14) — Chapter 3 and Chapter 15:
  new sections and examples.
- **rev 4** (2026-10-11) — Cross-references take the published documents' short
  names, the ones the footer uses — Python Reference, Python Specification,
  MCP Reference, MCP Tutorial, Modules Tutorial. Nothing else changed.
- **rev 3** (2026-10-11) — The revision is the surface's: one number shared by
  every published document, the web pages and the service wire. This section
  says so, and the Version line moves from rev 1 to it. Nothing else changed.
- **rev 1** (2026-10-11) — The Version line states the document's revision and
  this section is added. Nothing else changed.