# DKE Python — Language Reference **Version:** alpha · API 1 **Status:** Published reference manual for DKE Python. **Audience:** Tenants writing DKE Python — the programmer's day-to-day lookup for verbs, types, statements, operators, classes, and modules. **This document as Markdown:** [dke-python-ref.md](/ref/dke/python/dke-python-ref.md) — the same text this page is rendered from, for readers and tools that would rather have the source than the page. --- ## 1. About this reference This is the **reference manual** for **DKE Python**, the language a DKE tenant writes and submits to the DKE service at `dke.langsyn.net`. It is the published description of the language: what each construct means, what it produces, and how to write it — one entry at a time, with a worked example for each. Read it alongside its two companions: - the [**Tutorial**](/tutorial/dke/python/), which teaches the same language in task order, from a first program to classes, provenance and modules; - the [**Wire & Tool Contract**](/ref/dke/mcp/), which specifies the transport that carries a program to the service — the tool surface, request shapes, the response envelope and the error model. Where this Reference and the running service appear to differ, tell us: one of the two is wrong, and it matters which. The language and this document are open under the MIT license. The DKE service that runs DKE Python is LangSyn's proprietary product — the language is published; the implementation is not. DKE Python is a **Python-flavoured surface** over DKE's knowledge-operation semantics: `def` declarations, bare assignment, `match`/`case`, `try`/`except … as`, and an explicit `self` receiver. It is **indentation-significant**. Source files use the extension `.dpy`. --- ## 2. A program at a glance A DKE Python source file is a **module**: one or more `def` declarations. Every declaration is stored under its own name and is independently invocable. ``` # greet.dpy — a one-declaration module. def greet(K: string, s: string): remember(K.s.mood, "cheerful", "op1") # write a claim m = current(K.s.mood) # read it back (bare assignment) match m: # consume the discriminator case active_claim: print("mood = " + str(m.value)) case empty: print("no mood recorded") ``` Reading the shape: - `def greet(K: string, s: string):` — a **declaration** (§7.1): the `def` keyword, name, typed parameters (`name: type`), a `:` and an indented suite. - `remember(…)`, `current(…)` — **verb calls** (§5): the built-in verb surface written as function calls with a dotted `K.s.a` slot path as the first argument. - `match` / `case` — a **statement** (§7.8): exhaustive discriminator dispatch. (Python uses `case`; the base member uses `when`.) - `m.value` — **field access** (§11) on an `active_claim`. Compile it, then run it at the wire surface with `run greet.greet("Cat", "felix")`; in another program, call it with a plain call `greet(K, s)` (there is no call keyword). **Learn from inside the language.** Send a unit whose body is `--help` for orientation, or `--help ` for one of `header`, `types`, `verbs`, `statements`, `scripts`. ``` --help verbs ``` --- ## 3. Natural language A source has **no header line**: it is the program body from its first line. The natural language a source is written in — which keyword vocabulary its statements use, and the language its responses render in — is set **out of band**, by the `language` parameter supplied when the source is submitted, not by the source. - When the `language` parameter is omitted, the language is **English** (`eng`), which is the language this Reference describes. The parameter's accepted values belong to the wire contract and are listed in the DKE MCP Reference; a value outside that set is declined at the parameter gate, before the engine. - **This Reference describes the English surface.** Every keyword, verb, operator spelling and rendered response shown here is the `eng` one. Any other keyword vocabulary is a separate surface over the same semantics, and is described in its own documents rather than in this one. - A program's meaning is independent of the language it is written in: the same program in any supported keyword vocabulary denotes the same thing. The natural language is a property of how you talk to the service — set per call — not a property stored in the program. --- ## 4. Types DKE Python has a **closed, flat** type vocabulary shared across the family: no subtyping, no generics, no user-defined record types. Programs compose by operating on the store through verbs. ### 4.1 The base types | Type | Produced by | Category | Notes | |------|-------------|----------|-------| | `string` | literals, user data, values | primitive | no ordering; `==` / `!=` only | | `int` | literals, `.length`, counts | primitive | signed 64-bit | | `bool` | comparison + logical results, `True` / `False` | primitive | | | `value` | `active_claim.value` (a claim's stored content) | tagged union | `int` \| `bool` \| `string` \| `datetime` \| `duration` \| `real` \| `null` \| `blob` \| `scientific`; consume with `match` (§7.8) | | `datetime` | `datetime("…Z")` literal, a datetime `value` read | value class | a UTC instant; renders as RFC 3339; a write-verb value + `case datetime as d:` | | `duration` | `duration("…")` literal, a duration `value` read | value class | a length of time; renders as ISO 8601 (`PnDTnHnMnS`); a write-verb value + `case duration as u:` | | `real` | `3.5` literal, a real `value` read | value class | a fractional number, written `3.5` or with an exponent `1e5` (Specification §3.5.7); renders exactly as CPython `repr(float)` (fixed, or scientific for extreme magnitudes); computes under `+ - * /` (§6.3) + ordered comparison (§6.1); a write-verb value + `case real as r:` | | `blob` | `blob("…")` / `blob_b64("…")` literal, a blob `value` read | value class | an opaque byte string, written `blob("…")` or `blob_b64("…")` (Specification §3.5.8); renders as canonical uppercase hex; a write-verb value + `case blob as b:` | | `scientific` | `scientific("…")` literal, a scientific `value` read | value class | a number carrying its significant figures, written `scientific("6.022e23")` or `sci"6.022e23"` (Specification §3.5.14); reads back canonical (`60.220e21` → `6.0220e22`), with 4-s.f. and 5-s.f. of the same magnitude distinct; a write-verb value + `case scientific as s:` | | `active_claim` | `current(K.s.a)`, a field read | discriminator | one live claim, or `empty` | | `claim_list` | `get(K.s.a)`, `list_values(K.a)`, `caveats(K.s)`, `dependents(h)`, `conflicts()` | finite collection | element `active_claim` | | `proof_tree` | `why(K.s.a)`, `why(K.s.a, t"…")` | finite collection | element `active_claim` (the derivation's participating claims); also fields `.root`, `.truncated` | | `diagnosis` | `why_not(K.s.a)`, `what_needs(K.s.a)` | finite collection | element `string` (the lines of the explanation) | | `subject_set` | `subjects(K.a, v)`, `list_subjects(K)`, `list_subjects(K.a)` | finite collection | element `string` | | `string_list` | `list_categories()`, `list_attributes(K)`, `list_pinned()`, `list_scripts()` | finite collection | element `string` | | `verify_result` | `verify(K.s.a, v)` | discriminator | fields `.match`, `.actual`, `.expected`, `.conflicted` | | `result_type_set` | `list_result_types()` | finite collection | element `string` | | `refuse_info` | the binding of `except refuse as e` (§10) | handler binding | fields `.reason`, `.teaching_hint`, `.discriminator` (§11.2) | | `engine_error_info` | the binding of `except engine_error as e` (§10) | handler binding | fields `.reason`, `.code` (§11.2) | | `empty` | the second arm of an `active_claim` match | discriminator sentinel | `case empty:` only, not a type name | Beyond the base types there are four **constructed** type formers — client- built values that never round-trip the service: `list` (an ordered sequence, §6.7), `tuple` (a fixed-length heterogeneous sequence, §6.8), `dict` (a mapping from a hashable key — a scalar or a tuple of hashables — to a value, kept in insertion order, §6.9), and `set` (a collection of unique hashable elements — a scalar or a tuple of hashables — presented sorted, §6.10). A `list` 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`. 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` 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`, `dict`, …), 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 ` / `except engine_error as ` 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 (…)` (§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. Verbs The built-in verb surface is written as **function calls** — a verb name and a parenthesized, comma-separated argument list: `remember(K.s.a, v, src)`, `current(K.s.a)`, `list_attributes(K)`. The first argument is the dotted `K.s.a` slot path (or a name literal / handle, per the verb). Read verbs bind by **assignment** (`cur = current(K.s.a)`). Path slots: `K` (kind), `K.s` (kind + subject), `K.s.a` (full cell), `K.a` (kind + attribute). Each segment is either a **bare name** written literally — `remember(Greeting.hello.text, …)`, which is what the examples throughout use — or a `string`-typed parameter or binding in scope, which is how a script is parameterized over the slot it writes. The two forms compile to the same path; a bare name is not a variable reference and needs nothing declared. The call form's compound heads (`list_attributes`, `list_values`, `list_subjects`, `list_categories`, `list_result_types`, `list_pinned`, `list_scripts`) are single snake_case tokens — **soft keywords** recognized as a verb only immediately before `(`, so the same spelling stays a usable ordinary identifier elsewhere. ### 5.1 Write verbs (statement position) #### `remember(K.s.a, v, src)` Records value `v` at cell `K.s.a` attributed to `src`. Permissive. The value is a scalar literal (`string` / `int` / `bool`) and is stored **with its type** — the claim reads back through `.value` at the type it was written (§4.1, `value`), and query verbs match it type-aware (`subjects`, `verify`, `agreement`). An optional pair of trailing `datetime` bounds gives a **validity window** — the fact is valid only between them (both inclusive); either bound may be `null` for an open side. Omit the pair for an always-valid fact. A windowed write is selected by an as-of read (§5.4) whose time falls in the window — that is how it is read back, and on the traversal verbs how it is found at all. ``` 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.a, v, src)` Supersedes the claim; establishes one on an empty cell. Accepts the same optional trailing `datetime` validity window as `remember`. ``` update(K.s.mood, "playful", "op2") ``` **Choosing between them.** Neither verb is a fallback for the other. `remember` asserts something new; `update` says *revise my earlier reading*, and because it also establishes a value on an empty cell it works the first time as well as the tenth. A producer meant to run more than once — a loader, a CI step, anything pointed at data that changes — means `update`, and should ask for it by name. `remember` being Permissive means a re-assert succeeds rather than refusing; it does not make the two interchangeable, because what is lost is a reader of the program being able to tell which was meant. Supersession is per SOURCE, for both verbs. Revising your own claim leaves every other source's claim at that cell standing, so a re-run never quietly settles a disagreement the store is holding — see `prefer` (§5.1) for the verb that records a judgment between sources. **A write establishes the kind.** Neither verb requires the kind to exist beforehand: writing `K.s.a` when nothing named `K` has been recorded stores the claim and brings `K` into being. It is the complement of `forget(K.s)` below, which removes the last subject and takes the kind with it — a kind stands for exactly as long as something is recorded under it. Declaring a `class` (§8) fixes the schema a kind's fields are checked against; it is not permission to write, and the two directions are deliberately not symmetric. Within a declared class, writing a field the class does not declare is a `type_error` (§8.3). A write to a kind no class declares is accepted. Knowing which of those you are relying on is worth settling before you build on it: a producer that writes its own bookkeeping under an undeclared kind is using the second, and will keep working; a typo'd field name inside a declared class is the first, and will be refused. A module-qualified path and an unqualified one name different cells. `m.K.s.a` and `K.s.a` are two cells, not one, and a value written through one is not read back through the other. #### `forget(K.s.a)` / `forget(K.s)` / `forget(K.s.a, v, src)` / `forget(K.s.a, t"…")` / `forget(
, recorded_before=t"…")` Permanently removes data. **Hard and irreversible** — nothing is kept in history and nothing can be reinstated. Path-scoped: `forget(K.s.a)` reclaims every value ever recorded at the cell, not just the current one, and `forget(K.s)` removes the whole subject, after which its kind is gone. Claim-scoped: `forget(K.s.a, v, src)` removes the single claim recording value `v` from source `src`, leaving every other claim at that cell untouched — the way to drop one side of a disagreement without discarding the other. Both `v` and `src` are required, because a value alone does not name a claim: two sources may record the same value at one cell. ``` forget(Project.dke.license, "MIT", "registry_one") ``` `v` is matched **by value and by type**, and both halves matter because a cell can hold the same text in two types. `5` and `"5"` are different claims, so `forget(K.s.a, "5", src)` does not reach an integer claim — write the value the way you wrote it, and `forget(K.s.a, 5, src)` reaches it. Every type you can write, you can name: `string`, `int`, `bool`, `real`, `datetime`, `duration` and `blob`. ``` 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 ``` Type equality here is **exact**. `==` compares `int` and `real` numerically, so `1 == 1.0` is `True` and a query reaches both — but a removal names a specific claim and takes it permanently, so an `int` literal does not reach a stored `real`. Write the `real` and it does. Naming a claim the cell does not hold is a refuse, not a silent no-op; call `get(K.s.a)` to see the values and sources actually recorded there. Where the value and source match and only the **type** differs, the refusal says so and names the type it found — a read renders `5` and `"5"` identically, so that is the one place the difference is visible. To see a stored value's type yourself, `match` over a claim's `.value` (§7.8). Time-scoped: `forget(K.s.a, t"…")` removes the values at that cell whose validity window covers the instant named, and leaves the rest. It addresses by **when a value was true** rather than by what it says, so it is the way to drop a period you no longer want to keep without knowing what was recorded in it. The same instant you would pass to `current(K.s.a, t"…")` to read what was in force selects what is removed. ``` forget(Sensor.probe.reading, t"2021-06-01T00:00:00Z") # the values in force then ``` A time-scoped call takes a `K.s.a` path only. An instant narrows which values at **one cell** are named, and a subject holds many cells with many windows rather than one window to narrow; `forget(K.s)` already removes a whole subject and needs no instant to do it. An instant **no value covers** removes nothing and succeeds — unlike the claim-scoped form, which refuses. The difference is what is being named: a claim either exists or it does not, so naming one that is absent is a mistake worth reporting, while a moment nothing was true at is an ordinary answer. Range-scoped: `forget(
, recorded_before=t"…")` trims **history**. It removes the older versions that fall before the instant, and **never a value in force** — whatever an address currently says survives every range, including one whose instant is far in the future. That is the difference between this form and every other one above: the others can empty what they name, and this one cannot. **Three widths.** The range is the only form that takes more than a cell, and that is the point of it — trimming a year of history one cell at a time is not a thing anyone can do: | Address | Trims the history of… | |---|---| | `forget(K.s.a, )` | one cell | | `forget(K.s, )` | every cell of one subject | | `forget(K, )` | every cell of every subject of the kind | Each answers a different number over the same store, and the safety property is the same predicate at all three, so none of them can reach a value in force. A kind-wide range cannot empty anything. ``` forget(Sensor, recorded_before=t"2026-01-01T00:00:00Z") ``` `K` is an address **only with a range**. A bare `forget(K)` is refused at compile time and told about this form: emptying a whole kind is not something to reach by leaving a path short. To remove one subject entire, name it — `forget(K.s)`. Four spellings, choosing an axis and a boundary: | Keyword | Removes the older versions… | |---|---| | `recorded_before=t"…"` | **written** before that instant | | `recorded_at_or_before=t"…"` | written before it, or exactly at it | | `valid_before=t"…"` | that stopped **being true** before that instant | | `valid_at_or_before=t"…"` | that stopped being true before it, or exactly at it | ``` forget(Sensor.probe.reading, recorded_before=t"2026-01-01T00:00:00Z") ``` The two axes answer different questions and select different versions, so choosing between them is the substance of the call rather than a detail. Ask `recorded_*` when the reason is age — *this was written years ago and I no longer need it*. Ask `valid_*` when the reason is subject matter — *this stopped being true before we cared*. A version whose validity window was never closed has no `valid_*` answer at all and no `valid_*` range reaches it, which is why a `valid_before=` call can report removing nothing where `recorded_before=` would remove several. That is not a failure; it is the two axes disagreeing, which they are entitled to do. **There is deliberately no `after` form.** It would name the versions *newer* than the instant, which includes the value in force — so it would undo part of a cell's history rather than trim its tail, and the safety property above would not hold. Removing a current value is what `forget(K.s.a)` and the claim-scoped form are for, and both say so at the call site. Removing nothing is a success, not a refusal: a cell that has only ever held one value has no older versions to trim, and every range over it reports zero. Use `would_forget` (below) when the difference matters before you act — and at the wider addresses, prefer to. The two-argument forms are told apart by the **type** of the second argument. A `datetime` is the time-scoped form; anything else begins the claim-scoped one and its `src` is still required. Removal **cascades** into facts derived from the target rather than refusing while they exist; a derived conclusion that some other standing rule still supports is re-derived and stays. Needs a `read-write-delete` key. ``` 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 ``` **This verb takes no confirmation, and that is deliberate.** The tool surface gates `forget_module` behind `confirm: true` and leaves `forget_rule` and `forget_constraint` ungated, sorting them by whether what they destroy can be brought back: a module's data cannot, a rule's conclusions can, since recompiling the module reinstates them, and a constraint destroys nothing but its own declaration. That sorting has no answer for `forget`, because here it depends on the ARGUMENT rather than on the verb. Three cases, and only the last is beyond recall: - a **rule conclusion** comes straight back — the standing rule re-derives it on the next read; - a fact a **module's top level** wrote comes back on the next `import` of that module, because importing runs the top level again; - a fact **you wrote from your own data** does not come back from anything in the store, and takes its derived conclusions with it. So a blanket confirmation would add a step to two cases that do not need one, and a caller typing it for the third has already decided. What guards an address you cannot afford to lose is `pin` — it refuses `forget(K.s.a)` and `forget(K.s)` while it stands — and it has to be set in advance, which is the honest shape of the guarantee: this surface offers no undo after the fact. #### `assert(K.s.a, src)` Asserts the value at `K.s.a` is **known to be absent** per `src`. No value. ``` assert(K.s.chip_id, "vet") ``` #### `prefer(K.s.a, src)` At a location where sources disagree, states that you go by `src`. Records your judgment beside the claims: every claim stays, nothing is discarded, and the location stays in disagreement. Reads are unchanged — `get(K.s.a)` still returns every claim; each carries `.preferred`, `True` on the one you act on. Standing rules are unchanged too: a preference marks the claim you go by, and does not change what any rule derives. ``` prefer(Sensor.r1.temp, "registry_two") ``` #### `unprefer(K.s.a)` Withdraws the preference at `K.s.a`. Removes the judgment only — every claim at the location survives, as does the disagreement. ``` unprefer(Sensor.r1.temp) ``` #### `pin(K.s.a)` Protects the address. While it is pinned, `forget(K.s.a)` is refused, and so is `forget(K.s)` — removing the subject would take the pinned cell with it. Pinning an already-pinned address changes nothing. ``` pin(K.s.color) ``` #### `unpin(K.s.a)` Lifts the pin, so the address can be removed again. Unpinning an address that is not pinned changes nothing. `list_pinned()` reads what is currently protected. ``` unpin(K.s.color) ``` ### 5.2 Read verbs (expression position) #### `current(K.s.a)` → `active_claim` The single live claim, or the `empty` case. Consume with `match` or `.value`. An optional `datetime` reads the value as of another time — past or future: `current(K.s.a, t"…")`. Refuses where no single claim is the answer — a location holding two live values, whether they were recorded there or a rule concluded both. Catch it, or read the set with `get`. ``` cur = current(K.s.color) ``` #### `get(K.s.a)` → `claim_list` The full claim history. Iterable. An optional `datetime` reads the claims valid as of another time — past or future: `get(K.s.a, t"…")`. ``` hist = get(K.s.mood) ``` #### `caveats(K.s)` → `claim_list` The claims at subject `K.s` that are in disagreement — the same question `conflicts()` asks store-wide, narrowed to one subject. ``` cav = caveats(K.s) ``` #### `conflicts()` → `claim_list` Every claim currently in disagreement, store-wide. (No slot argument.) Two claims disagree when they stand at one location with different values. Who recorded them does not enter into it — a rule that concludes on both sides of a disagreement is one producer, and the location it concludes at is in disagreement like any other. ``` confs = conflicts() ``` Answers which locations are in disagreement. Disagreement is a state the store holds, not an error: both claims remain and reads keep working. The service never chooses between the claims — you say which source you go by with `prefer`, and that judgment leaves the disagreement standing. A standing rule reading a location in disagreement derives from each value that satisfies its condition, so the disagreement travels into the conclusion instead of stopping at the premise; `why` on a conclusion shows the claims it was drawn from. How it clears depends on what disagrees. Between claims you wrote, `update` or `forget` one of them. Between **conclusions** those do not reach: a conclusion is in force exactly while its condition holds (§8.8), so `forget` withdraws it and the rule records it again, and `update` adds a claim of your own beside the two already standing. Two rules that both hold and conclude different values for one field is that case, and both conclusions carry the same `derived` provenance, so there is no source to `prefer` between them either. It clears when the rules stop both concluding — narrow one rule's condition, or `forget rule` one of them. #### `list_values(K.a)` / `list_values(K.a, t"…")` → `claim_list` Every value claim for attribute `K.a` across subjects. An optional `datetime` lists the claims valid as of that time instead of now (§5.4). ``` vals = list_values(K.color) then = list_values(K.color, t"2027-06-01T00:00:00Z") ``` #### `subjects(K.a, v)` → `subject_set` Subjects of kind `K` whose attribute `a` currently equals `v`. The value `v` is a scalar literal (`string` / `int` / `bool`) and the match is **type-aware**: `subjects(K.a, 42)` matches the `int` `42`, not the text `"42"`. Numbers are one family, so an `int` literal also matches a stored `real` of the same number — `subjects(K.a, 5)` finds a `5.0`. It is the number that is compared, never its spelling. ``` 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 ``` #### `list_subjects(K)` / `list_subjects(K.a)` → `subject_set` Every subject of kind `K`, or only those carrying a claim for attribute `a`. The two differ whenever a subject is reachable through an attribute its siblings lack — that subject is in the first and not the second. Either form takes an optional trailing `datetime`, listing the subjects a traversal would find at that time rather than now (§5.4). ``` 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") ``` #### `list_attributes(K)` / `list_attributes(K.s)` → `string_list` Attribute names for a kind, or for one subject. The two answer different questions and only the second takes an as-of time (§5.4): `K` gives the attribute names recorded for the kind, which describes the store's shape and already covers every time; `K.s` reads one subject's claims, which are what a validity window applies to. ``` 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 ``` **An empty enumeration that is really a missing import.** The `list_*` reads answer with a collection, so "nothing is there" and "that kind is not here" look alike. Where the store can distinguish them it refuses rather than answering empty: when the name asked for is itself a stored module, and when some stored module declares a class of that name. Each refusal names the module and the `import` that reaches it. Both are gated on the kind being absent, so an enumeration that is legitimately empty still answers empty. #### `list_categories()` → `string_list` Every kind (category) known to the store. A kind a module declares is named in the qualified form `.` — the form the read verbs take, given an `import` of that module (§9); a kind no module declares is named as written. The name a listing gives you is a name the language accepts. Takes no as-of time, for the same reason `list_attributes(K)` does not — a kind is recorded rather than valid, so the answer already covers every time. ``` cats = list_categories() # e.g. ["Loose", "shop.Widget"] ``` ### 5.3 Provenance and reasoning #### `why(K.s.a)` → `proof_tree` The derivation of the current value. The returned `proof_tree` is an **iterable finite collection** of the claims that participated in the derivation: `.length`, `for … in`, and `[i]` yield those claims, each an `active_claim` carrying `.value` / `.source` / `.trust` / `.created_at` / `.path` (§4.1, §11.2). `.root` still yields the top `active_claim` — the queried claim. A participating claim may stand at a different location than the one you asked about — that is what a premise is — so read `.path` rather than assuming. A derivation can run deeper than a proof is rendered. `.truncated` is `True` when the answer stops short of the whole derivation, and `False` when what you have is all of it. Check it before treating a proof as complete. ``` 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)) ``` **`why(K.s.a, t"…")` — the derivation as it stood then.** An optional trailing `datetime` (§5.4) answers with the premises that were in force at that instant rather than now. A conclusion rests on claims that carry validity windows (§5.1), so it can hold at one time and not another; the anchored form is what reads back the derivation that used to hold. This is how you account for an answer that **changed**. Ask the same cell at two instants, and the difference between the two trees names the premise that moved: ``` 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)) ``` An anchored derivation may be absent where the bare one is not, and the reverse. Absence here is the `empty` discriminator (§4.1), not a zero-length `proof_tree` — so `.length`, `[i]` and `for … in` are for an answer you have established is a proof. It means no conclusion was derivable at that instant, which is a different finding from a conclusion that is derivable and false. When there is no derivation, `why_not` is the verb that explains the absence. #### `why_not(K.s.a)` → `diagnosis` Why a conclusion is **not** there. `why` needs a claim to explain; when a read comes back empty the question is a different one, and this answers it — naming the condition that blocked the conclusion, at the cell you can act on. It separates cases that every other verb renders identically. An empty read looks the same whether a condition was never recorded, was recorded with a validity window that does not cover the time you asked about, was recorded and fails its test, is required to be absent and is present, or is recorded by sources that disagree. Those need opposite fixes, so the answer says which one you have — recording a fact you already hold is not a weaker version of the right move, it is the wrong one. When no standing rule concludes the cell at all, that is its own answer — your model has no path to the conclusion, which is a different problem from an unmet condition and usually a more useful thing to learn. The cell you ask about is checked before any of that. If it holds a claim whose validity window does not cover the time asked about, you are told so and given the value — the fact is there and out of force, and what it needs is a wider window or an as-of the window covers, not another write. Whatever the rules have to say follows it, so you get both. When the conclusion does hold, you are told so and pointed at `why`. The result is an iterable finite collection of lines: printing it shows the whole explanation, iterating it takes one line at a time. It is a read and writes nothing, and it takes no `as_of` — a diagnosis is about the store as it stands. ``` 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) ``` #### `what_needs(K.s.a)` → `diagnosis` What would make a conclusion hold. Where `why_not` names what is blocking now, this names the facts that would unblock it — walking through conditions your standing rules can themselves derive, and stopping at the ones only you can supply. Each line says which it is, so the answer is a list of things to do rather than a description of the problem. A condition you already recorded, whose validity window does not cover the time asked about, is named as that rather than as a fact to record — what it needs is a wider window or a different as-of, not another write. The walk is bounded by the shape of your rule set: each rule is entered once per question, so a rule set that refers to itself in a circle reports the circle rather than following it. Like `why_not` it is a read, takes no `as_of`, and returns a `diagnosis`. ``` 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) ``` #### `verify(K.s.a, v)` / `verify(K.s.a, v, src)` → `verify_result` Checks whether `K.s.a` currently holds `v` (optionally per `src`). The value `v` is a scalar literal (`string` / `int` / `bool`) and the check is **type-aware**: `.match` is `true` only when the stored value and its type agree with `v` — except that `int` and `real` are one numeric family, so a stored `5.0` matches the literal `5`. Fields `.match` (`bool`), `.actual`, `.expected` (`string`). ``` v = verify(K.s.color, "orange") if v.match: print("confirmed") ``` #### `agreement(K.s.a, v)` → `int` Returns how many **distinct sources** recorded `v` at `K.s.a` — the quantitative sibling of `verify` (verify asks *is `v` present?*, agreement asks *how many sources say `v`?*). Type-aware, like `verify`. A count of corroboration, **not a judgment of truth**: the language reports how many sources recorded the value and never ranks, certifies, or assumes the independence of those sources — which ones to trust is the caller's judgment (read them by name with `get`). Counts every source, so it takes **no** source argument (a type_error); an unrecorded value reports `0`. ``` orange = agreement(K.s.color, "orange") # e.g. 2 ``` #### `would_forget(
, recorded_before=t"…")` → `int` Returns how many older versions the matching **`forget` range would remove** — and removes none of them. Ask what a removal costs before paying for it. It takes the same four keywords as the range form of `forget` (`recorded_before` / `recorded_at_or_before` / `valid_before` / `valid_at_or_before`) and the **same three addresses** — `K.s.a`, `K.s`, `K` — so every removal you can write has a preview you can write. One of the keywords is **required**: there is no bare `would_forget(K.s.a)`, because previewing an unbounded removal only ever answers *everything here*, which needs no instrument and would make the one call worth checking look as though it had been checked. ``` 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") ``` It is a **read**, so a read-only key can call it: finding out whether you want to remove something should not require holding the ability to remove it. It records nothing — a preview leaves no trace in the removal record, which stays a record of what was actually destroyed rather than of what was considered. The number the preview gives is the number the removal reclaims, at whichever width you asked — the two read the same selection rather than agreeing by convention, so a preview taken at `K` and a removal run at `K` cannot disagree. `0` means the range names nothing, which is the ordinary answer at a cell with no history to trim, and it is worth distinguishing from a `valid_*` range that finds nothing because the versions carry no closed validity window (see `forget` above). Asking the `recorded_*` question as well is how you tell those two apart. #### `writers(K.s.a, v)` → `int` Returns how many **distinct access keys** wrote `v` at `K.s.a` — `agreement` on the other provenance axis. `agreement` counts what was **cited**; `writers` counts who **wrote**. The difference matters: three sources cited by one key is corroboration one party assembled, while one source written by three keys is three parties independently recording the same thing. Type-aware and judgment-free like `agreement`, and it takes **no** source argument (a type_error). A claim written outside an authenticated call has no key and is not counted — so `writers` can be lower than `agreement` at the same cell, and reports `0` where every claim was written unauthenticated. ``` a = agreement(K.s.color, "orange") # 2 — two sources cited w = writers(K.s.color, "orange") # 1 — but one key wrote both ``` #### `dependents()` → `claim_list` The claims the engine derived from a claim — its downstream in the dependency graph. The operand is a claim read from `get`/`current` (bind it to a name first). A base fact with no rules firing on it has no dependents (an empty `claim_list`). ``` 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**: | verb | anchored form | what it answers at that time | |---|---|---| | `current` | `current(K.s.a, t"…")` | the single value active then | | `get` | `get(K.s.a, t"…")` | the claims valid then | | `why` | `why(K.s.a, t"…")` | the derivation as it stood then (§5.3) | | `list_subjects` | `list_subjects(K, t"…")` / `list_subjects(K.a, t"…")` | the subjects a traversal finds | | `list_values` | `list_values(K.a, t"…")` | the values recorded at the attribute | | `list_attributes` | `list_attributes(K.s, t"…")` | the attributes the subject carries | 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 #### `list_result_types()` → `result_type_set` The set of read-result-type names. ``` rts = list_result_types() ``` ### 5.6 Script-data reads (in-language) Read-only, so they **run inside a program**. #### `list_scripts()` → `string_list` Bare names of every stored script. ``` 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. | Wire form | What it does | |-----------|--------------| | `compile from ""` | provide + store + **run** a module; its `def`s become callable by name (§7.11) | | `compile ` | reload a stored module by name — re-run its body (§7.11) | | `run from ""` | **execute instructions WITHOUT storing anything** — "try it" to `compile`'s "keep it" (MCP §4.2). A program reads, writes, and calls compiled scripts; a definition (`def` / `class` / `@rule` / computed field) belongs to `compile`. To call stored code: `import ` then `.(...)` | | `list scripts` | list signatures (also runs in-language) | | `forget script ` | remove a script (idempotent) | | `info script ` | compile provenance | | `list rules` | list the names of your standing rules (§8.8) | | `list modules` | list stored modules — name, script count, created-at (MCP §9.4) | | `info module ` | a module's record — init language, its `module.script` names, the classes it declares, its `version` if it has one, updated-at, created-at; `` is BARE (MCP §9.4) | | `forget module ` | delete a whole module + its scripts, kinds, and data; needs `confirm`; refuses on a live cross-module reference; `` is BARE (MCP §9.4) | | `forget rule ` | remove ONE standing rule and withdraw what it derived, leaving the rest of its module in place; `` is the `module.rule` name from `list rules` | | `checkup` | report your store against the standing rules over it — which premise cells hold nothing, which of your kinds no rule reads (§8.8) | The in-language `import ` 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 `def`s become callable by name, its rules stand); an inline `run` **executes it once and stores nothing** — data it `remember`s 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 `compile`d 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, )` — the ``-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. Operators DKE Python uses **word-form logical operators** (`and` / `or` / `not`), the comparisons `== != < > <= >=`, and the arithmetic / concatenation operators `+ - * / %`. ### 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, list)`, 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 * ` (either order) stretches it (`duration("PT1H") * 2.5` is `PT2H30M`) and `duration / ` 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, ` / 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` (§6.7), `x in s` over a `set` (§6.10), `k in d` over a `dict` (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 in :` 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=`** 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(, 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` for two `int`s, `tuple` 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` 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=])` / `any(xs)` / `all(xs)`** — `sorted` returns a **new** `list` 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` from a `list>` of pairs — `dict(zip(keys, vals))`; `tuple(x)` collects the elements into a **variadic homogeneous tuple** `tuple` (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 `string`s** 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`, differing scalars → `list` (`[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 + tuple` is `tuple`, 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` indexes and slices by the same rules (`xs[i]`, negative from-end permitted; `xs[a:b:c]` yields a new `list`); 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` — 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` — 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` `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` — 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` — 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` on the client side (immutable, bounded, never round-trips the service). Elements are inferred to a common type: homogeneous → `list`, mixed scalars → `list`, empty `[]` → `list`; lists nest. The empty list is compatible with any `list` — 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>`), `",".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> 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` 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, 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 x = point[0] # 3 — constant index mixed = (1, "ana", True) # tuple same = (3, 4) == point # True wide = point + (5,) # tuple ``` ### 6.9 Dicts A **dict literal** `{k1: v1, k2: v2}` builds a constructed `dict` 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`, `d.values()` → `list`, and `d.items()` → `list>`, 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` 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`); 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`; - **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` — 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` 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>` — pairs elements position by position, up to the **shortest** input (`zip(["a", "b"], [1, 2, 3])` yields two tuples). - `enumerate(xs [, start])` → `list>` — 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. Statements Every statement is one logical line, or a `:`-headed block with an indented suite. Indent with **spaces only**. ### 7.1 Declaration ``` def audit(K: string, s: string): 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`, `set`, `dict`, `tuple`, nestable (`dict>`) — so a collection crosses a function boundary as an argument or return value (`def total(xs: list) -> int:`, `def doubled(xs: list) -> list:`). 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` (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 = e` is equivalent to `x = x 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, , )`. An **annotated assignment** `x: = ` gives the binding its type explicitly (`n: int = 5`, `xs: list = [1, 2, 3]`); the annotation must agree with the initializer, and a bare `x: ` with no value is rejected (write `x: = `). **Chained assignment** `a = b = ` binds every target to one value (evaluated once). **Tuple unpacking** `a, b = ` 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() ``` Appends ``'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` 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 `return`s, 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 : elif : else: ``` `` 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: ``` Iterates a **finite collection** — a store-derived collection, a constructed `list` (§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 ` arm; the one read-only class, `null`, is a bare arm only — attaching `as ` 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 ` 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 ` 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: except refuse as r: except engine_error as e: else: # runs only if the body raised nothing finally: # always runs, last ``` Python's own `except … [as …]:` shape. Both handlers are optional, and so is each handler's `as ` 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(""):` 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 ` **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 from ""` stores a module by name and runs it (§5.7). Every module in a store arrived that way. The bare `import ` 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 `** 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 ` 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 " 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. Classes, methods, and reasoning Classes group typed **fields** with the **methods** over them and give a typed handle — an **instance** — for one named member (§8.1–8.6). A class may **extend** another, inheriting its fields and methods (§8.10), and `isinstance` tests an instance's class (§8.11). The section then covers the **derivation** features — computed fields (§8.7), standing rules (§8.8), and hypothesis (§8.9) — where the engine records or supposes values on your behalf. The class surface adds no new types and no new verbs; termination is preserved throughout. `class` and `return` are keywords. ### 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 :` — **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 ` of that type, or local `name = ` 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 :` 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_error`s. ### 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 in (, in )*` — 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 (and )*` — every premise must hold: | premise | example | holds when | |---|---|---| | comparison | `o.total > 1000` | the field stands in that order (`< <= > >=`) to the bound. A numeric bound may be negative (`r.temp < -10`); a quoted bound (`o.name < "m"`) orders the field alphabetically instead. The two readings never mix, so a field carrying both text and numbers never answers by accident. | | equality | `o.lic == "MIT"` | the field holds exactly that value — a quoted string, an integer (negative included), or `True` / `False`. Over numbers it reads the **number**: `o.total == 5` holds for `5.0`, and not for the text `"5"`. | | inequality | `o.total != 5` | the field holds some **recorded** value other than the given one. A field with no value holds neither `==` nor `!=` — comparing against nothing is not a comparison. Ask that with `absent`. | | join | `c.caller == f` | the field holds another subject the rule binds. The right side is one of the `for` names, not a value: that is how a rule relates two subjects to each other. `==` also **ranges** the name on its right, so the conclusion may be about it; `!=` does not. The right side is a subject; to compare against a second **field**, write that field — the next row. | | field comparison | `o.delivered > o.deadline` | the two fields' stored values stand in that order — numerically between numbers, chronologically between instants, alphabetically between texts — or are equal / unequal under `==` / `!=`. Both fields must have a value: a subject with no `deadline` has nothing to be late against and is not concluded about. The two may belong to the same subject or to different subjects the same `for` binds (`c.amount > l.cap`). One token separates this from a join — a bare subject on the right is a join, a subject followed by a field is this. A specific subject (`Order.o1.total`) cannot be named on the right; a rule ranges over the subjects it binds, and `current(...)` is what asks about one | | relation | `Reach.x.y == True` | the three-segment path holds that value, with **bound names** in its last two slots. It binds both names, and a bound name in the field position asks for **every** cell of that subject rather than requiring one to be known. | | absence | `absent(o.shipment)` | the subject has **no value recorded** for that field — missing information, not a field recorded as `false` or empty. The stricter of the two cell-negatives: a value a rule concluded makes it false. | | not asserted | `not_asserted(b.flies)` | **nobody has recorded a value** for that field. Narrower than `absent`: it reads only what people wrote, so a value a rule concluded leaves it holding. Shape-only — there is no form taking a value, because *did a person record THIS value* is answered by reading the field. Ranges no subject, as `absent` does not. | | nonexistence | `none(c in Call: c.caller == f and c.tainted == True)` | **no row of that kind satisfies every premise inside**. Where `absent` asks about one cell of one subject, this asks about a whole set. The inner premises are the ordinary premise grammar and may name the outer rule's rows — `c.caller == f` is what ties the set to the subject being concluded about. It holds **vacuously** for a subject the set never mentions: a function with no callees at all satisfies "none of its callees is tainted". That is also why it is enough on its own to say which subjects a rule applies to, where an `absent` is not. A `none(...)` inside another is refused; conclude the inner one into a field with its own rule and quantify over that. | - `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. ```python @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 (`__none`, 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 ` = ` 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 `.`, a field of a subject the `for` clause bound, or the three-segment `..` 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, ` = ()` or ` = (.)` — `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 ` removes ONE standing rule and reclaims what it derived, leaving the rest of its module in place; `` 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 .` 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 ` for a kind of yours no rule reads, `violated …` 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(, , …, )` 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 `, ` 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(, …, )` 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. Modules A `.dpy` source file is a **module** — the unit you submit, store and import. Modules introduce no new types (§4) and no new verbs (§5): a module body is written in the language already described here, and compiling or importing a module is the operation that runs that body. ### 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 ` 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 ``` Loads a module already stored under ``: it makes that module's names available (§9.6) and runs its body once (§9.1). `` 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 ` resolves `` 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](/ref/dke/reasoning-modules/) — 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. --- ## 10. Errors Two static diagnostic kinds; runtime adds two catchable outcomes. | Category | Stage | Recoverable in source? | |----------|-------|------------------------| | parse (`parse_error`) | static — token structure | no | | type (`type_error`) | static — semantic rule | no | | `refuse` | runtime — verb call | yes, via `except refuse as` | | `engine_error` | runtime — service layer | yes, via `except engine_error as` | Common triggers: - **parse** — tab in indentation or a bad dedent; unterminated string; reserved word (`class`, `return`, …) as an identifier; an empty module (whitespace and comments only). - **type** — undeclared identifier; a wire-only script verb in a program body; a non-exhaustive `match`; a `for` over a non-collection; a type mismatch; a non-existent field. - **`refuse`** — the store rejects a well-formed request: out-of-surface slot, wrong slot count, index out of bounds, division / modulo by zero, integer overflow, `commit` outside a branch. Also a service budget on how much one run may build — see below. - **`engine_error`** — the service composed a well-formed request that failed at the engine layer. **A service budget is not catchable.** A service may limit how much data a single run builds. This is separate from the language's own guarantees: bounded iteration bounds how LONG a program runs, not how much it HOLDS at once, so a program can terminate as promised and still build more than the service will hold. Such a limit is reported as a refuse but `except refuse` does not catch it — a handler able to swallow a resource limit could retry inside a bounded loop and defeat it. Build fewer values in one run, or split the work across runs. --- ## 11. Accessors and field tables ### 11.1 Universal accessors - `.kind → string` — for any discriminator and for `proof_tree`. - `.length → int` — for any `string` (its character count — Unicode characters, not bytes) or finite collection (its element count). ### 11.2 Field access by type | Type | Field | Field type | |------|-------|------------| | `active_claim` | `value` | `value` (union; §4.1) | | `active_claim` | `source` | `string` | | `active_claim` | `path` | `string` (cell path `K.s.a`; the cell a `dependents`/`conflicts` claim lives at) | | `active_claim` | `claim_id` | `string` (positional `path#n`, not stable) | | `active_claim` | `created_at` | `string` (RFC 3339 UTC µs; empty for pre-stamping claims). Orders claims, does not measure elapsed time — compare it, never subtract it; use `duration` to record how long something took. Claims recorded in the same microsecond share a stamp and tie under sorting | | `active_claim` | `trust` | `string` — how the claim came to hold its value: `asserted` (someone recorded it) or `derived` (a rule concluded it). Engine-established, never caller-asserted: citing `"derived"` as a `source` still reads `asserted` | | `active_claim` | `preferred` | `bool` (a recorded judgment says act on this one) | | `active_claim` | `maintained` | `bool` — `False` when the claim holds a derived value its rule can no longer keep current: the value is the last one that rule produced, and the data behind it has moved on. `True` for every asserted claim and every derivation still being kept current. Not a conflict and not a preference — nothing disagrees, the value is simply not being kept up, and every read still serves it. Established at read rather than recorded on the claim, so it appears as soon as the rule stops keeping the value current and clears on its own; read it alongside the value it qualifies rather than carrying it forward | | `active_claim` | `written_by` | `string` (the access key that wrote the claim; empty when **no key wrote it** — either the write was not authenticated, or a rule concluded the claim and there was no write. `trust` tells those apart; `why` accounts for a derived claim as a key accounts for a written one). Observed, never asserted — contrast `source`, which the writer states | | `active_claim` | `valid_from` | `value` (union; §4.1) — the start of the claim's **validity window**: the world-time it says something about, as distinct from when it was recorded. The `null` class when the claim has no start bound, so read it by matching, never by comparing against a sentinel instant. A conclusion carries the overlap of its premises' windows | | `active_claim` | `valid_to` | `value` (union; §4.1) — the end of that window, `null` when the claim has no stated end. Only the `datetime` and `null` classes ever arise for either field, but a `match` still needs a `case default:` arm: exhaustiveness is checked against the whole union | | `proof_tree` | `root` | `active_claim` | | `proof_tree` | `truncated` | `bool` (`True` when the proof stops short of the whole derivation) | | `verify_result` | `match` | `bool` | | `verify_result` | `actual` | `string` (the value that stands; empty at a location that is unwritten **or** in disagreement — `conflicted` tells you which) | | `verify_result` | `expected` | `string` | | `verify_result` | `conflicted` | `bool` (the location holds competing values, so there is no single `actual`; `match` still answers over all of them. A source-scoped `verify(K.s.a, v, src)` is never marked) | | `refuse_info` | `reason` | `string` — what was refused, written for a reader and in the script's own language. Report this | | `refuse_info` | `teaching_hint` | `string` — how to correct the call; empty when there is no suggestion. An aid to a human reader, never a second reason and never something to branch on | | `refuse_info` | `discriminator` | `string` — a short tag naming which refusal this is, for a program that must branch rather than report. The tag set is not part of this contract (§4.2); a refusal from your own `raise (…)` carries the exception name you wrote | | `engine_error_info` | `reason` | `string` — what failed, written for a reader | | `engine_error_info` | `code` | `string` — a short tag naming which failure this is, in the role `discriminator` plays for a refusal. The tag set is not part of this contract (§4.2) | 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 | Value | `[int]` yields | |------------|----------------| | `claim_list` | `active_claim` | | `proof_tree` | `active_claim` | | `string_list` | `string` | | `subject_set` | `string` | | `result_type_set` | `string` | | `string` | `string` (the one character at that position) | | `list` | `T` (negative from-end index permitted) | | `tuple` | the indexed position's type (**constant** index only) | | `dict` | `V` (indexed by a key of type `K`, not an `int`) | 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 | Method | Result | |--------|--------| | `s.find(sub)` | `int` — first character position of `sub`, `-1` if absent | | `s.count(sub)` | `int` — number of non-overlapping occurrences (empty `sub` = `length + 1`) | | `s.startswith(prefix)` / `s.endswith(suffix)` | `bool` — whether `s` begins / ends with the argument (a string, or a tuple of strings → any of them) | | `s.replace(old, new)` | `string` — copy with all occurrences of `old` replaced (empty `old` inserts `new` in every gap) | | `s.upper()` / `s.lower()` | `string` — full Unicode case mapping (may expand, e.g. `ß`→`SS`, so length can change; `lower` applies the Greek word-final `Σ`→`ς` rule) | | `s.strip([chars])` / `s.lstrip([chars])` / `s.rstrip([chars])` | `string` — remove characters from both ends / left / right (whitespace, or the `chars` set) | | `s.partition(sep)` / `s.rpartition(sep)` | `tuple` — split once at the first / last `sep` into `(before, sep, after)` | | `s.splitlines()` | `list` — the lines of `s`, split at `\n` / `\r\n` / `\r` | All are total (never refuse) and count characters, except `partition` / `rpartition`, which refuse on an explicit empty separator. --- ## 12. Keywords The keyword surface **localises per natural-language surface**, and the surface is chosen per call (MCP §8.1, which names the tag for each). This Reference describes the English one, where the structural keywords are English: `def` `class` `return` `match` `case` `if` `else` `for` `in` `try` `except` `as` `branch` `commit` `rollback` `and` `or` `not` `print` `True` `False`. Verb head-words (`remember`, `current`, `get`, …) and their prepositions (`of`, `where`, `since`, `per`) localise correspondingly (§5), and on this surface they are the English spellings this document uses throughout. Two words keep their English spelling on every surface, and a program written in another one writes them in English or the call is not recognised: the two diagnostic verbs. They are not held back by the surface — they exist only in English, so there is no other spelling to write instead. Everything else in the keyword surface localises, including the `except` handler kinds, `print`'s keyword arguments, the method receiver, and the compound verb heads, each of which appeared in this list until they did. **English on every surface.** `why_not` `what_needs` `import` (§7.11) is a **contextual keyword** — the import statement only at statement head, an ordinary identifier elsewhere. Type names (`string`, `int`, …) are likewise contextual, not reserved — but avoid all of these as identifiers. --- ## 13. Quick reference card ``` DECLARE def name(K: string, n: int): # `def`; name: type params ASSIGN hist = get(K.s.a) # bare assignment (no let) PRINT print("x = " + str(n)) # string|int|bool|discriminator WRITE remember(K.s.a, v, src) update(K.s.a, v, src) forget(K.s.a) assert(K.s.a, src) pin(K.s.a) forget(K.s) unpin(K.s.a) READ current(K.s.a) -> active_claim get(K.s.a) -> claim_list why(K.s.a) -> proof_tree verify(K.s.a, v[, src]) -> verify_result why_not(K.s.a) -> diagnosis what_needs(K.s.a) -> diagnosis subjects(K.a, v) -> subject_set list_attributes(K) -> string_list caveats(K.s) conflicts() list_values(K.a) list_subjects(K[.a]) LISTS list_categories() list_pinned() list_scripts() list_result_types() SCRIPT list_scripts() -> string_list TYPES string int bool | active_claim verify_result empty (discriminators) claim_list proof_tree diagnosis string_list subject_set result_type_set (collections) | handle OPS == != < > <= >= (int cmp) and or not (bool) + - * / % (int) + (string concat) .field [i] COLLS [1, 2, 3] list (1, "a") tuple {"k": 1} dict {1, 2} set # constructed, client-side xs[i] xs[a:b] x in xs .length [e for x in xs if c] zip(a, b) enumerate(xs) sum(xs) min(xs) max(xs) min(a, b, c) # reduce (vs sum(K.col) store fold) sorted(xs) sorted(xs, reverse=True) any(xs) all(xs) bool(x) tuple(xs) d[k] d.get(k, x) k in d d.keys() d.values() d.items() s.union(t) s.intersection(t) IF if c: … / else: … FOR for c in list: … # finite collections only (list / dict-keys / set) MATCH match d: case active_claim: … / case empty: … TRY try: … / except refuse as r: … / except engine_error as e: … BRANCH branch b: … commit / rollback CALL name(args) # plain call; no call keyword CLASS class Sensor: temp: string def record(self, v: string, src: string): remember(self.temp, v, src) def label(self) -> string: return "sensor" INSTANCE s = Sensor(room) remember(s.temp, "21", "op1") s.record("22", "op1") reading = s.temp name = s.label() match s: case Sensor: … / case default: … ERRORS parse type (static) refuse / engine_error (runtime, catchable) HELP --help [header|types|verbs|statements|scripts] ``` --- ## 14. Python tooling and type checking DKE Python is a Python-syntax surface: a standard Python parser accepts `.dpy`, so **formatters** (black), **linters** (ruff / flake8), **language servers**, and syntax highlighting work on `.dpy` files as they stand. For **type checkers** (pyright / mypy), which additionally want every name in scope, DKE ships a stub, **`dke.pyi`**, declaring the builtin surface — the verbs, the value factories, the type names, the `@rule` decorator, and the `branch` context manager, none of which the source imports. A checked copy that opens with the one-line prelude `from dke import *` then type-checks; the service compiles the original headerless source unchanged. The core surface (verbs, slot paths, values, control flow, rules, aggregates, transactions) checks clean. Two DKE constructs mean something different to a Python checker than to the DKE service — kinds-as-classes construction (`Sensor(room)`) and the `case as :` type match — so relax the codes they trigger (the `dke.pyi` header lists the exact settings). The DKE service remains the authority on types. --- *Companion documents: the [**Tutorial**](/tutorial/dke/python/), which teaches this language in task order, and the [**Wire & Tool Contract**](/ref/dke/mcp/), which specifies the transport that carries a program to the service.*