DKE Python — Language Reference

4.1 The base types

Beyond the base types there are four constructed type formers — client- built values that never round-trip the service: list<T> (an ordered sequence, §6.7), tuple<T1, …, TN> (a fixed-length heterogeneous sequence, §6.8), dict<K, V> (a mapping from a hashable key — a scalar or a tuple of hashables — to a value, kept in insertion order, §6.9), and set<T> (a collection of unique hashable elements — a scalar or a tuple of hashables — presented sorted, §6.10). A list<T> is produced by a list literal, a comprehension, s.split(...), and a list slice; the other three by their own literals (§6.8–§6.10), comprehensions (§6.11), and the collection builtins zip / enumerate (§6.12) — none by a read verb. Each shares the read surface it can support (index, .length, for … in, membership) with per-type refinements, and all render in print / +. None is one of the base types — they are type formers over them.

This table is the type vocabulary. No count of it is written anywhere — not here, not in the Tutorial, not in the Specification — because the table is the list and a restated total is a second copy that drifts. empty has a row because you write it in a match arm, and it is not one of the types: it names the absent arm of an active_claim, and the compiler refuses it as an annotation in exactly those words.

Three groupings drive the static rules:

• Primitives — string, int, bool.
• Finite collections — claim_list, string_list, subject_set, result_type_set, proof_tree (all store-derived), plus the client-built list<T>. These, together with a constructed dict (walked over its keys) and set (walked in sorted order), are the types a for … in may iterate (§7.7); every one also has a .length (§11). claim_list and proof_tree yield active_claim elements; the other three store-derived collections yield string; a list<T> yields T. A proof_tree additionally offers a .root accessor (§11.2). (A tuple is heterogeneous, so it is not a for … in iterand, §6.8.)
• Discriminators — active_claim (+ its empty case) and verify_result. Consumed by a match, alongside the value union.
• The value union — the stored content of a claim (active_claim.value), one of nine classes: int, bool, string, datetime, duration, real, null, blob, or scientific. Eight are write-producible — int, bool, string, datetime, duration, real, blob, scientific (a program writes one and reads it back at that class). The remaining class, null (an explicit absent value), is read-only: it is asserted via assert (§5.1), no value literal produces it, but a claim carrying one is discriminable on read. Consume the union with a value match (§7.8) to recover the typed content, or render it directly.
• datetime — a UTC instant written with the datetime("…Z") literal (e.g. datetime("2026-01-02T03:04:05Z"), RFC 3339 with a required Z and optional 1–9 fractional-second digits). A write verb stores it typed and it reads back as the datetime class of value; it renders as its RFC 3339 text.
• duration — a length of time written with the duration("…") literal (e.g. duration("PT1H30M"), an ISO 8601 duration PnDTnHnMnS; calendar years and months are not accepted). The lowest-order term may carry a decimal fraction of up to nine digits, so durations are exact to the nanosecond (duration("PT0.5S")); only the last term may be fractional, and a span must fit within about ±292 years. A write verb stores it typed and it reads back as the duration class of value; it renders as ISO 8601 in a canonical form with trailing fractional zeros removed, so duration("PT90M") reads back as PT1H30M and duration("PT1.500S") as PT1.5S.
• real — a fractional number written as a decimal literal 3.5, a leading-dot .5 (== 0.5), or a trailing-dot 5. (== 5.0); _ may separate digits as in 1_000.5. A lone . with no adjacent digit is the field operator, so .name is a field access, and 5.name is the real 5.0 then name (a parse error), not a field on an integer. A literal may also carry an exponent 1e5, 1.5e-3, 2E10, .5e2 (e/E, optional sign, digits — a real even without a point; 1e with no digit stays an integer 1). A write verb stores it typed and it reads back as the real class of value. It renders exactly as CPython repr(float): shortest round-trip, fixed-point for a decimal exponent in [-4, 15] (trailing zeros dropped — 3.50 → 3.5, 5.0 → 5.0), scientific (1e+20, 1.5e-08) beyond that, and -0.0 for negative zero — the same text on the wire, on write-through, and on read-back, with one exception: a cell holds zero without a sign, so a -0.0 written to a cell reads back 0.0. An exponent past the top of the finite range (1e400) is a parse error; one past the bottom (1e-400) underflows to 0.0. A case real as r: arm binds r : real. Reals compute: + - * / and the ordered comparisons accept them and promote int → real; / is always true division and always yields a real (§6.3).
• blob — an opaque byte string written as a hex literal blob("48656C6C6F") (an even count of hex digits) or a base64 literal blob_b64("SGVsbG8=") (RFC 4648; the same bytes) — two input spellings for one byte space; the empty blob("") / blob_b64("") is a valid zero-byte blob. A write verb stores it typed and it reads back as the blob class of value in a single canonical uppercase-hex form regardless of the input spelling (a value written blob_b64("SGVsbG8=") reads back 48656C6C6F); it renders as its hex text. A case blob as b: arm binds b : blob.
• scientific — a number carrying its significant figures, written with the scientific("…") factory (e.g. scientific("6.022e23")) or the short form sci"6.022e23" — a mantissa and a required exponent. A write verb stores it typed and it reads back as the scientific class of value, in a canonical form with the mantissa normalized to one leading digit and the significant figures preserved, so scientific("60.220e21") reads back 6.0220e22. The figures are part of the value: scientific("6.022e23") (four figures) and scientific("6.0220e23") (five) are the same magnitude but distinct values — the property a real cannot hold. A case scientific as s: arm binds s : scientific.

There is no absence-of-value type and no null literal. To assert that a value is known to be absent, use assert(K.s.a, src) (§5.1), which carries no value. A parameter may be annotated with any of the value-class scalars (string, int, bool, datetime, duration, real, blob, scientific), a read-result type (claim_list, active_claim, …, for calls between procedures), a collection type (list<int>, dict<string, int>, …), or a declared class (§8) — a parameter so typed takes an instance of that class. A value-class-scalar parameter supplied over the wire is passed as its canonical text (a datetime as RFC 3339 UTC, a duration as ISO 8601, a real as a decimal with a point, a blob as hex) and refuses if malformed. A class field (§8) is typed by a value-class scalar only — a field holds one stored value. Neither empty nor null is a type — both name absence; value arises only from .value field access.

4.2 Handler bindings

The except refuse as <var> / except engine_error as <var> handlers of a try (§7.9) each bind a value whose fields are all string and always present — a field with nothing to say holds "", since the language has no absent value. A refuse binds .reason, .teaching_hint, and .discriminator; an engine error binds .reason and .code. The fields are listed in §11.2. These types cannot be written as parameter types.

.reason is written for a reader and is what a program should report. The .discriminator of a refuse and the .code of an engine error play the same role for a program that must branch rather than report: each is a short tag naming which failure this is. The set of tags either can take is not part of this contract and is not enumerated here — branch on the tags you have observed and keep a fallback arm. The one exception is a refusal you raised yourself with raise <ExcType>(…) (§7.15), whose tag is the exception name your own source wrote.

.teaching_hint suggests how to correct the call, and is empty when there is no suggestion. It is an aid to a human reader — never a second reason, and never something to branch on.

5.1 Write verbs (statement position)

remember(K.s.color, "orange", "op1")     # string
remember(K.s.count, 42, "op1")           # int — reads back as int
remember(K.s.rate, "3.0", "src", datetime("2019-01-01T00:00:00Z"), datetime("2021-01-01T00:00:00Z"))  # valid 2019–2021
remember(K.s.plan, "active", "ops", datetime("2024-01-01T00:00:00Z"), null)  # valid 2024 onward, open end

update(K.s.mood, "playful", "op2")

forget(Project.dke.license, "MIT", "registry_one")

remember(Reading.probe.n, 5, "sensor")      # an int claim
forget(Reading.probe.n, "5", "sensor")      # refused - no text claim there
forget(Reading.probe.n, 5, "sensor")        # removes it

forget(Sensor.probe.reading, t"2021-06-01T00:00:00Z")   # the values in force then

forget(Sensor, recorded_before=t"2026-01-01T00:00:00Z")

forget(Sensor.probe.reading, recorded_before=t"2026-01-01T00:00:00Z")

forget(K.s.mood)      # the cell and its full history
forget(K.s)           # the whole subject; its kind is gone
forget(K.s.mood, t"2024-01-01T00:00:00Z")   # only what was true at that instant

assert(K.s.chip_id, "vet")

prefer(Sensor.r1.temp, "registry_two")

unprefer(Sensor.r1.temp)

pin(K.s.color)

unpin(K.s.color)

5.2 Read verbs (expression position)

cur = current(K.s.color)

hist = get(K.s.mood)

cav = caveats(K.s)

confs = conflicts()

vals = list_values(K.color)
then = list_values(K.color, t"2027-06-01T00:00:00Z")

hits  = subjects(K.color, "orange")     # text match
warm  = subjects(K.temp, 42)            # int match — not the text "42"
five  = subjects(K.amt, 5)              # finds a stored 5 and a stored 5.0

everyone = list_subjects(K)             # every subject of the kind
coloured = list_subjects(K.color)       # only those with a colour
then     = list_subjects(K, t"2027-06-01T00:00:00Z")

attrs = list_attributes(K)                             # the kind's attribute names
mine  = list_attributes(K.s)                           # this subject's, now
then  = list_attributes(K.s, t"2027-06-01T00:00:00Z")  # …and at that time

cats = list_categories()        # e.g. ["Loose", "shop.Widget"]

5.3 Provenance and reasoning

pt = why(K.s.color)
n  = pt.length                     # how many claims participated
r  = pt.root                       # the queried claim
first = pt[0]                       # a participating claim → active_claim
for c in pt:                        # iterate the derivation's claims
    print("via " + str(c.source))

before = why(Order.o1.review, t"2024-03-01T00:00:00Z")
after  = why(Order.o1.review, t"2024-09-01T00:00:00Z")

for c in after:
    print("now rests on " + str(c.path) + " = " + str(c.value))
for c in before:
    print("then rested on " + str(c.path) + " = " + str(c.value))

d = why_not(Device.b.online)
print(d)             # rule `device_is_online` needs Device[b].checks > 0,
                     # and nothing is recorded there
win = why_not(Device.w.online)
print(win)           # 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
n = d.length
for line in d:
    print(line)

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

v = verify(K.s.color, "orange")
if v.match:
    print("confirmed")

orange = agreement(K.s.color, "orange")   # e.g. 2

n = would_forget(Sensor.probe.reading, recorded_before=t"2026-01-01T00:00:00Z")
if n > 100:
    print("that would drop a lot of history")
else:
    forget(Sensor.probe.reading, recorded_before=t"2026-01-01T00:00:00Z")

a = agreement(K.s.color, "orange")   # 2 — two sources cited
w = writers(K.s.color, "orange")     # 1 — but one key wrote both

base = get(K.s.a)
for c in base:
    deps = dependents(c)
    for d in deps:
        print("derived cell = " + str(d.path))     # .path is the dependent's K.s.a

5.4 Reading as of a time

Six read verbs accept an optional trailing datetime (§4.1) naming the time the read is answered as of:

Omitting the argument reads the present, so a bare call and its anchored form differ only where a validity window (§5.1) is in play — a fact written without one is valid at every time, and reads the same either way.

The time may be future as well as past. A commitment written for later — a release date, a scheduled rate change, a contract that starts next quarter — is not part of the present, so nothing at the present reports it. The anchor is what reads it back, and on the three enumerations it is what finds it at all: without one, a store can hold a fact that no traversal reaches.

remember(Release.v2.ships, "2027-03-01", "roadmap",
         t"2027-01-01T00:00:00Z", t"2027-12-31T00:00:00Z")

when = t"2027-06-01T00:00:00Z"
list_subjects(Release, when)        # ["v2"]
list_attributes(Release.v2, when)   # ["ships"]
list_values(Release.ships, when)    # the claim
current(Release.v2.ships, when)     # "2027-03-01"

Two reads take no as-of time. list_attributes(K) gives the attribute names recorded for a kind, and list_categories() the kinds recorded in the store. Both describe what the store holds rather than what is true at a moment, so each already covers every time and an anchor could only narrow a complete answer. This is why list_attributes takes one in its K.s form and not in its K form — the first reads a subject’s claims, the second a kind’s vocabulary. Offering a time where none is accepted is a compile error naming the form that takes one.

5.5 Result-type introspection

rts = list_result_types()

5.6 Script-data reads (in-language)

Read-only, so they run inside a program.

names = list_scripts()

5.7 Wire-only verbs (not callable in a program)

Callable at the dke.langsyn.net wire surface but rejected in a program body — they mutate the script set or answer administrative provenance.

The in-language import <module> statement (§7.11) loads a stored module inside a program body and so is not listed here.

compile and run are the two ways to submit a source, and they differ in one respect: compile stores the compilation (the module’s defs become callable by name, its rules stand); an inline run executes it once and stores nothing — data it remembers persists, but no script is left for later instructions to call or for list scripts to report. Neither needs a def: bare top-level statements are a complete program, which is the shortest form for a one-off question (such a program takes no arguments — a def is what gives it parameters). Any number of procedures run (they may call one another; the last top-level def is the entry); a source that defines standing rules (a @rule or a computed field) cannot take effect in a run and is refused — such a source is compiled to activate its rules. Both report what the module body did — its output and its store effects — since both run it, and compile additionally states what it installed. → §9.3, MCP §4.1, §4.2

5.8 Aggregate query functions

A read-only fold over a whole attribute — one attribute across every subject of a kind — returning a value (§4.1). Bind it to a name on its own line, then use it; an aggregate may not be a bare argument to another call.

n     = count(Reading.value)          # single-attribute fold
p90   = percentile(Reading.value, 90)  # ranked fold, rank 0–100
slope_xy = slope(Point.x, Point.y)     # two-attribute fold (both attributes of one kind)
mean  = avg(Reading.value)            # bind first, then use `mean`

• Single-attribute fn(K.attr) — count, sum, product; avg, median, midpoint, mode, geomean, harmmean, rms; min, max, span, variance, stdev, iqr, mad, cv; skewness, kurtosis, entropy.
• Identity / positional fn(K.attr) — distinct (how many distinct values), argmin / argmax (which subject holds the min / max value), first / last (the earliest- / latest-recorded current value).
• Ranked percentile(K.attr, <int>) — the <int>-th percentile (rank 0–100).
• Two-attribute fn(K.x, K.y) (both attributes of one kind) — covariance, correlation, slope, intercept, rsquared.

The result’s class follows the attribute (a numeric attribute yields a number; a datetime / duration attribute a datetime / duration) — except distinct (always an int) and argmin / argmax (always a string, the subject); first / last follow the attribute. Destructure with match or use it wherever a value is expressible. Fold names are soft keywords — recognised only right before (, so they stay ordinary identifiers elsewhere. An aggregate over a attribute with no data is a refuse; a value-comparing fold (sum, avg, min, max, argmin, argmax, …) over an attribute whose values are not numbers (a text attribute, or one mixing numbers with non-numeric values) is likewise a refuse — the fold declines rather than treating a non-number as zero. The folds that don’t compare values numerically — count, mode, entropy, distinct, first, last — read how the values are distributed, or return a stored value unchanged, so a string, bool, datetime, duration or scientific attribute folds under all six without refusing on that ground. A blob value is the exception: count folds an attribute holding one, and the other five refuse over it — a blob is opaque, so there is nothing in it to group by, to tell apart, or to hand back as a result.

6.1 Comparison

== != over (string, string), numeric operands (int / real, mixed compared numerically — 1 == 1.0 is True, matching the ordered comparisons and Python; a bool or a non-numeric mismatch stays strict), (bool, bool), two discriminators (compares .kind), a value against a scalar / another value (Python-faithful — a class mismatch is false, never a coercion; §4.1), or two constructed lists of a matching element type ((list<T>, list<T>), element-wise + kind-strict — an empty list unifies with any list, differing element types are a type error; §6.7); < > <= >= over numeric operands (int or real, mixed allowed — compared numerically) or two strings — a string comparison is lexicographic by Unicode codepoint, so "apple" < "banana" and (uppercase first) "Z" < "a", matching Python; a shorter string that is a prefix orders first ("a" < "ab"). A string compared against a number is a type error. < > <= >= also order two datetimes (chronologically — the earlier instant first) or two durations (by length — the shorter first). Both compare by value, not spelling: duration("PT90M") < duration("PT1H30M") is False, and so is >, since the two are the same length; a datetime written with fractional seconds orders against one written without them by the instants they denote. A datetime compared against a duration, a number, or a string is a type error. datetime and duration also COMPUTE together: datetime + duration (either order) and datetime - duration shift an instant, datetime - datetime gives the length between two instants, and duration + duration / duration - duration add and subtract lengths. A duration also scales: duration * <number> (either order) stretches it (duration("PT1H") * 2.5 is PT2H30M) and duration / <number> splits it (duration("PT1H") / 4 is PT15M). Dividing a duration by another duration asks how many times one fits into the other and gives a plain real — duration("PT3H") / duration("PT45M") is 4.0, not a length — while % gives the length left over (duration("PT3H10M") % duration("PT45M") is PT10M). Shifts respect the calendar (datetime("2024-02-28T12:00:00Z") + duration("P1D") is 2024-02-29T12:00:00Z). Addition, subtraction, % and scaling by an int are exact to the nanosecond; scaling by a real rounds to the nearest nanosecond, halves away from zero. Subtracting a later instant from an earlier one yields a negative duration, which renders and reads back with a leading - (duration("-PT2H")). Two datetimes have no sum, duration - datetime is meaningless, duration * duration is an area rather than a time, <number> / duration is a frequency rather than a time, and //, ** are undefined over temporal values; a span past ~±292 years, an instant outside years 0001..9999, or a division or remainder by a zero-length duration, is a catchable refuse. < > <= >= also order two lists of an orderable element type or two tuples of the same type with orderable elements — element-wise lexicographic: the first unequal pair decides, and a prefix orders first ([1, 2] < [1, 2, 3], (1, 2) < (1, 3)). An orderable element is a number, a string, a datetime, a duration, or a nested list/tuple whose own elements are orderable, so the rule recurses all the way down ([[1], [2]] < [[1], [3]], [[2]] < [[10]] — element 2 < 10, not a string compare). Comparisons chain: a < b < c is (a < b) and (b < c) — each adjacent pair compared, the results conjoined.

== / != also compare two tuples of a matching tuple type (kind-strict — a differing arity or position type is a type error; equal tuples agree position by position, §6.8) and two sets of a matching element type (element-wise and order-independent — two sets are equal when they hold the same elements, §6.10). Two dicts of a matching key and value type also compare with == / !=, order-independent — equal when they hold the same key→value mapping regardless of insertion order (kind-strict, and an empty dict unifies with any dict so {} == {"a": 1} is False rather than a type error, §6.9).

6.1a Membership

in / not in over (string, string) → bool — substring containment: sub in s is True when sub occurs anywhere in s (the empty string is in every string) — or element containment: x in xs over a constructed list<T> (§6.7), x in s over a set<T> (§6.10), k in d over a dict<K, V> (testing its keys, §6.9), and x in t over a homogeneous tuple, each True when the collection holds a matching element (the item’s type must match the element / key type). Membership does not test a store-derived collection — to iterate one, use the for <var> in <collection>: statement (§7), whose in is the loop keyword, not this operator.

if "@" in address:      ...
if 4 in [3, 1, 4]:      ...
if "red" in tags:       ...   # set membership
if "ana" in ages:       ...   # dict key membership

6.2 Logical

and, or, not over any value — every value has a truth value (truthiness): False / 0 / 0.0 / "" / empty collections / None are falsy, everything else truthy. and / or are short-circuit and operand-return — a and b is a when a is falsy else b; a or b is a when a is truthy else b — so name or "anon" returns the string. Their result type joins the operands (identical → that type; int/real → real; two different value scalars → value); a non-unifiable pair is a type_error. not always yields a bool. not binds looser than comparison, so not a == b is not (a == b).

6.2a Conditional expression (ternary)

a if c else b yields a when c is truthy (any value), else b. The two branches must share a type (numeric promotion int/real → real), which is the result type. Evaluation is short-circuit — only the selected branch runs, so an untaken branch that would refuse is never reached (safe if d == 0 else 1 / d). It binds lower than every operator and is right-associative.

grade = "pass" if score >= 60 else "fail"

6.3 Arithmetic

+ - * / // % ** over numeric operands (int or real); prefix - negates an int. The numeric operators promote: int × int stays int, and any real operand yields a real. One exception and one detail: - / is true division — it always yields a real, so int / int promotes (7 / 2 is 3.5, 8 / 2 is 4.0). The floored integer quotient is // (7 // 2 is 3, -7 // 2 is -4 — floor rounds toward −∞). - % and // are the floor pair — both take the sign of the divisor (-7 % 2 is 1, -7.5 % 2 is 0.5), so a == (a // b) * b + (a % b) holds at either operand class. A remainder of zero takes the divisor’s sign too, which only a real can show: 6.0 % -2 is -0.0.

** is power, right-associative, binding tighter than the prefix - (-2 ** 2 is -4, 2 ** 3 ** 2 is 512): int ** non-negative int is an int (2 ** 10 is 1024); a real operand yields a real; an int base with a negative exponent refuses with a teaching hint — write the base as a real (2.0 ** -1 is 0.5). Reals compute to IEEE-754-double precision and render in canonical decimal form. Division / modulo by zero, integer overflow, and out-of-range real results refuse at runtime. Two ** shapes refuse for reasons that are not overflow: a zero base under a negative exponent (0 ** -1) is a division by zero and says so, and a negative base under a fractional exponent ((-8) ** 0.5) is a complex number, which this language has no type for — the one case where ** declines what Python computes. A negative base under an integral exponent ((-8.0) ** 3.0 is -512.0) and a zero base under a non-negative one (0 ** 0 is 1) are ordinary.

* also does sequence repetition: a string or a constructed list repeated by an int (either order) — "ab" * 3 is "ababab", "-" * 20 a rule, [0] * 4 is [0, 0, 0, 0], [1, 2] * 3 is [1, 2, 1, 2, 1, 2]. A non-positive count yields the empty sequence ("x" * 0 is ""); the count must be an int.

abs(x) — the built-in absolute value: abs(-5) is 5, abs(-3.5) is 3.5; it keeps the argument’s numeric type and takes exactly one number (a non-number, or a different argument count, is a type error).

round(x[, n]) — half-to-even (“banker’s”) rounding: round(0.5) and round(2.5) are 0 and 2, round(0.125, 2) is 0.12. The optional digit count n is an int (negatives allowed: round(35, -1) is 40). Result type: round(int, …) → int; round(real) (no n) → int; round(real, n) → real (a real even at n = 0, so round(2.5, 0) is 2.0). Rounding follows the stored double, so round(2.675, 2) is 2.67 (matching CPython).

sum(iterable) / min(…) / max(…) — reduce an in-memory iterable, distinct from the same-named store-aggregate folds sum(K.col) / … (the argument shape selects: a bare K.col path → fold; anything else → this reduce). sum adds numeric elements (all-int → int, empty → 0, any real → real). min/max take one iterable or two-plus scalar values → the extreme by numeric or lexicographic (string) order; elements/values must share an orderable type (numeric, string, or a nested list/tuple of those — the comparison recurses). min/ max of a runtime-empty iterable is a catchable refuse (ValueError), unless a keyword-only default=<value> is supplied — min([], default=0) is 0 — which is returned only when the iterable is empty and whose type must match the element type (min(<iterable>, default=…); default= is invalid with multiple positional values). The higher-order key= argument is not provided (DKE Python has no first-class functions to pass).

divmod(a, b) — the floored quotient and the remainder as one pair, equal to (a // b, a % b): divmod(7, 2) is (3, 1) and divmod(-7, 2) is (-4, 1) (the quotient floors toward negative infinity, the remainder takes the divisor’s sign, and q * b + r == a always holds). Both operands must be numeric, and the pair promotes together — tuple<int, int> for two ints, tuple<real, real> when either is real, never a mixed pair: divmod(7.5, 2) is (3.0, 1.5). A zero divisor, and the most-negative int over -1, are catchable refuses.

reversed(xs) — a new list<T> holding the elements in the reverse of the order the iterable yields them, so a dict contributes its keys and a set its sorted elements, backwards. The result is an ordinary list, not a lazy iterator (reversed("abc") is ['c', 'b', 'a']) — the same eager convention as zip/enumerate.

sorted(xs[, reverse=<bool>]) / any(xs) / all(xs) — sorted returns a new list<T> in ascending order (descending with reverse=True; a stable sort, reverse= keyword-only, no key=); elements must be orderable — numeric, string, datetime, duration, or a nested list/tuple of those (the sort recurses lexicographically, so sorted([[10], [2], [1, 3]]) is [[1, 3], [2], [10]]). any/all fold truthiness (§6.2) to a bool — any([]) is False, all([]) is True.

format(value, spec) / repr(value) — format renders a value per the Python format mini-language (format(3.14159, ".2f") → "3.14", format(42, "05") → "00042", format(255, "x") → "ff"): [[fill]align][0][width] [.precision][type], type ∈ s d f x X o b; a sign flag / # / grouping / the e/g/% types are a catchable refuse. repr(x) gives the repr text (a string keeps its quotes). Both power f-string {v:spec} / {v!r} (§6.4a).

ord(s) / chr(i) — the Unicode codepoint round-trip. ord(s) returns the integer codepoint of a one-character string (ord("A") is 65, ord("æ") is 230); a string of any other length is a catchable refuse. chr(i) returns the one-character string for a codepoint i in range(0x110000) (chr(97) is "a", chr(937) is "Ω"); an i outside that range — or a lone surrogate (U+D800..U+DFFF), which has no UTF-8 encoding — is a catchable refuse.

Type conversions. str(x) renders any value to text (total, the +/print rendering); int(x) and float(x) convert a string / int / real / bool to an int / real. int(3.9) truncates toward zero (3), int(" -7 ") is -7; a string that is not a valid number (int("abc"), int("3.5")) or an out-of-range value is a catchable refuse (Python ValueError). int(s, base) parses a string in an explicit radix: base is 2..36 (or 0 to auto-detect from a 0x/0o/0b prefix), a 0x/0o/0b prefix is accepted when it matches base, an optional leading sign and _ digit separators are allowed, and a digit outside the base, an out-of-range base, or a base-0 decimal with a leading zero refuses (int("ff", 16) is 255, int("0b101", 2) is 5, int("z", 36) is 35). An explicit base with a non-string value is a type error, as in Python. Collection conversions: list(x) collects a finite collection’s elements (a string yields its characters, a homogeneous tuple its elements — list((1,2,3)) → [1, 2, 3]) into a list; set(x) collects them into a deduped, sorted set (elements must be hashable — a scalar or a tuple of hashables); dict(x) builds a dict<K, V> from a list<tuple<K, V>> of pairs — dict(zip(keys, vals)); tuple(x) collects the elements into a variadic homogeneous tuple tuple<T, ...> (runtime length, indexed by a runtime int, not unpackable). bool(x) returns the truthiness (§6.2) of any value as a bool (bool([]) → False, bool("x") → True).

6.4 Concatenation

+ joins two strings into a new string. A string + a non-string operand is a type error (as in Python, which raises TypeError) — convert the non-string side with str(…) ("count = " + str(xs.length)); there is no implicit string coercion. An f-string applies str(…) to each field for you (§6.4a). With two list operands + concatenates into a new immutable list — the way to combine two, since lists have no append: [1, 2] + [3, 4] is [1, 2, 3, 4]. The result element type follows the list-literal rule (§6.7): same type → list<T>, differing scalars → list<value> ([1] + [3.5]), an empty operand takes the other side ([] + [1]); a non-scalar mismatch is a type error. A list plus a non-list, non-string operand is a type error.

With two tuple operands + concatenates into a new immutable tuple: (1, 2) + (3,) is (1, 2, 3). A tuple is heterogeneous, so the result keeps each operand’s positions and their types rather than settling on one element type — tuple<int, string> + tuple<bool> is tuple<int, string, bool>, and a constant index into the result reads the position it names (after t = (1, "a") + (5,), t[2] is an int). The empty tuple takes the other side (() + (1,)). A tuple plus a non-tuple operand is a type error. When one side is a tuple whose length is only known at run time, the result is too, so it needs a single element type covering both sides — the same unification list concatenation uses, and element types that do not unify are a type error.

print("count = " + str(xs.length))
print("items = " + str(xs))
combined = xs + [99]              # concatenate two lists
pair = (1, "a") + (True,)         # concatenate two tuples

Adjacent literals — two or more string literals separated only by whitespace are joined at compile time, with no +, so a long constant can span lines without a run-time concatenation: "one " "two" is "one two" and "a" "b" "c" is "abc". An f-string joins the run too, in either order and any mixture (f"a" "b", "a" f"{x}", f"{x}" f"{y}"), which is the idiomatic way to write a long interpolated message across lines — and the whole run is one interpolated string, costing what the single f-string it replaces costs. A typed-value literal (t"…", d"…", x"…") does not join: concatenation is for strings. Render one with str(…) and use +, or interpolate it.

Triple-quoted literals — a string delimited by """ runs until the next """, so it may span multiple lines (each newline is a literal \n) and hold lone "/"" characters without escaping: """line one … line two""". The escapes are the same as a single-quoted string and the value is an ordinary string. A triple-quoted f-string (f"""…""") is not yet supported.

Escapes — a backslash inside a string begins an escape, and the set is closed: \\ a backslash, \" a double quote, \n line feed, \t tab, \r carriage return, \a bell, \b backspace, \f form feed, \v vertical tab. Three take hex digits and are written into the value as UTF-8: \xNN is one byte from exactly two digits, \uNNNN a codepoint up to U+FFFF, and \UNNNNNNNN a codepoint up to U+10FFFF — the only escape that reaches above the BMP. Anything else after a backslash is a parse error rather than a literal backslash, so a Windows path is written "C:\\tmp". Two values are refused rather than encoded: a surrogate (U+D800..U+DFFF, written either way), and any escape that would produce a NUL — \0, \x00 and \u0000 alike — so a string never carries an interior NUL.

Named-character escape — \N{name} is the codepoint with that Unicode character name, matched case-insensitively, across every script: "\N{BULLET}" is "•", "\N{GREEK SMALL LETTER ALPHA}" is "α", and "\N{CJK UNIFIED IDEOGRAPH-4E00}" is "一". A name Unicode does not assign is a parse error.

6.4a Formatted strings (f-strings)

An f-string — a string literal with an f (or F) prefix — writes a value into text directly: each { … } field holds an expression that is evaluated and written in place. f"a{x}b" has the same value as "a" + str(x) + "b", so a field is rendered the way + renders that value (§6.4) and an f-string is always a string (even a lone field: f"{n}" is "42", not the int 42). A field holds any expression — a bound variable, arithmetic, a method call, an index or slice; a store read is bound to a name first (§7.2), as with +. Write {{ or }} for a literal brace. A field may carry a conversion and/or a format spec: {x!r} uses repr(x), {x!s} uses str(x); {x:spec} applies the format mini-language — f"{x:.2f}", f"{n:>5}", f"{s:*^8}" — and they combine ({x!r:>10}). A field may end in a self-documenting =: f"{x=}" writes the field’s source text up to the = (whitespace preserved) followed by the value, defaulting to repr — f"{x=}" is "x=5", f"{ x = }" is " x = 5", f"{s=}" is "s='hi'" — and a :spec/!conv overrides that default (f"{x=:.2f}" is "x=5.00"). A trailing ==/>=/<=/!= is a comparison, not the debug =. Not yet: !a, a dynamic spec ({x:{w}}), or a string literal inside a field (each a compile/runtime error).

print(f"count = {xs.length}")
name = "Merlin"
print(f"hi {name}, first char {name[0]}, upper {name.upper()}")

6.5 Field access, indexing, and slicing

x.field (see §11) composes on any computed value — a method result, an index, or a slice — not only a bare name (text.upper().length, xs[0].value, hist[-1].source); a store read is still bound to a name first (§7.2). The builtin len(x) is an alias for x.length (a string’s character count or a collection’s element count). xs[i] (zero-based; index is int; out-of-range refuses). A string may also be indexed to read a single character (s[i] → a one-character string; a negative index counts from the end, so s[-1] is the last character) and sliced for a substring — s[a:b], with either bound optional (s[a:], s[:b], s[:]) and negative bounds counting from the end (s[-3:], s[:-1]), plus an optional step s[a:b:step] (a negative step reverses, so s[::-1] is s reversed and s[::2] is every other character). Slicing is total: it never refuses; bounds are clamped and an inverted range yields "" — the sole exception is a step of 0, a catchable refuse. A constructed list<T> indexes and slices by the same rules (xs[i], negative from-end permitted; xs[a:b:c] yields a new list<T>); from-end (negative) positions apply to a string and a constructed list, while a store-derived collection index is non-negative. Positions count characters (a string) or elements (a list). A tuple slices too — t[a:b] yields a tuple — but its bounds must be constant integers (a tuple is heterogeneous); list(t[a:b]) converts the result to a list.

6.6 String methods

A string carries these built-in methods (all character-counting, all total except split, the justify family, and index/rindex, noted below): - s.find(sub[, start[, end]]) → int / s.rfind(...) → int — the first / last position of sub, or -1; the optional start[, end] window searches s[start:end] and the index is into the whole s (B8). - s.index(sub[, start[, end]]) → int / s.rindex(...) → int — like find / rfind, but a missing sub refuses (catchable, §10) instead of returning -1. - s.count(sub[, start[, end]]) → int — the number of non-overlapping occurrences of sub in the window (an empty sub yields the window’s length + 1). - s.startswith(prefix[, start[, end]]) → bool / s.endswith(suffix[, ...]) → bool — whether the window of s begins / ends with the argument (an empty argument yields True). The argument may instead be a tuple of strings — True if the window matches any of them (an empty tuple yields False). - s.replace(old, new[, count]) → string — a copy of s with each non-overlapping occurrence of old replaced by new, at most count times when given (an empty old inserts new in every gap, as in CPython: "abc".replace("", "-") → -a-b-c-). - s.upper() → string / s.lower() → string — the full Unicode case mapping. A character may expand to more than one ("straße".upper() is "STRASSE", "file".upper() is "FILE", "İ".lower() is "i̇"), so a case transform can change the length (which .length reflects). lower() also applies the Greek word-final rule ("ΟΔΟΣ".lower() is "οδος", final ς). - s.capitalize() → string — first character titlecased, the rest lowercased. - s.title() → string — the first character of each word titlecased, the rest lowercased (a word is a run of cased characters; any non-letter, including an apostrophe, starts a new word — so "they're".title() is "They'Re"). - s.swapcase() → string — each uppercase character lowercased and vice versa. (These four case transforms use the full Unicode mapping above, including the Greek word-final rule where they lowercase.) - s.casefold() → string — aggressive, context-free folding for caseless matching: like lower but more so ("STRAßE".casefold() is "strasse", "fi" folds to "fi"), and it does not apply the Greek word-final rule, so "ΟΔΟΣ".casefold() is "οδοσ" (a medial σ, unlike .lower()’s "οδος"). Use a.casefold() == b.casefold() for caseless equality. - s.zfill(width) → string — left-pad with '0' to width characters, keeping a leading +/- sign first; width ≤ s.length is a no-op. - s.ljust(width[, fill]) / s.rjust(width[, fill]) / s.center(width[, fill]) → string — justify s in a field of width characters, padding right / left / both with fill (a single character, default space). width ≤ s.length is a no-op; a fill that is not exactly one character refuses (catchable). - s.strip([chars]) / s.lstrip([chars]) / s.rstrip([chars]) → string — s with characters removed from both ends / the left / the right. With no argument they remove whitespace; with a chars argument they remove any character that occurs in the chars set. - s.removeprefix(prefix) / s.removesuffix(suffix) → string — s with a leading prefix / trailing suffix removed if present, else s unchanged (an empty suffix is a no-op). - s.expandtabs([tabsize]) → string — each tab replaced by spaces to the next tab stop (multiple of tabsize, default 8); the column counts characters and resets after \n/\r. tabsize ≤ 0 removes tabs. - s.split([sep[, maxsplit]]) → list<string> — the substrings of s split at each occurrence of sep (empty pieces kept); an optional maxsplit caps the splits (≤ maxsplit + 1 pieces, B8). With no argument, s splits on runs of whitespace, dropping empty pieces. An explicit empty separator is a catchable refuse (§10). - s.rsplit([sep[, maxsplit]]) → list<string> — like split, but a bounded maxsplit takes its splits from the right ("a,b,c".rsplit(",", 1) is ['a,b', 'c']); with no maxsplit the result equals split. - sep.join(xs) → string — the list<string> xs concatenated with sep between adjacent elements (an empty list yields ""). A list of any other element type is a type error. - s.partition(sep) / s.rpartition(sep) → tuple<string, string, string> — split s once at the first / last occurrence of sep into (before, sep, after); when sep is absent, partition yields (s, "", "") and rpartition yields ("", "", s). An explicit empty separator is a catchable refuse (§10). - s.splitlines() → list<string> — the lines of s, split at \n / \r\n / \r, with the trailing-newline empty line dropped ("" yields []). - The character-class predicates — each () → bool, testing every character of s against its Unicode class: s.isspace(), s.isdigit(), s.isdecimal(), s.isnumeric(), s.isalpha(), s.isalnum(), s.isupper(), s.islower(), s.istitle(), s.isascii(). All but isascii are False on the empty string (the whole-string rule is “non-empty and all characters match”); "".isascii() is True. isupper/islower require at least one cased character and no character of the opposite case; istitle tests the titlecase pattern. They classify by full Unicode, so "blåbær".islower() and "ÆØÅ".isalpha() are True.

domain = email.strip()[email.find("@") + 1:]
label  = raw.replace("_", " ").upper()
paid   = invoice.endswith("PAID")
tidy   = title.strip("*_ ")
parts  = "a,b,c".split(",")          # ['a', 'b', 'c']
line   = " ".join(["a", "b", "c"])   # "a b c"
addr   = "user@host".partition("@")  # ('user', '@', 'host')
rows   = "one\ntwo".splitlines()     # ['one', 'two']
digits = code.isdigit()              # True if code is all digits
at     = path.index("/")             # position of "/", or refuses if absent

6.7 Constructed lists and comprehensions

A list literal [e1, e2, …] builds a constructed list<T> on the client side (immutable, bounded, never round-trips the service). Elements are inferred to a common type: homogeneous → list<T>, mixed scalars → list<value>, empty [] → list<unknown>; lists nest. The empty list is compatible with any list<T> — wherever two list types must agree it takes the concrete side’s type: [1, 2] if c else [], a re-binding (xs = [] then xs = [1]), a nested sibling ([[1, 2], []] is list<list<int>>), ",".join([]), and [] == xs. A constructed list is indexed, sliced, measured (.length), iterated (for … in), tested for membership (x in xs), searched (xs.index(v[, start[, end]]) → the first index of v, within an optional codepoint window and refusing if absent; xs.count(v) → how many times v occurs), and compared (== / !=); it renders in print and +.

A comprehension [expr for x in xs if cond] builds a new list by bounded iteration: it binds each element of the finite source xs to x, keeps those the optional cond (truth-tested) admits, and collects expr. The loop variable is comprehension-local (it may shadow an outer name and does not leak). Multiple for clauses form the flat cartesian product ([a + b for a in xs for b in ys]) — the first clause is the outermost loop, and a later clause’s source may reference earlier loop variables ([y for row in grid for y in row]); a clause may carry several if filters (applied conjunctively). A comprehension whose result is itself a comprehension also nests.

nums    = [3, 1, 4, 1, 5]
evens   = [n for n in nums if n % 2 == 0]     # [4]
caps    = [w.upper() for w in "a,b".split(",")]  # ['A', 'B']
grid    = [[x for x in nums] for r in caps]   # list<list<int>>
pairs   = [a + b for a in [1, 2] for b in [10, 20]]  # [11, 21, 12, 22]
flat    = [y for row in [[1, 2], [3, 4]] for y in row]  # [1, 2, 3, 4]

6.8 Tuples

A tuple literal (e1, e2, …) builds a constructed tuple<T1, …, TN> on the client side — a fixed-length, heterogeneous sequence in which each position keeps its own type (immutable, bounded, never round-trips the service). A comma makes the tuple: (e) is a grouped expression, (e,) a one-element tuple, (a, b) a two-element tuple, () the empty tuple; tuples nest (((1, 2), 3) is a tuple<tuple<int, int>, int>). A tuple is indexed by a compile-time constant integer — t[0] has the type of the first position, t[-1] the last; a non-constant or out-of-range index is a compile-time error (every position stays reachable by a literal index). It is measured with .length and compared with == / != (kind-strict — two tuples compare only when they share a tuple type; a differing arity or position type is a type error). Unlike a list, a tuple is not written after for … in (its positions have no single element type). It renders in print and + as (e1, e2, …), a one-element tuple as (e,). Two tuples concatenate with + (§6.4), the result keeping every position’s own type.

point = (3, 4)             # tuple<int, int>
x     = point[0]           # 3      — constant index
mixed = (1, "ana", True)   # tuple<int, string, bool>
same  = (3, 4) == point    # True
wide  = point + (5,)       # tuple<int, int, int>

6.9 Dicts

A dict literal {k1: v1, k2: v2} builds a constructed dict<K, V> on the client side — a mapping from hashable keys (a scalar or a tuple of hashables) to values, kept in insertion order (immutable, bounded, never round-trips the service). Keys are homogeneous and drawn from a scalar value class (string / int / bool / datetime / duration / real / blob); values are homogeneous too (a mix of scalar value classes gives a value-typed value part). The empty dict is {}. When a key is written twice the entry keeps its first position but takes the last value ({"x": 1, "x": 9} is {'x': 9}). A dict is: - read by key — d[k] returns V; the key’s type must match K, and a key absent at run time is a catchable refuse (§10), never a silent default; - tested — k in d / k not in d over its keys (§6.1a); - measured — .length, its entry count; - walked — for k in d: binds each key in insertion order (§7.7); - projected — d.keys() → list<K>, d.values() → list<V>, and d.items() → list<tuple<K, V>>, each in insertion order; - read defensively — d.get(key, default) returns the value for key, or default when the key is absent. A default is required (there is no None for a 1-argument form); the result type is the join of V and the default’s type.

It renders in print and + as {k1: v1, k2: v2} in insertion order. Two dicts compare with == / != order-independently — equal when they hold the same key→value mapping regardless of insertion order ({"a": 1, "b": 2} == {"b": 2, "a": 1} is True); it is kind-strict, and an empty dict unifies with any dict.

ages = {"ana": 30, "bo": 25}
ages["ana"]                   # 30
"bo" in ages                  # True
names = ages.keys()           # ['ana', 'bo']
pairs = ages.items()          # [('ana', 30), ('bo', 25)]

6.10 Sets

A set literal {a, b, c} (no colons) builds a constructed set<T> on the client side — a collection of unique hashable-scalar elements (immutable, bounded, never round-trips the service). A { … } with a colon is a dict (§6.9), so — because the empty braces {} are the empty dict — the empty set has no literal (an emptied set produced by an operation renders set()). Elements are homogeneous (a mix of scalar value classes gives a set<value>); duplicates are removed at construction. A set renders and is walked (for x in s:) in a deterministic sorted order — a defined refinement of Python, whose set order is unspecified. A set is: - tested — x in s / x not in s (§6.1a); - measured — .length; - combined — s.union(t), s.intersection(t), s.difference(t), and s.symmetric_difference(t), each taking a set of a matching element type and returning a new sorted set<T>; - compared — == / !=, element-wise and order-independent (two sets of a matching element type are equal when they hold the same elements).

It renders in print and + as {e1, e2, …} in sorted order.

tags   = {"red", "green", "red", "blue"}   # {'blue', 'green', 'red'}  (unique, sorted)
"red" in tags                              # True
warm   = {"red", "orange"}
shared = tags.intersection(warm)           # {'red'}
both   = tags.union(warm)                  # {'blue', 'green', 'orange', 'red'}

6.11 Dict and set comprehensions

Alongside the list comprehension (§6.7), a set comprehension {expr for x in xs if cond} builds a new set<T> — deduping and sorting, with expr hashable (a scalar or a tuple of hashables) — and a dict comprehension {key: value for x in xs if cond} builds a new dict<K, V> in insertion order, last value winning on a repeated key and key a hashable scalar. Both iterate a finite source, bind each element to the comprehension-local x, keep those the optional cond admits, and collect the result — the same bounded iteration as a list comprehension, so both terminate and evaluate entirely on the client side. A brace form with a : in its head is a dict comprehension; without one, a set comprehension.

squares = {n: n * n for n in [1, 2, 3]}    # {1: 1, 2: 4, 3: 9}
parity  = {n % 2 for n in [1, 2, 3, 4]}     # {0, 1}   (deduped, sorted)

6.12 zip and enumerate

Two builtin functions pair finite collections into tuples, each returning an ordinary list that composes with every list read: - zip(a, b, …) → list<tuple<…>> — pairs elements position by position, up to the shortest input (zip(["a", "b"], [1, 2, 3]) yields two tuples). - enumerate(xs [, start]) → list<tuple<int, T>> — numbers each element, from 0 by default or from an optional int start (positional or the start= keyword; may be negative).

Each argument is any finite collection (a dict contributes its keys, a set its sorted elements).

zip(["ana", "bo"], [90, 85])   # [('ana', 90), ('bo', 85)]
enumerate(["ana", "bo"])       # [(0, 'ana'), (1, 'bo')]
enumerate(["ana", "bo"], 1)    # [(1, 'ana'), (2, 'bo')]
for name, score in zip(names, scores):   # tuple unpacking (§7.7)
    print(name + " scored " + str(score))

7.1 Declaration

def audit(K: string, s: string):
    <suite>
def doubled(n: int) -> int:          # value script: returns an int
    return n * 2

The def keyword, name, typed parameters (name: type), an optional -> type return type, :, indented body. A type is a scalar / read-result type (§5.5) or a parameterized collection — list<T>, set<T>, dict<K, V>, tuple<T, ...>, nestable (dict<string, list<int>>) — so a collection crosses a function boundary as an argument or return value (def total(xs: list<int>) -> int:, def doubled(xs: list<int>) -> list<int>:). A parameter may carry a default (def f(x: int, y: int = 1)) — a constant expression whose type matches the parameter; a defaulted parameter may not precede a required one. Two declarations in a unit must not share a name; a unit compiles its declarations in order and a call may target only an earlier one (compile-before-call).

A final parameter may be variadic — written *name: T — collecting the surplus positional arguments into a tuple<T, ...> (possibly empty): def total(label: string, *nums: int) -> int: accepts total("a", 1, 2, 3) with nums = (1, 2, 3). A variadic must be last, there may be at most one, its element type is required, it takes no default, and it cannot be passed by keyword; inside the body it is an ordinary tuple (nums[0], len(nums), for n in nums, sum(nums)). There is no **kwargs — use explicit named parameters or a dict parameter.

A script with no -> type is a void script (no value); one written def name(...) -> type: is a value script — it produces a value of type and MUST return a value on every path (§7.12). Only a value script may be called as an expression (§7.4).

7.2 Assignment (bind a read)

hist = get(K.s.color)

Bare assignment — there is no let introducer. The right side must not be a statement-only verb (no value). Augmented assignment x += e (and -= *= /= %= //= **=) is accepted on a bare name; x <op>= e is equivalent to x = x <op> e. It does not apply to a field (obj.field += e is rejected): a field is a provenance-carrying claim, not a mutable cell, and a compound assignment names no source — update a field by reading it, then writing the new value back with remember(obj.field, <new value>, <source>). An annotated assignment x: <type> = <expr> gives the binding its type explicitly (n: int = 5, xs: list<int> = [1, 2, 3]); the annotation must agree with the initializer, and a bare x: <type> with no value is rejected (write x: <type> = <value>). Chained assignment a = b = <expr> binds every target to one value (evaluated once). Tuple unpacking a, b = <tuple> destructures a tuple into named targets — the right side must be a tuple of exactly the target count, written parenthesized ((1, 2)) or as a bare comma-list (b, a); the whole right side is evaluated before any target binds, so a, b = b, a swaps (§7.7). A target may itself be a parenthesized target list, so nested unpacking (a, b), c = ((1, 2), 3) (or a, (b, c) = …) destructures a tuple of tuples, each level arity-checked independently. One target may be starred (a, *rest = (1, 2, 3) → rest = [2, 3], always a list): it absorbs the surplus elements (which must share one type), the RHS needing at least the fixed-target count.

7.3 print

print(<expr>)

Appends <expr>’s rendering to the transcript, written as a call — print("temp=" + str(t.value)). The argument is string, int, bool, a value, a constructed collection, or a discriminator; a store-derived finite collection is not rendered directly (build a string with +). A constructed list<T> renders [e1, e2, …]; a tuple renders (e1, e2, …); a dict renders {k1: v1, k2: v2} in insertion order; a set renders {e1, e2, …} in sorted order (an empty set, set()) — each element rendered recursively.

7.4 Script call (invocation)

audit_subject(K, s)                  # statement: run for effects, discard any value
total = summed(a, b)                 # value-call: bind what a value script returns

A plain call of a stored script — there is no call keyword (a script is called like any function). Static, compile-time inline expansion; no recursion, no cycles. Arguments bind by position, or by keyword (greet("World", greeting="Hi")); a keyword may not precede a positional argument, and an omitted argument uses the parameter’s default (§7.1).

A value script (§7.1) may be called in expression position — its call yields what the script returns, and composes anywhere an expression may: y = f(x), return f(x), print(f(x)), f(a) + g(b), or nested f(g(x)) (evaluated inner-first, left-to-right). A void script called as a value is a type_error — call it as a statement instead.

7.5 Verb-call statement

A write verb (§5.1) in statement position:

remember(K.s.color, "orange", "op1")

7.6 if

if <cond>:
    <suite>
elif <cond>:
    <suite>
else:
    <suite>

<cond> may be any value — it is tested for truthiness (§6.2), so if xs: / if s: / if n: branch on non-empty / non-zero as in Python; each elif and the else are optional. An elif is equivalent to an else: containing a nested if.

7.7 for … in

for c in hist:
    <suite>

Iterates a finite collection — a store-derived collection, a constructed list<T> (§6.7), a dict (binding each key in insertion order, §6.9), or a set (in sorted order, §6.10) — or a string, binding each character (a one-character string, by Unicode character); a tuple and any other iterand is a type_error. The collection is snapshotted at entry. A comprehension (§6.7, §6.11) is the same bounded iteration in expression position. Bounded iteration is what gives DKE Python its termination guarantee.

A target list unpacks each element (a tuple) into named variables — for i, x in enumerate(xs):, for a, b in zip(xs, ys):, for k, v in d.items(): — each element must be a tuple of the target arity. The targets are loop-body-scoped, like the single loop variable.

Inside a for body, break stops the loop and continue skips to the next element (each resolves to the innermost enclosing loop; both may sit inside a nested if/match/try). Either outside a loop is a compile-time error, and a break/continue must be inside a loop in its own def, not merely called from one. Both only shorten the (bounded) iteration, so termination still holds.

for c in claims:
    if c.value == "":
        continue                     # skip blanks
    if c.value == stop:
        break                        # stop at a sentinel
    print(c.value)

A for may end with an else: clause: it runs once after the loop completes, but not if a break left the loop. An empty collection (zero iterations) still runs it. The else runs after the loop, so the loop variable is out of scope there.

for c in hist:
    print(c.value)
else:
    print("no more history")           # runs unless a break fired above

7.8 match (discriminator dispatch)

match cur:
    case active_claim:
        print("value = " + str(cur.value))
    case empty:
        print("absent")

The scrutinee must be a discriminator (active_claim, verify_result). Arms exhaustively cover the discriminator’s cases. Python uses case where the base member uses when.

(A match whose scrutinee is a bare instance variable is the distinct class match, §8.6.)

A match whose scrutinee is a value (a claim’s .value, §4.1) is a value match: the case labels are the nine value-classes int, bool, string, datetime, duration, real, null, blob, and scientific. The eight write-producible classes (int, bool, string, datetime, duration, real, blob, scientific) may bind the typed content with a named as <var> arm; the one read-only class, null, is a bare arm only — attaching as <var> to it is a type_error:

match cur.value:
    case int as n:      print("next = " + str((n + 1)))     # n : int
    case string as s:   print("text = " + str(s))
    case duration as u: print("span = " + str(u))           # u : duration
    case real as r:     print("value = " + str(r))          # r : real — renders decimal
    case blob as b:     print("bytes = " + str(b))          # b : blob — renders hex
    case null:          print("an absent value")       # bare — no `as`
    case default:       print("other class")

Arms cover all eight classes or provide case default:; a bound as <var> is typed at the arm’s class and scoped to that arm.

An ordinary assignment inside an arm is not arm-scoped, and the contrast is worth stating because one match has both rules in it. The as <var> binding exists only inside its arm; a name you assign in an arm belongs to the enclosing scope and is readable after the match, which is how a match computes a value for the code below it. Reading the arm binding after the match is an undeclared-identifier type_error; reading the assigned name is ordinary.

label = "none"
match cur.value:
    case int as n:  label = "int " + str(n)   # `n` lives only here
    case default:   label = "other"
print("after: " + label)                       # `label` is readable; `n` is not

7.9 try

try:
    <suite>
except refuse as r:
    <suite>
except engine_error as e:
    <suite>
else:
    <suite>            # runs only if the body raised nothing
finally:
    <suite>            # always runs, last

Python’s own except … [as …]: shape. Both handlers are optional, and so is each handler’s as <var> binding — except refuse: catches without naming the exception (omit as when the body does not use the refuse/engine_error info). A refused statement does not bind and transfers control to except refuse; an engine error to except engine_error. With no matching handler, the outcome propagates. An optional else (allowed only alongside an except) runs when the body raised nothing; a refuse in the else is not caught here. An optional finally runs on every exit path — clean, caught, propagating, or a break/continue leaving the block — and runs last; if the finally itself raises or breaks, that supersedes. A try needs at least one except or a finally.

try:
    remember(Reading.probe.taken_at, "not a timestamp", "sensor")
except refuse as r:
    print(r.reason)
    if r.teaching_hint != "":
        print(r.teaching_hint)              # empty when there is no suggestion
except engine_error as e:
    print(e.reason)

Report .reason; add .teaching_hint when it is non-empty, since it says how to correct the call. Branch on .discriminator (or an engine error’s .code) only where the program must act differently — see §4.2.

7.10 branch / commit / rollback

with branch("experiment"):
    remember(K.s.color, "tigret", "audit")
    if ok:
        commit
    else:
        rollback

A with branch("<name>"): block groups writes transactionally: clean exit commits; an uncaught refuse / engine error rolls back. Bare commit / rollback end the branch explicitly — the branch is over at that statement, so a write in the block’s remaining lines is an ordinary, immediately durable one. Ordinary invocation is not transactional.

7.11 import (module)

import catalog                       # in a program body: load a stored module

A DKE Python file is a module (see the Modules contract); import <module> loads one: it runs the module’s body once and makes its names available under the module’s namespace. import is a contextual keyword — the import statement only at statement head, an ordinary identifier elsewhere. A module may import another module; an import cycle is rejected when the module loads. Loading a module already loaded reconciles it: only the cells whose values changed are rewritten, so re-import is safe to repeat. → §9.1, §9.3, §9.5

A module’s names are namespaced. A kind a module declares with class is addressed under the module name — catalog.Product — and a cell of it is read with the module-qualified construction module.Kind(subject).field:

p = catalog.Product("widget").price    # read catalog's Product widget, field price
print("price = " + str(p.value))

Two modules may each declare a Product without collision (catalog.Product, store.Product, distinct). A script a module declares with def is addressed the same way — module.script — and that qualified name is how the service surface names it: the name info and forget take, the name list scripts reports, and the name instructions call once the module is imported (warehouse.restock, store.restock, distinct). A script’s own body still calls its siblings unqualified; the qualifier is the address, used from outside at the service surface. → §9.6

An import also brings the module’s kinds into scope unqualified, so after import catalog a bare Product means catalog.Product:

import catalog
def restock():
    remember(Product.widget.price, "9", "ops")   # catalog's Product

A kind the unit declares itself wins over an imported one of the same name, and if two imported modules declare the same kind the program is refused — name the module to say which you mean (catalog.Product). → §9.6

Provide a module from the wire. compile <name> from "<source>" stores a module by name and runs it (§5.7). Every module in a store arrived that way. The bare import <module> is the in-language form written in a program. → §9.3, §9.4

Data at module scope. A write verb (§5.1) written at a module’s top level — not inside a def — is a data declaration: it runs when the module is compiled or imported. A module that only declares a schema, installs a rule, or writes data defines no callable script and is loaded for its body’s effect. → §9.2, §9.7

# in a module body, at top level:
remember(Rate.vat.pct, 25, "2026-finance-act")   # runs when compiled or imported

7.12 return

def classify(n: int) -> string:
    if n > 100:
        return "big"
    else:
        return "small"                # every path returns → value script (§7.1)
def find(xs: claim_list, stop: string):
    for c in xs:
        if c.value == stop:
            return                     # bare early exit → any script
        print(c.value)

A bare return ends the current script early and is valid in any script. A return <expr> yields a value and is valid only in a value script (§7.1); the expression’s type must match the declared -> type (an int satisfies -> real). A value script must return on every path — a trailing return, or an if/else (or exhaustive match) where each branch returns; a for alone never satisfies it. A return <expr> in a void script, or a value script that can fall off its end, is a type_error. A return exits past any enclosing for/try (running a try’s finally first) and never runs a for … else.

7.13 print

print("hi", who)                 # one line: "hi <who>"
print(1, 2, 3)                   # "1 2 3"
print("a", "b", sep=", ")        # "a, b"
print("x", end="!")              # "x!"
print()                          # an empty line

Writes one output line. Each argument is rendered to its text form (exactly as print) and the pieces are joined by sep (default a single space), then end (default a newline) is appended. sep and end are string-literal keyword arguments. Output is line-oriented — each print writes exactly one line — so a trailing newline in end is that line, and end="" reads the same as the default (there is no continuing a line). A boolean prints as True / False.

7.14 pass

if x > 0:
    print("positive")
else:
    pass                         # do nothing

A no-op statement: it does nothing and produces no output. Use it where a block would otherwise be empty.

7.15 raise

def withdraw(amount: int):
    if amount <= 0:
        raise ValueError("amount must be positive")
    remember(Account.main.pending, amount, "teller")

try:
    withdraw(x)
except refuse as r:
    print("blocked: " + str(r.reason))          # "blocked: amount must be positive"
    print("kind: " + str(r.discriminator))      # "kind: ValueError"

Raises a recoverable error — a refuse — that an enclosing try catches with except refuse as r:. Name one of the built-in exceptions (ValueError, KeyError, TypeError, RuntimeError, …); the message becomes r.reason and the exception name r.discriminator. Every exception name behaves the same — there are no custom exception types. A raise never falls through, so a branch that ends in one satisfies a value script’s “return on every path”.

7.16 assert

def withdraw(amount: int):
    assert amount > 0, "amount must be positive"
    remember(Account.main.pending, amount, "teller")

assert x == 5                       # passes silently, execution continues
try:
    assert x > 100, "too small"
except refuse as r:
    print("caught: " + str(r.reason))            # "caught: too small"

Python’s assertion. assert cond evaluates the bool cond and, when it is false, raises an AssertionError — a refuse, equivalent to if not cond: raise AssertionError. assert cond, msg records msg on r.reason (evaluated only on failure); a bare assert cond gives an empty reason. A passing assertion produces no output and execution continues. This bare (parenthesis-free) assert statement is distinct from the absence-assertion verb assert(K.s.a, src) (§5.1), which records an explicit-absent claim.

8.1 Class declaration

class Sensor:
    temp: string                                 # typed field (primitive)
    def record(self, v: string, src: string):    # void method (explicit self)
        remember(self.temp, v, src)
    def label(self) -> string:                    # value method
        return "sensor"

Written class <Name>: — no marker. Fields are name: type with a primitive type; names unique within the class. Declaring a class stores nothing. A class may name a single base class it extends — class Dog(Animal): — inheriting the base’s members (§8.10).

8.2 Instance construction and binding

s = Sensor(room)

Sensor(room) names one member of Sensor identified by the string room; bound by assignment, its type is the class name. Construction records nothing. Reading a never-written field yields empty.

8.3 Field read and write

reading = s.temp                    # read → active_claim or empty
remember(s.temp, "21", "op1")       # write value + provenance source

A read has type active_claim; consume with match or .value. Accessing a field the class does not declare is a type_error. Inside a method the explicit receiver self (the first parameter) names the instance (self.temp).

8.4 Void method

s.record("21", "op1")               # statement position; self is supplied by the receiver

def name(self, params): — no return type; performs actions; called as a statement. The self argument is supplied by the receiver, not written at the call.

8.5 Value method

name = s.label()                    # expression position

def name(self, params) -> type: whose body is a single return <expr> of that type, or local name = <expr> bindings followed by a tail return (control flow inside a value method body is not yet supported); called in expression position. Resolved from the receiver’s class — the actual class when the receiver is held at a base type (§8.10); compile-before-call; no recursion.

8.6 Class match (dispatch by class)

match s:
    case Sensor:
        remember(s.temp, "22", "op1")
    case Actuator:
        remember(s.state, "on", "op1")

A match whose scrutinee is a bare instance variable dispatches over class names. Inside case <Class>: the instance is treated as that class; a case matches that class or any subclass, first match winning (§8.10). The arm set is closed and exhaustive — cover every class the instance could be, or provide a case default:. Non-exhaustive or unknown-class arms are type_errors.

8.7 Computed fields

A class field declared with an initializer the engine derives from the class’s other fields and keeps current as they change. The customer writes only the inputs; the derived field reads back like any field, with a derived provenance in place of a source.

class Order:
    price: int
    qty: int
    total: int = price * qty        # int: an arithmetic expression (+ - * %) over earlier fields
    big: bool = total > 1000        # bool: one ordered comparison of an earlier field

An int field is arithmetic (+ - * %) over earlier fields; a real field may also use /; a bool field is one ordered comparison (< <= > >=). Every reference is to a field declared earlier, so computed fields never form a cycle, and writing an input re-derives every field built on it. why over a computed field lists the inputs it was derived from (§5.3).

8.8 Standing rules

A named top-level declaration — a sibling of class / def, not a class member — that derives a field automatically: its conclusion is in force exactly while its condition holds, so a derived field always reflects the current data. The @rule decorator marks the def as a rule; absent names its one negative premise, inside a rule block only.

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

• for <var> in <Kind> (, <var> in <Kind>)* — the subjects the rule ranges over and the name it gives each. Names must be distinct. The bindings are a conjunction and carry no order; a nested for is not accepted, because nesting would read as a walk and a rule states a condition over the whole store.
• if <premise> (and <premise>)* — every premise must hold:

• not_asserted(...) is the one negative a rule may point at its own conclusion, and that is what it is for: a rule states a default and stops concluding the moment a person records something else. This is the idiom for “everything of this kind, unless…”, and it needs one thing a reader reaching for it usually leaves out: a positive premise to range the subjects. A negative says which subjects a rule does not apply to and never which ones it does, so if not_asserted(b.flies) alone is rejected — pair it with a premise that names the population, as b.species == "avian" does below.

@rule
def birds_fly():
    for b in Bird:
        if b.species == "avian" and not_asserted(b.flies):
            b.flies = True

Recording b.flies = False for one bird stops the rule concluding about that bird — its premise stopped holding, so no conflict is created and nothing has to be ordered. Removing the record returns the default. absent(b.flies) there would be self-cancelling and is refused, with a message naming not_asserted(...). - a rule using none(...) records an intermediate field on the subject’s kind, named after the field the rule CONCLUDES (<field>__none<N>, numbered from 1 in the order the none(...) premises are written) — a rule concluding f.safe records f.safe__none1. It is an ordinary derived field — it appears in list, in current, in checkup and in why for the conclusion drawn from it — and it holds True for exactly the subjects the none(...) excludes. Reading it is a supported way to see which rows the quantifier found. - the conclusion <cell> = <literal> is recorded with a derived provenance; the customer never writes it directly. The literal may be a negative integer (r.adjustment = -5). A cell is either <name>.<field>, a field of a subject the for clause bound, or the three-segment <Kind>.<subject>.<field> path used everywhere else in the language — except that its last two segments may be bound names, which is what records a fact about a pair. Every name in a conclusion must be bound: by the for clause, by a join, or by a relation premise. - the conclusion may instead be a fold over the rows the rule ranges over, <cell> = <fold>(<row>) or <cell> = <fold>(<row>.<field>) — c.order_count = count(o), c.total = sum(o.amount). See Folding the rows below.

Folding the rows. The for clause ranges over pairs, the conclusion names one of them, and the fold is taken over the other — grouped by the subject the conclusion is about:

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

@rule
def order_total():
    for c in Customer, o in Order:
        if o.customer == c:
            c.total = sum(o.amount)

A customer with four orders gets 4, one with a single order gets 1.

Not an aggregate query. §5.8 folds a whole attribute across every subject of a kind and answers once: count(Order.customer) is how many orders exist, where count(o) here is how many are this customer’s.

Which folds may appear. Any single-operand fold of §5.8 — every family there but ranked and two-attribute, whose extra argument a conclusion has nowhere to put. Each keeps its §5.8 meaning, the identity and positional folds included: argmax(o.amount) records the subject at this group’s maximum, distinct(o.region) a count of distinct values, and distinct(o) the number of distinct subjects.

What is folded, and what counts as a row. The folded row must be one the for binds. A row missing the folded field adds nothing to a fold over it and still counts as a row, since naming a field makes its presence a premise.

A fold ranges over the premises’ MATCHES, and a location holding more than one value in force matches once per value (§7.6) — two orders, one of which two sources agree belongs to this customer, make count(o) answer 3. Each fold follows the claims of the field IT reads, so the two shapes move independently: a second claim on the JOINED field raises count(o) and leaves sum(o.amount) alone, and only a second claim on the AMOUNT adds that amount again.

A derived field is an ordinary premise, so if c.order_count > 3 in a second rule is how “more than three orders is a regular” gets written.

What a conclusion may write — a class does not constrain it. A rule concludes into a path, and paths are open. Three consequences, each measured rather than inferred, and all three surprise a reader who has met class first:

• A rule may conclude about a kind no class declares. Nothing has to be declared before a rule writes it.
• A rule may conclude into a field its class does not declare. Declaring class Order: total: int does not close Order against a rule concluding o.review.
• The field’s declared type does not constrain the concluded value. A rule concluding s.mean = avg(r.v) over int readings records 1.5 into a field declared int, and nothing refuses.

That is not a contradiction of §8.3, which makes an undeclared field a type_error — it is the same rule seen from the other side. §8.3 governs instance access: o = Order("o1") binds an instance, and o.undeclared is refused because a class is a closed schema for the instance surface. A rule’s for o in Order binds a path, not an instance, and writing a path is the open surface the store has always had. A class is a schema you get checked against where you construct one, and a vocabulary you are not confined to where you reason.

A conclusion may be False as readily as True — o.big = False records the bool False, which is a recorded value and not an absence. The absent premise in the table above is what tells those two apart.

A rule that reads the same relation it writes applies to its own results:

@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

The first records every direct edge; the second joins a reach already known to a further edge and records the longer one. It settles on everything the graph connects rather than on a fixed number of steps. A name used twice in one cell agrees with itself, so Reach.x.x asks which subjects reach themselves:

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

Every name a rule binds must be ranged by a comparison, a join, or a relation premise — a name mentioned only in an absence test says which subjects nowhere — and a rule must not cancel itself out; either is rejected when the rule is defined. It ranges over finitely many subjects; termination is preserved. A derived field reads back like any other (current / get).

At the wire surface, list rules names the standing rules you have defined — names only; keep your own source for what each rule does.

forget rule <name> removes ONE standing rule and reclaims what it derived, leaving the rest of its module in place; <name> is the qualified module.rule name list rules prints. A conclusion another standing rule still supports is re-derived and stays — only this rule’s support is withdrawn — and the facts the rule read are untouched. Wire-only; needs a read-write-delete key.

checkup answers the question a silent rule leaves open. A rule that never fired and a rule that fired and found nothing return the same empty result, and when the reasoning came from a module you did not write, nothing else tells you which happened. It reports unmet <Kind>.<field> for a cell some rule reads that holds nothing — no-such-kind when nothing of that shape exists, no-values when the kind is there and the field is empty, and not-in-force when a value is recorded at the field but its validity window does not cover the time asked about, which is a fact you already hold rather than one to write — unread <Kind> for a kind of yours no rule reads, violated <name> <n> <subject> … for a standing constraint (§8.12) that does not hold, near A ~ B when those two lists contain names a letter or two apart, and a counts line. A near line is usually a mis-spelled kind name: writing facts under a kind spelled slightly differently from the one the reasoning reads produces both halves, and the pair names the mistake in a way neither half does alone. Findings name cells rather than rules — what an unmet cell needs is your data. A violated line is the exception that proves it: a constraint is a named invariant you declared, so the constraint is the right noun, and the subjects beside it are what make the finding actionable. The count is exact; at most five subjects are listed. Wire-only; takes no arguments and changes nothing.

8.9 Hypothesis

suppose(<field>, <value>, …, <field>) reads what the last field would be if each named field were set to the value beside it — letting standing rules and computed fields run under the suppositions — then discards everything. Nothing persists. Returns a value; bind it and read it, or concatenate it into a print.

would = suppose(Order.o1.total, 2000, Order.o1.review)   # true, if a rule sets review over 1000

Give a <field>, <value> pair per supposed fact. The field to read is always the last argument, alone — so a rule needing two facts at once can be asked about:

would = suppose(Order.o1.total, 2000,
                Order.o1.shipment, "sent",
                Order.o1.review)

Suppositions apply left to right: two naming the same field leave the later one standing, exactly as a later write wins over an earlier one. A hypothesis takes 1 to 16 of them — a cost bound rather than a semantic one, since each supposition is its own reasoning pass and the total grows faster than the count; over the limit is a compile error naming the number. If the read field has no value under the suppositions, suppose produces no value — a catchable refuse (guard it with try / except). Safe for preview, comparison, and what-if exploration; termination preserved.

suppose_absent(<field>, …, <field>) asks the opposite: what the last field would be if the other fields’ facts did not exist. Same isolation — the suppositions and everything that follows from them are discarded, and nothing is removed. It takes 1 to 16 fields to suppose away, applied left to right, and the read is the last argument — so suppose_absent(a, b, c) supposes away a and b, and reads c.

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

Returns an active claim that may be empty, matched exactly like current — not a value. The two hypothesis verbs differ here on purpose: suppose asks what a value would be, so a missing answer is an edge case and arrives as a catchable refuse; suppose_absent asks what would survive, and “nothing” is the answer it exists to give, so it arrives as an ordinary empty read.

A single hypothesis supposes facts into place or away, not both; mixing the two in one call is not available.

Use it before forget (§7.1), which cannot be undone. dependents tells you what points at a fact; this tells you what the answers become without it — while the fact is still there to keep. Supposes exactly one absence; termination preserved.

8.10 Inheritance

A class may extend one base class, named in parentheses; it inherits the base’s fields and methods and may add its own or override a method:

class Animal:
    sound: string
    def speak(self):
        remember(self.sound, "generic", "op1")

class Dog(Animal):                     # single inheritance (one base)
    breed: string
    def speak(self):
        super().speak()                # run the base's version, then extend it
        remember(self.breed, "collie", "op1")

Single inheritance only (class C(A, B): is an error). A subclass instance is accepted wherever the base is expected — a base-typed parameter, a binding, or a list element. A method call through a base-typed reference runs the actual class’s method (for a in animals: a.speak() runs each element’s own version); value methods dispatch the same way. Through a base-typed reference you may use any member the base declares; a subclass-only member needs isinstance (§8.11) or a class match (§8.6) first. The class set is closed and finite, so dispatch is bounded and termination preserved.

8.11 isinstance

isinstance(x, C) → bool: true when x’s class is C or a subclass of C. Inside the taken branch it narrows x to C, exposing that class’s members.

if isinstance(d, Dog):
    print("a dog")

8.12 Standing constraints

@constraint declares an invariant the store is watched against. It concludes nothing, writes nothing, and never fires:

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

It reads like a rule with violated where the conclusion would be, and that is what it is: the same for and if, and no head. violated is a statement rather than a value, and a reserved word only in that position.

Ask for it with checkup (§8.8), which reports one violated line per constraint that does not hold, naming the breaching subjects. It is never checked on write — recording a fact that breaches an invariant is not refused, because a store mid-edit is routinely inconsistent, and a write that fails on someone else’s invariant is a worse failure than a report saying so.

Why not just write a rule? A rule that concludes p.invalid = True records a fact ABOUT the store INSIDE the store, and the next rule reads it as an observation. A constraint has no conclusion to record, so there is nothing for a later rule to pick up. That is the whole difference.

A constraint binds exactly one row variable, and its premises are a comparison against a literal (p.stock < 0, p.tier == "gold") or an absence (absent(o.customer)), joined by and:

@constraint
def every_order_has_a_customer():
    for o in Order:
        if absent(o.customer):
            violated

Both limits have one cause: a rule is answered by the reasoning, and a constraint is answered by re-reading your store, so it can ask what a read can ask. To watch something outside that, conclude it into a field with a @rule and write the constraint over that field.

A constraint shares the name space of scripts and rules, and list rules does not list one — it derives nothing, so a caller enumerating rules to reason about what your store concludes would be misled by it.

Removing one. forget_constraint(name) drops a single constraint, addressed by the qualified name checkup prints. Nothing is reclaimed — a constraint concludes nothing, so the data it watched is untouched, including the subjects that breached it. Stopping the watch is not fixing the breach. forget_module still removes a module’s constraints along with the rest of it; the difference is that dropping one invariant no longer costs the other things that module brought.

9.1 A .dpy file is a module

A module’s top level is its body — a sequence of declarations and statements, read top to bottom. A body may contain, in any order:

• declarations — def (a callable script, §7), class (a kind schema, including computed fields, §8), a @rule-marked def (a standing rule, §8);
• data declarations — the write verbs remember / update / forget / assert, each with its per <source> provenance, written at module scope (§9.2);
• statements — anything legal inside a def body (§7): bounded for / if / match / try, reads bound by assignment, print, and commit / rollback;
• import statements (§9.3).

The body runs once, top to bottom, in source order, when the module is compiled or imported. A def becomes callable afterward; a class installs its schema and any computed fields; a @rule-marked def installs a standing rule; a data declaration performs its write; an ordinary statement runs.

A plain call is one of those statements, and it is how a module demonstrates itself: define a script and then call it, so importing the module both installs the script and runs it once. It follows from the two rules above rather than being a separate feature, which is why it is shown here — a rule you have to assemble from two lists is a rule most readers do not reach.

def greet():
    remember(Greeting.g1.text, "hello", "setup")
    print("greet ran")

greet()

Importing that module reports the script installed and the body’s write and print as having happened. The script stays callable afterward: the top-level call is one run, not the only one.

A module with no def is valid — one that only installs a schema, defines a rule, or writes data declares no callable script and is loaded for its body’s effect. A single-def source is simply a one-declaration module; there is no separate single-script verb.

Termination is unchanged. Every construct legal at module scope is already bounded — there is no while, for iterates only finite store-derived collections, and a script cannot recurse — so a module body always terminates, for the same reason a def body does. Module scope introduces no new iteration and no new recursion.

9.2 Data declarations at module scope

A write statement written at module scope — not inside a def — is a data declaration: an assertion of what is, or for forget a removal, applied when the module is compiled or imported.

remember(Rate.vat.pct, 25, "finance-act-2026")
update(Rate.vat.pct, 24, "finance-act-2027")
forget(Flag.legacy.enabled)

A data declaration is an ordinary write (§5) that happens to sit at module scope; it obeys every rule a write inside a def obeys.

9.3 import

import <module>

Loads a module already stored under <module>: it makes that module’s names available (§9.6) and runs its body once (§9.1). <module> resolves along the search path of §9.4. This is the one module operation written in a program body — a module may import another module. import is a contextual keyword, recognised only at statement head.

Because loading runs the module body, what that body prints and writes belongs to the run that imported it: the imported body’s output and store effects join the importing program’s transcript at the point of the import, and count in its verdict.

Loading order is an acyclic dependency order — a module is loaded before a module that imports it — and an import cycle, a module that imports itself directly or through another, is rejected when the module is loaded.

9.4 Name resolution and shadowing

import <module> resolves <module> against the modules stored in your store, each put there by an earlier compile (§5.7). There is no second place to look and no fall-through: a name that is not in your store is not found.

This is what makes a published module’s name a default rather than a reserved word. A module we publish, such as code, is a file you compiled into your own store, so import code resolves to whatever you compiled under that name — the copy you took from us, or your own edit of it, or something unrelated.

9.5 Re-submitting reconciles

Compiling a module whose name is already stored — or importing an already-loaded module — re-runs its body, and the re-run is a reconciliation:

• a data declaration whose value changed since the last run updates the stored cell;
• a data declaration whose value is unchanged leaves the cell as it is — an identical write is not recorded again;
• a class or rule install is likewise a no-op when nothing changed.

Reconciliation leaves the store reflecting the module’s current text, rewriting only the cells whose values changed, and is safe to repeat. This is the one place import differs from a language whose import runs a module body only once: a DKE Python module is durable store state, not process memory, so re-running re-applies it.

9.6 Namespacing

A module is a namespace. A name it introduces — a kind declared with class, a script declared with def — is addressed under the module name with a dot: code.Function, code.impact_of. Two modules may each declare a Function without collision; they are code.Function and finance.Function, distinct. Within a module’s own body, its own names are reachable unqualified.

An import brings the imported module’s kinds into scope unqualified. After import code, a bare Call in that unit means code.Call. A bare kind name resolves in this order:

1. a kind the unit declares itself wins — a unit’s own class Call is never redirected to an imported module’s Call; local beats imported;
2. otherwise, the one imported module that declares it;
3. if two or more imported modules declare it and the unit declares none, the program is refused, with a type_error naming the candidates — import order states dependency, not precedence, so the ambiguity is reported rather than resolved by position;
4. otherwise the name is unchanged — a kind no module declares is an ordinary global kind.

The qualified form is always available and always unambiguous, so it is both the way to reach a specific module’s kind past a local declaration of the same name and the fix for case 3.

A cell of a module-qualified kind is read with the module-qualified construction — module name, kind, subject in parentheses, then the field:

a = code.Function("f1").fanin          # code's Function f1, field fanin
print("fanin = " + str(a.value))

This reads like any field read (§8) and its result is an active_claim. The parenthesised subject is what distinguishes the construction from an ordinary dotted path (§7). Because each module’s names are addressed under its own module name, two modules that both declare a Function never read or write each other’s cells.

A script a module declares with def is likewise addressed module.script — the name a program calls after importing its module, the name info script and forget script take, and the name list scripts reports. Two modules may each declare a restock without collision.

An imported module’s scripts are callable from your own code under that same qualified name:

import code

def review(fn: string):
    who = code.callers_of(fn)          # a value call
    print(str(who.length) + " caller(s)")
    reach = code.impact_of(fn)         # its result is an ordinary list
    for r in reach:
        print("  reaches " + r)
    code.log_review(fn)                # a void call, as a statement

Such a call obeys the same rules as any other (§7): arguments are checked against the callee’s declared parameters, a value call must name a value script, and the callee must already be stored — which an imported module’s scripts are, since importing it stored them.

code.callers_of("f") and code.Function("f").fanin open with the same words. They are told apart by what follows the closing parenthesis: a module-qualified construction is not a value on its own, so a field always follows it; a call is a value, so nothing does.

A call is resolved when the calling module is compiled, and the callee’s body at that moment is the body the call runs. Importing a newer version of the callee’s module afterwards does not change a caller that was already compiled — it changes what module.script runs when called directly, and what the next compile of the caller picks up. Import the calling module again to move it onto the new version.

9.7 Published modules

A published module is an ordinary module — classes, rules and queries in one .dpy file — that we have written and published for you to use instead of writing the same declarations again. You download the file and compile it into your store, once. Nothing about it is privileged: it is the same kind of file you may write yourself, it resolves the same way (§9.4), and once compiled your store cannot tell the two apart.

Three things follow, and each is a consequence of the file being yours.

1. You can read it before you run it. It is source in this language. What it declares is what its lines say; its published documentation — for the modules we publish, the Reasoning Modules Reference — is a lookup over that source, not a substitute for it.
2. Its interface is enumerable once compiled. list modules reports it, info module reports the scripts it defines and the classes it declares, list reports its scripts with their signatures, and list rules its standing rules by name. This is a guarantee, not an artefact: a script that could not be discovered could not be called. A module’s SOURCE is not stored — the store keeps the compiled form, and there is no readback verb for any module — so the file you downloaded is the copy to keep.
3. Removal and editing are ordinary. forget rule removes one of its rules and forget module removes the whole module; nothing reinstates either. To reason without one of its rules, remove the rule or edit the line and compile again.

11.1 Universal accessors

• <expr>.kind → string — for any discriminator and for proof_tree.
• <expr>.length → int — for any string (its character count — Unicode characters, not bytes) or finite collection (its element count).

11.2 Field access by type

The last two types are the handler bindings of §4.2 — a program cannot write either name as a type, and they are listed here under the names .kind reports.

11.3 Indexing element types

A string also supports slicing — s[a:b] (either bound optional) yields the substring, s[a:b:step] adds a step (a negative step reverses: s[::-1]), and negative indices/bounds count from the end (s[-1], s[-3:]). Total and character-indexed; a step of 0 is a catchable refuse.

11.4 String methods

All are total (never refuse) and count characters, except partition / rpartition, which refuse on an explicit empty separator.