DKE Python — Tutorial

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:

# 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). 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):

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):

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). 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.

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 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 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:

# 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:

# 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:

# 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 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:

# 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) — 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.

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:

# 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:

# 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")

# 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:

# 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:

# 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:

That is the whole built-in vocabulary; the table in Python Reference §4.1 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:

# 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 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}).

# 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:

# 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.

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.

# 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.

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.

# 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 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.

# 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.

# 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 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.

# 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 gives the rules.

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:

# 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.

# 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:

# 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.

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.

# 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 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 lists them all, including the ones this tutorial does not reach.

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():

# 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:

# 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.

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:

# 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:

# 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 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.

# 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.

# 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:

# 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:

# 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:

# 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:

# 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:

# 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:

# 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:

# 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:

# 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.

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:

# 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:

# 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.

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:

# 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:

# 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 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.

# 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.

# 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.

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:

# 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)

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:

# 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:

# 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:

    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.

# 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.

    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:

# 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.

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):

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.

# 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):

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.

# builtins-demo.dpy — count with range, convert, round, and repeat.
def builtins_demo():
    print("range = " + str(list(range(4))) + " " + str(list(range(2, 7))) + " " + str(list(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):

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 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.

# 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):

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.

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):

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):

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):

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):

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.

# 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):

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):

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):

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.

# 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):

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.

# 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):

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). Each copies the way a list does — s.copy(), d.copy(), or dict(d).

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.

Importing

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

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:

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:

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:

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 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 and the Library Reference — starting with code, which reasons about call graphs, complexity and dependencies.