# DKE Python — Language Specification **Version:** alpha · API 1 **Status:** Published normative specification. **Audience:** Tenants writing DKE Python; authors of third-party tooling (linters, formatters, syntax highlighters, language servers, IDE plugins, alternative compilers). **This document as Markdown:** [dke-python-spec.md](/spec/dke/python/dke-python-spec.md) — the same text this page is rendered from, for the tooling authors above who would rather read the source than the page. --- ## 1. Status and scope This document is the **normative specification** of **DKE Python** — the language a DKE tenant writes and submits to the DKE service at `dke.langsyn.net`. DKE Python is a Python-flavoured concrete surface over DKE's knowledge-operation semantics. Source files use the extension `.dpy`. The language and this specification are open under the MIT license; the DKE service that runs DKE Python is LangSyn's proprietary product and is not open. Third parties are free to implement compilers, linters, formatters, syntax highlighters, language servers, IDE plugins, and alternative tooling against this document. A DKE client sends DKE Python source over the wire; DKE compiles, stores, and executes it. The published surface is the language; the implementation that runs it is LangSyn's product. ### 1.1 Conformance An implementation of DKE Python is **conforming** when, for every input program that this specification classifies as accepted, the implementation parses and accepts the program with the static-semantics outcomes this specification prescribes; and for every input program this specification classifies as rejected (parse_error, type_error), the implementation rejects it with the error class this specification names. Runtime outcomes (refuse, engine_error) are observable but depend on the target store's state; conformance applies to the SHAPE of those outcomes (status discriminator, transcript shape), not to the data. A third-party compiler that emits something other than what DKE emits internally is conforming as long as the **observable behaviour** matches: same input source plus same target store plus same arguments produces a transcript with the same shape and the same status discriminators across statements. The conformance keywords **MUST**, **MUST NOT**, **SHOULD**, **SHOULD NOT**, and **MAY** in this document carry their RFC 2119 meanings. ### 1.2 Relationship to DKE DKE Python is the contract between a tenant and the DKE service. Three documents divide that contract between them: - **this specification** — the **language**: lexical structure, grammar, type system, static and dynamic semantics, and the built-in verb surface; - the [DKE Wire & Tool Contract](wire/) — the **transport**: the tool surface, request shapes, response envelope, error model and billing, and the wire-visible behaviour of the compile/store/run lifecycle; - the [DKE Python Modules contract](modules/) — the **unit of submission**: what a module is, how `import` resolves one, and what re-submitting one does to a store. Internal storage shapes, code-generation strategies, and execution mechanisms are intentionally out of scope — they are the implementation's choices, and a conforming client must not rely on them. ### 1.3 Spec versioning This is an **alpha** release of the **DKE Python Spec**, describing **API version 1**. DKE Python is a Python-flavoured surface end to end: - **Declarations use `def`.** `def audit(K: string, s: string):` — the Python function-definition shape, with a `:`-headed indented body. - **Verbs are function calls.** The built-in verb surface (§7) is written as calls, e.g. `remember(K.s.a, v, src)`, `current(K.s.a)`, `list_attributes(K)`, `print(msg)`. - **Bare assignment binds a read.** `cur = current(K.s.a)` — there is no `let` introducer. - **`match` / `case`.** Discrimination is spelled `match :` with `case :` arms (where the base member uses `when`). - **`try` / `except`.** Handled blocks use Python's `except [as ]:` shape; the `as ` binding is optional (`except refuse:`). - **Script invocation is a plain call.** `audit_subject(K, s)` — there is no call keyword in the language; a program reaches a stored script by importing its module and calling it qualified (Wire §4.2, Reference §9.6). - **Word-form logical operators.** `and` / `or` / `not`. ### 1.4 What this specification does NOT define - The wire transport between the client and the target service. - The storage format used by the service to retain compiled scripts. - The internal representation of types at runtime. - DKE's error message text (only the error category is normative; message strings are quality-of-implementation). - Operational characteristics: performance, latency, quotas, throttling. ### 1.5 Independence from a live service This specification is **forward-looking**: it defines the conformance contract for any implementation of DKE Python and for the target service at `dke.langsyn.net`, independent of whether a given target service is reachable when this document is read. Parser/checker conformance (§12.1) does not depend on a live target. Third parties can build conforming parsers, type-checkers, linters, formatters, syntax highlighters, language servers, and IDE plugins against this specification and test them in isolation per §12.2. Compiler/runtime conformance (§12.1) is claimed against whichever target service an implementation connects to. --- ## 2. Notation Grammar productions use a small EBNF variant: - `lowercase` — non-terminal. - `'literal'` — terminal (matched verbatim, case-sensitive). - `UPPERCASE` — token class (defined in §3). - `A | B` — alternative. - `A B` — sequence. - `A?` — zero or one occurrence. - `A*` — zero or more occurrences. - `A+` — one or more occurrences. - `( A )` — grouping. - `NEWLINE`, `INDENT`, `DEDENT` — the layout tokens the lexer emits from the off-side rule (§3.2). - `# ...` — informal note. Where lexical and syntactic productions both apply, lexical rules take precedence (tokens are recognised first; the parser consumes the token stream). --- ## 3. Lexical structure ### 3.1 Source encoding DKE Python source MUST be valid UTF-8. A conforming implementation MUST reject ill-formed UTF-8 sequences with a parse_error that names the offending byte offset (and SHOULD name the invalid byte). ### 3.2 Whitespace, line terminators, and the off-side rule DKE Python is **indentation-significant**. Line feed (U+000A) and the carriage-return / line-feed pair both end a source line. A block is introduced by a header line ending in `:` and is delimited by indentation: ``` def f(K: string): ``` - Indentation is measured in **spaces**; a tab in indentation is a lexical error (parse_error). - A deeper indent opens a nested block (the lexer emits `INDENT`); returning to a shallower level closes as many blocks as needed (`DEDENT`). An indent that matches no open level is a parse_error. - Blank lines and comment-only lines do not affect block structure. - Inside `(` and `[`, newlines are not significant: a bracketed expression may span lines. - A backslash immediately before a line feed is an **explicit line continuation**: the two physical lines join into one logical line (no `NEWLINE` is emitted and the continuation line's leading spaces are not indentation). The `\` MUST be the last character on the line; a `\` followed by anything other than the line ending is a parse_error. ### 3.3 Comments A `#` begins a comment that runs to the end of the line. Comments are equivalent to whitespace and do not affect block structure. ### 3.4 Identifiers DKE Python identifiers follow **Unicode UAX #31** with the standard profile: ``` identifier := XID_Start XID_Continue* # written in NFC ``` An identifier starts with any codepoint having the Unicode `XID_Start` property and continues with any codepoint having `XID_Continue`. **Every script Unicode defines is available**, including those outside the Basic Multilingual Plane — Latin, `æ ø å`, CJK ideographs, Arabic, Hebrew, Devanagari, Thai, Armenian, Georgian, Tamil, Hiragana, Katakana, Hangul, Cyrillic, Greek and the rest, together with the decimal digits and the marks a script needs to spell its words. The `_` underscore is identifier-start by convention. **A name is written in Normalization Form C**, so it has one spelling and two names that look alike are alike. Where NFC composes, the composed codepoint is the name and the sequence is not: `é` is U+00E9, never `e` followed by U+0301. Where NFC does not compose, the marks are part of the name: `بِسْم` and `बिल्ली` carry their vowel marks, and `क़ीमत` begins with `क` followed by the nukta U+093C — the precomposed U+0958 is the spelling normalization removes. Whether a mark composes can depend on the letter before it, so the rule is about the **sequence**, not the codepoint: `أ` is U+0623, never `ا` followed by U+0654, while the same U+0654 after a letter it does not compose with is an ordinary part of a name. Writing a name in any other form is a parse error naming what differs and the letter to write instead. Identifiers are case-sensitive: `Cat`, `cat`, and `CAT` are distinct. ### 3.5 Literals #### 3.5.1 String literals ``` string-literal := '"' string-char* '"' | '"""' triple-char* '"""' # triple-quoted (may span lines) triple-char := any UTF-8 codepoint except '\' and the closing '"""' | newline # a literal line feed (U+000A) | # same escape grammar as below string-char := any UTF-8 codepoint except '"', '\', and newline | '\\' # backslash | '\"' # double quote | '\n' # line feed (U+000A) | '\t' # horizontal tab (U+0009) | '\r' # carriage return (U+000D) | '\a' # bell (U+0007) | '\b' # backspace (U+0008) | '\f' # form feed (U+000C) | '\v' # vertical tab (U+000B) | '\x' hex hex # one byte, two hex digits | '\u' hex×4 # one codepoint ≤ U+FFFF, UTF-8 encoded | '\U' hex×8 # one codepoint ≤ U+10FFFF, UTF-8 encoded | '\N{' name '}' # a codepoint by its Unicode name hex := '0'..'9' | 'a'..'f' | 'A'..'F' name := (letter | digit | ' ' | '-')+ # a Unicode character name ``` A conforming implementation MUST reject an unterminated string literal (newline or end-of-source before the closing `"`) with a parse_error. The `\x` escape denotes exactly two hex digits (one byte); `\u` denotes exactly four hex digits (one codepoint ≤ U+FFFF); `\U` denotes exactly eight hex digits (one codepoint ≤ U+10FFFF, the only escape able to name a codepoint above the BMP). Each is encoded as UTF-8. A `\u`/`\U` value in the surrogate range `U+D800`..`U+DFFF`, or a `\U` value above U+10FFFF, is rejected. The `\N{name}` escape denotes the codepoint whose Unicode character name is `name`, encoded as UTF-8 — e.g. `\N{BULLET}` is `•` (U+2022), `\N{GREEK SMALL LETTER ALPHA}` is `α`, and `\N{CJK UNIFIED IDEOGRAPH-4E00}` is `一`. **Every** named character is recognized, across all scripts — Latin, Greek, Cyrillic, Arabic, Devanagari, the CJK ideographs, Hangul syllables, and the rest. The name is matched **case-insensitively** but is otherwise exact (interior spaces and hyphens are significant; no leading or trailing space). A name Unicode does not assign is a parse_error. **No NUL byte.** Any escape that would produce a NUL byte — `\0`, the `\x00` byte escape, or a `\u` escape denoting U+0000 — is a parse_error, keeping string values C-string-safe end-to-end. Other escape sequences are reserved and MUST be rejected; future spec versions MAY assign them. **Adjacent literal concatenation.** Two or more string literals separated only by whitespace are concatenated into a single string at compile time, with no `+` operator: ``` "long text " "split over lines" # same value as "long text split over lines" "a" "b" "c" # same value as "abc" ``` The merge is a compile-time fold — the result is indistinguishable from the spelled-out literal. An **f-string** participates, in either order and in any mixture, and the whole adjacent run folds together: `f"a" "b"`, `"a" f"{x}"`, `f"{x}" f"{y}"` and `"a" "b" f"{x}" "c"` all concatenate. A run containing an interpolation is a single interpolated string, not a chain of joins, so it costs exactly what the one f-string it replaces costs. This is the idiomatic way to write a long interpolated message across lines: ``` message = ( f"hello {name} " "and welcome" ) ``` A **typed-value literal** — `t"…"`, `d"…"`, `x"…"`, `b64"…"`, `sci"…"` — does NOT participate, in either order: concatenation joins strings, and these are not strings. `t"2026-01-01T00:00:00Z" "x"` is a parse_error; render such a value with `str(…)` and join with `+`, or interpolate it in an f-string. **Triple-quoted strings.** A string may be delimited by `"""` instead of a single `"`. A triple-quoted literal ends only at the next `"""`, so it MAY span multiple lines — each embedded newline is a literal line feed (U+000A) — and a lone `"` or `""` inside it is ordinary content. The escape grammar is identical to a single-quoted string, and the leading newline (if the literal opens with one) is part of the value; there is no indentation stripping. The result is an ordinary `string` — the delimiter is purely lexical. An unterminated triple- quoted literal (end-of-source before the closing `"""`) is a parse_error. A triple-quoted **f-string** (`f"""…"""`) is not currently defined and is a parse_error. ``` banner = """usage: run """ # a two-line string with an embedded newline quoted = """he said "hi""" # value: he said "hi — the literal ends at the # first """, so the quote before it closes nothing # and no quote survives at the end tail = """he said "hi\"""" # value: he said "hi" — escape the last quote to # keep it ``` #### 3.5.2 Integer literals ``` int-literal := dec-int | hex-int | oct-int | bin-int dec-int := dec-digit ( '_'? dec-digit )* hex-int := '0' ( 'x' | 'X' ) '_'? hex-digit ( '_'? hex-digit )* oct-int := '0' ( 'o' | 'O' ) '_'? oct-digit ( '_'? oct-digit )* bin-int := '0' ( 'b' | 'B' ) '_'? bin-digit ( '_'? bin-digit )* ``` Integer literals are decimal by default; the `0x` / `0o` / `0b` prefixes (case-insensitive) select base 16 / 8 / 2. A single `_` may separate digits (`1_000_000`, `0xDE_AD`) and may also directly follow a base prefix (`0x_FF`); it may not otherwise lead, and it may not trail or double. A decimal literal with a **leading zero** and a nonzero digit is rejected (`010`, `007`) — octal requires the explicit `0o` prefix; an all-zero run (`0`, `00`, `0_0`) is the integer zero and is legal. A leading `-` is the prefix unary-minus operator (§4.4, §8.3), with one exception: `-9223372036854775808`, the smallest integer, is a literal. Its magnitude alone (`9223372036854775808`) is out of range and stays a parse_error, so the sign is part of this literal rather than an operator applied to it. The exception is exactly that one spelling — a **binary** minus is unaffected, so `1 - 9223372036854775808` remains a parse_error for its out-of-range operand. Integer values fit a signed 64-bit two's-complement range, and any other literal outside it is a parse_error. #### 3.5.3 Boolean literals ``` bool-literal := 'True' | 'False' ``` `True` and `False` are reserved words (§3.7). #### 3.5.4 No null literal DKE Python has no null literal. Absence-of-value is not expressible in the lexical surface; see also §5.1 (no absence-of-value type). The in-language way to assert that a value is absent at `K.s.a` is the `assert` verb (§7.1), which carries no value argument — the absence semantic is implicit in the verb head-word, not in a literal. #### 3.5.5 Datetime literals ``` datetime-literal := 'datetime' '(' '"' rfc3339-utc '"' ')' rfc3339-utc := date 'T' time frac? 'Z' date := dec-digit dec-digit dec-digit dec-digit '-' dec-digit dec-digit '-' dec-digit dec-digit # YYYY-MM-DD time := dec-digit dec-digit ':' dec-digit dec-digit ':' dec-digit dec-digit # HH:MM:SS frac := '.' dec-digit{1,9} # 1..9 fractional-second digits ``` A datetime literal denotes an **instant in UTC**, written as the factory call `datetime("")` over an RFC 3339 timestamp — e.g. `datetime("2026-01-02T03:04:05Z")`. Its static type is `datetime` (§5.1); its value class is `datetime` on the read side (§5.6). (The leading-prefix spelling `t"…"` is also accepted as a legacy form.) The argument is a single string literal. The trailing `Z` (UTC designator) is required. Fractional seconds are optional and carry 1 to 9 digits. A datetime whose text is not a well-formed RFC 3339 UTC timestamp — a missing `Z`, a malformed field, or more than 9 fractional digits — is a **parse_error**. (The field ranges — month `01`..`12`, a valid day, and so on — are validated by the target service; a value that is lexically well-formed but denotes no real instant is a runtime refuse.) Two datetime values that denote the same instant are equal; a value reads back with insignificant trailing fractional zeros removed, so `datetime("2026-01-02T03:04:05.500Z")` reads back as `2026-01-02T03:04:05.5Z` and `datetime("2026-01-02T03:04:05.000Z")` as `2026-01-02T03:04:05Z`. #### 3.5.6 Duration literals ``` duration-literal := 'duration' '(' '"' iso8601-duration '"' ')' iso8601-duration := '-'? 'P' days? ( 'T' hours? minutes? seconds? )? # >= one term days := dec-digit+ fraction? 'D' hours := dec-digit+ fraction? 'H' minutes := dec-digit+ fraction? 'M' seconds := dec-digit+ fraction? 'S' fraction := '.' dec-digit{1,9} # lowest-order term only ``` A duration literal denotes a **length of time**, written as the factory call `duration("")` over an ISO 8601 duration — e.g. `duration("PT1H30M")` (one hour thirty minutes). Its static type is `duration` (§5.1); its value class is `duration` on the read side (§5.6). (The leading-prefix spelling `d"…"` is also accepted as a legacy form.) The argument is a single string literal: a leading `P`, an optional day term `D`, and an optional time part introduced by `T` carrying any of `H`, `M`, `S` in that order; at least one term is required. Calendar years and months are **not** accepted (they have no fixed number of seconds). A duration whose text is not a well-formed ISO 8601 duration of this subset — a missing `P`, a stray unit, units out of order, or a bare `T` — is a **parse_error**. **Sub-second durations.** The lowest-order term present may carry a decimal fraction of up to nine digits, so `duration("PT0.5S")`, `duration("PT1.5H")` and `duration("PT0.000000123S")` are all well formed. Only the last term may be fractional — `duration("PT1.5H30M")` is a **parse_error**, since a fraction on a term followed by smaller terms is ambiguous. Durations are exact to the nanosecond: `duration("PT0.1S")` is exactly one tenth of a second, not the nearest binary approximation of it. A span must fit within roughly ±292 years; a longer one is a **parse_error** rather than a silently wrapped value. A duration reads back in a **canonical** form: equal durations render identically and smaller units roll up into larger ones, so `duration("PT90M")` reads back as `PT1H30M` and `duration("PT1.5H")` does too. A sub-second remainder reads back as a decimal fraction on the seconds term with trailing zeros removed, so `duration("PT1.500S")` reads back as `PT1.5S` and a whole number of seconds carries no fraction at all. Two durations that denote the same length are equal regardless of how they were written. **Negative durations.** A leading `-` negates the whole span, so `duration("-PT2H")` is two hours *backwards*. A leading `+` is not accepted — positive is the default and the sign would say nothing. Negative spans arise naturally from arithmetic (§8.3): subtracting a later instant from an earlier one gives one, and it renders with the same leading `-`, so every value the language computes is a value the language can also write. #### 3.5.7 Real literals ``` real-literal := int-part '.' frac-part? exponent? # 3.5, 5. (trailing dot), 1.5e-3 | '.' frac-part exponent? # .5 (leading dot), .5e2 | int-part exponent # 1e5 (exponent, no point) int-part := dec-digit ('_'? dec-digit)* frac-part := dec-digit ('_'? dec-digit)* exponent := ('e' | 'E') ('+' | '-')? dec-digit ('_'? dec-digit)* ``` A real literal denotes a **fractional number**, written as a decimal with a point — `3.5`, `0.25`, a **leading-dot** form `.5` (== `0.5`), or a **trailing-dot** form `5.` (== `5.0`) — and/or an **exponent** (`e`/`E`, an optional sign, and one or more digits), e.g. `1e5` (100000.0), `1.5e-3` (0.0015), `.5e2` (50.0), `6.022e23`. A literal with an exponent is a `real` even without a decimal point (`1e5`). The literal's static type is `real` (§5.1); its value class is `real` on the read side (§5.6). An exponent that leaves the finite `real` range **upward** — `1e400` — is a parse_error, because a cell has no infinity to hold. Leaving that range **downward** is not the same case: such an exponent is accepted and underflows to zero, so `1e-400` evaluates to `0.0`, which a cell holds exactly. A real is distinguished from an integer literal (§3.5.2) by the decimal point or the exponent: `3` is an integer, while `3.5`, `.5`, `5.`, and `3e0` are reals. A point is part of a real when it **follows** a digit (`5.`) or **precedes** one (`.5`); a point with a digit on neither side — a lone `.` — is the field/access operator (§4.4), not a real, so `.name` accesses a field. Because `5.` is a complete real, `5.name` is the real `5.0` followed by `name` (a parse error), not a field access on an integer. Likewise an `e`/`E` is part of a real **only** when followed by an optional sign and a digit — `1e5` is a real, but `1e` is an integer `1` followed by the identifier `e`. An exponent is decimal only; a base prefix (`0x`/`0o`/`0b`) never takes an exponent (`0xe5` is the hex integer 229). Underscores may separate digits for readability (`1_000.5`, `1_000e1`) and are not significant; a trailing digit-separator is not part of a real. A real renders as its **shortest round-tripping decimal** — the same text CPython's `repr(float)` produces: **fixed-point** when the value's decimal exponent is in `[-4, 15]` (insignificant trailing zeros are dropped, so `3.50` renders `3.5` and `5.0` renders `5.0`), **scientific** (`d[.ddd]e[+-]NN`, a signed two-or-more-digit exponent) for larger or smaller magnitudes (`1e20` renders `1e+20`, `1.5e-8` renders `1.5e-08`, `1e-5` renders `1e-05`), and `-0.0` for negative zero. The identical text is used on the wire, on write-through, and on read-back — there is no store-vs-display difference, with one exception: a cell holds zero without a sign, so a `-0.0` written to a cell reads back as `0.0`. A real is an **expressible** value: it renders in `print` and via `str(…)`. Reals are **computable**: `+`, `-`, `*`, `/`, `//`, `%`, and `**` accept real operands, and the ordered comparisons `<`, `>`, `<=`, `>=` accept them too (§8.1, §8.3). The numeric operators **promote**: an operation with an `int` and a `real` operand produces a `real`. `/` (true division) always produces a `real`, even for `int / int` (`7 / 2` is `3.5`); the floored integer quotient is `//` (§8.3). A real arithmetic result whose magnitude leaves the finite range, and real division by zero, are runtime refuses (§10.3) — the same discipline the integer operators follow. #### 3.5.8 Blob literals ``` blob-literal := hex-blob | b64-blob hex-blob := 'blob' '(' '"' ( hex-digit hex-digit )* '"' ')' b64-blob := 'blob_b64' '(' '"' base64-char* '"' ')' hex-digit := dec-digit | 'a'..'f' | 'A'..'F' base64-char := 'A'..'Z' | 'a'..'z' | dec-digit | '+' | '/' | '=' ``` A blob literal denotes an **opaque byte string**. It has two input spellings that denote the same byte space; the static type is `blob` (§5.1) either way, and its value class is `blob` on the read side (§5.6). (The leading-prefix spellings `x"…"` / `b64"…"` are also accepted as legacy forms.) - **Hex** — an even number of hexadecimal digits, written `blob("")` — e.g. `blob("48656C6C6F")` (five bytes). An empty `blob("")` is a valid zero-byte blob. Each byte is exactly two hex digits; an odd digit count, or any non-hex character, is a **parse_error**. - **Base64** — RFC 4648 base64, written `blob_b64("")` — e.g. `blob_b64("SGVsbG8=")` (the same five bytes as `blob("48656C6C6F")`). The content is a multiple of four characters drawn from `A`–`Z`, `a`–`z`, `0`–`9`, `+`, `/`, with zero to two trailing `=` padding characters; an empty `blob_b64("")` is a valid zero-byte blob. A wrong length, a non-alphabet character, or misplaced padding is a **parse_error**. Base64 is a convenience input spelling for pasting base64-encoded payloads; it produces exactly the bytes it encodes. Regardless of the input spelling, a blob **reads back** at the `blob` value class in a single canonical uppercase-hex form (so a value written `blob_b64("SGVsbG8=")` reads back `48656C6C6F`). A blob is an **expressible** value: it renders (as its hex text) in `print` and via `str(…)`; it is not otherwise operated on. #### 3.5.9 List literals A list literal builds a **constructed list** — a finite, ordered, immutable sequence of element values, evaluated on the client side: ``` list-literal := '[' ( expr ( ',' expr )* ','? )? ']' ``` The elements are arbitrary expressions, evaluated left to right; a trailing comma is permitted (`[1, 2,]`); the empty list is `[]`. Lists nest — a list may contain lists (`[[1, 2], [3]]`). The element type is inferred (§5.1): a list whose elements share a type is a `list`; a list mixing scalar value classes is a `list`; the empty list is `list`, refined by context. A literal that mixes a scalar with a non-scalar (`[1, [2]]`) has no common element type and is a type_error. A constructed list is a pure client-side value like a `string`: it is bounded at construction (a fixed element count), immutable, and never round-trips through the service. It is distinct from the store-derived finite collections of §5.1 (which are produced by read verbs); the two share the read surface (indexing, slicing, `.length`, `for … in`, membership, and the value-search methods `xs.index(v[, start[, end]])` → the first index of `v` within an optional codepoint window and `xs.count(v)` → the number of occurrences — `index` of an absent value is a catchable refuse, §10.3) but a constructed list additionally renders in `print` and `+` (§8.4, §8.7) and supports `==`/`!=` (§8.1) and comprehensions (§8.9). #### 3.5.10 Formatted string literals (f-strings) A formatted string literal — an **f-string** — is a string literal carrying a lowercase or uppercase `f` prefix (`f"…"` / `F"…"`) whose `{ … }` sections are **replacement fields**: an expression written between braces is evaluated and its value is written into the string in place of the field. ``` fstring-literal := ('f' | 'F') '"' ( fstring-char | replacement-field )* '"' fstring-char := string-char (§3.5.1) # '{{' and '}}' denote literal '{' and '}' replacement-field := '{' expr '='? ( '!' ('r' | 's') )? ( ':' format-spec )? '}' format-spec := [[fill] align] ['0'] [width] ['.' precision] [type] # §8.13 ``` The literal portions accept the same escapes as an ordinary string literal (§3.5.1). A doubled brace `{{` or `}}` denotes a single literal `{` or `}`. Each replacement field holds a full expression (§4.4) — a bound variable, a literal, an arithmetic expression, a built-in method call, an index or slice, or a field read. The value of an f-string is exactly the value of the equivalent `+` concatenation of its literal parts and its replacement-field expressions, in order: `f"a{x}b"` has the value `"a" + str(x) + "b"`, and a field is written using the same rendering `+` gives that value (§8.7) — an `int`/`real`/`bool`/list is rendered as `+` renders it. A field whose value is a store read must first bind it to a name (§4.3), the same rule the `+` operator follows. An f-string is always of type `string`, including when it is a single replacement field (`f"{n}"` is a `string`, not the type of `n`). A replacement field may carry a **conversion** and/or a **format spec**: `{x!r}` renders `repr(x)` (and `{x!s}` renders `str(x)`, the default); `{x:spec}` renders `format(x, "spec")` — the format mini-language of §8.5 (`f"{x:.2f}"`, `f"{n:>5}"`, `f"{s:*^8}"`), and the two combine as `{x!r:>10}`. A replacement field may end its expression with a **self-documenting `=`** (`f"{x=}"`): the field writes the field's source text from just after `{` up to and **including** the `=` **verbatim** (surrounding whitespace preserved), followed by the value. With no conversion or format spec the value defaults to `repr` (not `str`) — `f"{x=}"` is `"x=5"`, `f"{ x = }"` is `" x = 5"`, and `f"{s=}"` is `"s='hi'"` — while a `:format-spec` or `!conversion` overrides that default (`f"{x=:.2f}"` is `"x=5.00"`, `f"{x=!s}"` is `"x=5"`). A trailing comparison operator (`==`, `>=`, `<=`, `!=`) is NOT the debug `=`. A **string literal** written inside a field (`f"{\"a\"}"`) is a parse_error (bind it to a name first); an **empty** field `{}` is a parse_error. Not yet supported: the `!a` (ascii) conversion and a dynamic spec (`{x:{width}}`) — each a parse_error / runtime error with a teaching message. A conforming implementation MUST reject an unterminated f-string (newline or end-of-source before the closing `"`) with a parse_error. #### 3.5.11 Tuple literals A tuple literal builds a **constructed tuple** — a finite, ordered, immutable sequence whose positions may each hold a different type, evaluated on the client side: ``` tuple-literal := '(' ( expr ( ',' expr )* ','? )? ')' ``` A comma distinguishes a tuple from a parenthesized expression: `(e)` groups, `(e,)` is a one-element tuple, `(a, b)` a two-element tuple, and `()` the empty tuple. The element type is inferred per position (§5.1): `(1, "a", True)` is a `tuple`; tuples nest. Unlike a list, a tuple is heterogeneous, so it is indexed by a **constant** integer (§5.3) — `t[0]` has the type of the first position — and it is not written after `for … in`. A constructed tuple is a pure client-side value: bounded at construction, immutable, and never round-trips through the service. It renders in `print`, supports `==`/`!=` (§8.1), and concatenates with another tuple via `+` (§8.4) — the result keeping each operand's positions and their types, so a constant index into it reads the position it names. #### 3.5.12 Dict literals A dict literal builds a **constructed dict** — a finite, immutable mapping from hashable keys to values, kept in **insertion order**, evaluated on the client side: ``` dict-literal := '{' ( expr ':' expr ( ',' expr ':' expr )* ','? )? '}' ``` The empty dict is `{}`. Keys are homogeneous and must be 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 inferred type is `dict` (§5.1): `{"a": 1, "b": 2}` is a `dict`. When a key is written twice, the entry keeps its first position but takes the last value. A dict is read by key `d[k]` (a key absent at run time is a catchable refuse, §10.3), tested with `k in d` (§8.1), walked with `for k in d` over its keys (§6.3), measured with `.length`, and projected with `.keys()` / `.values()` / `.items()` (§8.6). A constructed dict is a pure client-side value, immutable and never round-tripping through the service; it renders in `print`. `+` is **not** defined over dicts, the same as in Python. #### 3.5.13 Set literals A set literal builds a **constructed set** — a finite, immutable collection of unique values, evaluated on the client side: ``` set-literal := '{' expr ( ',' expr )* ','? '}' ``` A `{ … }` with no colon is a set (a `{ … }` with a colon is a dict, §3.5.12); because the empty braces `{}` are the empty dict, the empty set has no literal form. Elements are homogeneous and must be a scalar value class (a mix of scalar value classes gives a `set`); duplicates are removed. The inferred type is `set` (§5.1). A set renders and is walked (`for x in s`) in a **deterministic sorted order** — this is a defined refinement of Python, whose set order is unspecified. A set is tested with `x in s` (§8.1), measured with `.length`, and combined with `.union` / `.intersection` / `.difference` / `.symmetric_difference` (§8.6). A constructed set is a pure client-side value, immutable and never round-tripping through the service. #### 3.5.14 Scientific literals ``` scientific-literal := 'scientific' '(' '"' scientific-numeral '"' ')' scientific-numeral := '-'? mantissa ( 'e' | 'E' ) '-'? dec-digit+ mantissa := dec-digit+ ( '.' dec-digit+ )? # a nonzero magnitude ``` A scientific literal denotes a **number carrying its significant figures**, written as the factory call `scientific("")` in scientific notation — e.g. `scientific("6.022e23")`. Its static type is `scientific` (§5.1); its value class is `scientific` on the read side (§5.6). (The leading-prefix spelling `sci"…"` is also accepted as a legacy form.) The argument is a single string literal: an optional leading `-`, a mantissa (digits with an optional decimal point) carrying at least one nonzero digit, then a **required** exponent — the letter `e` (or `E`), an optional sign, and one or more digits. The exponent is mandatory: it is what distinguishes a scientific value from a `real` (§3.5.7) and what makes the number of significant figures unambiguous. A numeral with no exponent, an all-zero mantissa, or a magnitude too large to represent is a **parse_error** (from the `sci"…"` form) or a refuse at write (from the factory form). Significant figures are part of the value. `scientific("6.022e23")` (four significant figures) and `scientific("6.0220e23")` (five — the trailing zero is significant) denote the **same magnitude but are distinct values**: each reads back with its own figures, and writing one to a cell does not replace the other. This is the one property a `real` cannot carry — a `real` is a floating-point number that forgets how many figures were written. A scientific reads back in a **canonical** form: the mantissa is normalized to a single nonzero leading digit with the significant figures preserved, so `scientific("60.220e21")` reads back as `6.0220e22`. Numerals that normalize to the same figures are the same value regardless of how they were written. ### 3.6 Operators and punctuation ``` ( ) [ ] . , : = == != < > <= >= + - * / // % ** ``` The token `=` appears in bare assignment (§4.3); a class field is written with a `remember` / `update` verb call (§13.3), not `=`. The token `:` ends a block header and separates a parameter or field name from its type. Newlines terminate simple statements (§3.2); there is no `;`. The word forms `and` / `or` / `not` are the logical operators (§8.2); there are no `&&` / `||` / `!` tokens. ### 3.7 Reserved words The following identifiers are reserved and MUST NOT be used as user identifiers (declaration names, parameter names, loop variables, handler bindings, assignment targets): **(a) Structural keywords** ``` def class return match case if else for in break continue try except as branch commit rollback ``` **(b) Logical operators** ``` and or not ``` **(c) Reserved word that teaches (not a statement)** ``` log ``` Output is written with `print(...)` (§8.7). `log` is not a statement; it is reserved only so a stray `log(...)` / `log ` produces a teaching diagnostic rather than a confusing parse error, and MUST NOT be used as a user identifier. **(d) Boolean literals** ``` True False ``` **(e) Verb surface vocabulary.** The verb head-words of the built-in verb surface (§7) — `remember`, `update`, `forget`, `assert`, `pin`, `verify`, `agreement`, `writers`, `current`, `get`, `why`, `caveats`, `dependents`, `conflicts`, `subjects`, `list`, `compile` — are recognised as built-in verb names. Programs SHOULD NOT use them as user identifiers. (`compile` is reserved by the service and is not available as a user identifier; like `forget script` and `info script` it is not executable inside a program body.) A conforming implementation MUST treat the (a)–(d) identifiers as reserved at the lexical level. **Contextual relaxation for dotted field access.** After a `.` in a path expression, an identifier-shaped token is parsed as a field name (permitting `claim.source`, `claim.value`, and similar even when the field name collides with a verb-surface word); whether the field is meaningful for the base type is decided by the typechecker (§6). The type names of §5.5 (`string`, `int`, `claim_list`, …) are contextual identifiers, not reserved words; programs SHOULD nonetheless avoid them as user identifiers. ### 3.8 Token classes | Class | Examples | |-------|----------| | `IDENT` | `Cat`, `mittens`, `audit_subject`, `猫` | | `STRING` | `"orange"`, `"op1"` | | `INT` | `42`, `0`, `9223372036854775807` | | `KEYWORD` | any reserved word from §3.7 | | `NEWLINE` / `INDENT` / `DEDENT` | layout tokens from the off-side rule (§3.2) | | punctuation/operators | as listed in §3.6 | | `EOF` | end of source | ### 3.9 Natural language The natural language a source is written in — which keyword vocabulary its statements use, and the language its responses are rendered in — is set **out of band**, by the **`language` parameter** supplied when a source is submitted, not by the source. When the parameter is omitted, the language is **English** (`eng`). `eng` is the default. 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. The parameter is the forward-compatible surface for additional natural languages. **This specification describes the English surface.** Every keyword, verb and rendered response given here is the `eng` spelling; any other keyword vocabulary is a separate surface over the same semantics and has its own specification. 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 therefore a property of how you are talking to the service — set per call — not a property stored in the program. A source has **no header line** and does not declare its natural language in-band. --- ## 4. Grammar ### 4.1 Programs ``` source := option-verb NEWLINE | module-body module-body := top-item+ top-item := decl | class-decl | rule-decl # decl §4.2, class-decl §13.1, rule-decl §14 | import-stmt | statement # import-stmt §4.3, statement §4.3 (incl. the four writes) — see Modules option-verb := '--' IDENT IDENT? ``` A source has **no header line**: it is the **module body** (Reference §9.1) from its first line. Its body admits, at the top level, not only declarations but also `import` statements (Reference §9.3), data declarations (write statements at module scope, Reference §9.2), and the other statements legal in a `def` body (§4.3). The module body runs once, top to bottom, when the module is imported (Reference §9.1); a file whose body is exactly one `def` is the common single-script case. The natural language the source is written in — the language of the knowledge it names and of its authored text — is set out of band (§3.9), not in the source; it also selects the language in which the script's own structured output — its invocation transcript (Wire §4.2) — is rendered. It does not select the response language of the surrounding service surface, which remains a property of the calling channel; the two may differ. **Option verbs.** A `--`-prefixed word in declaration position is an **option verb** — a compiler-directed verb, addressed to the implementation rather than the store. An option verb's spelling involves no language keyword, so `--help` means the same thing in every context. The supported set is `--help` (§4.2), which takes an optional topic word; an unknown option verb is a parse_error whose diagnostic names the supported set. An option verb never compiles and never stores anything, by construction. A source file may declare one or more scripts — a **compile unit**. Every declaration compiles and stores under its own name, in declaration order. Declaration order is compile order: a declaration may call only an EARLIER declaration of the same unit or an already-stored script (§6.8, §9.7, compile-before-call). Two declarations in one unit MUST NOT share a name. A unit need not declare a script at all: a module whose body only installs a schema, defines a rule, or writes data is valid (Reference §9.1, §9.7). A unit with an empty body — whitespace and comments only — is a parse_error. Except where an example shows a complete compile unit, program examples elsewhere in this document are fragments: a fragment omits the surrounding program scaffolding for brevity. ### 4.2 Declarations ``` decl := 'def' IDENT '(' params? ')' ( '->' type )? ':' NEWLINE INDENT stmt+ DEDENT params := param ( ',' param )* ( ',' var-param )? # optional trailing variadic (§4.2) | var-param param := IDENT ':' type ( '=' const-expr )? # QW-R6 default value var-param := '*' IDENT ':' type # variadic: surplus positionals → tuple type := type-name # a scalar / read-result type (§5.5) | 'list' '<' type '>' | 'set' '<' type '>' | 'dict' '<' type ',' type '>' | 'tuple' '<' type ( ',' type )* '>' ``` A declaration is the `def` keyword, a name, a parenthesised parameter list, an optional **`-> type`** return type, a `:`, and an indented suite. A parameter is `name: type` where `type` is one of the type names enumerated in §5.5 — a primitive (`string`, `int`, `bool`), a value-class scalar (`datetime`, `duration`, `real`, `blob`, `scientific`), or a read-result type such as `claim_list` — **or** a parameterized collection type: `list`, `set`, `dict`, or `tuple`, nestable (e.g. `dict>`). So a collection crosses a function boundary both as an argument and as a return value. (`empty` and `null` name absence and are never parameter types.) The declared objects are called *scripts* (the wire addresses them as such, see Wire §9.2). **Void scripts and value scripts.** A script with no `-> type` is a **void script**: it produces no value and is called for its store effects and `print` output. A script written `def name(...) -> type:` is a **value script**: it produces a value of the declared `type`, and every path through its body MUST end in a `return ` of that type (the exhaustive-return rule, §6.9). A value script may be called in expression position, its result bound or composed (§4.4, §6.8); a void script may not (using a void script's call as a value is a type_error). The return `type` is any of the parameter types above, including a collection type (`-> list`, `-> dict`, …); an empty-list `return []` satisfies any concrete `-> list`. The `return` statement itself is specified in §4.3 and §9.2.8. A parameter may carry a **default value** (`def f(x: int, y: int = 1)`). The default is a **constant expression** — a literal, or an operation over literals (so `-1`, `1 + 2`, `[1, 2]` qualify) — and its type must match the parameter's declared type (an `int` default is accepted for a `real` parameter). A parameter with a default may not precede one without (a required parameter after a defaulted one is a compile-time error). A call that omits a defaulted argument uses the default; a required parameter with no supplied argument is an error (§4.3, §9.7). **Variadic parameter.** A final parameter may be written `*name: T` — a **variadic** parameter that collects the surplus positional arguments into a `tuple` (a tuple whose every element is `T`), possibly empty. It must be the **last** parameter, there may be at most one, its element type `T` is required, and it takes no default. A call passes any number of trailing positional arguments of type `T` for it (`f(a, 1, 2, 3)`); it cannot be supplied by keyword. Inside the body the parameter is an ordinary `tuple` — indexed (`name[0]`), measured (`len(name)`), iterated (`for x in name`), and reduced (`sum`/`max`/comprehension). (There is no `**kwargs`; use explicit named parameters — with defaults where useful — or a `dict` parameter.) **`--help`** is the teaching option verb (§4.1) — the in-band way to learn the language from inside it. Bare `--help` yields the orientation lesson: the declaration shape, one complete example, and the topic index. `--help ` yields one topic's lesson; the topics are `header`, `types`, `verbs`, `statements`, and `scripts`. The lesson language follows the `language` parameter (§3.9). An unknown topic is a parse_error whose diagnostic names the topic index. ``` --help types ``` A unit whose body is a help form never compiles and stores nothing; on the wire it is classified parse_error, and its diagnostic message is the lesson. A conforming implementation whose surface faces a human directly (such as a CLI) SHOULD present the lesson without error framing and report success — asking for help is not a mistake. ### 4.3 Statements A statement is either a **simple statement**, ending with a `NEWLINE`, or a **block statement** (`if` / `for` / `match` / `try` / `branch`), whose body is a `:`-headed indented suite. ``` stmt := simple-stmt NEWLINE | block-stmt simple-stmt := assign-stmt | print-stmt | call-stmt | verb-call-stmt | commit-stmt | rollback-stmt | import-stmt | return-stmt # §9.2.8 | raise-stmt | assert-stmt | 'pass' # a no-op | 'break' # loop control, §9.2.7 | 'continue' block-stmt := match-stmt | for-stmt | if-stmt | try-stmt | branch-block assign-stmt := IDENT '=' expr | IDENT ':' type '=' expr # annotated assignment; the type must agree with the initializer | IDENT ( '=' IDENT )+ '=' expr # chained assignment; every target binds one value (§8.12) | IDENT aug-op expr # augmented assignment on a bare name; `x op= e` is `x = x op e` (a field names a source, so it uses `remember(...)`, not `op=`) | top-target ( ',' top-target )+ '=' expr ( ',' expr )* # tuple unpacking; nested targets + one optional `*rest` (§8.11) | '(' unpack-target ( ',' unpack-target )* ')' '=' expr # parenthesised target list (§8.11) top-target := unpack-target | '*' IDENT # a target, or THE single starred target (≤ one per list) unpack-target := IDENT | '(' unpack-target ( ',' unpack-target )* ')' # a name, or a nested tuple target aug-op := '+=' | '-=' | '*=' | '/=' | '%=' | '//=' | '**=' print-stmt := 'print' '(' ( print-arg ( ',' print-arg )* )? ')' print-arg := expr # a value to render | ( 'sep' | 'end' ) '=' STRING # keyword; a STRING literal only raise-stmt := 'raise' EXC-NAME ( '(' expr? ')' )? # a catchable refuse assert-stmt := 'assert' expr ( ',' expr )? # Python assertion; parenthesis-free (the absence-assertion verb, §7.1, is separate) call-stmt := IDENT '(' arg-list? ')' verb-call-stmt := IDENT '(' arg-list? ')' # a built-in verb call (§7); the head IDENT is a verb head-word commit-stmt := 'commit' rollback-stmt := 'rollback' import-stmt := 'import' module-name # load a module, Reference §9.3 module-name := IDENT ( '.' IDENT )* return-stmt := 'return' expr? # early exit / value, §9.2.8 match-stmt := 'match' expr ':' NEWLINE INDENT case-clause+ DEDENT case-clause := 'case' IDENT ( 'as' IDENT )? ':' ( simple-stmt NEWLINE | NEWLINE INDENT stmt+ DEDENT ) for-stmt := 'for' IDENT ( ',' IDENT )* 'in' expr ':' NEWLINE INDENT stmt+ DEDENT # a target list unpacks each element (§8.11) if-stmt := 'if' expr ':' NEWLINE INDENT stmt+ DEDENT ( 'elif' expr ':' NEWLINE INDENT stmt+ DEDENT )* ( 'else' ':' NEWLINE INDENT stmt+ DEDENT )? try-stmt := 'try' ':' NEWLINE INDENT stmt+ DEDENT handler* handler := 'except' 'refuse' ( 'as' IDENT )? ':' NEWLINE INDENT stmt+ DEDENT | 'except' 'engine_error' ( 'as' IDENT )? ':' NEWLINE INDENT stmt+ DEDENT branch-block := 'with' 'branch' '(' STRING ')' ':' NEWLINE INDENT stmt+ DEDENT arg-list := arg ( ',' arg )* arg := expr # positional | IDENT '=' expr # QW-R6 keyword argument ``` In a call's `arg-list`, a **positional** argument fills the next unfilled parameter left-to-right; a **keyword** argument `name=value` fills the parameter of that name. A keyword argument may not precede a positional one (a compile-time error). A parameter filled by neither uses its default (§4.2); binding the same parameter both positionally and by keyword, naming a parameter that does not exist, supplying more positional arguments than parameters, or leaving a required parameter unbound are each errors. A **bare assignment** (`assign-stmt`) binds one name to an expression result; there is no `let` introducer, and the right-hand side MUST NOT be a statement-only verb (§7.4). A **call statement** whose head identifier is not a verb head-word is a stored-script invocation — how a program calls compiled code, including from inside a `run` (Wire §4.2). Resolution follows the compile-before-call rule (§6.8, §9.7). A call statement may name a void OR a value script; when it names a value script the returned value is discarded (§9.2.8). An **augmented assignment** (`IDENT aug-op expr`) rewrites to the plain form: `x op= e` is exactly `x = x op e`, evaluated once. It applies to a bare name only — a field names a source, so a field is written with `remember(...)` rather than an augmented operator. Because a variable keeps one type across a function (§6.9), the rewritten right-hand side must still have the variable's type: `/` is true division and yields a `real` (§8.3), so `/=` applies to a `real` target and `x /= 2` on an `int` is a type_error naming the type change, not a silent truncation. ``` # augmented-assign.dpy — `x op= e` is `x = x op e`, and `/=` needs a real target. def augmented(start: int) -> int: total = start total += 10 total -= 3 total *= 2 total //= 4 total %= 7 total **= 2 rate = 1.0 rate /= 8 print("total=" + str(total) + " rate=" + str(rate)) return total ``` Invoked with `5`, that prints `total=36 rate=0.125`. A **`return` statement** (`return-stmt`) ends the enclosing script. A bare `return` (no expression) exits early; it is valid in any script, void or value. A `return ` yields the expression's value and is valid only in a **value script** (§4.2): the expression's type MUST match the declared return type (an `int` value satisfies a `-> real` return, mirroring numeric promotion). A `return ` in a void script, or a value script that does not `return` on every path, is a type_error (§6.9). The return control-flow semantics are specified in §9.2.8. Each **case arm** of a `match` may be an inline statement or an indented suite; the arms must be exhaustive over the scrutinee's discriminator (§6.2). The optional `as IDENT` on a case label binds the matched content and is well-typed only on a value-match arm (§5.6, §6.2); elsewhere it is a type_error. Both `try` handler clauses are optional, in the fixed order shown (`except refuse` before `except engine_error`). The `as ` binding on a handler is itself optional — `except refuse:` fires the handler without naming the caught exception (Python's `except ValueError:`); omit it when the handler body does not use the refuse/engine_error info. `commit` and `rollback` are bare statements resolving to the enclosing `branch` block (§9.2.6). An **`import` statement** (`import `) loads a stored module by name (Reference §9.3); `import` is a **contextual keyword**, recognised only as the statement head immediately before a module name (like the aggregate fold names, §7.1.1), and an ordinary identifier elsewhere. A **`print` statement** (`print-stmt`) writes one output line. It renders each positional argument to its text form and joins them with `sep` (default a single space `" "`), then appends `end` (default a newline) — so `print(a, b)` writes one line ` ` and `print()` writes an empty line. `sep` and `end` are optional keyword arguments and MUST be string literals. Because output is line-oriented (each `print` writes exactly one line, as `print` does), a trailing newline in `end` is the line itself; `end=""` therefore reads the same as the default (there is no line continuation). `print` renders each value exactly as `print` and the `str()` conversion do — in particular a boolean renders as `True` / `False`. `print` is a **contextual keyword**, recognised only as a statement head immediately before `(`, and an ordinary identifier elsewhere. A **`pass` statement** is a no-op: it has no effect and produces no output. It exists so a block that would otherwise be empty stays well-formed (e.g. an `else` branch that does nothing). `pass` is a **contextual keyword**, recognised only as a complete statement on its own line, and an ordinary identifier elsewhere. A **`raise` statement** (`raise-stmt`) raises a **recoverable error** — a `refuse` (§10) — that an enclosing `try` catches with `except refuse as r:`. It names one of the built-in exception names (`ValueError`, `KeyError`, `TypeError`, `RuntimeError`, and the like); that name is recorded on the caught handler's `r.discriminator`, and a single message argument (rendered to its text form) on `r.reason`. A bare `raise ValueError` gives an empty reason. Every exception name behaves identically — there are **no custom exception types and no exception hierarchies**. A `raise` never falls through, so a branch that ends in one counts as returning for the exhaustive-return rule of a value script (§4.2). `raise` is a **contextual keyword**, recognised only as a statement head immediately before an exception name, and an ordinary identifier elsewhere. An **`assert` statement** (`assert-stmt`) is Python's assertion. `assert cond` evaluates `cond` (which MUST be a `bool`) and, when it is false, raises an `AssertionError` — equivalent to `if not cond: raise AssertionError`, a recoverable `refuse` (§10) an enclosing `try` catches with `except refuse as r:`. The optional second operand is the message: `assert cond, msg` records `msg` (rendered to its text form) on `r.reason`, exactly as `raise AssertionError(msg)` would, and is evaluated **only when the assertion fails**; a bare `assert cond` gives an empty reason. A passing assertion produces no output and execution continues. This is the **parenthesis-free** spelling of `assert` (the statement form); the same word heads the absence-assertion **verb** (§7.1) in its call form `assert(path, source)`, which records an explicit-absent claim — and that is unaffected by this statement form. ### 4.4 Expressions ``` expr := cond-expr cond-expr := or-expr ( 'if' or-expr 'else' expr )? # ternary; right-assoc; lower than `or` or-expr := and-expr ( 'or' and-expr )* and-expr := cmp-expr ( 'and' cmp-expr )* cmp-expr := add-expr ( cmp-op add-expr )* cmp-op := '==' | '!=' | '<' | '>' | '<=' | '>=' | 'in' | 'not' 'in' add-expr := mul-expr ( ( '+' | '-' ) mul-expr )* mul-expr := unary-expr ( ( '*' | '/' | '//' | '%' ) unary-expr )* unary-expr := ( 'not' | '-' ) unary-expr | pow-expr pow-expr := postfix-expr ( '**' unary-expr )? # right-assoc; tighter than unary `-` postfix-expr := primary-expr postfix* postfix := '.' IDENT '(' arg-list? ')' # method call (§13.4; string methods §5.3) | '.' IDENT # field access | '[' expr ']' # indexing (string / collection, §5.3) | '[' expr? ':' expr? ( ':' expr? )? ']' # slice (string / list / tuple, §5.3) primary-expr := STRING | INT | 'True' | 'False' | fstring-literal # formatted string literal (§3.5.10) | list-display # list literal / comprehension (§3.5.9, §8.9) | brace-display # dict/set literal or comprehension (§3.5.12, §3.5.13, §8.9) | tuple-display # tuple literal / grouping (§3.5.11) | builtin-call # zip / enumerate (§8.6), abs / round (§8.3) | IDENT '(' expr ')' # instance constructor (§13.2) | value-call # value-script invocation (§6.8) | IDENT | path-expr | IDENT '(' arg-list? ')' # a built-in read verb call, §7 value-call := IDENT '(' arg-list? ')' # a value script's call, in expression position list-display := '[' ( expr ( ',' expr )* ','? )? ']' # list literal (§3.5.9) | '[' expr ( 'for' IDENT 'in' expr ( 'if' expr )* )+ ']' # list comprehension (§8.9) brace-display := '{' ( expr ':' expr ( ',' expr ':' expr )* ','? )? '}' # dict literal (§3.5.12) | '{' expr ( ',' expr )* ','? '}' # set literal (§3.5.13) | '{' expr ( 'for' IDENT 'in' expr ( 'if' expr )* )+ '}' # set comprehension (§8.9) | '{' expr ':' expr ( 'for' IDENT 'in' expr ( 'if' expr )* )+ '}' # dict comprehension (§8.9) tuple-display := '(' expr ')' # grouping (no comma) | '(' ( expr ( ',' expr )* ','? )? ')' # tuple literal (§3.5.11) builtin-call := ( 'zip' | 'enumerate' | 'reversed' | 'abs' | 'round' | 'divmod' | 'str' | 'int' | 'float' | 'list' | 'set' | 'dict' | 'isinstance' ) '(' ( expr ( ',' expr )* )? ')' # zip/enumerate/reversed §8.6, abs/round/divmod §8.3, conversions §8.13, isinstance §13.9 path-expr := IDENT ( '.' IDENT )+ # K.s.a slot-grammar dotted path ``` Prefix `-` (unary minus) is an `int → int` operator; its runtime semantics are `0 - a` (§8.3), so negating the most-negative integer overflows and refuses rather than wrapping. The boundary between `path-expr` (a multi-segment dotted reference to a store cell) and `postfix-expr` with `.field` chains (field access on a value) is resolved by the typechecker (§6) using the type of the head identifier. The comparison operators **chain** (§4.6): `a < b < c` is `(a < b) and (b < c)` — each adjacent pair compared, the results conjoined. A **value-call** `f(args)` is a value script's invocation (§4.2) used as an expression: its value is what the callee `return`s, and its type is the callee's declared return type (§6.8). It composes like any expression — assigned (`y = f(x)`), returned (`return f(x)`), passed as an argument (`print(f(x))`, `g(f(x))`), or combined with operators (`f(a) + g(b)`); nested value-calls evaluate inner-first, left-to-right (§9.1). The head identifier disambiguates `IDENT(...)` between the three call-shaped primaries: a class name is an instance constructor (§13.2), a built-in name is that built-in (`zip`/`enumerate`/`len`/ `abs`/`str`/`int`/`float`/`list`/`set`/`dict`/a fold/a verb), and any other identifier bound to a value script is a value-call. A call to a **void** script (§4.2) in expression position is a type_error; call it as a statement (§4.3) instead. ### 4.5 Verbs The built-in verb surface (§7) 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 produce a value and may stand in expression position (bound by assignment or composed with operators); write verbs have no value and stand only as statements. Representative forms, as they read in a program: ``` remember(K.s.color, "orange", "op1") # write: (path, value, source) update(K.s.color, "black", "op1") forget(K.s.color) # path-scoped assert(K.s.nickname, "op1") # absence assertion: (path, source) cur = current(K.s.color) # reads hist = get(K.s.color) proof = why(K.s.color) attrs = list_attributes(K) # K or K.s subs = list_subjects(K.color) vals = list_values(K.color) hits = subjects(K.color, "orange") cur = current(K.s.color) # the current claim at this cell deps = dependents(cur) # claims derived from that claim v = verify(K.s.color, "orange") # optional: verify(K.s.a, v, src) n = agreement(K.s.color, "orange") # how many sources recorded "orange" ``` See §7 for each verb's slot shape and result type. A path whose segment count does not match the verb's slot shape is a runtime refuse (§7.2). ### 4.6 Operator precedence and associativity The conditional expression `a if c else b` (§8.10) binds **lower** than every operator in the table below — its `then` and `else` operands are full expressions, so `x + 1 if c else y * 2` groups as `(x + 1) if c else (y * 2)`, and it is right-associative (`a if p else b if q else c` is `a if p else (b if q else c)`). Below the conditional expression, lowest to highest precedence; binary operators are left-associative **except `**`, which is right-associative** (`2 ** 3 ** 2` is `2 ** (3 ** 2)`). | Level | Operators | |-------|-----------| | 1 | `or` | | 2 | `and` | | 3 | `not` (boolean, prefix) | | 4 | `==` `!=` `<` `>` `<=` `>=` | | 5 | `+` `-` (binary) | | 6 | `*` `/` `//` `%` | | 7 | `-` (prefix, arithmetic) | | 8 | `**` (power, right-associative) | | 9 | `.` (field / method) , `[]` (index) , instance / verb call | Boolean `not` binds **looser** than comparison (Python), so `not a == b` is `not (a == b)`; it is distinct from the arithmetic prefix `-`, which binds tightly (level 7). `**` binds more tightly than the prefix `-`, so `-2 ** 2` is `-(2 ** 2)` = `-4`; its right operand is a unary expression, so `2 ** -1` is well-formed. Comparison operators **chain** (Python semantics): `a op1 b op2 c …` is `(a op1 b) and (b op2 c) and …` — each adjacent pair is compared under §8.1 and the results conjoined with `and`. An interior operand is compared in both of its pairs; because DKE operands are side-effect-free (a store read is bound to a name first, §9.1) the result is well-defined. A single comparison (`a < b`) is unchanged. --- ## 5. Type system DKE Python has a closed type vocabulary shared across the family. There is no subtyping, no user-defined types, and no user-defined generics; the one built-in parametric type is the constructed `list` (§3.5.9, below). Programs compose by operating on the store through verb calls, not by defining records. ### 5.1 The base types | Type | Origin | Role | |------|--------|------| | `string` | user data; identifier-typed slots; values | primitive | | `int` | counts (`.length`), positions, timestamps | primitive | | `bool` | comparison + logical results | primitive | | `value` | the stored content of a claim (`active_claim.value`, §5.6) | tagged union | | `datetime` | a UTC instant, written `datetime("…Z")` (§3.5.5); the `datetime` class of `value` (§5.6) | value class | | `duration` | a length of time, written `duration("…")` (§3.5.6); the `duration` class of `value` (§5.6) | value class | | `real` | a fractional number, written `3.5` (§3.5.7); the `real` class of `value` (§5.6) | value class | | `blob` | an opaque byte string, written `blob("…")` or `blob_b64("…")` (§3.5.8); the `blob` class of `value` (§5.6) | value class | | `scientific` | a number carrying its significant figures, written `scientific("…")` (§3.5.14); the `scientific` class of `value` (§5.6) | value class | | `active_claim` | result of `current(K.s.a)` (single live claim) | discriminator | | `claim_list` | result of `get(K.s.a)`, `list_values(K.a)`, `caveats(K.s)`, `conflicts()`, `dependents()` | finite collection | | `proof_tree` | result of `why(K.s.a)` | finite collection (also `.root`, `.truncated`) | | `diagnosis` | result of `why_not(K.s.a)` and `what_needs(K.s.a)` | finite collection | | `subject_set` | result of `subjects(K.a, v)` and `list_subjects(K)` / `list_subjects(K.a)` | finite collection | | `string_list` | result of `list_categories()`, `list_attributes(K)`, `list_pinned()`, `list_scripts()` | finite collection | | `verify_result` | result of `verify(K.s.a, v)` | discriminator | | `result_type_set` | result of `list_result_types()` | finite collection | | `refuse_info` | the binding of `except refuse as e` (§10) | handler binding | | `engine_error_info` | the binding of `except engine_error as e` (§10) | handler binding | | `empty` | sentinel case of an `active_claim` match | discriminator | **All six** **finite collection** types may appear as the iterand of a `for … in`, which also admits a constructed `list` / `set` / `dict` and a `string` (§6.3). Four of them (`subject_set`, `string_list`, `result_type_set`, `diagnosis`) yield `string` elements; `claim_list` and `proof_tree` yield `active_claim` elements. A `diagnosis` is the explanation of an absence: printing it shows the whole answer, and iterating it takes that answer a line at a time. It carries no claims, because the question it answers is about a claim that is not there. A `proof_tree` is the collection of claims that participated in a `why` derivation — iterating it (or reading `.length` / `[i]`, §5.3) yields those claims, each an `active_claim` carrying the same fields a `claim_list` element does (`.value`, `.source`, `.trust`, `.created_at`); a `proof_tree` additionally offers a `.root` accessor naming the queried claim and a `.truncated` accessor saying whether the derivation shown is the whole one (§5.2). `match` is meaningful over the **discriminator** types (`active_claim` with its `empty` case, and `verify_result`) and over the `value` **tagged union**, which a `match` destructures by the class of the stored content (§5.6, §6.2). `empty` is never produced standalone; it is the second case of an `active_claim` discriminator. The typechecker recognises `empty` as a valid `case` label on an `active_claim` scrutinee, not as a standalone expression. `value` (§5.6) is not a user-composed type — it is the single built-in union, carrying whichever primitive a claim's content happens to be. There is still no subtyping and no user-defined types. **Constructed lists (`list`).** Separately from the store-derived finite collections above, a program may **build** a finite list on the client side with a list literal (§3.5.9) or a comprehension (§8.9): `[1, 2, 3]` is a `list`, `["a", "b"]` a `list`, `[[1], [2]]` a `list>`. `list` is the one **element-parametric** type — `T` is the element type, itself any expressible type including another `list`. A literal whose elements share a type is a `list`; a literal mixing scalar value classes is a `list`; the empty list is `list` until context fixes `T`. An empty `list` is compatible with any `list`: wherever two list types must agree — the two branches of a conditional expression (`[1, 2] if c else []`), a variable's re-binding (`xs = []` then `xs = [1]`), the sibling elements of a nested list literal (`[[1, 2], []]` is `list>`), a list-typed method argument (`",".join([])`), and list equality (`[] == xs`) — an empty list takes the concrete side's element type. A constructed list shares the **read surface** of the finite collections — indexing `xs[i]` (including a negative from-end index), slicing `xs[a:b:c]`, `.length`, `for … in`, and membership `x in xs` (§5.3) — and additionally supports equality (§8.1), **concatenation** with another list (`xs + ys`, §8.4), **repetition** by an `int` count (`xs * n`, §8.3), renders in `print` and `+` (§8.4, §8.7), and is produced by a comprehension (§8.9) and by `s.split(...)` (§8.6). Unlike the store-derived collections it never round-trips through the service: it is a pure client-side value, bounded at construction and immutable. `list` is not one of the base types — it is a type former over them. **Constructed tuples, dicts, and sets.** Three further **type formers** build finite, immutable client-side values alongside `list`: - `tuple` — a fixed-length **heterogeneous** sequence built by a tuple literal (§3.5.11): `(1, "a")` is a `tuple`. Each position keeps its own type; a tuple is indexed by a constant integer, **sliced** by constant bounds (`t[1:]` → a sub-tuple, §5.3), and compared with `==`/`!=` (§8.1). - `tuple` — a **variadic homogeneous** tuple: a tuple of **runtime** length whose every element is `T`, built by `tuple(iterable)` (§8.13). Because its length is not static it is indexed by a **runtime** `int` (`t[i]` → `T`) and **cannot be unpacked**; it compares (`==`) against any tuple whose elements agree with `T`. - `dict` — a **mapping** from a hashable key type `K` (a scalar, or a tuple whose positions are recursively hashable) to a value type `V`, built by a dict literal (§3.5.12) or a dict comprehension (§8.9), kept in insertion order. - `set` — a collection of **unique** hashable elements (a scalar, or a tuple whose positions are recursively hashable), built by a set literal (§3.5.13) or a set comprehension (§8.9), presented in sorted order. All three, like `list`, are pure client-side values that never round-trip through the service, and none is one of the base types. A key or set element is restricted to a scalar value class (the eight cell value classes); a list, tuple, dict, or set is not itself a key or set element. The base types do not include an absence-of-value type. Absence is asserted through the `assert` verb (§7.1), which carries no value argument — so the absence semantic stays implicit in the verb head-word rather than being represented as a typed value. ### 5.2 Field access The expression `.` is well-typed when the table below has a row for the value's type and field; otherwise it is a type_error. `` is any expression (a postfix in the grammar, §4.4), so a field accessor composes on a **computed** value — a method result, an index, or a slice — not only on a bare name: `text.upper().length`, `xs[0].value`, and `history[-1].source` are all well-typed reads. (A store read remains bound to a name first, §9.1: a verb call is not itself a value expression, so `current(K.s.a).value` is written as two lines — `c = current(K.s.a)` then `c.value`.) | Type | Field | Field type | |------|-------|------------| | `active_claim` | `value` | `value` (§5.6) | | `active_claim` | `source` | `string` | | `active_claim` | `path` | `string` | | `active_claim` | `claim_id` | `string` | | `active_claim` | `created_at` | `string` | | `active_claim` | `trust` | `string` | | `active_claim` | `preferred` | `bool` | | `active_claim` | `maintained` | `bool` | | `active_claim` | `written_by` | `string` | | `active_claim` | `valid_from` | `value` (§5.6) | | `active_claim` | `valid_to` | `value` (§5.6) | | `proof_tree` | `root` | `active_claim` | | `proof_tree` | `truncated` | `bool` | | `verify_result` | `match` | `bool` | | `verify_result` | `actual` | `string` | | `verify_result` | `expected` | `string` | | `verify_result` | `conflicted` | `bool` | | `refuse_info` | `reason` | `string` | | `refuse_info` | `teaching_hint` | `string` | | `refuse_info` | `discriminator` | `string` | | `engine_error_info` | `reason` | `string` | | `engine_error_info` | `code` | `string` | The last two rows name types a program cannot write: `refuse_info` and `engine_error_info` arise only as the binding of a `try` handler (§5.4), and are listed here under the names `.kind` reports for them. Field access on them is governed by this table like any other type. `claim_id` is a positional descriptor, not a persistent identity: the claim's cell path followed by `#` and its 1-based position in the result that produced it (a `get` element reads `Cat.felix.color#2`); a claim obtained through `current` carries the designator `current` in place of a position. `claim_id` is not stable across mutations of the cell; programs that need a claim's content use `.value` and `.source`. `written_by` names the access key that wrote the claim. It is derived from the credential the call was authenticated with — never from anything the program or the caller states — so unlike `source` it cannot be asserted, only observed. An access key identifier is never empty, so a claim with a writer is always distinguishable from a claim without one. `written_by` is empty when **no key wrote the claim**, which happens two different ways: the write was not authenticated, or nothing wrote the claim at all because a rule concluded it (§14). `trust` is what tells those two apart, and the distinction matters — a derived claim has no writer because there was no write, not because a write went unattributed. `valid_from` and `valid_to` report the **validity window** the claim was written with (§7.1) — the stretch of world-time the claim says something about, as distinct from when it was recorded. A **conclusion** reports the window it inherits from its premises (§14.4): the overlap of the windows of every premise it was drawn from. Both are typed `value` rather than `datetime` because a bound may be **open**. A claim valid from a date with no stated end has a `valid_to` of the `null` class (§5.6), and a claim written with no window at all has `null` for both. So a program reads these fields by matching, not by comparing: there is no sentinel instant standing for "no bound", and a program that compared against one would be reading a date the store does not hold. Only the `datetime` and `null` classes ever arise here, but a `match` still needs a `case default:` arm, since exhaustiveness (§6.2) is checked against the whole union. ``` # claim-window.dpy — a claim reports the window it is valid in, and a # conclusion reports the overlap of the windows it was drawn from. @rule def flagged(): for e in Emp: if e.status == "active" and e.dept == "eng": e.flagged = True def show(label: string, c: active_claim): match c.valid_to: case datetime as d: print(label + " until " + str(d)) case null: print(label + " has no end") case default: pass def window_report(): remember(Emp.e1.status, "active", "hr", t"2020-01-01T00:00:00Z", t"2022-12-31T00:00:00Z") remember(Emp.e1.dept, "eng", "hr", t"2021-01-01T00:00:00Z", t"2023-12-31T00:00:00Z") remember(Emp.e2.ongoing, "yes", "hr", t"2021-01-01T00:00:00Z", null) a = current(Emp.e1.dept, t"2021-06-01T00:00:00Z") show("dept", a) d = current(Emp.e1.flagged, t"2021-06-01T00:00:00Z") show("flagged", d) o = current(Emp.e2.ongoing) show("ongoing", o) ``` ``` OK script window_report(): 3 claims written, 3 prints remember Emp.e1.status = "active" remember Emp.e1.dept = "eng" remember Emp.e2.ongoing = "yes" print dept until 2023-12-31T00:00:00Z print flagged until 2022-12-31T00:00:00Z print ongoing has no end ``` `dept` is valid until 2023-12-31 and the conclusion drawn from it only until 2022-12-31, because the other premise stops there. That difference is the whole of what these two fields add: an as-of read (§7.1) tells you whether a claim is in force at an instant you name, one instant at a time, and these say where the window ends without your having to find it by asking. `maintained` is `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 since. It is `True` for every asserted claim and for every derivation whose rule is still keeping its value current. Nothing about an unmaintained claim is in disagreement with anything: it is neither a conflict (§13) nor a matter of preference (§12), and it continues to be served by every read. The store says the value is not being kept up rather than letting it pass as current, and a reader guards on it directly: ``` c = current(Totals.all.sum) match c: case active_claim: if not c.maintained: print("this total is not being kept current") case empty: pass ``` The mark is established when the claim is read, not recorded on it, so it appears as soon as the rule stops keeping the value current and clears on its own once that is no longer so. A program must therefore read it alongside the value it qualifies rather than carrying it forward: a `maintained` kept from an earlier read describes the earlier read. `truncated` is `True` when a `proof_tree` shows **less than the whole derivation** — the tree is cut off rather than complete. A proof that ended and a proof that was cut short are otherwise indistinguishable, and a cut one reads as whole, so a program that treats a derivation as exhaustive checks this first. `trust` says how the claim came to hold its value. It is one of two words: `asserted` — someone recorded this value — or `derived` — a rule concluded it. Like `written_by` and unlike `source`, it is established by the engine and cannot be written: a caller may cite the literal string `"derived"` as a `source`, and that claim still reads `trust` as `asserted`, because citing a word is not the same as being concluded by a rule. Together the two fields separate the three cases a reader meets: | `trust` | `written_by` | what happened | |---------|--------------|---------------| | `asserted` | a key | someone recorded this value, and this key did it | | `asserted` | empty | someone recorded this value, without an authenticated key | | `derived` | empty | no one recorded it — a rule concluded it | Asking who wrote a derived claim has no answer. Asking *why it holds* does: `why_not(K.s.a)` and `what_needs(K.s.a)` answer about a conclusion that is **not** there. `why` requires a claim to explain; when a read comes back empty the question is a different one, and these two answer it. `why_not` names the condition that blocked the conclusion and distinguishes five cases that are otherwise one observable: a condition never recorded, a condition recorded whose validity window does not cover the time asked about, a condition recorded that fails its test, a condition required to be absent that is present, and a condition whose sources disagree. `what_needs` names the facts that would make the conclusion hold, walking through conditions the standing rules can themselves derive and stopping at the ones only the caller can supply. Both are reads and write nothing; both answer `no standing rule concludes this` when no rule produces the cell at all, which is a different finding from an unmet condition and usually a more useful one. Where the cell asked about itself holds a claim whose validity window does not cover the time asked about, that is reported first, before anything the standing rules have to say: the fact is recorded and out of force, so what it needs is a wider window or an as-of the window covers rather than another write. Both take no `as_of`: a diagnosis is about the store as it stands. `why(K.s.a)` returns the derivation (§7.1), which is the account of a derived claim in the same way a key is the account of a written one. Anchored, `why(K.s.a, t"…")` returns the derivation **as it stood at that instant**, built from the premises whose validity windows covered it. This is what explains a changed answer: a conclusion can hold at one instant and not at another because a premise moved, and asking the same cell at two instants gives two derivations whose difference names the premise that moved. A `proof_tree` is a finite collection (§5.1) whose elements are `active_claim`s, so a program can hold both and compare them. An anchored derivation may be absent where the unanchored one is not, and the reverse. Absence here is the `empty` discriminator (§5.1) rather than a zero-length `proof_tree`, so the collection surface is for an answer already established to be 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` explains the absence. `source` and `written_by` answer different questions and are not interchangeable. `source` is the origin the writer *cited* for the content — a claim about the data, which the engine records and cannot check. `written_by` is *who performed the write* — a fact about the act, established by authentication. A claim may cite a trusted registry and have been written by anyone holding a key to the store. `path` is the claim's cell path (`Cat.felix.color`) — the `claim_id` descriptor without its `#`-position suffix. It is most useful for the reads whose claims live at cells the call site did not name: `dependents` (the cell each derived claim lives at) and `conflicts` (each conflicting cell). `created_at` is the claim's creation moment: the UTC wall-clock instant at which the claim was recorded, rendered as an RFC 3339 timestamp with microsecond precision and a literal `Z` suffix — e.g. `2026-07-04T09:15:42.123456Z`. The value is fixed when the claim is created and is the same string no matter how the claim was obtained (`current` and `get` agree). A claim recorded before the service began stamping creation moments carries the empty string. Lexicographic comparison of two non-empty `created_at` values orders them chronologically (RFC 3339 UTC is sortable). Two claims recorded within the same microsecond carry the same `created_at`, so equal values mean *recorded in the same microsecond*, not *recorded at the same moment*, and the field does not say which of the two came first. Sorting by `created_at` is a correct chronological sort in which such claims tie. `created_at` **orders claims; it does not measure elapsed time.** Ordering is the whole of what it guarantees: given two claims with different stamps, it tells you which was recorded first. The difference between two `created_at` values is **not** the time that passed between them, and no reading of it as a duration is supported — when two claims are recorded in quick succession their stamps may differ by an amount unrelated to the interval between them. This is why `created_at` is a `string` and not a `datetime`: temporal arithmetic on it is rejected at compile time rather than producing a plausible wrong answer. To record how long something took, measure it with your own clock and store the result as a `duration` (§3.5) — that value means what it says, composes with `datetime` arithmetic, and is what the aggregate folds are defined over. **Universal accessors**: - `.kind` returns `string` for any discriminator value (`active_claim`, `empty`, `verify_result`, and the try-handler discriminators of §5.4) and for `proof_tree`. The returned string is the type name as written in §5.1. - `.length` returns `int` for any `string` or any finite collection. For a `string` the result is the number of characters (Unicode characters, not bytes); for a collection it is the number of elements. The Python builtin **`len(x)`** is accepted as an alias — `len(x)` is exactly `x.length` (and a type_error when `x` is neither a string nor a finite collection). ### 5.3 Indexing and slicing **Indexing.** The expression `[]` selects one element. It is well-typed when the value is a finite collection or a `string`; the result type is: | Value type | Element type | |-----------------|--------------| | `claim_list` | `active_claim` | | `proof_tree` | `active_claim` | | `string_list` | `string` | | `subject_set` | `string` | | `result_type_set` | `string` | | `string` | `string` | | `list` | `T` | | `tuple` | the indexed position's type | | `dict` | `V` (indexed by a key of type `K`, not an `int`) | **Tuple indexing.** A tuple is heterogeneous, so `t[i]` has a type only when `i` is a **compile-time constant** integer (a literal, an optional leading minus, or a constant `+`/`-` of such): `t[0]` has the type of the first position, `t[-1]` the last. A non-constant tuple index is a type_error, and a constant index out of range is a compile-time error (both reachable without loss of function — every position is reachable by a literal index). **Dict indexing.** `d[k]` looks a value up by key; the key's type must match the dict's `K`, and the result is `V`. A key absent at run time is a catchable refuse (§10.3). Because dict keys are scalars (not necessarily `int`), dict indexing is resolved by the key type rather than the `` rule below. Indexing a `string` returns the one-character string at that position; positions count characters (Unicode characters, not bytes), starting at `0`. A **negative** index counts from the end: `s[-1]` is the last character, `s[-2]` the one before it, down to `s[-len]` (the first). Negative from-end indexing is defined for a `string` and for a **constructed `list`** (`xs[-1]` is the last element); a **store-derived** collection (§5.1) takes a non-negative index only. An index still out of range after the from-end shift — of a string or a constructed list, or a *non-negative* index of a store-derived collection — is a runtime refuse (§10.3), not a static error. The index expression MUST be of type `int`. **Slicing.** The expression `[:]` returns the substring from character position `` up to (but not including) position ``. Both bounds are optional: `s[:]` runs to the end of the string, `s[:]` starts at the beginning, and `s[:]` is the whole string. Each bound that is present MUST be of type `int`. Slicing applies to a `string` (result `string`) and to a **constructed `list`** (result `list` — a slice yields a new list of the same element type, preserving immutable value semantics); it does not apply to the store-derived collections. **Step.** A slice may carry an optional third component — the **step** — `[::]`. The step (an `int`, default `1`) selects every ``-th character. A **negative** step walks the string in reverse: `s[::-1]` is `s` reversed, and `s[::-2]` takes every other character from the end. When a step is present the bound defaults follow the step's direction: a positive step defaults `` to the beginning and `` to the end, while a negative step defaults `` to the last character and `` to before the first. A step of `0` is a catchable runtime **refuse** (`slice_step_zero`); it is the only non-total slice. A **negative** bound counts from the end, like indexing: `s[-3:]` is the last three characters, `s[:-1]` all but the last. A negative bound past the start of the string resolves to `0`. Slicing is otherwise **total** — it never refuses. A bound beyond the ends of the string is clamped to it, and a start at or past the end (or at or past the end bound) yields the empty string `""`. Positions count characters, consistent with indexing and `.length`. A negative *step* is the reverse direction; a negative *bound* is a from-end position — the two are independent (`s[-1:-4:-1]` walks the last three characters backwards). A **constructed `list`** slices by the identical rules — optional bounds, an optional step (with `xs[::-1]` reversing), clamped out-of-range bounds, negative from-end bounds, and the step-`0` refuse — producing a new `list`. `xs[a:b]` selects the elements at positions `a` up to (but not including) `b`; positions count elements, consistent with list indexing and `.length`. A **`tuple`** slices by the same rules and **yields a tuple** (Python's `t[a:b]` → `tuple`). Because a tuple is heterogeneous, the slice's result type is the sub-tuple of the selected positions — so the bounds MUST be **constant integers** (`t[1:]`, `t[:2]`, `t[1:-1]`, `t[::-1]`); a computed bound is a type_error (like a computed tuple index, §5.3). `list(t[a:b])` (§8.13) then converts the sub-tuple to a `list` — the idiom behind starred unpacking. **String methods.** A `string` value carries these built-in methods: | Method | Signature | Result | |--------|-----------|--------| | `s.find(sub[, start[, end]])` | `(string[, int[, int]]) → int` | the character position of the first occurrence of `sub` in `s`, or `-1` if absent; the optional `start[, end]` window searches `s[start:end]` and the result is an index into the whole `s` (negative bounds count from the end) | | `s.rfind(sub[, start[, end]])` | `(string[, int[, int]]) → int` | the character position of the **last** occurrence of `sub` in the `start:end` window, or `-1` if absent | | `s.index(sub[, start[, end]])` | `(string[, int[, int]]) → int` | like `find`, but **refuses** (§10.3, `substring_not_found`) instead of returning `-1` when `sub` is absent from the window | | `s.rindex(sub[, start[, end]])` | `(string[, int[, int]]) → int` | like `rfind`, but **refuses** (`substring_not_found`) when `sub` is absent from the window | | `s.count(sub[, start[, end]])` | `(string[, int[, int]]) → int` | the number of non-overlapping occurrences of `sub` in the `start:end` window; an empty `sub` yields the window's `length + 1` | | `s.startswith(prefix[, start[, end]])` | `((string \| tuple)[, int[, int]]) → bool` | `True` if the `start:end` window of `s` begins with `prefix` (an empty `prefix` yields `True`). `prefix` may instead be a **tuple of strings** — `True` if the window begins with **any** of them (an empty tuple yields `False`) | | `s.endswith(suffix[, start[, end]])` | `((string \| tuple)[, int[, int]]) → bool` | `True` if the `start:end` window of `s` ends with `suffix` (an empty `suffix` yields `True`). `suffix` may instead be a **tuple of strings** — `True` if the window ends with **any** of them (an empty tuple yields `False`) | | `s.replace(old, new[, count])` | `(string, string[, int]) → string` | a copy of `s` with each non-overlapping occurrence of `old` replaced by `new`, at most `count` times when given (default: all); an empty `old` inserts `new` in each gap | | `s.upper()` | `() → string` | `s` with each character replaced by its full Unicode uppercase — a character may expand to several (`ß`→`SS`, `fi`→`FI`), so the result can be longer than `s` | | `s.lower()` | `() → string` | `s` with each character replaced by its full Unicode lowercase (a character may expand, `İ`→`i̇`); a Greek `Σ` becomes word-final `ς` when it ends a word (preceded by a cased character, not followed by one), else `σ` | | `s.capitalize()` | `() → string` | `s` with its first character titlecased and the rest lowercased | | `s.title()` | `() → string` | `s` with the first character of each word titlecased and the rest lowercased — a word is a maximal run of cased characters, so any non-letter (space, digit, apostrophe) starts a new word | | `s.swapcase()` | `() → string` | `s` with each uppercase character lowercased and each lowercase character uppercased (the full mapping above; the lowercasing applies the word-final `Σ`→`ς` rule) | | `s.casefold()` | `() → string` | `s` case-folded for caseless matching — the full Unicode case-folding mapping, more aggressive than `lower` (`ß`→`ss`) and **context-free** (both `Σ` and `ς` fold to `σ`; NO word-final rule, so `"ΟΔΟΣ".casefold()` is `"οδοσ"`, unlike `.lower()`'s `"οδος"`) | | `s.strip([chars])` | `([string]) → string` | `s` with leading and trailing characters removed — whitespace when `chars` is omitted, otherwise any character that occurs in `chars` | | `s.lstrip([chars])` | `([string]) → string` | like `strip`, but removes only **leading** characters | | `s.rstrip([chars])` | `([string]) → string` | like `strip`, but removes only **trailing** characters | | `s.removeprefix(prefix)` | `(string) → string` | `s` with a leading `prefix` removed if `s` begins with it, otherwise `s` unchanged | | `s.removesuffix(suffix)` | `(string) → string` | `s` with a trailing `suffix` removed if `s` ends with it (and `suffix` is non-empty), otherwise `s` unchanged | | `s.expandtabs([tabsize])` | `([int]) → string` | `s` with each tab replaced by spaces to advance to the next tab stop (a multiple of `tabsize`, default `8`); the column counts characters and resets to zero after each `\n` or `\r`. A `tabsize ≤ 0` removes tabs | | `s.zfill(width)` | `(int) → string` | `s` left-padded with `'0'` to `width` characters; a leading sign (`+`/`-`) stays first and the zeros follow it. `width ≤ s.length` returns `s` unchanged | | `s.ljust(width[, fill])` | `(int[, string]) → string` | `s` left-justified in a field of `width` characters, padded on the right with `fill` (a single character, default `' '`) | | `s.rjust(width[, fill])` | `(int[, string]) → string` | `s` right-justified — padded on the **left** with `fill` | | `s.center(width[, fill])` | `(int[, string]) → string` | `s` centred in a field of `width` characters, padded with `fill`; when the padding cannot be split evenly the extra character goes on the **left** iff both the margin and `width` are odd (CPython's rule). `width ≤ s.length` returns `s` | | `s.split([sep[, maxsplit]])` | `([string[, int]]) → list` | the substrings of `s` split at each non-overlapping occurrence of `sep` (empty pieces kept); an optional `maxsplit` caps the number of splits (≤ `maxsplit + 1` pieces); with **no** argument, `s` is split on runs of whitespace with empty pieces dropped and leading/trailing whitespace ignored | | `s.rsplit([sep[, maxsplit]])` | `([string[, int]]) → list` | as `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)` | `(list) → string` | the elements of the `list` `xs` concatenated with the separator `sep` between each adjacent pair (an empty list yields `""`) | | `s.isspace()` | `() → bool` | `True` if `s` is non-empty and every character is whitespace | | `s.isdigit()` | `() → bool` | `True` if `s` is non-empty and every character is a digit | | `s.isdecimal()` | `() → bool` | `True` if `s` is non-empty and every character is a decimal digit | | `s.isnumeric()` | `() → bool` | `True` if `s` is non-empty and every character is numeric (includes decimals, fractions, and numeral characters) | | `s.isalpha()` | `() → bool` | `True` if `s` is non-empty and every character is a letter | | `s.isalnum()` | `() → bool` | `True` if `s` is non-empty and every character is a letter or a numeric character | | `s.isupper()` | `() → bool` | `True` if `s` has at least one cased character and none of them is lowercase or titlecase | | `s.islower()` | `() → bool` | `True` if `s` has at least one cased character and none of them is uppercase or titlecase | | `s.istitle()` | `() → bool` | `True` if `s` is titlecased — every uppercase/titlecase character follows an uncased one and every lowercase character follows a cased one, with at least one cased character | | `s.isascii()` | `() → bool` | `True` if every character is in the ASCII range (U+0000–U+007F); the **empty** string is ASCII (`"".isascii()` is `True`) | All character positions and widths count **characters** (Unicode codepoints), not bytes (§5.2). The case transforms (`upper`/`lower`/`capitalize`/`title`/ `swapcase`/`casefold`) apply the **full** Unicode case mapping — a character may map to more than one (so the result, and its `.length`, can grow) — and the forms that lowercase apply the Greek word-final `Σ`→`ς` rule; `casefold` is the sole exception (context-free, no word-final rule). The character-class predicates (`is…`) classify each character by its Unicode properties. Every method is total except `split`, `ljust`/`rjust`/`center`, and `index`/`rindex`: `split` refuses (§10.3, `empty_separator`) only when an **explicit** separator argument is the empty string (the argument-free whitespace form never refuses), `ljust`/`rjust` /`center` refuse (`fill_not_one_char`) when an explicit `fill` argument is not exactly one character, and `index`/`rindex` refuse (`substring_not_found`) when the substring is absent. `s.split` and `sep.join` bridge the `string` and constructed-`list` surfaces: `split` produces a `list` (§5.1) and `join` consumes one; `join`'s argument MUST be a `list` (a list of any other element type is a type_error). These are the only method calls the language defines on a built-in value. `upper()` and `lower()` apply a **character-for-character** case mapping: each character maps to its single cased form, so the result always has the same number of characters as `s` (a character whose case change would need more than one character — for example `ß` — is left unchanged). `strip()`, `lstrip()`, and `rstrip()` remove leading and/or trailing characters; with no argument they remove whitespace, and with a `chars` argument they remove any character that occurs in `chars` (the `chars` argument is a **set** of characters, not a prefix or suffix). The interior is untouched, and stripping a string down to nothing yields `""`. ### 5.4 Try-handler discriminator types A `try` statement's `except` handlers may each introduce one bound identifier (via the optional `as `, §9.2), carrying a discriminator type the user cannot write as a type annotation. When a handler omits `as ` it binds nothing and the types below simply do not arise for that handler: - **`except refuse as r`** — `r` has fields `reason`, `teaching_hint`, `discriminator`, all of type `string`. `r.kind` returns the literal string `"refuse_info"`. `reason` states what was refused, in the script's natural language. `teaching_hint` carries a suggestion for correcting the call, and is empty when there is none — it is an aid to a human reader, never a second reason. `discriminator` is a short tag naming which refusal this is, for a program that must branch rather than report; a refusal raised by `raise (…)` (§4.3) carries the exception name as its tag. - **`except engine_error as e`** — `e` has fields `reason`, `code`, both of type `string`. `e.kind` returns the literal string `"engine_error_info"`. `reason` states what failed; `code` is a short tag naming which failure this is, in the same role `discriminator` plays for a refusal. Every one of the five fields is a `string` and is always present; the ones that may carry nothing carry `""` (§5.1: the language has no absent value). The **set of tags** `discriminator` and `code` can take is deliberately not specified. Both are readable, comparable, and safe to branch on within a release, but the vocabulary is not a stable contract and this document does not enumerate it: a program that must behave differently for different failures should branch on the tags it has observed and keep a fallback arm. Programs that report rather than branch should use `reason`, which is written for a reader. These types are produced only by their corresponding handlers; they cannot be passed as parameters, returned by verbs, or written in a type annotation. Their fields are in the §5.2 table under the names `.kind` reports. ### 5.5 Type names in source Fifteen type names are valid as `type-name` tokens: the three primitives (`string`, `int`, `bool`), the five **value-class scalars** (`datetime`, `duration`, `real`, `blob`, `scientific`), and the seven read-result types from §5.1 (`active_claim`, `claim_list`, `proof_tree`, `subject_set`, `string_list`, `verify_result`, `result_type_set`). A parameter or return annotation (§4.2) additionally admits a parameterized **collection type** built from these names — `list`, `set`, `dict`, `tuple` — nestable to any depth. A **parameter** (§4.2) may be typed by any of the fifteen. A value-class-scalar parameter supplied over the wire is given as its canonical text — a `datetime` as RFC 3339 UTC (§3.5.5), a `duration` as ISO 8601 (§3.5.6), a `real` as a decimal with a point (§3.5.7), a `blob` as hex (§3.5.8), a `scientific` as its canonical numeral (§3.5.14) — and refuses if the text is malformed. A **class field** (§13.1) must be a value-class scalar — one of the eight types the engine stores as a cell value (`string`, `int`, `bool`, `datetime`, `duration`, `real`, `blob`, `scientific`) — because a field holds one stored value; the read-result types are not stored values and are not valid field types. The name `empty` is valid as a `match` case label (§6.2) but NOT as a `type-name` token. The names `refuse_info` and `engine_error_info` name the try-handler discriminator types (§5.4) but are NOT writable as `type-name` tokens. The name `value` (§5.6) names the claim-content union; it arises only from `.value` field access and is likewise NOT writable as a `type-name` token. The name `null` (§5.6) is the **absence** value class — it arises only from a `case null:` match arm and, having no payload to pass or store, is NOT a `type-name` token (a parameter or field is never `null`-typed). Type names are contextual identifiers, not reserved words (§3.7). ### 5.6 The `value` union The `.value` field of an `active_claim` (§5.2) has type `value`: the **stored content of a claim, carrying its own type**. A value written as an integer reads back as an `int`; a value written as a boolean reads back as a `bool`; a value written as text reads back as a `string`; a value written as a `datetime("…Z")` datetime literal (§3.5.5) reads back as a `datetime`; a value written as a `duration("…")` duration literal (§3.5.6) reads back as a `duration`; a value written as a `3.5` real literal (§3.5.7) reads back as a `real`; a value written as an `blob("…")` blob literal (§3.5.8) reads back as a `blob`. The type is a property of the claim, fixed when the claim is recorded, and is the same however the claim is obtained (`current` and `get` agree, as for every other field). `value` is a **tagged union** over its value classes: ``` value = int | bool | string | datetime | duration | real | null | blob | scientific ``` Eight of the nine classes are **write-producible** from DKE Python — a program writes an `int`, `bool`, `string`, `datetime`, `duration`, `real`, `blob`, or `scientific` and reads it back at that class. The remaining class, `null` (an explicit absent value), is **read-only**: it is asserted through the `assert` verb (§7.1), which carries no value argument, so no value literal produces it — but a claim carrying one is discriminable on read (see below). A program consumes a `value` in one of three ways: - **Destructure it** with a `match` (§6.2) to obtain the typed content: ``` c = current(Sensor.room.count) match c.value: case int as n: print("next = " + str((n + 1))) # n : int — arithmetic is well-typed case bool as b: print("flag = " + str(b)) # b : bool case string as s: print("text = " + str(s)) # s : string case datetime as d: print("time = " + str(d)) # d : datetime — renders RFC 3339 case duration as u: print("span = " + str(u)) # u : duration — renders ISO 8601 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 scientific as s: print("sci = " + str(s)) # s : scientific — renders the canonical numeral case null: print("an absent value") # detect-only — no `as` binding ``` A **write-producible** class (`int`, `bool`, `string`, `datetime`, `duration`, `real`, `blob`, `scientific`) supports a named `case as :` arm that binds `` to the content **at the arm's class type**, scoped to that arm, so arithmetic and other type-specific operators apply without a cast. This is the only way to recover an `int` (for arithmetic), a `bool` (for logical operators), or a `datetime` / `duration` / `real` / `blob` (to render or re-store, §8.4) from a claim's content. The one **read-only** class, `null`, is written as a **bare** `case null:` arm — it discriminates the class but binds no payload; attaching `as ` to it is a type_error (an absent value has no content to bind). - **Render it** directly. A `value` is expressible: `print()` appends its textual rendering (§8.7), and `str(…)` renders it (`"count=" + str(c.value)` → `string`, §8.4). Rendering never requires knowing the class. - **Compare it** with `==` / `!=` against a scalar literal or another `value` (§8.1). The result is always `bool`; a class mismatch compares unequal rather than coercing (`c.value == 41` is `false` when the content is the text `"41"`). A value match covers the nine named classes above, **or** any subset of them plus a `case default:` catch-all (§6.2). `case default:` keeps a `match` well-defined without enumerating every class, and also covers any class the service might add beyond this set in a later revision. A `value` cannot be written in a type annotation (§5.5) and is never constructed by a program — it arises only from reading a claim. --- ## 6. Static semantics ### 6.1 Scoping DKE Python is **lexically, function-scoped** for variables. An assignment `x = ` binds `x` in the enclosing script body, not in the `:`-headed suite that contains it: an assignment inside an `if`, `for`, `match`, `except`, or `branch` block updates the enclosing binding and its value **persists past the block**. A `for` loop body may therefore accumulate into an outer variable, and an `if` branch may conditionally reassign one. A re-assignment MUST keep the variable's type — assigning a value of a different type to a name already in scope is a type_error (§6.4); a same-type re-assignment is permitted. A name first introduced inside a block is visible within that block and its nested blocks; to read a variable *after* a block, bind it in an enclosing scope first. Script parameters are in scope for the entire body. Two bindings are **block-local** and do not leak past their block: the `for` loop variable and the `except` handler variable. Each is visible only within its own block; when the block ends the name is restored to whatever it held beforehand, or becomes unbound if it was not previously bound. `match` case clauses do not bind a new name; the scrutinee's binding (if any) stays visible inside every case body. A `branch` block rolls back the **store** on abort (§9.2.5), never variable bindings: a variable assigned inside a branch keeps its value whether the branch commits or rolls back — variables are not transactional. A path segment that names an in-scope variable (`current(k.s.a)` with `k`, `s` parameters) is resolved to that variable's value; a segment that is not an in-scope name at the point of the call is a literal kind/subject/attribute name. Because this is decided from lexical scope, a variable never captures a same-named literal segment introduced later. A resolved segment MUST be a name — the identifier shape of §3.4. A value that is not (it holds a space, a `.`, leads with a digit, or is empty) raises a `refuse` (§10) naming the value, the variable it arrived in, and which of the kind / subject / attribute positions it filled. Naming the value is what makes the refusal usable where the segments come from data: a loop writing one claim per row runs on a single line, so the line identifies the loop and only the value identifies the row. Being a `refuse` rather than an error is what lets a handler take it per row (§9.3) — see the tutorial's *Loading many facts at once* for the skip-the-bad-rows-and-keep-the-rest shape. Where the path's leading segment is a declared class, a segment that names BOTH an in-scope variable and a declared field of that class is **rejected at compile time** — the two readings write to different places and the compiler will not guess between them. Rename the variable (or address a field the variable is not named after): ```python class Box: label: string def put(id: string, label: string): remember(Box.id.label, label, "op") # rejected: `label` is both ``` ```python def put(id: string, text: string): remember(Box.id.label, text, "op") # writes Box..label ``` This restricts only the ambiguous spelling, not the capability: a segment holding a variable that is *not* a declared field of the class still resolves to that variable's value, so a computed attribute name remains expressible. A kind with no class declaration has no declared fields, so every segment there keeps the plain in-scope-variable-else-literal reading. The class may be declared by an **imported module** as well as by this one — `M.Class..` and, where the bare name resolves to it (Reference §9.6), `Class..` are checked against that module's declared fields. Where a name is declared both here and by an import, this unit's own declaration is the one checked, matching how the bare name resolves. ### 6.2 Match exhaustiveness A `match` statement's case clauses MUST cover the case set of the scrutinee's type: | Scrutinee type | Required case set | |----------------|-------------------| | `active_claim` | `{ active_claim, empty }` | | `verify_result` | `{ verify_result }` | | `value` (§5.6) | `{ int, bool, string, datetime, duration, real, null, blob, scientific }`, **or** any subset plus `case default:` | Any other scrutinee type is a type_error — except a bare instance variable, whose `match` is the distinct **class match** construct (§13.5), dispatching over class names. A missing case is a type_error (`bad-nonexhaustive-match`); a case label not in the set is a type_error; a repeated case label is a type_error. Case order is not significant. **Value match.** When the scrutinee has type `value` (§5.6), the case labels are the nine value-classes `int`, `bool`, `string`, `datetime`, `duration`, `real`, `null`, `blob`, and `scientific`. Like a class match (§13.5), the arms MUST either cover all nine classes or provide a `case default:` catch-all; a value match that is neither exhaustive nor defaulted is a type_error. A **write-producible** class (`int`, `bool`, `string`, `datetime`, `duration`, `real`, `blob`, `scientific`) MAY bind the content with a named `case as :` arm — `n : int` inside `case int as n:` — scoped to the arm; the binding is optional (`case int:` with no `as` is well-formed). The one **read-only** class, `null`, is a bare `case null:` arm only: attaching `as ` to it is a type_error, because an absent value has no content to bind. A `case default:` arm likewise MUST NOT carry an `as` binding (it spans more than one class, so no single payload type exists). The bound identifier obeys the reserved-word rule (§6.6) and is visible only within its arm. ### 6.3 Bounded iteration A `for x in :` statement MUST have `` of a finite collection type (`claim_list`, `proof_tree`, `string_list`, `subject_set`, `result_type_set`, `diagnosis`, or a constructed `list`, `set`, or `dict`) or a `string`. Iterating a `diagnosis` binds its report **lines**, each a `string` (§5.1). Iterating a `dict` binds its **keys**; iterating a `set` binds its elements in sorted order; iterating a `string` binds each **character** — a one-character `string`, by Unicode character (not by byte), matching Python. A `tuple` is deliberately **not** iterable (it is heterogeneous — index it by a constant, §5.3). Any other iterand type is a type_error (`bad-unbounded-for`). The loop variable `x` carries the collection's element type (§5.3) within the loop body. A **comprehension** (§8.9) is bounded iteration in expression position, subject to the same finite-iterand rule. This rule, together with the absence of any recursion construct (§9.7), gives DKE Python its termination guarantee (§9.5). ### 6.4 Assignment type agreement A bare assignment `x = ` binds `x` to the initializer's static type. Binding a statement-only verb (§7.4) is a type_error — the right-hand side carries no result value. ### 6.5 Name arguments The name argument of the wire verbs (`compile`, `forget script`, `info script`) is a **bare identifier** whose form is identifier-shaped per §3.4: first codepoint `XID_Start`, remaining codepoints `XID_Continue`. The identifier is a **name**, not a string value; it denotes the script or module it names, verbatim. A violation is rejected at compile time (parse_error). ### 6.6 Reserved-word constraint A user identifier (declaration name, parameter name, loop variable, handler binding, assignment target) MUST NOT be any of the reserved words in §3.7 (a)– (d). DKE raises this at the lexer or parser; a conforming implementation MAY raise it at the typechecker. ### 6.7 Scope resolution for plain identifiers and paths A bare identifier in expression position MUST resolve to a parameter, an assignment binding, a `for` binding, or an `except` handler binding visible in the current scope. An unresolved identifier is a type_error (`bad-undeclared`). A dotted path `H.` is classified by the type of its head identifier `H`: - If `H` is in scope with any non-`string` type, the path is a **field-access chain** on `H`'s value; each segment after `H` MUST be a field of the previous segment's type (§5.2). - If `H` is in scope with type `string`, the path is a **slot-grammar reference** addressing the store cell named by kind `H` and the following slot segments; slot-grammar references are meaningful only as verb-call arguments. A `string`-typed segment resolves to that binding's value at invocation; otherwise the segment is taken verbatim as a slot name. - If `H` is not in scope, the path is a type_error — the kind position of a verb path MUST be a `string`-typed identifier in scope. ### 6.8 Calls between scripts A call `()` whose head is not a verb head-word resolves as a stored-script invocation under the **compile-before-call** rule: the callee MUST be an EARLIER declaration of the same compile unit or an already-stored script. A forward reference to a LATER declaration of the same unit is rejected. The same-unit call graph is therefore acyclic by construction (§9.7). Argument count and types are checked against the callee's declared parameters at compile of the unit. This holds for both call positions. A **call statement** (§4.3) may name a void or a value script and discards any result. A **value-call** in expression position (§4.4) MUST name a value script (§4.2); its result type is the callee's declared return type, and naming a void script — or a script not yet declared — where a value is expected is a type_error. The compile-before-call rule makes a value-call's return type known at the call site. ### 6.9 Exhaustive return A value script (`def f(...) -> type:`, §4.2) MUST return a value on **every** path through its body. A conforming implementation checks this conservatively: a suite *definitely returns* iff its last statement definitely returns, where - a `return ` definitely returns; - an `if`/`else` with a non-empty `else` definitely returns iff **both** its `then` and `else` suites do; - a `match` (already exhaustive, §6.2) definitely returns iff every arm does; - every other statement (including a `for`, which may run zero times) does not. A value script whose body does not definitely return is a type_error. The check is sound (it never accepts a value script that could fall off its end with no value) and conservative (it may reject a value script that happens to return on every dynamic path but not by the structural rule above — add a trailing `return`). A void script (no `-> type`) is never subject to this rule; a bare `return` in it is a plain early exit (§9.2.8). --- ## 7. Verb surface DKE Python reuses DKE's published canonical verb surface, shared with the base member. Each verb has a fixed **call form**, a fixed position (statement, expression, or both), and a fixed result type when used in expression position. The path argument uses the slot symbols `K` (kind), `K.s` (kind + subject), `K.s.a` (kind + subject + attribute), `K.a` (kind + attribute). ### 7.1 The in-language verbs | Call form (canonical) | Position | Result type | |-----------------------|----------|-------------| | `remember(K.s.a, v, src)` / `remember(K.s.a, v, src, t"…", t"…")` | stmt | (void) | | `update(K.s.a, v, src)` / `update(K.s.a, v, src, t"…", t"…")` | stmt | (void) | | `forget(K.s.a)` / `forget(K.s)` / `forget(K.s.a, v, src)` / `forget(K.s.a, t"…")`  /  `forget(
, recorded_before=t"…")` | stmt | (void) | | `assert(K.s.a, src)` | stmt | (void) | | `prefer(K.s.a, src)` | stmt | (void) | | `unprefer(K.s.a)` | stmt | (void) | | `pin(K.s.a)` | stmt | (void) | | `unpin(K.s.a)` | stmt | (void) | | `current(K.s.a)` / `current(K.s.a, t"…")` | expr | `active_claim` | | `get(K.s.a)` / `get(K.s.a, t"…")` | expr | `claim_list` | | `why(K.s.a)` / `why(K.s.a, t"…")` | expr | `proof_tree` | | `why_not(K.s.a)` | expr | `diagnosis` | | `what_needs(K.s.a)` | expr | `diagnosis` | | `caveats(K.s)` | expr | `claim_list` | | `dependents()` | expr | `claim_list` | | `conflicts()` | expr | `claim_list` | | `verify(K.s.a, v)`  /  `verify(K.s.a, v, src)` | expr | `verify_result` | | `agreement(K.s.a, v)` | expr | `int` | | `writers(K.s.a, v)` | expr | `int` | | `would_forget(
, recorded_before=t"…")`  /  `recorded_at_or_before=` / `valid_before=` / `valid_at_or_before=` | expr | `int` | | `subjects(K.a, v)` | expr | `subject_set` | | `list_subjects(K)` / `list_subjects(K.a)`  /  either with `, t"…"` | expr | `subject_set` | | `list_attributes(K)`  /  `list_attributes(K.s)` / `list_attributes(K.s, t"…")` | expr | `string_list` | | `list_values(K.a)` / `list_values(K.a, t"…")` | expr | `claim_list` | | `list_categories()` | expr | `string_list` | | `list_pinned()` | expr | `string_list` | | `list_result_types()` | expr | `result_type_set` | | `list_scripts()` | expr | `string_list` | 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. They are **soft keywords**: recognized as a verb only immediately before `(`, so the same spelling remains a usable ordinary identifier elsewhere. `branch`, `commit`, and `rollback` are language constructs (§4.3, §9.2.5, §9.2.6), not verbs, and are spelled directly in DKE Python syntax. **As-of reads.** `current`, `get`, `why`, `list_subjects`, `list_values` and `list_attributes(K.s)` accept an optional `datetime` (§3.5.5) final argument naming the time the read is answered **as of**. `current(K.s.a, t"…")` yields the single value active then, `get(K.s.a, t"…")` the claims valid then, and `why(K.s.a, t"…")` the derivation as it stood then — the premises that were in force at that instant, which is not always the derivation that holds now and is sometimes a derivation where none holds now at all; the three enumerations list what a traversal would find at that time — `list_subjects(K, t"…")` the subjects of the kind, `list_values(K.a, t"…")` the values at the attribute, `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 (below) is in play. A fact carried without a window is valid at all times, so its as-of value is its present value. The time may be **future as well as past**. A scheduled commitment written with a window that has not yet opened is not part of the present, so nothing at the present reports it — the anchor is how it is read back, and on the enumerations it is how it is found at all. **An enumeration that finds nothing says why, when the reason is an import.** The `list_*` reads answer with a collection, so "nothing is there" and "that kind is not here" are the same empty result. Where the store can tell the two apart it refuses instead of answering empty, in the two cases a missing `import` produces: - the name is itself a stored module (`list_attributes(catalog.Widget)` with no `import catalog` reads `catalog` as a kind and `Widget` as a subject); - some stored module declares a class of the name asked for (`list_attributes(Widget)` reads a global kind `Widget`, which does not exist, while `catalog` declares one). Both name the module and the `import` that reaches it. Both are gated on the kind being **absent**, so an enumeration that is legitimately empty — a kind that exists with no subjects yet, or a name no module declares — still answers empty and means it. **Kind names in a listing are addressable.** `list_categories()` names a kind a module declares in the qualified form `.` — the form §7.1's verbs take, given an `import` of that module (Reference §9.6). A kind no module declares carries no qualifier and is named as written. A name a listing returns is always a name the language accepts. Two reads take no as-of argument, because neither answers about an instant. `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. Note that `list_attributes` therefore 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 one where it is not accepted is a compile error naming the form that takes it. **Validity windows.** `remember` and `update` accept an optional pair of trailing `datetime` (§3.5.5) bounds — a **from** time and a **to** time — naming the window during which the written fact is valid: `remember(K.s.a, v, src, datetime("2019-01-01T00:00:00Z"), datetime("2021-01-01T00:00:00Z"))`. Either bound may be the literal `null`, leaving that side **open** — `t"2024-…", null` is valid from 2024 onward with no end, and `null, t"2024-…"` up to 2024 with no start; at least one bound must be given. Omitting the pair records an **always-valid** fact (the default). Both bounds are inclusive. A windowed fact is selected by an as-of read whose time falls inside its window (above), so two writes at one cell with non-overlapping windows — and **distinct sources**, since one source may not assert two different current values at a cell — model a value that changed over time. **Forget is hard, and every form names what it takes.** `forget` takes a path — `K.s.a` (one cell) or `K.s` (a whole subject) — or that path plus the value and source that name one claim, `forget(K.s.a, v, src)`. Both `v` and `src` are required in the claim-scoped form, because a value alone does not name a claim: two sources may record the same value at one cell. `v` MAY be of any type a value can be written with — `string`, `int`, `bool`, `real`, `datetime`, `duration` or `blob` — and it is matched **by value and by type together**. A cell may hold one text in two types, so `5` and `"5"` name different claims and a literal of the wrong type names none: the call is a refuse, and the refusal states the type recorded there. Type equality in this form is EXACT. §8.1 makes `int` and `real` one numeric family for comparison, and that widening does NOT extend here: a removal names a specific claim and takes it permanently, so an `int` literal never reaches a stored `real`. A fourth form is **time-scoped**: `forget(K.s.a, t"…")` removes the values at that cell whose validity window (§7.1) covers the instant named, and leaves every other value there standing. It is the removal counterpart of an as-of read — the same instant that would tell you what was in force selects what to remove. The time-scoped form takes a `K.s.a` path only: an instant narrows which values AT A CELL are named, and a subject holds many cells with many windows rather than one window to narrow. Offering a time on a `K.s` path is a compile error naming the two forms that would have worked. The two-argument forms are told apart by the **type** of the second argument, not by counting: a `datetime` is the time-scoped form, anything else is the start of the claim-scoped one and its source is still required. A fifth form is **range-scoped** and is spelled with a keyword argument: `forget(K.s.a, recorded_before=t"…")` removes the older versions before the instant, and **never the value in force**. It is the only removal form that cannot empty what it names, and that guarantee is the reason it is a separate address rather than an option on the others. It is also the only form that takes more than a cell. Three widths — `K.s.a` (one cell), `K.s` (every cell of one subject), `K` (every cell of the kind) — and the safety property is the same predicate at each, so a kind-wide range cannot empty anything. `K` is an address ONLY with a range: a bare `forget(K)` is refused at compile time. Four keywords choose an axis and a boundary: `recorded_before=` / `recorded_at_or_before=` select by when a version was **written**, `valid_before=` / `valid_at_or_before=` by when it stopped **being true**. A version carrying no closed validity window is not named by any `valid_*` range, so the two axes may report different counts over the same cell; that is the axes disagreeing, not an error. There is no `after` spelling: it would name the versions newer than the instant, reaching the value in force, and removing a current value is what the first four forms are for. The range form is keyword-only. A positional instant already means the time-scoped form above, the two select disjoint sets of versions, and a call that could be read as either would have no diagnostic available to catch it. `would_forget(K.s.a, recorded_before=t"…")` returns, as an `int`, how many versions the matching range would remove — removing none of them, recording nothing, and requiring only a read grant. It takes the same three widths as the range removal, so every removal that can be written has a preview that can be written, and both read one selection rather than agreeing by convention. The bound is required; there is no bare form. Removal is **irreversible**. `forget(K.s.a)` permanently removes every value ever recorded at the cell, not just the current one; `forget(K.s)` removes the whole subject, after which its kind is gone; `forget(K.s.a, v, src)` removes exactly the claim it names and leaves every other claim at that cell standing; `forget(K.s.a, t"…")` removes the values in force at that instant and leaves the rest. Nothing is retained in history and nothing can be reinstated. This is the D of CRUD, and it means what it says. **Removal cascades; it does not refuse.** Forgetting a fact that other facts were derived from succeeds, and those derived facts go with it. Derived facts are conclusions the engine can rebuild, not data you wrote — so a conclusion that some other standing rule still supports is re-derived immediately and stays. The practical guarantee is that a removal always completes: "removed" never means "removed unless something pointed at it." **Removal needs the delete grant.** A key scoped `read-write` can add and revise but cannot remove; removal requires a `read-write-delete` key. A key's scope is fixed when the key is issued and is not something a program can change, so a `forget` that exceeds it is refused before any statement runs. **Absence-assertion verb carries no value.** `assert(K.s.a, src)` asserts that the value at `K.s.a` is known to be absent per `src` — an assertion observably distinct from there being no claim at all. **One data-read script verb runs in-language; the rest are wire-only.** The `list_scripts()` verb executes from inside a program, reading stored script data (`list_scripts()` → `string_list` of names). The remaining script-lifecycle verbs — `forget script` and `info script` (Wire §9.2) — are **wire-only**: using one inside a program body is rejected at compile time with a type_error that teaches the wire route. The service stores no source text, so there is no source-readback verb. #### 7.1.1 Aggregate query functions An **aggregate query** computes a summary value over a whole attribute of stored data — the values of one attribute across every subject of a kind. It is a **read-only** expression: it never changes the store. Three call shapes, by the function's arity: | Shape | Call form | Meaning | |-------|-----------|---------| | single-attribute | `fn(K.attr)` | fold `K.attr` over all subjects of `K` | | ranked | `percentile(K.attr, )` | the ``-th percentile (rank `0`–`100`) of `K.attr` | | two-attribute | `fn(K.x, K.y)` | fold the paired `(K.x, K.y)` values (same kind `K`) | The available folds: | Family | Functions | |--------|-----------| | totals | `count`, `sum`, `product` | | central tendency | `avg`, `median`, `midpoint`, `mode`, `geomean`, `harmmean`, `rms` | | spread | `min`, `max`, `span`, `variance`, `stdev`, `iqr`, `mad`, `cv` | | shape | `skewness`, `kurtosis`, `entropy` | | identity / positional | `distinct`, `argmin`, `argmax`, `first`, `last` | | ranked | `percentile` | | two-attribute (association / regression) | `covariance`, `correlation`, `slope`, `intercept`, `rsquared` | The **identity / positional** folds answer *"which"* and *"when-ordered"*, where the others answer *"how much"*: `distinct(K.attr)` is the number of **distinct values** in the attribute (where `count` counts the values THEMSELVES, so a location holding two values in force contributes two — §7.6); `argmin(K.attr)` / `argmax(K.attr)` return the **subject** whose value is smallest / largest (the identity, where `min`/`max` return the value); `first(K.attr)` / `last(K.attr)` return the **earliest- / latest-recorded** current value (by when it was recorded, not by magnitude). When several subjects tie for the extreme, `argmin`/`argmax` return the first subject in name order. The two-attribute folds take two attributes of **one** kind (`slope(Point.x, Point.y)`); both attributes are read over the same subjects. `K`, `attr`, `x`, `y` follow the ordinary slot-grammar rules (§7.2) — each may be a literal name or a `string` parameter/variable resolved at runtime. **Result type.** An aggregate query returns a `value` (§5.1). Its runtime class follows the attribute(s): a numeric attribute yields a number (`int` or `real`); over a `datetime` or `duration` attribute, a fold yields a `datetime` or `duration` as appropriate. Three folds do not follow the attribute: `distinct` always yields an `int` (a count), and `argmin`/`argmax` always yield a `string` (the subject), regardless of the attribute's class; `first`/`last` follow the attribute like the value folds. Because the class is not fixed at compile time, bind the result to a name and destructure it with `match` (§9.2.3) to consume a specific class, or use it directly wherever a `value` is expressible (`print`, `+`, `==`). **Units, for a fold over a `datetime` or `duration` attribute.** Most folds return a `duration` (or `datetime`), which carries its own units — `stdev` over durations reads back as `PT1H30M`, and the question does not arise. Four folds instead return a **plain number** whose magnitude depends on a unit that has to be chosen: `variance` (a squared span), `covariance` (a span times the other attribute's unit), `slope` where the *first* attribute is temporal (a rate per unit of time), and `product`. **For these, the unit is the SECOND.** So a variance over durations of one and two minutes is `3600` (seconds squared), and a slope against a `datetime` is a change per second. This is worth stating because nothing about the value itself reveals which unit was chosen, and a statistic read in the wrong unit is wrong by a large factor rather than visibly broken. **Position.** An aggregate query reads the service, so — like `current` and the other reads — it is used in **expression position bound to a name on its own line** (`m = avg(Reading.value)`), then referenced; it may not be written as a bare argument to another call. An aggregate over an attribute with no data is a runtime refuse (§10.3). A fold that **compares by value** — `sum`, `avg`, `min`, `max`, `stdev`, `argmin`, `argmax`, and the rest — over an attribute whose values are **not numbers** (a text attribute, or one mixing numbers with non-numeric values) is likewise a runtime refuse: the fold declines rather than treating a non-number as zero. The folds that do **not** 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 this 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. The fold names are **soft keywords**: recognized as an aggregate only immediately before `(`, so every name remains a usable ordinary identifier elsewhere. ### 7.2 Slot validity Slot identifiers (kind, subject, attribute, source names) are strings under §3.4 (UAX #31). At runtime, an implementation MAY refuse a slot containing characters not in the target service's identifier alphabet; this is a refuse, not a type_error. Values (the `v` in `remember`, `update`, `verify`, and `subjects`) are **scalar literals** — a `string`, an `int`, or a `bool` — and are NOT identifier-shaped; the two **write verbs** (`remember`, `update`) additionally accept a `datetime` literal (§3.5.5), a `duration` literal (§3.5.6), a `real` literal (§3.5.7), or a `blob` literal (§3.5.8). The value slot is type-checked against these types; a compound value (a `claim_list`, a path, and so on) is a type_error. - A **write verb** (`remember`, `update`) records the value **with its literal type**: `remember(K.s.a, 42, src)` stores the `int` `42`, `remember(K.s.a, True, src)` stores the `bool` `true`, `remember(K.s.a, "42", src)` stores the text `"42"`, `remember(K.s.a, datetime("2026-01-02T03:04:05Z"), src)` stores a `datetime`, `remember(K.s.a, duration("PT1H30M"), src)` stores a `duration`, `remember(K.s.a, 3.5, src)` stores a `real`, and `remember(K.s.a, blob("48656C6C6F"), src)` stores a `blob`. The recorded type is a property of the claim and reads back through `.value` (§5.6). - The **query verbs** (`verify`, `agreement`, `writers`, `subjects`) compare **type-discriminatingly**: the query literal's type is part of the match, so `subjects(K.a, 42)` selects the subjects whose value at `K.a` is the `int` `42` and does **not** select a subject carrying the text `"42"`; `subjects(K.a, "42")` selects text `"42"` only. `verify(K.s.a, v)` reports a match only when the stored value and its type agree with `v`. This is the same equality `==` follows (§8.1), applied at the query boundary: a class mismatch compares unequal rather than coercing, and no value is widened or narrowed to fit — **with §8.1's one numeric exception, which applies here too.** `int` and `real` are one numeric family, so `subjects(K.a, 5)` selects a subject whose value is the `real` `5.0` as well as one whose value is the `int` `5`, and `verify(K.s.a, 5)` matches a stored `5.0`. It is the number that is compared, never its spelling — so a stored `5.0` matches the literal `5` while a stored `5.5` does not, and a matched claim still reads back at the type it was written (`.value` on that claim is `5.0`, not `5`). Everything else stays discriminating — the text `"5"` is a different class and does not match, and a `bool` is not a number (`True` does not match `1`). This is what makes a query verb and a rule premise answer "which subjects have `K.a == 5`" the same way (§14.2); when they differed, the rule surface was the one following this rule. `datetime`, `duration`, `real`, and `blob` are **not** query-slot types in this version: such a literal in `verify` / `agreement` / `writers` / `subjects` is a type_error. A `real`-valued claim is therefore reached with the equal `int` literal where one exists (`subjects(K.a, 5)` finds `5.0`); where none does (`5.5`), read the claim back and match its `value` (§5.6). - `agreement(K.s.a, v)` returns, as an `int`, **how many distinct sources recorded `v` at `K.s.a`** (type-aware, as above). It is a count of corroboration, **not a judgment of truth**: a value recorded by many sources is not thereby correct, and the language does **not** assert those sources are independent — it reports only how many recorded the value and never ranks or certifies them. Which sources to trust is the caller's judgment; read them by name with `get` (§7.1). `agreement` counts every source, so it takes **no** source argument (one is a type_error). A cell that never held `v` reports `0`. - `writers(K.s.a, v)` returns, as an `int`, **how many distinct access keys wrote `v` at `K.s.a`** (type-aware, as above). It is the companion of `agreement` on the other provenance axis, and the two answer genuinely different questions: `agreement` counts what was **cited**, `writers` counts who **wrote**. Three sources cited by one key is corroboration a single party assembled; one source written by three keys is three parties independently recording the same thing. Reading either as the other is the mistake this pair exists to prevent. Like `agreement` it is a count, never a judgment, and it takes **no** source argument. A claim written outside an authenticated call has no key and is not counted — so `writers` may be lower than `agreement` at the same cell, and a cell whose claims were all written unauthenticated reports `0`. A path whose segment count does not match the verb's slot shape is a runtime refuse with a teaching message. ### 7.3 Source argument The source attribution of the write verbs (`remember`, `update`), of `assert`, and of the optional third argument of `verify` is the last call argument and MUST be a `string`. The source identifier's content is subject to the runtime constraints of the target service (typically: XID-shaped, no `@` / `:` / `/`); a non-conforming source is a runtime refuse. ### 7.4 Statement-position vs expression-position A verb listed as **stmt** in §7.1 MUST appear only as a statement (not bound by an assignment, not embedded in a larger expression). Binding a stmt-position verb is a type_error (§6.4). A verb listed as **expr** produces a value of the named result type and may bind an assignment, be a `match` scrutinee (if a discriminator), be iterated (if a finite collection), or be composed with operators per §8. ### 7.5 Write-verb semantics - **Writes are permissive.** `update(K.s.a, v, src)` on a location with no active claim succeeds and establishes the claim — it does not require a prior `remember`. - **`pin` marks; it does not protect.** `forget` on a pinned location succeeds and removes the claim (and its pin). - **Writes are durable as executed.** A later statement's failure does not undo earlier writes; transactional grouping is the `branch` construct's job (§9.2.5). - **`forget` removes what you address.** `forget(K.s.a)` removes the whole cell and `forget(K.s)` the whole subject, as above. `forget(K.s.a, v, src)` removes **one claim** — the one recording value `v` from source `src` — and leaves every other claim at that cell untouched. The value and the source are **both** required: a value alone does not name a claim, since two sources may record the same value at one cell. Naming a claim the cell does not hold is a refuse (§10.3), not a silent no-op; `get(K.s.a)` lists what is actually there. `forget(K.s.a, t"…")` addresses by **time** instead of by value: it removes the values at that cell whose window covers the instant. An instant no value covers removes nothing and is not an error — unlike the claim-scoped form, it names a moment rather than a claim, and a moment nothing was true at is an ordinary answer. ### 7.6 Disagreement between sources Two claims may stand at one location with **different values from different sources**. That is a state the store holds, not an error. - **Both claims remain.** Neither write fails and neither claim is discarded. Reads at the location keep working. - **Disagreement is between VALUES at a location.** It is a property of what the claims say. Which caller recorded a claim does not enter into it, and neither does which source each one cites: a rule that concludes on both sides of a disagreement is a single producer, and the location it concludes at is in disagreement like any other. `conflicts()` and `caveats()` report it. - **Nothing resolves a disagreement for you.** The service never chooses between the claims and never marks a disagreement settled. No verb takes a disagreement as its argument. What it will do is **record which source you act on**: `prefer(K.s.a, src)` states that at this location you go by `src`. That is your judgment held beside the claims — it changes no claim, discards nothing, and leaves the location in disagreement. - **A disagreement ends when the claims change.** `update` one of them, or `forget` one of them, and the location is no longer in disagreement. It clears as a consequence of ordinary claim writes — that is the only way it clears. - **A standing rule reads every value at a location in disagreement** (§14) and derives from each one that satisfies its condition. Two sources disagreeing `m` against `n` therefore yield two conclusions, one drawn from each, and the disagreement travels into the conclusion rather than stopping at the premise. Deriving from both sides is not a resolution: nothing chooses between the claims, and the location stays in disagreement. - **A preference covers the sources it weighed.** It holds until you withdraw it with `unprefer(K.s.a)`. If a further source later disagrees at that location, that is a disagreement you have not spoken to, and `.preferred` reads `False` on every claim there until you state a preference over the sources now present. Deriving is unaffected either way — a preference records a judgment and marks a claim; it does not steer a rule. `conflicts()` (§7.1) answers which locations are in disagreement at the moment you call it; `caveats(K.s)` asks the same question about one subject. A read of a location where you have stated a preference returns **every** claim standing there, exactly as it did before — a preference marks a claim, and changes neither what a read gives back nor what a rule derives. Each claim carries **`.preferred`** (§5.2): `True` on the one you act on, `False` on the rest. It reports whether your judgment is in force, so it reads `False` on every claim at a location where a source you have not weighed is disagreeing. `current(K.s.a)` still refuses a location holding competing values; use `get(K.s.a)`. It refuses on the CLAIMS standing there, not on how many sources wrote them — a rule reading a location in disagreement concludes once per side (§14.4), and all of its conclusions cite the same `derived` provenance, so a derived location can hold competing values from one source. Counting sources would have made that location read as settled and returned one of its two values. `verify(K.s.a, v)` answers at such a location rather than refusing, and it answers about **every** claim standing there: `.match` is `True` when `v` is one of the competing values, so at a location holding both `"20"` and `"99"`, verifying either one matches. Both are recorded there, and the store reports what it holds rather than choosing between them. Because there is no single value at such a location, `.actual` reports **none** — it is the empty string — and **`.conflicted`** (§5.2) is `True` to say why. That distinction is the point of the field: an empty `.actual` also arises at a location where nothing has been written, and the two are not the same observation. `.conflicted` is `False` there, and `False` at any ordinary location, where `.actual` reports the value that stands. A **source-scoped** `verify(K.s.a, v, src)` is never marked conflicted. It asks what one source recorded, which has a single answer however loudly the others disagree — so `.actual` carries that source's value even at a location in disagreement. --- ## 8. Built-in operators and functions ### 8.1 Comparison | Operator | Signature | |----------|-----------| | `==`, `!=` | `(string, string)`, numeric `(N, N)` for `N ∈ {int, real}` (mixed `int`/`real` compares numerically, `1 == 1.0` is `True`), `(bool, bool)`, `(D, D)` for a discriminator `D` (compares `.kind`), `value` against any of `string` / `int` / `bool` / `value`, `(list, list)` for a matching element type `T`, `(tuple<…>, tuple<…>)` for a matching tuple type, `(set, set)` for a matching element type, or `(dict, dict)` for a matching key and value type `→ bool` | | `<`, `>`, `<=`, `>=` | `(N, N) → bool` for numeric operands `N ∈ {int, real}` (mixed `int`/`real` compares numerically), `(string, string) → bool` **lexicographically** by character (Unicode codepoint order), `(datetime, datetime) → bool` **chronologically**, `(duration, duration) → bool` by **length**, `(list, list) → bool` for an orderable `T`, or `(tuple, tuple) → bool` for two tuples of the same type with orderable elements — lists and tuples compare **element-wise lexicographically** | | `in`, `not in` | `(string, string) → bool` — substring **membership** (`sub in s` is `True` when `sub` occurs anywhere in `s`; the empty string is in every string) — or element **membership** `→ bool`: `x in xs` over a constructed `list`, `x in s` over a `set`, `x in t` over a homogeneous `tuple`, or `k in d` over a `dict` (testing its **keys**); `not in` is the negation of any | **String ordering** (`<`, `>`, `<=`, `>=` on two strings) compares **lexicographically** — character by character in Unicode codepoint order, the shorter string ordering first when it is a prefix of the longer (`"a" < "ab"`). So an uppercase letter orders before a lowercase one (`"Z" < "a"`), matching Python. Each ordered comparison takes two operands of the same family — two numbers, two strings, two `datetime`s, two `duration`s, or two collections; a string compared against a number is a type_error (no coercion). Comparisons **chain** (`a < b < c` is `(a < b) and (b < c)`, §4.6). **Temporal ordering** (`<`, `>`, `<=`, `>=`) compares two `datetime` values **chronologically** — the earlier instant orders first — and two `duration` values by **length**, the shorter first. Both compare by value, not by spelling: `duration("PT90M") < duration("PT1H30M")` is `False` and so is `>`, because the two denote the same length (§3.5.6), while `duration("PT90M") <= duration("PT1H30M")` is `True`. Likewise a datetime written with fractional seconds orders against one written without them by the instants they denote, not by their text (`datetime("2026-01-02T03:04:05Z") < datetime("2026-01-02T03:04:05.5Z")`). A `datetime` and a `duration` are different things — an instant and a length — so comparing one against the other, or against a number or string, is a type_error. Temporal values are **orderable elements**, so they may also be sorted (`sorted(timestamps)`) and compared inside lists and tuples. **List and tuple ordering** (`<`, `>`, `<=`, `>=`) is **element-wise lexicographic** (Python): the first pair of unequal elements decides, and if one sequence is a prefix of the other the shorter orders first (`[1, 2] < [1, 2, 3]`, `(1, 2) < (1, 3)`). Two lists must share an **orderable** element type; two tuples must be the **same tuple type** with orderable elements (a homogeneous or heterogeneous fixed tuple, or a variadic tuple — a cross-type / different-arity tuple ordering is a deferred rung). An **orderable** element type is a numeric type, `string`, `datetime`, `duration`, or a **nested list/tuple whose own element types are (recursively) orderable** — so the comparison recurses all the way down (`[[1], [2]] < [[1], [3]]`; `[[2]] < [[10]]` is `True` because element `2 < 10`, not a comparison of rendered text). A non-orderable element (e.g. `[1] < ["a"]`, mixing `int` and `string`) is a type_error. An empty list orders before any non-empty list (`[] < [1]`). **Numeric equality** (`==` / `!=`) coerces across `int` and `real`: `1 == 1.0` is `True`, `2.0 == 2` is `True`, `1 == 2.0` is `False` — the same numeric comparison the ordered operators use, and matching Python. A `bool` operand (`True == 1`) or a non-numeric one (`"7" == 7`) still requires a matching type. **List equality** (`==` / `!=`) is element-wise and **element-type strict**: the two lists must have a matching element type (`list == list` is a type_error; the element-wise numeric coercion Python does, `[1] == [1.0]` → `True`, is a deferred follow-on — the SCALAR `1 == 1.0` coerces, above), an empty `list` unifies with any list (`[] == [1]` compares to `False` rather than type-erroring), and lists compare unequal when their lengths differ or any pair of elements differs (recursively, for nested lists). **List membership** (`x in xs`) tests a constructed `list` and requires `x` compatible with the element type `T`. The `in`/`not in` operator does **not** test a store-derived set; to walk one, use the `for in :` statement (§6.3, §9.2.2), whose `in` is the loop keyword, not this operator. **Tuple equality** is kind-strict like list equality: two tuples compare only when they have a matching tuple type (a differing arity or position type is a type_error), and equal tuples agree position by position. **Set equality** is element-wise and order-independent — two sets of a matching element type are equal when they hold the same elements (a differing element type is a type_error). **Set membership** (`x in s`), **dict membership** (`k in d`, over keys), and **tuple membership** (`x in t`, over a homogeneous tuple's elements) require the item compatible with the set element type, dict key type, or tuple element type. **Dict equality** (`==` / `!=`) is **order-independent** (Python dict equality): two dicts of a matching key and value type are 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 like list equality — a differing key or value type (`dict == dict`) is a type_error — and an empty dict unifies with any dict, so `{} == {"a": 1}` compares to `False` rather than type-erroring. A `value` (§5.6) may be compared with `==` / `!=` against a scalar literal or another `value` without first destructuring it; the result is `bool` regardless of the runtime class, and a class mismatch compares **unequal** rather than coercing (`c.value == 41` is `false` when the content is text). This mirrors Python's cross-type `==`. Ordering (`<`, `>`, …) requires numeric operands (`int` or `real`), so a `value` must be destructured through `match` (§5.6) into a numeric arm before it can be ordered. ### 8.2 Logical | Operator | Signature | |----------|-----------| | `and` | `(T, U) → T ⊔ U` — short-circuit, **operand-return** | | `or` | `(T, U) → T ⊔ U` — short-circuit, **operand-return** | | `not` | `any → bool` | **Truthiness.** Every value has a **truth value**, so any value may be used where a condition is expected — an `if` / `elif` condition (§9.2.1), a comprehension `if` filter (§8.9), the condition of a conditional expression `a if c else b` (§8.10), and the operands of `and` / `or` / `not`. **Falsy** values are `False`, `0`, `0.0` (and `-0.0`), a zero `scientific`, a zero `duration`, the empty string `""`, an empty `list` / `set` / `dict` / `tuple`, an empty `blob`, and `None`; every other value — every non-zero number, every non-empty container, every `datetime`, every class instance — is **truthy**. This matches CPython. **`and` / `or` return an operand, not a coerced bool.** `a and b` evaluates `a`; when `a` is **falsy** it returns `a` (leaving `b` unevaluated), otherwise it returns `b`. `a or b` evaluates `a`; when `a` is **truthy** it returns `a` (leaving `b` unevaluated), otherwise it returns `b`. So `name or "anonymous"` is `name` when it is a non-empty string and `"anonymous"` when it is empty; `count or 0` is the first non-zero of the two; `x > 0 and label` is `label` when `x > 0`, else `False`. Both are **short-circuit** — the right operand is evaluated only when the left does not already decide the result, so a right operand that would refuse is not reached when the left short-circuits. The **result type** is the join `T ⊔ U` of the two operand types: identical types collapse to that type; an `int` / `real` pair promotes to `real`; an empty-list operand unifies to the concrete list type; and two **different value scalars** (`x > 0 and "yes"` → `bool` or `string`) yield a `value` (§5.6 — expressible and equatable). Two operands with no common result type — e.g. a `list` and a `dict` — are a type_error (`and` / `or` must be able to name the type of whichever operand it returns). For two `bool` operands the result is a `bool`, identical to a plain boolean `and` / `or`. **`not` always yields a `bool`.** `not x` is `True` when `x` is falsy and `False` when `x` is truthy, for any value `x`. DKE Python uses the **word forms** `and` / `or` / `not`; there are no `&&` / `||` / `!` tokens. In precedence (§4.6) `or` binds loosest, then `and`, then `not`, then the comparison operators — so `not a == b` is `not (a == b)` and `a or b and c` is `a or (b and c)`. ### 8.3 Arithmetic | Operator | Signature | |----------|-----------| | `+` | `(int, int) → int`; `(N, N) → real` when at least one operand is `real` | | `-`, `*` | `(int, int) → int`; `(N, N) → real` when at least one operand is `real` | | `/` | `(N, N) → real` — **true division** (always a `real`, including `int / int`: `7 / 2` is `3.5`) | | `//` | `(int, int) → int`; `(N, N) → real` when a `real` operand — **floor division** (rounds toward −∞: `-7 // 2` is `-4`) | | `%` | `(int, int) → int`; `(N, N) → real` when a `real` operand — **floor modulo** (result takes the sign of the divisor: `-7 % 2` is `1`, `-7.5 % 2` is `0.5`) | | `**` | `(int, int) → int` when the exponent ≥ 0; `(N, N) → real` when a `real` operand — **power** (right-associative) | | `-` (prefix) | `int → int` — unary negation, equivalent to `0 - x` | | `+` (temporal) | `(datetime, duration) → datetime` (either order); `(duration, duration) → duration` | | `-` (temporal) | `(datetime, duration) → datetime`; `(datetime, datetime) → duration`; `(duration, duration) → duration` | | `*` (temporal) | `(duration, N) → duration` (either order) — scale a length | | `/` (temporal) | `(duration, N) → duration` — split a length; `(duration, duration) → real` — how many times one fits into the other | | `%` (temporal) | `(duration, duration) → duration` — the length left over | The numeric operand set is `N ∈ {int, real}`. `+`, `-`, `*`, `//`, `%`, `**` **promote**: when both operands are `int` the result is `int`; when at least one is `real` the other is promoted to `real` and the result is `real`. `/` is the exception — it is **true division** and always produces a `real`, so `int / int` promotes (`7 / 2` is `3.5`, `8 / 2` is `4.0`); a floored integer quotient is `//` (`7 // 2` is `3`). `//` and `%` are the matched **floor** pair: both round toward −∞ / take the sign of the divisor, so the identity `a == (a // b) * b + (a % b)` holds — and it holds at both operand classes, so `-7.5 % 2` is `0.5` just as `-7 % 2` is `1`. A remainder of zero takes the divisor's sign as well, which is visible only on a real: `6.0 % -2` is `-0.0`. **Temporal arithmetic.** `datetime` and `duration` compute together, with the operand types deciding what an operation means. Adding a `duration` to a `datetime` **shifts** the instant (`t + duration("PT1H")` is an hour later, and subtracting shifts it earlier); subtracting one `datetime` from another gives the **length between them**; and two `duration`s add and subtract to a `duration`. A `duration` also **scales**: multiplying by a number stretches it (`duration("PT30M") * 3` is `PT1H30M`, `duration("PT1H") * 2.5` is `PT2H30M`) and dividing by a number splits it (`duration("PT1H") / 4` is `PT15M`). Dividing a `duration` **by another `duration`** asks how many times one fits into the other and yields a plain `real` — the answer has left the temporal domain, so `duration("PT3H") / duration("PT45M")` is `4.0`, not a length. The matching `%` gives the length **left over**: `duration("PT3H10M") % duration("PT45M")` is `PT10M`. Shifts respect the calendar, so `datetime("2024-02-28T12:00:00Z") + duration("P1D")` is `2024-02-29T12:00:00Z` in a leap year and `2023-03-01T12:00:00Z` in a common one. Addition, subtraction, `%`, and scaling by an `int` are **exact to the nanosecond** — no result is rounded. Scaling by a `real` (`*` or `/`) rounds to the **nearest nanosecond**, halves away from zero, since a fractional nanosecond is not a `duration`. Combinations that name nothing are type errors: two `datetime`s have no **sum** (only a difference), a `duration` minus a `datetime` is meaningless (the operand order carries the meaning), a `duration` times a `duration` is an area rather than a time, a number divided by a `duration` is a frequency rather than a time (division is not commutative here), and `//` and `**` are not defined over temporal values. Subtracting a later instant from an earlier one yields a **negative** `duration` (§3.5.6), which renders and reads back with a leading `-`. A result whose span exceeds what a `duration` holds (about ±292 years), or whose instant falls outside years 0001 through 9999, is a **catchable refuse** rather than a wrapped value; so is dividing or taking a remainder by a zero-length `duration`. **Sequence repetition.** `*` is additionally overloaded so a `string` or a constructed `list` may be repeated by an `int` count (either order): `"ab" * 3` is `"ababab"`, `"-" * 5` is `"-----"`, `[0] * 4` is `[0, 0, 0, 0]`, and `[1, 2] * 3` is `[1, 2, 1, 2, 1, 2]`. A `string * int` yields a `string`; a `list * int` yields a `list`. A **non-positive** count yields the empty sequence (`"x" * 0` and `[9] * -1` are `""` and `[]`), matching Python. The count MUST be an `int` — a `real` or non-`int` repeat count, and a `string`/`list` multiplied by anything but an `int`, is a type_error. The result is bounded (the count is a finite `int`), so termination (§9.5) is preserved. **`abs(x)`.** The built-in `abs` returns the absolute value of a number: `abs(x)` takes exactly one operand and preserves its numeric type — `abs(-5)` is the `int` `5`, `abs(-3.5)` is the `real` `3.5`. A non-numeric argument, or an argument count other than one, is a type_error. `abs` of the most-negative `int` refuses at runtime (its negation is out of range), the same as unary minus (§8.3 above). **`ord(s)`, `chr(i)`.** The Unicode codepoint round-trip. `ord(s)` takes a **one-character** `string` and returns its integer codepoint (`ord("A")` is `65`, `ord("æ")` is `230`); `chr(i)` takes an `int` codepoint in `range(0x110000)` and returns the one-character `string` for it (`chr(97)` is `"a"`, `chr(937)` is `"Ω"`). A non-`string` `ord` argument or a non-`int` `chr` argument (or an argument count other than one) is a type_error. At runtime, `ord` of a string whose length is not one, and `chr` of a codepoint outside `range(0x110000)` — or of a lone surrogate (`U+D800`..`U+DFFF`), which has no UTF-8 encoding — are catchable refuses (§10.3). **`round(x[, n])`.** The built-in `round` rounds a number **half to even** ("banker's rounding"): a value exactly halfway between two candidates goes to the even one, so `round(0.5)` and `round(2.5)` are both `0` and `2`, and `round(0.125, 2)` is `0.12`. The optional second operand `n` is an `int` digit count (it may be negative). The result type follows the operands: `round(int, …)` is an `int`; `round(real)` **without** a digit count is an `int` (rounded to the nearest whole number); `round(real, n)` is a `real` — a `real` even at `n = 0`, so `round(2.5, 0)` is `2.0`. A negative `n` rounds to a power of ten (`round(35, -1)` is `40`). Because a `real` holds an IEEE-754 double, rounding follows the stored value, not the written decimal — `round(2.675, 2)` is `2.67` (the nearest double to `2.675` is slightly below it), matching CPython. A non-numeric first argument, a non-`int` digit count, or an argument count other than one or two is a type_error; a result whose magnitude leaves the `int` range refuses at runtime. **`divmod(a, b)`.** Returns the pair `(a // b, a % b)` — the floored quotient and the remainder, computed in one call. Both operands must be numeric, and the pair promotes together: `tuple` when both are `int`, `tuple` when either is `real` — never a mixed pair. `divmod` is defined in terms of `//` and `%`, so it takes exactly the operands those two share (§8.3 above); a non-numeric operand, or an argument count other than two, is a type_error. The quotient rounds toward negative infinity and the remainder takes the sign of the **divisor**, exactly as the two operators do, so `divmod(7, 2)` is `(3, 1)`, `divmod(-7, 2)` is `(-4, 1)`, `divmod(7.5, 2)` is `(3.0, 1.5)`, and `q * b + r == a` always holds. A zero divisor is a runtime refuse (§10.3), and `divmod` of the most-negative `int` by `-1` refuses on overflow, the same as `//` and `%`. **`sum(iterable)`, `min(…)`, `max(…)`.** These reduce an in-memory iterable (a `list` / `set` / `dict` / `string` / store-derived collection), distinct from the same-named store-aggregate folds `sum(K.col)` / `min(K.col)` / `max(K.col)` (§12), which take a bare `K.col` column path — the argument shape selects the form. `sum(iterable)` adds numeric elements: all-`int` → `int` (an empty iterable is `0`), any `real` element → `real`; a non-numeric element is a type_error. `min` and `max` take **either** one iterable **or** two-or-more scalar values, returning the smallest / largest by numeric or (for strings) lexicographic order; the elements or values must share an orderable type — numeric, `string`, or a nested list/tuple of those, in which case the comparison recurses lexicographically (§8.1). `min`/`max` of a **runtime-empty** iterable is a catchable refuse (Python's `ValueError`); `min([])` on a literal empty list is instead a compile-time type_error (its element type is unknowable) — unless a keyword-only **`default=`** is given, which is returned for an empty iterable in place of the refuse (`min([], default=0)` is `0`). The `default=` is valid only with a single iterable argument (not with multiple positional values), and its type must match the element type. The higher-order `key=` argument is not provided (there are no first-class functions to pass as a key). `**` is **right-associative** and binds more tightly than the multiplicative and unary operators (§4.6): `2 ** 3 ** 2` is `2 ** (3 ** 2)` = `512`, and `-2 ** 2` is `-(2 ** 2)` = `-4`. An `int` base raised to a **non-negative** `int` exponent yields an `int` (`2 ** 10` is `1024`); a `real` operand yields a `real`. An `int` base with a **negative** `int` exponent is a runtime refuse with a teaching message — the result would be fractional, so write the base as a `real` (`2.0 ** -1` is `0.5`). Division by zero (`/` or `//`, integer or real) and modulo by zero are runtime refuses (§10.3). Integer overflow — any integer `+`, `-`, `*`, `//`, `%`, `**`, or prefix `-` whose mathematically correct result falls outside the signed 64-bit range — is a runtime refuse with a teaching message rather than wrapping. A real arithmetic result whose magnitude leaves the finite range is likewise a runtime refuse, carrying the `arithmetic_overflow` discriminator (§5.2). Reals compute to the precision of an IEEE-754 double and render in the canonical decimal form of §3.5.7. `**` refuses in two further cases at runtime, and **neither of them is an overflow**. Both forms compile: the fault is in the values, not the shapes. A **zero base under a negative exponent** (`0 ** -1`, `0.0 ** -2`) is a division by zero written differently, and refuses at runtime as one — discriminator `division_by_zero`, carrying the same wording Python gives that route. A **negative base under a fractional exponent** (`(-8) ** 0.5`) has no real value; Python answers it with a complex number, which DKE Python has no type for, so it too refuses at runtime, with the discriminator `complex_result`. That second case is the one place in `**` where this language declines a computation Python performs, and it is stated here rather than left to be discovered. Neither restriction reaches the neighbouring shapes: a negative base under an **integral** exponent is ordinary (`(-8.0) ** 3.0` is `-512.0`), and so is a zero base under a **non-negative** one (`0 ** 0` is `1`, `0 ** 1` is `0`). ### 8.4 String concatenation The `+` operator concatenates **two strings**: | Form | Signature | |------|-----------| | `(string, string) → string` | string concatenation | A `+` with one `string` operand and one **non-string** operand is a **type error** — as in Python, which raises `TypeError`, DKE Python does **not** implicitly render the other side. Convert it with `str(…)`, which renders any expressible value to its text form: `"count = " + str(xs.length)`, `"flag = " + str(b)`, `"at = " + str(t.value)`. An **f-string** applies `str(…)` to each field automatically, so `f"count = {xs.length}"` is the idiomatic form (§8.5). (Strict `+` is a DKE Python rule; there is no implicit string coercion.) **List concatenation.** With **two `list` operands** (and no `string`), `+` concatenates: `[1, 2] + [3, 4]` is `[1, 2, 3, 4]`, a new immutable list. Because lists have no mutation (no `append`), `+` is the way to combine two. The result element type follows the list-literal rule (§5.1): two lists of the same element type give that type (`list + list` → `list`), two lists of differing **scalar** element types box into `list` (`[1] + [3.5]` → `list`), and an empty operand takes the other side (`[] + [1]` → `list`); a non-scalar element mismatch is a type_error, the same kind-strictness list literals apply. A `list` combined with a non-`list`, non-`string` operand (`[1] + 5`) is a type_error. **Tuple concatenation.** With **two `tuple` operands**, `+` concatenates: `(1, 2) + (3,)` is `(1, 2, 3)`, a new immutable tuple. The result type is the two operands' **position lists joined**, not an element type unified — a tuple is heterogeneous and indexed by a constant (§3.5.11, §5.3), so its type is the sequence of its positions, and `tuple + tuple` is `tuple`. A constant index into the result therefore reads that position's own type: after `t = (1, "a") + (5,)`, `t[2]` is an `int` and `t[1]` a `string`. Both arities are known at compile time, so this is exact. The empty tuple takes the other side (`() + (1,)` → `tuple`). A `tuple` combined with a non-`tuple` operand (`(1,) + [2]`, `(1,) + 5`) is a type_error. A concatenation involving a **variadic** tuple — one whose length is not known until run time — has no static arity, so its result is a variadic tuple and needs one element type covering both sides. That type is unified by the rule list concatenation uses above: equal element types give that type, and differing **scalar** element types box into `value`. Element types that do not unify (a collection element beside a scalar one) are a type_error, because no static type describes an unknown-length run of one type followed by positions of another. Two fixed tuples never meet this restriction. ### 8.5 Field access See §5.2 and §5.4 for the full table of well-typed field accesses. Accessing a field not in the table is a type_error. ### 8.6 Indexing, slicing, and string methods See §5.3. Indexing selects one element; the index expression MUST be `int`, and an out-of-range index refuses at runtime (§10.3). A `string` may additionally be indexed to read a single character (a negative index counts from the end — `s[-1]` is the last character), **sliced** (`s[start:end:step]`, all three components optional; negative bounds count from the end and a negative step reverses, e.g. `s[::-1]`) to read a substring, and transformed by the string methods `s.find`, `s.rfind`, `s.index`/`s.rindex` (like `find`/`rfind` but refusing when the substring is absent), `s.count`, `s.startswith`, `s.endswith`, `s.replace`, `s.upper`, `s.lower`, the strip family `s.strip`/`s.lstrip`/`s.rstrip`, the character-class predicates `s.isspace`/`s.isdigit`/`s.isdecimal`/`s.isnumeric`/`s.isalpha`/`s.isalnum`/ `s.isupper`/`s.islower`/`s.istitle`/`s.isascii` (each `() → bool`), the list-bridge methods `s.split` (→ `list`) and `sep.join` (a `list` → `string`), and the collection-returning methods `s.partition` / `s.rpartition` (→ `tuple`, splitting once at the first / last occurrence of the separator) and `s.splitlines` (→ `list`, splitting at line boundaries) (§5.3). A constructed `list` (§5.1) is indexed (`xs[i]`, negative from-end permitted) and sliced (`xs[a:b:c]`, yielding a new `list`) by the same rules. Slicing and every string method **except `split`/`partition`/`rpartition` and `index`/`rindex`** are **total** — they never refuse: an out-of-range slice bound is clamped, an inverted range yields `""` (or the empty list), `find` returns `-1` when the substring is absent, `startswith`/`endswith` and the `is…` predicates return a `bool`, and case mapping is character-for-character (length-stable). `split`/`partition`/`rpartition` refuse only on an **explicit empty separator** (`empty_separator`, §10.3), `index`/`rindex` refuse when the substring is absent (`substring_not_found`), and a slice **step of `0`** is likewise a catchable refuse (§5.3). All positions count characters (a string) or elements (a list) (§5.3). **Dict and set methods, and the collection builtins.** A `dict` (§5.1) is projected with `d.keys()` (→ `list`), `d.values()` (→ `list`), and `d.items()` (→ `list>`), each in insertion order, and read defensively with `d.get(key, default)` — the value for `key`, or `default` when the key is absent. A default is **required** (DKE Python has no `None` to return for the 1-argument form); the result type is the join of `V` and the default's type (the same unification `and` / `or` use, §8.2). A `set` is combined with `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`. Two builtin functions pair collections into tuples: `zip(a, b, …)` → `list>` pairs elements position by position up to the shortest input, and `enumerate(xs [, start])` → `list>` numbers each element, from `0` by default or from an optional `int` `start` (given positionally or as the `start=` keyword; `start` may be negative). Each argument to `zip`/`enumerate` is any finite collection (a `dict` contributes its keys, a `set` its sorted elements); the result is an ordinary `list` and composes with all list reads (`for pair in zip(a, b): … pair[0] …`). Three more read a whole iterable. **`sorted(iterable [, reverse=])`** returns a **new** `list` of the elements in ascending order — descending when `reverse` is `True` (a stable sort; the `reverse=` argument is keyword-only, and a higher-order `key=` is not provided) — the elements must be orderable: numeric, `string`, or a nested list/tuple whose own elements are (recursively) orderable, in which case the sort recurses lexicographically (§8.1). **`any(iterable)`** and **`all(iterable)`** fold **truthiness** (§8.2) over the elements to a `bool`: `any` is `True` when at least one element is truthy (`False` for an empty iterable), `all` is `True` when every element is truthy (`True` for an empty iterable). **`reversed(iterable)`** returns a **new** `list` holding the elements in the reverse of the order the iterable yields them — the same order `for` walks, so a `dict` contributes its keys and a `set` its sorted elements, and `reversed` gives that order backwards. The result is an ordinary `list` (`reversed("abc")` is `['c', 'b', 'a']`), so it indexes, iterates, and composes like any other; an argument that is not a finite collection, or an argument count other than one, is a type_error. ### 8.7 The `print` statement ``` print() ``` Appends output to the script's transcript. `print` is written as a call — `print("temp=" + str(t.value))`. Evaluates `` and appends its rendering. The argument type MUST be a type for which a textual rendering is defined: `string`, `int`, `bool`, a `value` (§5.6, rendered by its class), a constructed `list`, or any discriminator type. A constructed `list` renders as `[e1, e2, …]` — the elements comma-separated in brackets, each rendered recursively (a nested list renders in full, e.g. `[[1, 2], [3]]`; an empty list is `[]`). A **string element inside any collection** is rendered as its `repr` — single-quoted, switching to `"` only when the value contains a `'` and no `"`, with `\`, the quote, and `\n`/`\r`/`\t` escaped (e.g. `['a', 'b']`, byte-matching CPython `str([...])`) — so a nested string is unambiguous, while a **bare top-level string** printed on its own stays unquoted (`print("a")` → `a`). A constructed **tuple** renders `(e1, e2, …)` (a one-element tuple `(e,)`); a **dict** renders `{k1: v1, k2: v2}` in insertion order; a **set** renders `{e1, e2, …}` in sorted order (the empty set, only reachable as a computed result, renders `set()`) — each element rendered recursively. The **store-derived** finite collections and `proof_tree` MUST NOT be passed directly to `print` (they carry no scalar rendering); access a `string`-shaped field or build a string with `+` instead. ### 8.8 No I/O, no closures, no first-class functions DKE Python has no I/O surface other than (i) verb calls against the store and (ii) `print`. It has no closures, no anonymous functions, no first-class function values, and no captured environments. The only callable is a top-level stored script, via a plain call (§4.3, §9.7). ### 8.9 Comprehensions A **comprehension** builds a constructed collection by bounded iteration in expression position. There are three forms — a **list** comprehension (`[…]`), a **set** comprehension (`{…}`, no colon), and a **dict** comprehension (`{… : …}`): ``` comp-clause := 'for' IDENT 'in' iter-expr ( 'if' cond-expr )* list-comprehension := '[' expr comp-clause+ ']' set-comprehension := '{' expr comp-clause+ '}' dict-comprehension := '{' expr ':' expr comp-clause+ '}' ``` Each form has one or more `for` **clauses**. A single-clause comprehension iterates the finite `` (any finite collection type, a constructed `list`/`set`/`dict`, or a `string` — by character, §6.3), binds each element to ``, evaluates the optional `` (tested for **truthiness**, §8.2 — any value), and, for each element the condition admits, contributes a value to a new collection. A **list** comprehension appends `` → `list` (`T` the type of ``); a **set** comprehension collects `` → `set`, removing duplicates and sorting (the `` must be hashable — a scalar or a tuple of hashables); a **dict** comprehension maps ` : ` → `dict` in insertion order, last value winning on a repeated key (`` must be hashable the same way). `` (and ``) MUST produce a value; a statement-position verb is a type_error. A comprehension with **more than one `for` clause** is the flat **cartesian product**: the first clause is the outermost loop, each following clause nests inside the previous, and `` (and a dict's ``) is evaluated only in the innermost scope. A later clause's `` may reference the loop variables bound by earlier clauses (`[y for row in grid for y in row]` flattens `grid`). A clause may carry **multiple `if` filters** (`for x in xs if p if q`), which apply conjunctively (equivalent to `if p and q`). The loop variable `` of each clause is **comprehension-local**: it is in scope within the clauses to its right, the ``s, `` (and a dict comprehension's ``), may shadow an outer or earlier binding of the same name, and does not leak to the enclosing scope. A list comprehension whose `` is itself a comprehension nests naturally (`[[y for y in row] for row in grid]` is a `list>`). A comprehension is bounded iteration over a finite source, so it terminates (§9.5) and, like a list literal, evaluates entirely on the client side (no service round-trip). ``` evens = [n for n in nums if n % 2 == 0] # list → list uniq = {n % 2 for n in nums} # set → set (deduped, sorted) squares = {n: n * n for n in nums} # dict → dict pairs = [a + b for a in xs for b in ys] # cartesian product (multi-clause) flat = [y for row in grid for y in row] # inner source sees the outer var tags = get(K.s.tags) # a read is bound first (§9.1)… labels = [c.value for c in tags] # …then iterated → list shouted = [w.upper() for w in text.split(" ")] # compose with split → list ``` The `` is any expression of a finite type; a store read (a verb call) is bound to a name first (as `tags` above) rather than written inline, consistent with §9.1. ### 8.10 Conditional expression A conditional expression `a if c else b` yields `a` when the condition `c` is **truthy** and `b` otherwise. The condition `c` may be any value (tested for truthiness, §8.2). The two branches must have the same type — which is the type of the whole expression — with numeric promotion (an `int`/`real` pair yields `real`); a mismatched pair (e.g. `int` and `string`) is a type_error. ``` grade = "pass" if score >= 60 else "fail" step = n // 2 if n > 0 else 0 ``` Evaluation is **short-circuit**: `c` is evaluated first, then **only** the selected branch — the unselected branch never runs, so a branch that would refuse (a division by zero, an out-of-range index) is not reached when it is not chosen. The conditional expression is right-associative and binds lower than every operator (§4.6). It is terminating by construction (a single selection, no iteration). ### 8.11 Tuple unpacking A **target list** — two or more names separated by commas on the left of an `=`, or between `for` and `in` — destructures a **tuple** into its named positions: ``` a, b = (1, "two") # a = 1, b = "two" a, b = b, a # swap — the RHS may be a bare comma-list x, y, z = 10, 20, 30 # (an implicit tuple), parentheses optional (a, b), c = ((1, 2), 3) # NESTED — a = 1, b = 2, c = 3 p, (q, r) = 1, (2, 3) # nested target anywhere in the list a, *rest = (1, 2, 3, 4) # STARRED — a = 1, rest = [2, 3, 4] first, *mid, last = (1, 2, 3, 4) # star absorbs the middle: mid = [2, 3] for i, x in enumerate(xs): # i = index, x = element print(i + ": " + str(x)) for k, v in inventory.items(): # k = key, v = value print(k + " = " + str(v)) ``` - **Assignment unpacking** (`a, b = `) requires the right-hand side to be a `tuple` whose arity **exactly** matches the number of targets. The RHS may be written as a **parenthesized tuple** (`(1, 2)`) or as a **bare, unparenthesized comma-list** (`b, a`) — the two are equivalent, so the swap idiom `a, b = b, a` works. The whole right-hand side is evaluated **before** any target is bound, so a swap reads each name's prior value. Each target binds the tuple's value at its position (with that position's type). A right-hand side that is not a tuple, or a tuple of a different arity (too few OR too many values), is a type_error. - **Nested targets** — a target may itself be a parenthesized target list, so `(a, b), c = ` (or `a, (b, c) = `, and deeper) destructures a tuple of tuples in one statement. Each nesting level is checked for **exact arity** independently: `(a, b), c = ((1, 2, 3), 4)` is a type_error because the inner tuple has three values, not two. A fully-parenthesized top-level list is the same as the unparenthesized one — `(a, b) = t` is `a, b = t` — while a single trailing comma makes a one-element tuple target: `(a,) = t` binds `a` to `t`'s sole element (and `(a) = t`, a bare parenthesized name, is the plain assignment `a = t`). - **Starred target** — **one** target in the list may be starred (`*rest`); it absorbs the elements the fixed targets do not, as a **`list`** (Python's rule: a starred target is always a list, even from a tuple). `a, *rest = (1, 2, 3)` gives `a = 1`, `rest = [2, 3]`; the star may lead or sit in the middle (`*init, z = t`, `a, *mid, b = t`), and it absorbs zero elements when the tuple is exactly the fixed count (`a, *mid, b = (1, 2)` → `mid = []`). The RHS must be a tuple with **at least** as many elements as the fixed targets (too few is a type_error). Because the absorbed elements become one `list`, they must share a single type — a heterogeneous run is a type_error (index the tuple by position instead). A list may hold **at most one** star, and a lone `*rest = t` (no sibling, no trailing comma) is rejected — write `*rest, = t` or `a, *rest = t`. - **`for`-loop unpacking** (`for a, b in :`) requires each **element** of the finite iterand to be a `tuple` of the target arity — the shape `enumerate` (§8.6), `zip` (§8.6), and a dict's `.items()` (§8.9) produce, which is what makes this the idiomatic way to consume them. Each target binds per iteration, scoped to the loop body (like the single loop variable, it does not outlive the loop, §6.7). Unpacking is defined only over the fixed-arity `tuple` type, so the arity check is static (a `list`, whose length is a runtime property, is not unpackable — bind it and index it). It introduces no iteration, so termination (§9.5) is preserved. ### 8.12 Chained assignment `a = b = ` binds **every** target on the left to the one value of ``, which is evaluated once: ``` a = b = 0 # a and b both 0 lo = hi = mid = start # three names, one value ``` Each target is a plain name (there is no chained field write or subscript assignment). The value's type is bound to every target, so a later `b = "text"` — reassigning a name first bound as an `int` — is a type_error like any other (the one-type-per-variable rule, §6.1). This is a convenience form for initialising several names to the same value; it introduces no iteration, so termination (§9.5) is preserved. ### 8.13 Type conversions The built-in **scalar conversions** turn a value from one type into another: | Call | Accepts | Produces | |------|---------|----------| | `str(x)` | any expressible value | its text form (`string`) — total; the same rendering `+`/`print` use | | `int(x)` | `string` / `int` / `real` / `bool` | an `int` | | `int(s, base)` | a `string` + an `int` `base` | an `int` | | `float(x)` | `string` / `int` / `real` / `bool` | a `real` | - `str(x)` never fails — it renders any value the way `print`/`+` do (a number as its decimal, a `bool` as `True`/`False`, a `datetime` as its RFC 3339 text, a collection as its element preview). Note that a `bool` renders `True`/`False`, capitalised and Python-faithful, under every language surface — including any whose boolean literals are spelled with different words. The lowercase `true`/`false` is the engine's stored token and is never what a read shows. Exercised in §C.29. - `int(x)` from a **`real`** truncates toward zero (`int(3.9)` is `3`, `int(-3.9)` is `-3`); from a **`bool`** yields `1` / `0`; from a **`string`** parses a decimal integer, tolerating surrounding whitespace and a leading sign (`int(" -7 ")` is `-7`). A string that is not a decimal integer (`int("3.5")`, `int("abc")`), or a value out of the 64-bit range, is a **catchable refuse** (§10.3) — Python's `ValueError`. - `int(s, base)` parses the `string` `s` in an explicit radix. `base` is `2`..`36`, or `0` to auto-detect the radix from a `0x` / `0o` / `0b` prefix. A prefix is also accepted when it matches `base`; an optional leading sign and `_` digit separators (between digits, or once right after a prefix) are allowed. A digit outside the base, an out-of-range `base`, a malformed separator, 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. - `float(x)` from an `int` / `bool` widens to a `real`; from a **`string`** parses a decimal real, including exponent form (`float("1e3")` is `1000.0`), tolerating surrounding whitespace. A non-numeric string, or a non-finite result, refuses. Each scalar conversion takes exactly one argument — except `int`, which also accepts the two-argument `int(s, base)` form above (any other count, or a non-convertible argument type, is a type_error). **`bool(x)`** returns the **truthiness** of any value as a `bool` (§8.2) — `bool([])` is `False`, `bool("x")` is `True`. The **collection conversions** build one collection from another: | Call | Accepts | Produces | |------|---------|----------| | `list(x)` | any finite collection, a `string`, or a homogeneous `tuple` | a `list` — the elements (a `string` yields its characters) | | `set(x)` | any finite collection of hashable scalars, a `string`, or a homogeneous `tuple` | a `set` — the unique elements, sorted | | `dict(x)` | a `list>` (a list of pairs) | a `dict` — the mapping | | `tuple(x)` | any finite collection, or a `string` | a **variadic** `tuple` — the elements as an immutable, runtime-length tuple | - `list(x)` collects the elements of a finite collection (`list`, `set`, `dict` — over its **keys** —, or a store-derived collection) into a new `list`; a `string` yields its characters as one-character strings (`list("ab")` is `["a", "b"]`). A **`tuple`** is also accepted (though a tuple is not otherwise iterable): `list((1, 2, 3))` is `[1, 2, 3]`. Because a `list` has one element type, the tuple must be **homogeneous** — every element the same type — else it is a type_error (index a heterogeneous tuple by position instead). - `set(x)` collects the elements into a `set` — **deduped and sorted** (§5.1); the elements must be hashable scalars (a collection of non-scalars is a type_error). - `dict(x)` builds a mapping from a **list of two-element tuples** — the shape `zip` (§8.6) and a dict's `.items()` (§8.9) produce, so `dict(zip(keys, vals))` and `dict(pairs)` are the idiomatic constructions. A duplicate key keeps its first position and takes the last value (§8.9). Anything other than a `list>` is a type_error. - `tuple(x)` collects the elements into a **variadic homogeneous tuple** `tuple` — a tuple of **runtime** length whose every element is `T`. Unlike a fixed `tuple` (from a tuple literal), it is indexed by a **runtime** `int` (`t[i]` → `T`, out-of-range refuses) and **cannot be unpacked** (it has no static arity). It compares (`==`) against another tuple whose elements agree with `T`. Because a DKE `list` is already immutable, `tuple(xs)` mainly signals intent. **`repr(x)`** returns the **repr** text of any value as a `string` — a `string` keeps its quotes (`repr("hi")` is `"'hi'"`), a collection renders with repr elements; for most other values `repr` matches `str`. **`format(value, spec)`** renders a value per the Python **format mini-language**, returning a `string`; it also powers an f-string `{value:spec}` (§3.5.10). The supported spec grammar is `[[fill]align][0][width][.precision][type]`: - **align** — `<` left, `>` right, `^` center; an optional **fill** character precedes it (default space). With no align, numbers are right-aligned and other values left-aligned. - **`0`** — zero-pad a number (the fill becomes `0`, placed after a leading sign). - **width** — the minimum field width in characters. - **`.precision`** — decimals for the `f` type; the maximum character count for a string. - **type** — one of `s` (string), `d` (decimal int), `f` (fixed-point real), `x` / `X` (lower/upper hex int), `o` (octal int), `b` (binary int); the default renders as `str`. So `format(3.14159, ".2f")` is `"3.14"`, `format(42, ">5")` is `" 42"`, `format(42, "05")` is `"00042"`, `format(255, "x")` is `"ff"`. Unsupported spec features — a sign flag (`+`/`-`/space), `#`, digit grouping (`,`/`_`), and the `e`/`E`/`g`/`G`/`%`/`n`/`c` types — are a catchable refuse (Python's `ValueError`), not a silent mis-format. --- ## 9. Dynamic semantics ### 9.1 Evaluation order Expressions evaluate **strictly, left to right**. The sub-expressions of a binary operator evaluate before the operator; the index expression of `[]` evaluates before the indexing; an argument list evaluates left to right before the call. The short-circuit operators `and`, `or` are the only exceptions: the right operand evaluates only if needed. Statements within a suite execute in textual order; an assignment's binding becomes visible immediately after its initializer evaluates. ### 9.2 Control flow #### 9.2.1 `if` `if :` with an optional `else:`. The condition may be any value — it is tested for **truthiness** (§8.2), so `if xs:` / `if s:` / `if n:` branch on non-empty / non-zero exactly as CPython does. #### 9.2.2 `for` `for x in :`. The `` is one of the six finite collections, a constructed `list`/`set`/`dict`, or a `string` (§6.3); `x` is bound to each element in order — for a string, each character (a one-character string); the body executes once per element. The collection is snapshotted at entry; mutating the underlying store during the loop does not change the iteration. A `for` MAY carry a trailing `else:` clause: ``` for x in : S else: Se ``` `Se` runs once, after the loop finishes, UNLESS the loop was left by a `break` (§9.2.7). An empty `` — zero iterations — still runs `Se`. `Se` executes in the scope enclosing the loop; the loop variable `x` is not in scope there (§6.7 — the loop variable does not outlive the loop). Because `Se` is straight-line, the termination guarantee (§9.5) is unaffected. #### 9.2.3 `match` `match :`. The scrutinee is evaluated once; control transfers to the `case` clause whose label matches the runtime discriminator of the scrutinee value. Clauses are exhaustive per §6.2; one and only one clause runs. When the scrutinee is a `value` (§5.6), the label matched is the runtime **class** of the stored content (`int`, `bool`, or `string`); if no named arm matches that class, the `case default:` arm runs. An arm's `as ` binding, if present, receives the content typed at the arm's class for the duration of the arm. #### 9.2.4 `try` ``` try: S except refuse as r: Sr except engine_error as e: Se else: So finally: Sf ``` Statements in `S` execute in order. If a statement raises a refuse, its result does NOT bind and control transfers to the `except refuse` handler (if present) with `r` bound to a `refuse_info`. If a statement raises an engine_error, control transfers to the `except engine_error` handler (if present) with `e` bound to an `engine_error_info`. If the corresponding handler is absent, the refuse / engine_error propagates out of the `try` and out of the script. After a handler completes, execution continues with the statement following the `try`. The `except` handlers MAY be followed by two optional clauses, in this order: - **`else:`** — permitted only when at least one `except` handler is present. `So` runs iff `S` completed with no refuse or engine_error. `So` is **outside** the protected region: a refuse or engine_error raised in `So` is NOT caught by this `try`'s handlers and propagates. - **`finally:`** — `Sf` runs on **every** exit path from the `try`: after a clean body, after a handler, after `else`, when a refuse or engine_error propagates uncaught, and when a `break` or `continue` in `S` leaves the `try`. `Sf` runs last. If `Sf` itself raises, or issues a `break` / `continue`, that outcome supersedes whatever the `try` was about to do. A `try` MUST have at least one `except` handler or a `finally` clause; a bare `try:` with neither is a compile-time error. The clause order is `try` → `except`* → `else` → `finally`. #### 9.2.5 `branch` block ``` with branch(""): S ``` A `branch` block opens an isolated branch named ``, executes `S`, and on normal completion commits the branch. If any statement in `S` raises an uncaught refuse or engine_error, the implementation MUST roll back the branch and re-raise. #### 9.2.6 `commit` / `rollback` Both are bare statements. Written inside a `branch` block, they resolve to that block's branch and terminate it. The block's remaining statements still execute, and they execute with **no branch open**: a write among them is an ordinary durable write, outside the resolved branch and unaffected by it, and the implementation MUST report it as it reports any other write. Outside a `branch` block, each is a refuse (no active branch). Nested branching is forbidden. #### 9.2.7 `break` / `continue` Both are bare statements, valid only lexically inside a `for` loop (§9.2.2) — `break` or `continue` outside a loop is a compile-time error (not a runtime refuse). `break` stops the loop immediately; `continue` skips the rest of the current iteration and proceeds to the next element. Both may appear nested inside an `if`, `match`, or `try` block within the loop body, and each resolves to the **innermost** enclosing `for` loop; a `break`/`continue` in an inner loop does not affect an outer loop. Because a `for` iterates a finite collection and these statements only ever **shorten** the iteration (never extend it), the termination guarantee (§9.5) is preserved. Loop context does not cross a function boundary: a `break`/`continue` must be inside a loop in its **own** definition, not merely called from within a loop. #### 9.2.8 `return` A `return` statement ends the enclosing script immediately. It bubbles **past** any enclosing `for`, `match`, `if`, or `try` — a `return` is not a loop signal, so it does not run a `for … else` and is not drained by a loop the way `break` / `continue` are (§9.2.7). One interaction is fixed: a `return` leaving a `try` still runs that `try`'s `finally` clause **first** (§9.2.4), and if the `finally` itself returns, breaks, or continues, that outcome supersedes the pending `return`. - **Bare `return`** (no expression) exits the script with no value. It is valid in any script. Statements after the taken `return` in the same suite do not run. - **`return `** (a value script only, §4.2) evaluates `` and exits, delivering the value. When the script was reached as a **value-call** in a caller (`y = f(args)`, §4.4), the value binds the caller's target; when the script was run at the top level (Wire §4.2), the value is surfaced on the invocation result. Because a `return` only ever **shortens** execution (it starts no iteration and scripts do not recurse, §9.7), the termination guarantee (§9.5) is preserved. ### 9.3 Refuses as control flow A refuse is a recoverable runtime outcome of a verb call. Refuses arise from input that the store rejects (out-of-surface slot, incomplete slots, ambiguous match, invalid source slot, write conflict, …). The list of refuse reasons is defined by the target service; DKE Python guarantees only that a refused statement's binding does not produce a value and that control transfers to the enclosing `except refuse` handler if present. A statement that would bind a value and refuses leaves the target identifier **unbound**; any subsequent reference within the same block is a refuse on the same path. ### 9.4 Engine errors An engine_error indicates that the target service composed a well-formed request from the user's source but the request failed at the engine layer. Engine_errors are distinct from refuses; they indicate a service-side issue, not a user-side correction opportunity. They are caught by `except engine_error`. ### 9.5 Termination guarantee **DKE Python guarantees bounded termination** (it is bounded-terminating). Every well-typed program terminates on every input; this is the family-wide guarantee, identical across editions. The guarantee follows by structural induction: - The only iteration construct is the `for … in` over a finite collection (§6.3). The collection's length is determined at iterand evaluation; the loop runs that many times. - There is no `while`, no unbounded loop, no goto, no continuation. - There is no recursion. A stored-script call is inlined at compile time (§9.7); a direct or indirect call cycle between scripts is a compile error. - All other control-flow constructs (`if`, `match`, `try`, `branch`) reduce body size, not increase it. A target service MAY additionally impose execution budgets (statement count, wall-clock time, **the amount of data one run may build**) for operational reasons; such budgets are NOT part of the language specification. Note what termination does and does not promise: it bounds how LONG a program runs, not how much it HOLDS at once, and those are separate properties — a program can be bounded-terminating and still build a collection larger than the service can hold. A budget of this kind refuses the run (§10.3-class, reported as a refuse) rather than failing it, and is not catchable by `try` (§9.3): a handler able to swallow a resource limit could retry inside a bounded loop and defeat it. ### 9.6 Determinism contract Given (i) the same DKE Python source, (ii) the same target store state at invocation start, and (iii) the same argument values, two invocations of one program MUST produce **byte-identical** transcripts. This holds across re-invocation, across implementation process restarts, and across implementation versions that share the same spec version (§11). Determinism applies to the response shape — the response header's call frame (with its success verdict) and the ordered sequence of `print` outputs and store effects the body lists (Wire §4.2); the exact prose of that human render is presentation, not a versioned contract (Wire §4.2). Determinism does NOT constrain the wire encoding of the request or any internal representation. ### 9.7 No runtime recursion; inline expansion DKE Python has no runtime function-call mechanism. A stored-script call `(args)` (§4.3, §6.8) is **compile-time inline expansion**: each invocation site is replaced by the callee's body with parameter bindings substituted. Consequently callees MUST be compiled before callers, cycles are forbidden (a compile error), and inlining is one-shot (recompiling a callee after the caller does not change the caller's stored body until the caller is also recompiled). A **value-call** in expression position (`y = f(args)`, §4.4) follows the same model: it is not a runtime call either, and a value script that a caller reaches by value-call is subject to the identical compile-before-call, no-cycles rule. Because value delivery is a compile-time construction over the callee's body, a value-call adds no recursion and no runtime call frame; the termination guarantee (§9.5) is unchanged. --- ## 10. Error model DKE Python distinguishes four error categories. Every conforming implementation MUST classify outcomes into one of these: | Category | Stage | Recoverable in source? | Exit code (CLI) | |----------|-------|------------------------|-----------------------------| | `parse_error` | static (lexer / parser) | no | 4 | | `type_error` | static (typechecker) | no | 5 | | `refuse` | runtime (verb call) | yes (`except refuse`) | 1 (uncaught) | | `engine_error` | runtime (verb call) | yes (`except engine_error`) | 2 (uncaught) | Exit code 0 indicates success; exit code 3 indicates a CLI argument error (not a language-level outcome). ### 10.1 `parse_error` The source is not a well-formed token stream or does not match the grammar of §4. Examples: - A tab in indentation, or a dedent that matches no open level (§3.2). - Unterminated string literal. - Codepoint outside XID at identifier position. - A reserved word (§3.7) in user-identifier position. - An empty compile unit — no declarations after whitespace and comments. - A non-exhaustive `match` written with a missing arm (raised as type_error, §10.2) versus a malformed `case` header (parse_error). - A name argument that is not an identifier-shaped bare word (§6.5). A conforming implementation MUST report the line and column of the first offending token. ### 10.2 `type_error` The source parses but violates a rule in §5 or §6. Examples: - Use of an unbound identifier — including the kind position of a verb path (§6.7). - A wire-only script verb in a program body (`forget script`, `info script` — §7.1). - A `match` whose case set does not cover the scrutinee's discriminator set, contains a case not in the set, or repeats a case (§6.2). - A `for … in` over a non-collection (§6.3). - Binding a statement-only verb by assignment (§6.4). - `.` for a non-existent field. - An operand-type mismatch outside the §8.4 string-concat overload — including a chained comparison (§4.6). - A non-`string` source argument (§7.3). A conforming implementation MUST report the line and column of the offending construct. ### 10.3 `refuse` A runtime outcome of a verb call (or built-in operation) that the target service rejects with a teaching message. Examples: - `remember(K.s.a, v, src)` where the cell already carries a different value under the same source. - `subjects(K.a, v)` where `K` is not a known kind. - A verb path whose segment count does not match the verb's slot shape (§7.2). - Index out of bounds on `claim_list[i]`. - Division by zero; integer overflow. - `commit` outside a branch. A refuse carries a `refuse_info` (`reason`, `teaching_hint`, `discriminator`). When wrapped in `try: … except refuse as r:`, control transfers to the handler with `r` bound. The exact reason taxonomy is defined by the target service; a conforming implementation MUST surface whatever reason strings the service returns without altering them. ### 10.4 `engine_error` A runtime outcome indicating that the target service composed a well-formed request from the source but the request failed at the engine layer. Carries an `engine_error_info` (`reason`, `code`). Caught by `try: … except engine_error as e:`. ### 10.5 Diagnostic format (informative) A command-line surface prints diagnostics in the form ``` ::: ``` where `` is `parse_error` or `type_error`. The text after `` is quality-of-implementation; a third-party tool MAY choose any format. --- ## 11. Versioning and compatibility ### 11.1 Spec version The **DKE Python Spec** is at **alpha · API 1**: the published surface carries the release stage and the API version it describes, and no document revision number. A source carries no version marker: an implementation accepts a conforming source by its structure (§4), not by a version match. Were the specification to adopt numbered releases, revisions would be tracked as a `MAJOR.MINOR` document version: - **MAJOR** increments on a breaking change (a previously accepted program becomes rejected) or an observable-behaviour change (e.g. a change to the invocation transcript, Wire §4.2). - **MINOR** increments on a backward-compatible addition or a backward-compatible revision that rejects no previously accepted program and changes no observable behaviour. A document revision changes no source: an implementation accepts a conforming source by its structure (§4). Across a breaking change, source compatibility is not guaranteed. ### 11.2 Reserved for future use The following surface area is reserved in v4.x and MUST NOT be used: - Escape sequences in string literals other than `\\`, `\"`, `\n`, `\t`, `\r`, `\xNN`, `\uNNNN`. - The names `empty`, `refuse_info`, `engine_error_info` as `type-name` tokens (§5.5). (The `0x` / `0o` / `0b` numeric prefixes, `_` separators, and prefix unary minus are part of the language.) ### 11.3 Compatibility with the target service A DKE Python program is portable across target services that implement DKE's canonical verb surface verbatim. Behaviour differences caused by different target-service surfaces are not language differences; the language layer is the same. --- ## 12. Conformance ### 12.1 Conforming implementations An implementation MAY conform as one of: - **Parser/checker** (static-only): accepts the language defined in §3–§6, rejects with the correct error class per §10.1 / §10.2, produces a typed AST. Sufficient for linters, formatters, syntax highlighters, and language servers. - **Compiler/runtime** (full): in addition, implements the lifecycle of the Wire & Tool Contract against a target service and the dynamic semantics (§9), satisfying the determinism contract (§9.6) and the termination guarantee (§9.5). A conforming implementation MUST document which class it implements and which spec version it claims. ### 12.2 Conformance suite (informative) A minimal conformance suite for a parser/checker exercises: - Every reserved word from §3.7 (a)–(d) in user-identifier position → parse_error. - A tab in indentation and a bad dedent → parse_error. - An empty compile unit (whitespace and comments only) → parse_error. - An unterminated string → parse_error. - A non-XID codepoint at identifier head → parse_error. - A name argument that is not an identifier-shaped bare word → parse_error. - An unbound identifier → type_error. - A `match` on `active_claim` missing the `empty` case → type_error. - A `match` on `active_claim` with an extra case, and one with a duplicate case → type_error. - A `for … in` over an `active_claim` → type_error. - Binding a statement-only verb by assignment → type_error. - A chained comparison `a < b < c` → type_error. - A `.nonexistent` → type_error. - A `forget script` / `info script` in a program body → type_error. - Every verb in §7.1 in its call form → accepted. - A module body with a top-level data declaration and no `def` → accepted (a module need not declare a script; Reference §9.1, §9.7). - An `import ` statement at module scope → accepted (Reference §9.3). - A cross-module qualified read `module.Kind(subject).field` → accepted (Reference §9.6). - Re-importing an already-loaded module → accepted; it reconciles (Reference §9.5). - An `import` cycle (a module that imports itself, directly or transitively) → rejected when the module is loaded (Reference §9.3). DKE ships with such a suite; third-party implementations are encouraged to share theirs. --- ## 13. Classes and methods A **class** groups a set of typed **fields** with the **methods** that operate on them, and gives programs a typed handle — an **instance** — for one named member of the class. Classes are an optional surface: a program that declares none is exactly a program without classes. Classes introduce no new types (§5) and no new verbs (§7), and they preserve the termination guarantee (§13.6). One class may **extend** another (§13.8); a method call on a reference whose class is not fixed until run time then runs the method of the instance's actual class — a choice over the fixed, finite set of classes the program declares, never an open-ended lookup. `class` and `return` are reserved keywords (§3.7 (a)). A top-level construct is either a script declaration (§4.2) or a class declaration (§13.1). ### 13.1 Class declarations ``` class-decl := 'class' IDENT ( '(' IDENT ')' )? ':' NEWLINE INDENT class-member+ DEDENT class-member := field-decl | method-def field-decl := IDENT ':' type-name ( '=' expr )? NEWLINE ``` A class declaration is the keyword `class`, the class name, an optional **base class** in parentheses, a `:`, and an indented body of field declarations and method definitions. A class takes **no marker**. A class may name a single base class it **extends** — `class Dog(Animal):` — inheriting the base's fields and methods (§13.8); naming more than one base is not supported. A **field** is `name: type` whose `type` is a **value-class scalar** — a primitive (`string`, `int`, `bool`) or one of the value classes the engine stores as a cell value (`datetime`, `duration`, `real`, `blob`). A field is a stored value slot the customer writes and reads. Field names are unique within a class. A field may instead carry an **initializer** — `name: type = expr` — making it a **computed field** whose value the engine *derives* from the class's other fields and maintains automatically. A computed field's type is `int`, `real`, or `bool`, and the customer never writes it directly. See §13.7. ``` class Sensor: temp: string # methods follow ``` Declaring a class introduces no storage and performs no action; it is a compile-time description the compiler uses to typecheck field access and method calls. ### 13.2 Instances An **instance** names one member of a class, identified by a string: ``` instance-ctor := IDENT '(' expr ')' # the class name applied to a name expression ``` `Sensor(room)` is an instance of `Sensor`, bound by assignment: ``` s = Sensor(room) ``` Constructing an instance records nothing — it is not a write; it yields a typed reference for reading and writing the instance's fields and calling its methods. Reading a field that has never been written yields `empty` (§13.3). ### 13.3 Field access Given an instance `s` of a class that declares a field `f`: - **Read** — `s.f` yields the current claim for that field: an `active_claim` when the field has a value, or `empty` when it does not. Consume it with `match` (§6.2) or `.value` (§5.2). ``` reading = s.temp ``` - **Write** — `remember(s.f, , )` records a new value for the field together with its provenance source (§7.3): ``` remember(s.temp, "21", "op1") ``` Field access is available on an instance variable and, inside a method body, on the explicit receiver `self` (§13.4). Reading or writing a field the class does not declare is a type_error. ### 13.4 Methods A **method** is a `def` inside a class body whose first parameter is the explicit receiver `self`. Inside the body, `self.f` names field `f` of the instance the method was called on. ``` method-def := void-method | value-method void-method := 'def' IDENT '(' 'self' ( ',' param )* ')' ':' NEWLINE INDENT stmt+ DEDENT value-method := 'def' IDENT '(' 'self' ( ',' param )* ')' '->' type-name ':' NEWLINE INDENT stmt* 'return' expr NEWLINE DEDENT ``` - A **void method** — `def name(self, params):` — declares no return type; it performs actions and yields no value, called as a statement. ``` def record(self, v: string, src: string): remember(self.temp, v, src) ``` - A **value method** — `def name(self, params) -> type:` — declares a return type and is called in expression position. Its body is either a single `return ` or a sequence of local `name = ` bindings followed by a tail `return ` of the declared type; the locals compute intermediate values (`self` fields and parameters are in scope). Control flow inside a value method body (an `if`/`for`/`match`, or a non-final `return`) is not yet supported and is a parse_error with a teaching hint. ``` def label(self) -> string: return "sensor" def combined(self, a: int, b: int) -> int: s = a + b # a local binding … return s * 2 # … then a tail return ``` A method is **called** on an instance with `instance.method(args)` — the `self` argument is supplied by the receiver, not written at the call: ``` s.record("21", "op1") # void method, statement position name = s.label() # value method, expression position ``` A method call is resolved from the receiver's class. When that class is fixed where the call is written, exactly one method body applies. When the receiver is held at a base-class type — a base-class parameter, or an element of a list of mixed subclasses — the call runs the method of the instance's **actual** class (§13.8); because a class hierarchy is closed and finite, the candidate bodies are a bounded, program-declared set, not an open-ended lookup. Methods obey **compile-before-call** exactly like scripts (§6.8); method recursion — direct, mutual, or through an override and `super` (§13.8) — is not expressible, so the call graph is acyclic (§13.6). Argument count and types are checked against the method's declared parameters. ### 13.5 Dispatch by class When code must branch on which class an instance belongs to, it uses a `match` whose scrutinee is a bare instance variable and whose `case` arms name classes: ``` class-match := 'match' IDENT ':' NEWLINE INDENT class-case+ default-case? DEDENT class-case := 'case' IDENT ':' ( simple-stmt NEWLINE | NEWLINE INDENT stmt+ DEDENT ) default-case := 'case' 'default' ':' ( simple-stmt NEWLINE | NEWLINE INDENT stmt+ DEDENT ) ``` ``` 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 is a **class match**; a `match` over any other expression is an ordinary discriminator match (§6.2). Inside a `case :` arm the instance is treated as that class, so its fields and methods resolve to that class. The arm set is **closed and exhaustive**: it MUST cover the instance's class — or, under inheritance (§13.8), every class the instance could belong to — or provide a `case default:` arm. A class match that is neither exhaustive nor defaulted is a type_error, and a `case` naming an unknown class is a type_error. When the instance's class is fixed where the match is written, the arm is chosen there; when the instance is held at a base-class type, the arm whose class is the nearest match for the instance's actual class is chosen from the fixed arm set (§13.8) — a bounded selection over the program's classes, never an unbounded lookup. ### 13.6 Termination Classes preserve the termination guarantee of §9.5. Method dispatch — direct calls (§13.4), class matches (§13.5), and the dispatch on an instance's actual class under inheritance (§13.8) — always selects from the fixed, finite set of classes and methods the program declares; even when the actual class is not known until run time, the selection is over that bounded set, so it introduces no unbounded lookup. Methods are non-recursive by construction; iteration remains the bounded `for … in` of §6.3. Every method body is therefore a finite, non-recursive program over bounded iteration. ### 13.7 Computed fields A **computed field** is a field declared with an initializer: ``` field-decl := IDENT ':' type-name ( '=' expr )? NEWLINE ``` Its value is not written by the customer; the engine **derives** it from the class's other fields and keeps it current as those fields change. A computed field's declared type is `int`, `real`, or `bool`. ``` class Order: price: int qty: int total: int = price * qty # a computed value big: bool = total > 1000 # a computed flag ``` Given `Order.o1.price = 10` and `Order.o1.qty = 5`, reading `Order.o1.total` yields `50`; writing `Order.o1.price = 200` re-derives it. The customer writes only `price` and `qty`; `total` and `big` are maintained automatically. A computed field reads back like any field (`current`, §7.1) with a `derived` provenance in place of a source. **The initializer.** Every identifier in the initializer must name another field of the same class **declared earlier** (a computed field may build on an earlier computed field), and the initializer must reference at least one such field. The form depends on the declared type: - An **`int`** field is an arithmetic expression over `int` fields and integer literals using `+`, `-`, `*`, `%` (§8). Division (`/`) is not written in an `int` field — its result may be fractional; declare the field `real`. - A **`real`** field is an arithmetic expression using `+`, `-`, `*`, `/`, `%` over `int` and `real` fields and numeric literals (§8.3). Division that does not divide evenly yields a `real` value (§3.5.7). - A **`bool`** field is a single ordered comparison — `<`, `<=`, `>`, `>=` — of one earlier field against a numeric literal or another earlier field. Its left side is a single field: to compare a computed value, declare that value as its own field first (`total: int = price * qty`, then `big: bool = total > 1000`). Because every reference points at an *earlier* field, a class's computed fields form no cycle. A computed field participates in `match` (§6.2) and expressions (§8) exactly as a written field of the same type would. **Termination.** Computed fields preserve the termination guarantee of §9.5: a derivation is a finite, acyclic expression over the class's own fields, evaluated once per change; it introduces no loop and no recursion. ### 13.8 Inheritance A class may **extend** one other class — its **base class** — named in parentheses after the class name: ``` class Animal: sound: string def speak(self): remember(self.sound, "generic", "op1") class Dog(Animal): breed: string def speak(self): super().speak() remember(self.breed, "collie", "op1") ``` A class extends **at most one** base (single inheritance). Naming more than one — `class C(A, B):` — is a compile-time error, as is naming a base that is not a class declared earlier in the program, or naming the class itself. **Inherited members.** A subclass has every field and method of its base, plus those it declares. `Dog` above has `sound` and `speak` from `Animal` and its own `breed`; an inherited method reads and writes the base's fields on the subclass instance. Inheritance is transitive: a class three levels deep has the members of every class above it. **Overriding.** A subclass may declare a method with the same name as one it inherits; the subclass's version then applies to instances of the subclass. Above, `Dog.speak` overrides `Animal.speak`. **`super`.** Inside an overriding method, `super().(args)` runs the base class's version of `` on the same instance — the inherited step — which the override can then extend. `super` is available only inside a method body and names the current class's base. (Constructor chaining — a `super().__init__(...)` call — is not part of this version; construction takes only the instance name, §13.2.) **Substitutability.** A subclass instance is accepted wherever its base class is expected: as a parameter typed with the base, as a binding used at the base type, or as an element of a list whose element type is the base. No cast is written — a `Dog` value is an `Animal` value. **Dispatch under inheritance.** When a method is called on a reference whose class is fixed where the call is written, exactly one body applies (§13.4). When the reference is held at a base-class type — a base-typed parameter, or an element of a list of mixed subclasses — the call runs the method of the instance's **actual** class: ``` class Cat(Animal): def speak(self): remember(self.sound, "meow", "op1") def herd(a: Animal): a.speak() # runs Dog.speak, Cat.speak, or Animal.speak, # according to a's actual class def demo(d1: string, c1: string): animals = [Dog(d1), Cat(c1)] # a list of mixed subclasses for a in animals: a.speak() # each element runs its own class's speak ``` Value-returning methods (§13.4) dispatch the same way. Because a program's classes form a closed, finite hierarchy, the set of methods any one call can reach is bounded and known from the program text; there is no open-ended lookup, and termination (§13.6) is preserved. **Reading a member under a base type.** Through a base-typed reference you may read or write any field, and call any method, the **base** declares — these are present on every instance. Reading a field or calling a method that only a *subclass* declares first requires establishing the instance's class, with `isinstance` (§13.9) or a class match (§13.5); otherwise it is a type_error. **Class match under a hierarchy.** A class match (§13.5) on a base-typed instance selects the arm whose class is the nearest match for the instance's actual class, resolved at run time; a `case :` arm matches that class or any of its subclasses, first match winning. The arm set stays closed and exhaustive over the hierarchy — cover every case or provide `case default:`. ``` def classify(a: Animal): match a: case Dog: print("kind=dog") case Cat: print("kind=cat") case default: print("kind=other") ``` ### 13.9 `isinstance` `isinstance(x, C)` reports whether the instance `x` belongs to class `C` — **true** when `x`'s class is `C` or any subclass of `C`, **false** otherwise. It returns a `bool`. ``` if isinstance(d, Dog): print("d is a Dog") if isinstance(d, Animal): # a Dog is an Animal print("d is an Animal") if isinstance(an, Dog): # a plain Animal is not a Dog print("an is a Dog") else: print("an is not a Dog") ``` When `x`'s class is fixed where the call is written, the result is a compile-time constant; when `x` is held at a base type, it is decided from the instance's actual class. Inside the taken branch of an `isinstance` test the reference is treated as the tested class, so its subclass-only fields and methods become accessible (§13.8). --- ## 14. Standing rules A **standing rule** is a named statement that derives facts automatically. It states a condition over the stored data and a conclusion to record whenever that condition holds. Once defined, a rule's conclusion **always reflects the current data**: it is in force exactly while its condition holds, so a derived fact is never stale. A computed field (§13.7) derives one field of one class from that class's own fields; a standing rule is written on its own and is named. ### 14.1 The rule block A rule is a `def` marked with the `@rule` decorator, named like any script, then a `for` clause naming the subjects it ranges over, an `if` clause stating the condition, and an indented conclusion: ``` @rule def needs_review(): for o in Order: if o.total > 1000 and absent(o.shipment): o.review = True ``` ``` rule-decl := '@rule' NEWLINE 'def' IDENT '(' ')' ':' NEWLINE INDENT 'for' subject-binding ( ',' subject-binding )* ':' NEWLINE INDENT 'if' premise ( 'and' premise )* ':' NEWLINE INDENT conclusion NEWLINE DEDENT DEDENT DEDENT subject-binding := IDENT 'in' kind-name ``` The `for` clause names the kinds the rule ranges over and the name it gives each subject (`for o in Order`). Every name the rule uses — in a premise or in its conclusion — is one of those subject variables. The `@rule` marker distinguishes a rule from an ordinary script; `for`, `in`, `if`, and `and` read here exactly as they do elsewhere in the language, and `absent` names the rule's one negative premise (§14.2). A rule may bind **more than one** subject, separated by commas, and then relate them with a join premise (§14.2). Each name must be distinct. The bindings are a conjunction and carry no order: they are separated by commas rather than written as nested `for` blocks precisely because nesting would suggest an iteration sequence, and a rule states a condition over the whole store rather than describing a walk through it. A nested `for` inside a rule is not accepted. ``` @rule def taint_spreads(): for f in Fn, c in Call, g in Fn: if f.tainted == True and c.caller == f and c.callee == g: g.tainted = True ``` Read plainly: whenever a tainted function `f` is the caller of some call `c`, and `c`'s callee is `g`, then `g` is tainted too. Because the conclusion writes the same field the first premise reads, the rule applies to its own results, and the taint reaches everything the call graph connects — not to a fixed number of steps. Two of the three subjects are named by the join rather than compared: `c` and `g` are found through `f`, which is what lets one rule follow a chain. ### 14.2 Premises The `if` clause is one or more **premises** joined by `and`; the rule holds only when every premise holds: ``` premise := comparison | equality | join | field-cmp | relation | absence | not-asserted | nonexistence comparison := IDENT '.' IDENT ord-op ( ['-'] number | STRING ) # o.total > 1000, o.name < "m" equality := IDENT '.' IDENT eq-op literal # o.lic == "MIT", o.total != 5 join := IDENT '.' IDENT eq-op IDENT # c.caller == f field-cmp := IDENT '.' IDENT ( eq-op | ord-op ) IDENT '.' IDENT # o.delivered > o.deadline relation := IDENT '.' IDENT '.' IDENT eq-op literal # Reach.x.y == True absence := 'absent' '(' IDENT '.' IDENT ')' # absent(o.shipment) not-asserted := 'not_asserted' '(' IDENT '.' IDENT ')' # not_asserted(b.flies) nonexistence := 'none' '(' IDENT 'in' IDENT ':' premise ( 'and' premise )* ')' # none(c in Call: c.caller == f) eq-op := '==' | '!=' ord-op := '<' | '<=' | '>' | '>=' ``` - A **comparison** (`o.total > 1000`) holds when the field, read as a number, stands in the given order to the numeric literal. The bound may be **negative** (`r.temp < -10`), so a threshold over a signed quantity — a temperature, a balance, an elevation — is expressible. The bound may also be a **quoted string** (`o.name < "m"`), in which case the field is read as text and ordered **alphabetically**, by Unicode code point. The two readings do not mix: a text bound compares only against fields holding text, and a numeric bound only against fields holding numbers, so a column carrying both never answers by accident. - An **equality** (`o.lic == "MIT"`) holds when the field holds exactly that value. It takes the same literals a conclusion takes: a quoted string, an integer (negative included), or `True` / `False`. Equality over numbers is over the **number**, so `o.total == 5` holds for a field recorded as `5` and for one recorded as `5.0`; a field holding the *text* `"5"` is a string, not the number, and does not hold. - An **inequality** (`o.total != 5`) is the exact complement of `==` over values that are **recorded**: it holds when the field holds some value that is not the given one — including a value of another kind, so a field holding the text `"5"` does hold `o.total != 5`, the same reading that keeps it out of `o.total == 5`. A field with **no value recorded**, or one recorded as explicitly empty, holds NEITHER `==` nor `!=`: comparing against nothing is not a comparison. Ask that question with `absent(...)`, which is about whether a value exists rather than what it is. - A **join** (`c.caller == f`) holds when the field holds the **subject of another subject the rule binds**. The right side is a subject name from the `for` clause rather than a value, which is how a rule relates two subjects: it reads a field as a reference and follows it. A field written with `remember` holds a subject exactly when the value recorded there is that subject's name, so a join and a plain equality are the same test — what differs is that a join says which subject the answer is about, and so lets the conclusion be about that subject instead. A join with `==` also **ranges** the subject on its right, which is what allows a conclusion about a subject no premise compared. `!=` does not: it says which subjects are excluded, which names no definite set of subjects (§14.5). The right side of a join is a subject. To compare against a second **field**, write that field — see the next entry, which is a different premise. - A **field comparison** (`o.delivered > o.deadline`) holds when the two fields' stored values stand in the given order. Both operator families apply: the ordered ones compare as §8.1 does — numerically between two numbers, chronologically between two instants, alphabetically between two texts — and `==` / `!=` compare for equality. One token tells a join from a field comparison: a bare subject on the right is a join, a subject followed by a field is this. The two fields may belong to the **same** subject or to different subjects the same `for` binds: ``` @rule def late(): for o in Order: if o.delivered > o.deadline: o.late = True @rule def over(): for c in Charge, l in Limit: if c.amount > l.cap: c.over = True ``` **A field comparison requires both fields to have a value.** A subject with no `deadline` recorded has nothing to be late against, so the rule does not conclude about it — the same reading `==` and `!=` already have, and `absent(...)` remains the way to ask whether a value exists at all. The right side names one subject and one field. A **specific** subject (`Order.o1.total`) cannot be named there: a rule ranges over the subjects it binds, and asking about one named subject is what `current(...)` answers. - An **absence** (`absent(o.shipment)`) holds when the subject has **no value recorded** for that field. This is the one negative premise, and it means the plain absence of information — not a field recorded as `false` or empty. - A **not-asserted** (`not_asserted(b.flies)`) holds when **nobody has recorded a value** for that field. It is the narrower of the two negative premises: `absent(...)` asks whether the cell is empty, this asks only whether a person put something there, so a value a rule concluded leaves it holding while `absent(...)` goes false. Like an absence it is shape-only — there is no `not_asserted(b.flies, True)` form, because *did a person record this particular value* is a different question and is answered by reading the field. **This is what lets a rule state a default and yield to a recorded fact.** *Birds fly, unless someone has said otherwise about this bird* is one rule: ```python @rule def birds_fly(): for b in Bird: if b.species == "avian" and not_asserted(b.flies): b.flies = True ``` Record `b.flies = False` for a penguin and the rule stops concluding about that bird — not because the conclusion was overwritten, but because its premise stopped holding. Remove that record and the default returns. No conflict is created and nothing has to be ordered, which is the difference between a default and a fight between two sources. **A rule may name its own conclusion in `not_asserted(...)`, and this is the one place that is allowed.** `absent(b.flies)` in the rule above would be self-cancelling — the rule's own conclusion would falsify its own premise — and is refused with a message pointing here. `not_asserted(...)` reads only what people wrote, and a rule's conclusion is not that, so the question stays answerable no matter how many times the rule fires. - A **nonexistence** (`none(c in Call: c.caller == f and c.tainted == True)`) holds when **no row of that kind satisfies every premise inside it**. Where an absence asks about one cell of one subject, this asks about a whole set — "none of its callees is tainted", "no order of this customer is unpaid" — which is the difference between naming a fact and quantifying over a relation. The inner premises are the ordinary premise grammar and may name the outer rule's rows, so `c.caller == f` is what ties the inner set to the subject being concluded about. **It holds for a subject the set never mentions.** A function with no callees at all satisfies "none of its callees is tainted" — vacuously, and that is the intended reading. This is why a `none(...)` is enough on its own to say which subjects a rule applies to (§14.5): the subjects it concludes about are precisely the ones no inner row reaches, so they can be reached by nothing else. **What it records.** The rule is answered in two stages, and the intermediate is an ordinary derived 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 visible wherever any derived field is — `list`, `current`, `checkup`, and in `why` for the conclusion drawn from it — and it holds `True` exactly for the subjects the `none(...)` excludes. Nothing about it is hidden, and reading it is a supported way to see which rows the quantifier found. ### 14.3 The conclusion ``` conclusion := cell '=' ( literal | '-' INT | fold ) # o.review = True, r.adjustment = -5, # c.order_count = count(o) cell := IDENT '.' IDENT # a subject and one of its fields | IDENT '.' IDENT '.' IDENT # a kind, a subject, a field fold := fold-name '(' IDENT ')' # count(o) — fold the rows | fold-name '(' IDENT '.' IDENT ')' # sum(o.amount) — fold one field fold-name := any single-operand fold of §7.1.1 # count, sum, avg, argmax, … ``` Whenever the condition holds, the engine records the named field of the named subject as the given literal, which may be a **negative** integer (`r.adjustment = -5`). As with a computed field, the customer never writes that field directly. A cell can be named in two lengths. The **two-segment** form, `o.review`, names a field of a subject the `for` clause bound, and is what most rules use. The **three-segment** form is the same `Kind.subject.field` path used everywhere else in the language — `remember(Order.o1.total, …)` — except that the last two segments may be **bound names** rather than literals. That is what lets a rule record a fact about a **pair**: ``` @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 rule records every direct edge; the second joins a known reach to a further edge and records the longer one. Because the second reads the same relation it writes, it applies to its own results and settles on **everything the graph connects** — not on a fixed number of steps. Reading a relation with a bound name in the field position asks for **every** cell of that subject, so `Reach.x.y` in a premise finds each `y` that `x` reaches rather than requiring one to be known in advance. **A cycle needs nothing further.** A subject that reaches itself is in one, so the query is the relation read with the same name twice: ``` @rule def in_cycle(): for x in Fn: if Reach.x.x == True: x.cyclic = True ``` A name used twice in one cell **agrees with itself** rather than standing for two things: `Reach.x.x` holds only where the subject and the field are the same name, which is what makes this a cycle test and not a list of everything reachable. A name in the subject or field position of a conclusion must be bound by the rule — by the `for` clause, by a join, or by a relation premise. A relation premise binds both of its names, which is how the second rule above ranges `y` without comparing it to anything. **A conclusion may fold the rows instead of naming a literal.** `c.order_count = count(o)` records, for each customer, how many `Order` rows met the condition *with that customer*. 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) @rule def regular(): for c in Customer: if c.order_count > 3: c.regular = True ``` A customer with four orders gets `4`; a customer with one gets `1`. That per-subject answer is the difference from an aggregate **query** (§7.1.1), which folds a whole attribute across every subject of a kind and yields a single number: `count(Order.customer)` is how many orders exist, and `count(o)` here is how many are *this customer's*. Two shapes, by what is folded: | Written | Folded | |---------|--------| | `count(o)` | the rows themselves — a bare row variable | | `sum(o.amount)` | one field of those rows | **Which folds may appear.** The **single-operand** folds of §7.1.1 — every family there except *ranked* and *two-attribute*. `percentile(o.amount, 90)` and `slope(o.x, o.y)` need an argument a conclusion has nowhere to put, and are refused here rather than admitted half-formed. The rest keep their §7.1.1 meanings exactly, the identity and positional folds included: `argmax(o.amount)` records the **subject** holding this group's largest amount, and `distinct(o.region)` records how many distinct regions this group covers. **A row missing the folded field contributes nothing to a fold over that field, and still counts as a row.** Four orders of which three carry an amount give `count(o)` of `4` and `sum(o.amount)` over the three. Naming a field makes its presence a premise — the same reading a field comparison has (§14.2). **A fold ranges over the premises' MATCHES, and a location holding more than one value in force matches once per value.** §7.6 already states the general rule — a standing rule reads every value at a location in disagreement and derives from each — and a fold is where it becomes visible as arithmetic. Take two orders, and let a second source also record that the first belongs to this customer. That order now matches twice, and `count(o)` answers `3` for two orders. **Each fold follows the claims of the field IT reads**, so the two shapes move independently, and the difference is worth knowing before reading a number: | what holds two values in force | `count(o)` | `sum(o.amount)` | |---|---|---| | nothing | `2` | `30` | | the joined field (`o.customer`) | `3` | `30` — unchanged | | the folded field (`o.amount`) too | `3` | `50` — the amount is added twice | `count(o)` folds the join's matches, so a second claim on the joined field raises it. `sum(o.amount)` folds the amount's own claims and does not see the join's extra match at all; only a second claim on the amount adds it again. **For the number of distinct subjects, fold `distinct(o)`**, which answers `2` over the same data and is what `subjects(Order.customer, c)` counts in program position. Nothing here is special to folds — an ordinary conclusion is derived once per matching value too — but a literal conclusion records the same value twice and looks unchanged, while a count does not. **The folded row must be bound by the `for` clause**, like every other name a rule uses. Folding a name the rule does not range over is refused, and the refusal names that name. The third rule above is the ordinary case that makes the first two worth having: a derived field is a premise like any other (§14.4), so "a customer with more than three orders is a regular" is one comparison against a column nobody wrote. A fold may not, directly or through other rules, feed a premise that the same fold depends on — see §14.5. ### 14.4 What a rule does Defining a rule takes effect immediately and continuously: - A rule's conclusion is **in force exactly while its condition holds over undisputed data** — evaluated over the data present at definition time and kept current as data is written or removed (including when a value is first recorded for a field an `absent(...)` premise required to be absent). A conclusion in force carries a `derived` provenance (§7.1) in place of a source. - When a conclusion's condition ceases to hold, the conclusion ceases to be in force; when it comes to hold, the conclusion is in force. A rule therefore states an **invariant** over the data, not a one-time action. - **A premise in disagreement carries the disagreement into the conclusion** (§7.6). While a premise location holds claims from different sources with different values, a rule reading it derives once from each value that satisfies its condition, and every such conclusion is in force. This holds whether the disagreement arose before or after the conclusion was first derived: a conclusion already standing is not withdrawn when its premise comes into dispute, and the contesting value's conclusion joins it. Conclusions collapse back to one when the disagreement clears — where the disagreeing claims were written, by `update`ing or `forget`ting one of them; where they are themselves conclusions, neither reaches, since a conclusion `forget` withdraws is recorded again while its condition holds and an `update` adds a further claim beside the two, so that disagreement clears by changing the rules that produce it. The outcome depends on the data, never on the order the claims arrived: recording the disagreement first and the rule second reaches the same conclusions as the reverse. A derived field reads back exactly like any other field (`current`/`get`, §7.1); its value reflects the rules currently in force. **A conclusion is valid while its premises are.** A premise may carry a validity window (§7.1), and a conclusion drawn from windowed premises is valid over the time they are **all** valid together — the overlap of their windows, and no wider. Nothing else about the rule changes: the conclusion is in force exactly while its condition holds, and its window says which times that condition is being asked about. ``` # window-overlap.dpy — a conclusion drawn from two windowed premises is valid # over the time both premises are valid, and not outside it. @rule def flagged(): for e in Emp: if e.status == "active" and e.dept == "eng": e.flagged = True def overlap_report(): remember(Emp.e1.status, "active", "hr", t"2020-01-01T00:00:00Z", t"2022-12-31T00:00:00Z") remember(Emp.e1.dept, "eng", "hr", t"2021-01-01T00:00:00Z", t"2023-12-31T00:00:00Z") inside = get(Emp.e1.flagged, t"2021-06-01T00:00:00Z") print("inside the overlap: " + str(len(inside))) after = get(Emp.e1.flagged, t"2023-06-01T00:00:00Z") print("after it: " + str(len(after))) ``` ``` OK script overlap_report(): 2 claims written, 2 prints remember Emp.e1.status = "active" remember Emp.e1.dept = "eng" print inside the overlap: 1 print after it: 0 ``` The two premises overlap from 2021-01-01 to 2022-12-31, so that is when the conclusion is valid. An as-of read (§7.1) inside the overlap finds it and one outside does not, which is why the second read above answers empty although `dept` is still valid then. A bare read answers about the present, so once the overlap has passed the conclusion is **absent from the present** — the correct answer, and not a rule that stopped working. A premise carrying **no** window is valid at all times and therefore narrows nothing: a conclusion drawn from one windowed and one unwindowed premise takes the windowed one's bounds. A premise with one open bound narrows only the side it names. **Premises that never overlap conclude nothing.** Where the windows have no time in common there is no moment at which the condition holds, so the rule records no conclusion at all — at no time, the present included. That is not an error and is not reported as one: the rule is well-formed, it applied, and the data gave it nothing to conclude. `why_not` (§7.1) on the cell names the premise that is not in force at the time asked about, which is what tells this apart from a rule that never applied and from a cell no rule concludes. **A window carries through a chain.** A conclusion is an ordinary premise to any rule that reads it, and it carries its own window when it is read that way. A rule concluding from a conclusion is valid over the same overlap the first one was, and a chain of rules narrows to the time every fact along it is valid. ### 14.5 Well-formed rules Two things make a rule usable; a rule that lacks either is rejected when you define it, with a message that names the rule. - **A rule must say which subjects it applies to** — every subject it binds, not just one of them. A subject whose only mention is an absence test never says *which* subjects, so the rule has nothing to work over (`for o in Order … if absent(o.shipment): …` — which orders?). The same applies to a `not_asserted(...)`, for the same reason and not a second one: it names one cell and describes subjects without saying where to find them. In the defeasible rule of §14.2 the `b.species == "avian"` premise is what ranges `b`, and a default worth stating almost always has such a premise already — the population it is a default FOR. Four premises range a subject: a **comparison**, a **join** (either side, `==` only — a `!=` join says which subjects are excluded, which is the same non-range an absence has), a **relation** premise, which ranges both of its names, and a **nonexistence** (§14.2). Give each subject at least one of those. A nonexistence ranges where an absence does not, and the difference is not arbitrary even though both are negative: an absence names one cell and nothing else, so it describes subjects without saying where to find them. A `none(...)` carries a whole inner rule, and the subjects it concludes about are exactly the ones that inner rule does not reach — a set the engine can enumerate, because it is the kind's own subjects minus the ones the inner premises matched. So the range is not an extra requirement placed on the author; it falls out of what the premise means. This is what lets *"a function is safe when none of its callees is tainted"* be written as it reads, with no unrelated anchor field invented to give the rule something to stand on. - **A rule's outcome must settle.** A rule — alone or together with others — must not chase its own tail: if recording its conclusion would remove the very condition that produced it, there is no answer to settle on, and the rule is rejected. You may build rules on stored data and on one another freely; the only thing ruled out is a set that cancels itself. **A fold (§14.3) settles on the same terms, for a second reason.** A fold reads a whole group before it can answer, so a fold whose own result feeds — directly or through other rules — a premise that fold depends on is asking for a number that changes as soon as it is written. That set is rejected at definition too. Counting from data other rules derive is fine; what is ruled out is a count that is a member of what it counts. ### 14.6 Termination Standing rules preserve the termination guarantee of §9.5. A rule ranges over finitely many stored subjects; its premises are tested, not iterated; and §14.5 rules out the one self-cancelling construction under which the outcome could fail to settle. Every set of rules therefore reaches a fixed set of derived facts in finite time. ### 14.7 `list rules` ``` list rules ``` Lists the **names** of the standing rules you have defined, one per line — the rule-authoring counterpart of `list scripts` (Wire §9.2). `list the standing rules` is an accepted synonym. Listing order is implementation-defined but MUST be stable across reads with no intervening rule definition. Only the rule **names** are returned; the listing carries no premises or conclusions. To see what a rule does, keep your own source — the service stores no rule source. `list rules` is **wire-only** and its response is rendered text, not a typed value; there is no expression-position `list rules` inside a program (unlike `list scripts`, which additionally binds a `string_list`). An empty store — no rules defined — lists nothing. ### 14.8 `forget rule` ``` forget rule ``` Removes **one** standing rule and everything it derived. `` is the qualified `module.rule` name that `list rules` (§14.7) prints. The removal is hard, the same as any other removal (§7.1): the rule stops firing and leaves `list rules`, and the facts it concluded are reclaimed. Facts a removed rule concluded do **not** all disappear. A conclusion that another standing rule still supports is re-derived and stays — only the support this rule contributed is withdrawn. So removing one of two rules that agree leaves their shared conclusion standing, on the surviving rule. Removing a rule does not touch the facts it **read**. Premises are your data; only conclusions are the rule's. An address with no rule behind it is refused, naming the address, and nothing is removed. `forget rule` is **wire-only** — there is no expression-position form inside a program — and it needs a `read-write-delete` key, as every removal does. To bring a removed rule back, `compile` its module again: the rule returns and re-derives its conclusions over the facts that are still there. This holds of every rule in a store. There is no class of rule this verb declines to remove, and nothing reinstates a rule you did not ask to have back — a module is in your store because you compiled it there. ### 14.9 `checkup` ``` checkup ``` Reports the store against the standing rules in force over it. It takes no arguments, changes nothing, and needs only a read key. It exists because a rule that never fired and a rule that fired and found nothing produce the same empty result. Where the reasoning came from a module the reader did not write, nothing else in this specification distinguishes the two: §14.7 gives rule names and no premises, and the data verbs (§7.1) describe the store without reference to the reasoning over it. The response is a counts line followed by findings, one per line, in a closed set of forms: | Form | Holds when | |---|---| | `unmet . no-such-kind` | some standing rule's premise reads that cell and the store holds no kind of that name | | `unmet . no-values` | the kind is present and no claim stands at that field for any subject | | `unmet . not-in-force` | the kind is present and a claim stands at that field, and every such claim carries a validity window (§7.1) that does not cover the time asked about | | `unread ` | the kind holds claims and no standing rule's premise reads it | | `near ~ ` | `A` is unread, `B` is the kind of an unmet `no-such-kind` cell, and their names differ only slightly | | `violated …` | a standing constraint (§14.10) does not hold; `` is how many subjects breach it, and at most **five** of them are listed | | `counts rules= unfirable= kinds= unread= constraints= violated=` | always; `unfirable` counts rules with at least one unmet premise, `violated` counts constraints that do not hold | Kinds are named in the addressable form (`.` for a kind a module declares), which is the form §7.1's verbs take. Findings name **cells and never rules**. A cell is part of a module's interface — `info_module` (Wire §9.4) already enumerates the classes a module declares — while which premise belongs to which rule is part of its body, which is not readable. Rules are therefore counted, not named. A `violated` finding names the **constraint and the offending subjects, and not the cell** — the mirror of that rule rather than an exception to it. An `unmet` finding is about the store's SHAPE, so a cell is the right noun and naming the rule would map a premise to a body. A `violated` finding is about one named invariant the author declared, so the constraint is the right noun, and naming the cell would map a condition to that constraint's body in exactly the way the paragraph above forbids. The subjects are what make it actionable: knowing that `stock_never_negative` broke is worth little without knowing which products broke it, and a subject id is data the reader already owns. The COUNT is exact and the list is capped at five, so a constraint breached by a whole kind reports the scale of the breach without putting the store's subject list in a report meant to be read. `checkup` is **wire-only**: there is no expression-position form inside a program, and using the name in a program body is an ordinary identifier. An empty store yields the counts line alone. Listing order within each form is implementation-defined but MUST be stable across reads with no intervening change to the store. --- ### 14.10 `@constraint` A **constraint** watches a condition and reports. It concludes nothing, writes nothing, and can never fire: ``` @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` clauses, and no head. `violated` is a statement, not a value — it marks the block as a constraint body and is a reserved word only in that position. **A breach does not become data.** The alternative without this construct is a rule concluding `p.invalid = True`, which records facts ABOUT the store INSIDE the store, and then feeds them to other rules as though they were observations. A constraint has no conclusion to record, so there is nothing for a later rule to read. That is the whole difference, and it is why a constraint is not simply a rule whose head you ignore. A constraint is evaluated by `checkup` (§14.9), which reports one `violated` finding per constraint that does not hold. It is never evaluated 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 that says so. ``` @constraint def every_order_has_a_customer(): for o in Order: if absent(o.customer): violated ``` **Premises are a subset of the §14.2 grammar**, and the subset is the whole of what a constraint can be asked. Two shapes are admitted: | premise | example | |---|---| | a comparison against a literal | `p.stock < 0`, `p.tier == "gold"` | | an absence | `absent(o.customer)` | Several joined by `and` are allowed, and hold when a subject satisfies all of them. Anything else — a premise relating two rows, a quantifier, a premise that selects on how a value came to be recorded — is refused when the constraint is defined, naming the two shapes that are accepted. A constraint also binds **exactly one row variable**. A rule may relate two kinds (`for c in Customer, o in Order`); a constraint may not. Both restrictions have one cause and it is worth stating rather than hiding: a rule is answered by the standing reasoning over your store, and a constraint is answered by RE-READING that store. A read asks about one kind and one condition, so a constraint is one read per premise with the answers intersected — and the premises above are exactly those a read can express. To check something outside that, conclude it into a field with a `@rule` and write the constraint over that field. The rule does the reasoning, the constraint does the watching, and neither grows the other's job. **Naming.** A constraint shares the name space of scripts and rules, and `list rules` (§14.7) does not list it — a constraint is not a rule and a caller enumerating rules to reason about derivation would be misled by one. `checkup`'s counts line reports how many stand, and the qualified name it prints is also the address `forget constraint` (§14.11) takes. **Termination** is not a question a constraint raises. It derives nothing, so it cannot feed itself, and its evaluation is a bounded pass over the subjects of one kind. ### 14.11 `forget constraint` ``` forget constraint ``` Removes **one** standing constraint. `` is the qualified `module.constraint` name that `checkup` (§14.9) prints in a `violated` finding and counts on its `constraints=` line. **Nothing else changes**, and that is the whole of why this verb is separate from `forget rule` (§14.8). A constraint concludes nothing, so there is no conclusion to withdraw and no fact to reclaim. Removing a rule raises a question about the facts it derived; removing a constraint raises none, because it derived none. After the removal the store holds exactly what it held before, and the only difference is that `checkup` no longer reports on that invariant. The data the constraint watched is **untouched — including the subjects that breached it**. A breach was never recorded (§14.10), so there is nothing to clean up: the products with negative stock are still there, and their stock is still negative. Stopping the watch is not fixing the breach, and this verb does not pretend otherwise. An address with no constraint behind it is refused, naming the address, and nothing is removed. `forget constraint` is **wire-only** — there is no expression-position form inside a program — and it needs a `read-write-delete` key, as every removal does. To bring a removed constraint back, `compile` its module again. Before this verb the only way to drop one invariant was `forget_module` (Wire §9.4), which takes the module's classes, its scripts, its other constraints and the data in its kinds along with it — a price with no relation to what the one invariant cost. --- ## 15. Hypothesis A **hypothesis** reads what a value *would be* under supposed facts, without changing anything. `suppose(, , …, )` sets each named field to the value beside it, lets your standing rules (§14) and computed fields (§13.7) run as if those were true, reads the final field, and then discards the suppositions — the store is left exactly as it was. ``` r = suppose(Order.o1.total, 2000, Order.o1.review) ``` A scenario usually needs more than one fact to be true at once. Give as many `, ` pairs as it takes; the field to read is always the last argument, alone. ``` r = suppose(Order.o1.total, 2000, Order.o1.shipment, "sent", Order.o1.review) ``` Read: "if the order totalled 2000 **and** had shipped, would it need review?" A rule requiring both conditions can now be asked about, which one supposition could not do. Read: "if `Order.o1.total` were 2000, what would `Order.o1.review` be?" If a rule sets `review` when `total > 1000`, `r` is `true` — yet afterward `Order.o1.total` keeps its real value (or stays unset) and no `review` is recorded. Nothing the hypothesis touches persists. ``` hypothesis := 'suppose' '(' ( path ',' literal ',' )+ path ')' ``` - Each **supposition** `, ` sets one field to one literal value. A hypothesis takes **1 to 16** of them. They apply **left to right**, so two suppositions naming the same field leave the later one standing — the same rule an ordinary sequence of writes follows. A value taken from a variable is not yet available. - The **limit of 16** is a cost bound, not a semantic one. Each supposition is its own bounded reasoning pass, and the total cost grows faster than the count does (measured: 13 ms at two suppositions, 251 ms at 201, 1.5 s at 501). A scenario written by hand does not approach 16; the limit exists so that a program which would has a compile error naming the number rather than an invisible cliff at run time. - A single hypothesis supposes facts **into place** or supposes them **away** (§15.1), not both. Mixing the two in one hypothesis is not available. - The **read** `` names the field whose value is returned — a plain stored field, or one a rule or computed field derives from the supposition. - The result is a **value** (§5.6), bound to a name and consumed with `match` like a cell read or an aggregate (§7.1.1). Concatenating it into a `print` renders it directly. If the read field has no value under the supposition, `suppose` produces no value — a catchable condition (guard it with a `try` / `except` handler, or read a field a rule is known to derive). A hypothesis never writes: the suppositions and everything derived from them are discarded when `suppose` returns, so reading under a hypothesis has no side effect — safe for preview, comparison, and what-if exploration. It preserves the termination guarantee of §9.5: each supposition is one bounded reasoning pass, the number of them is fixed where the call is written, and there is one read. ### 15.1 Supposing a fact away `suppose_absent(, …, )` asks the opposite question: **what would this field say if those facts did not exist?** It supposes each named field's fact away, lets your standing rules and computed fields run without them, reads the final field, and discards the suppositions. ``` r = suppose_absent(Order.o1.total, Order.o1.review) ``` As with `suppose`, name as many fields as the question needs. The field to read is the last argument, alone — so `suppose_absent(a, b, c)` supposes away `a` and `b`, and reads `c`. ``` r = suppose_absent(Order.o1.total, Order.o1.shipment, Order.o1.review) ``` Read: "if `Order.o1.total` were not recorded, what would `Order.o1.review` be?" If a rule sets `review` from `total`, `r` is **empty** — the conclusion has nothing left to stand on. Afterwards `Order.o1.total` still holds its real value and `review` still holds its derived one; nothing was removed. ``` absence-hypothesis := 'suppose_absent' '(' ( path ',' )+ path ')' ``` - Each **supposition** `` names one field whose fact is supposed away. As with `suppose`, a hypothesis takes 1 to 16 of them, applied left to right. - The **read** `` names the field to read under that absence — a stored field, or one a rule or computed field derives. - The result is an **active claim** (§7.1) that may be **empty**, consumed with `match` exactly like `current`: ``` 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") ``` This is the one place where the two hypothesis verbs differ in what they hand back, and the difference is the point. `suppose` asks *what would this value be*, so a missing answer is an edge case and arrives as a catchable condition. `suppose_absent` asks *what would survive*, and **"nothing" is the answer it exists to give** — so it arrives as an ordinary empty read rather than as an error you must catch to learn what you asked. **Why the verb exists.** `forget` (§7.1) cannot be undone. `dependents` tells you what *points at* a fact; it does not tell you what the answers *become* without it. `suppose_absent` is the rehearsal: run it over the fields you care about before you remove anything, and see what disappears while it is still there to put back. Like `suppose`, it never writes, and it preserves the same termination guarantee: one bounded reasoning pass per supposition, a count fixed where the call is written, and one read. --- ## Appendix A — Full grammar in one block ``` source := option-verb NEWLINE | module-body # §4.1, Reference §9.1 module-body := top-item+ top-item := decl | class-decl | rule-decl | import-stmt | statement # §13, §14, Modules option-verb := '--' IDENT IDENT? decl := 'def' IDENT '(' params? ')' ( '->' type-name )? ':' NEWLINE INDENT stmt+ DEDENT # value script when '-> type' present (§4.2) params := param ( ',' param )* ( ',' var-param )? | var-param param := IDENT ':' type-name ( '=' const-expr )? var-param := '*' IDENT ':' type-name # variadic *args (§4.2) class-decl := 'class' IDENT ( '(' IDENT ')' )? ':' NEWLINE INDENT class-member+ DEDENT # §13.1, base class §13.8 class-member := field-decl | method-def field-decl := IDENT ':' type-name NEWLINE method-def := 'def' IDENT '(' 'self' ( ',' param )* ')' ':' NEWLINE INDENT stmt+ DEDENT # void, §13.4 | 'def' IDENT '(' 'self' ( ',' param )* ')' '->' type-name ':' NEWLINE INDENT stmt* 'return' expr NEWLINE DEDENT # value, §13.4 rule-decl := '@rule' NEWLINE 'def' IDENT '(' ')' ':' NEWLINE INDENT # §14.1 'for' subj-binding ( ',' subj-binding )* ':' NEWLINE INDENT 'if' premise ( 'and' premise )* ':' NEWLINE INDENT conclusion NEWLINE DEDENT DEDENT DEDENT subj-binding := IDENT 'in' kind-name # §14.1 premise := IDENT '.' IDENT ord-op ( ['-'] number | STRING ) # comparison, §14.2 | IDENT '.' IDENT eq-op literal # equality, §14.2 | IDENT '.' IDENT eq-op IDENT # join, §14.2 | IDENT '.' IDENT ( eq-op | ord-op ) IDENT '.' IDENT # field comparison, §14.2 | IDENT '.' IDENT '.' IDENT eq-op literal # relation, §14.2 | 'absent' '(' IDENT '.' IDENT ')' # absence, §14.2 ord-op := '<' | '<=' | '>' | '>=' eq-op := '==' | '!=' conclusion := rule-cell '=' ( literal | '-' INT | rule-fold ) # §14.3 rule-cell := IDENT '.' IDENT | IDENT '.' IDENT '.' IDENT # §14.3 rule-fold := fold-name '(' IDENT ( '.' IDENT )? ')' # §14.3 fold-name := any single-operand fold of §7.1.1 # count, sum, avg, argmax, … type-name := 'string' | 'int' | 'bool' | 'datetime' | 'duration' | 'real' | 'blob' # value-class scalars (§5.5) | 'active_claim' | 'claim_list' | 'proof_tree' | 'subject_set' | 'string_list' | 'handle' | 'verify_result' | 'result_type_set' | IDENT # a class name, in instance-binding position (§13.2) stmt := simple-stmt NEWLINE | block-stmt simple-stmt := assign-stmt | print-stmt | call-stmt | verb-call-stmt | commit-stmt | rollback-stmt | import-stmt | return-stmt # early exit / value (§9.2.8) | 'break' | 'continue' # loop control (§9.2.7) block-stmt := match-stmt | for-stmt | if-stmt | try-stmt | branch-block assign-stmt := IDENT '=' expr | IDENT aug-op expr # `x op= e` is `x = x op e` (§4.3) | IDENT ( '=' IDENT )+ '=' expr # chained assignment (§8.12) | top-target ( ',' top-target )+ '=' expr ( ',' expr )* # tuple unpacking; nested + one optional `*rest` (§8.11) top-target := unpack-target | '*' IDENT # a target or THE single starred target unpack-target := IDENT | '(' unpack-target ( ',' unpack-target )* ')' # a name or a nested tuple target aug-op := '+=' | '-=' | '*=' | '/=' | '%=' | '//=' | '**=' print-stmt := 'print' '(' ( expr | ('sep'|'end') '=' STRING ) ( ',' ( expr | ('sep'|'end') '=' STRING ) )* ')' # §8.7 call-stmt := IDENT '(' arg-list? ')' verb-call-stmt := IDENT '(' arg-list? ')' # a built-in verb call (§7) commit-stmt := 'commit' rollback-stmt := 'rollback' import-stmt := 'import' module-name # Reference §9.3 module-name := IDENT ( '.' IDENT )* # Reference §9.3 return-stmt := 'return' expr? # §9.2.8 match-stmt := 'match' expr ':' NEWLINE INDENT case-clause+ DEDENT # a bare-instance-variable scrutinee is a class match (§13.5) # a value scrutinee is a value match (§5.6, §6.2) case-clause := 'case' IDENT ( 'as' IDENT )? ':' ( simple-stmt NEWLINE | NEWLINE INDENT stmt+ DEDENT ) for-stmt := 'for' IDENT ( ',' IDENT )* 'in' expr ':' NEWLINE INDENT stmt+ DEDENT # a target list unpacks each element (§8.11) if-stmt := 'if' expr ':' NEWLINE INDENT stmt+ DEDENT ( 'elif' expr ':' NEWLINE INDENT stmt+ DEDENT )* ( 'else' ':' NEWLINE INDENT stmt+ DEDENT )? try-stmt := 'try' ':' NEWLINE INDENT stmt+ DEDENT handler* handler := 'except' 'refuse' ( 'as' IDENT )? ':' NEWLINE INDENT stmt+ DEDENT | 'except' 'engine_error' ( 'as' IDENT )? ':' NEWLINE INDENT stmt+ DEDENT branch-block := 'with' 'branch' '(' STRING ')' ':' NEWLINE INDENT stmt+ DEDENT arg-list := arg ( ',' arg )* arg := expr | IDENT '=' expr # positional | keyword (§4.3) expr := cond-expr cond-expr := or-expr ( 'if' or-expr 'else' expr )? # ternary; right-assoc; lower than `or` or-expr := and-expr ( 'or' and-expr )* and-expr := cmp-expr ( 'and' cmp-expr )* cmp-expr := add-expr ( ( '==' | '!=' | '<' | '>' | '<=' | '>=' ) add-expr )* add-expr := mul-expr ( ( '+' | '-' ) mul-expr )* mul-expr := unary-expr ( ( '*' | '/' | '%' ) unary-expr )* unary-expr := ( 'not' | '-' ) unary-expr | postfix-expr postfix-expr := primary-expr postfix* postfix := '.' IDENT '(' arg-list? ')' | '.' IDENT | '[' expr ']' | '[' expr? ':' expr? ( ':' expr? )? ']' primary-expr := STRING | INT | 'True' | 'False' | list-display # list literal / comprehension (§3.5.9, §8.9) | brace-display # dict/set literal or comprehension (§3.5.12, §3.5.13, §8.9) | tuple-display # tuple literal / grouping (§3.5.11) | builtin-call # zip / enumerate (§8.6) | IDENT '(' expr ')' # instance constructor (§13.2) | IDENT '(' arg-list? ')' # value-call: value-script invocation (§4.4, §6.8) | module-name '.' IDENT '(' expr ')' # module-qualified construction (Reference §9.6) | 'suppose' '(' ( path-expr ',' literal ',' )+ path-expr ')' # hypothesis (§15) | 'suppose_absent' '(' ( path-expr ',' )+ path-expr ')' # absence hypothesis (§15.1) | IDENT | path-expr | IDENT '(' arg-list? ')' # last: a built-in verb call (§7) list-display := '[' ( expr ( ',' expr )* ','? )? ']' | '[' expr ( 'for' IDENT 'in' expr ( 'if' expr )* )+ ']' brace-display := '{' ( expr ':' expr ( ',' expr ':' expr )* ','? )? '}' | '{' expr ( ',' expr )* ','? '}' | '{' expr ( 'for' IDENT 'in' expr ( 'if' expr )* )+ '}' | '{' expr ':' expr ( 'for' IDENT 'in' expr ( 'if' expr )* )+ '}' tuple-display := '(' expr ')' | '(' ( expr ( ',' expr )* ','? )? ')' builtin-call := ( 'zip' | 'enumerate' | 'reversed' | 'abs' | 'divmod' | 'str' | 'int' | 'float' | 'list' | 'set' | 'dict' ) '(' ( expr ( ',' expr )* )? ')' path-expr := IDENT ( '.' IDENT )+ literal := STRING | INT | 'True' | 'False' int-literal := dec-int | hex-int | oct-int | bin-int # see §3.5.2 string-char := ... | '\r' | '\x' hex hex | '\u' hex hex hex hex # see §3.5.1 ``` --- ## Appendix B — Reserved words (complete list) ``` # structural def class return match case if else for in try except as branch commit rollback # logical operators and or not # retired output verb (reserved so it teaches; use print(...) — §8.7) log # boolean literals True False # verb-surface vocabulary (recognised as built-in verb names, §7) remember update forget assert pin verify current get why caveats dependents conflicts subjects list source compile ``` The type names of §5.5 (`string`, `int`, `claim_list`, …) are contextual, not reserved; programs SHOULD nonetheless avoid them as user identifiers. `import` (Reference §9.3) is likewise a **contextual keyword** — recognised as the import statement only at statement head, immediately before a module name, and an ordinary identifier elsewhere — but programs SHOULD NOT use it as a user identifier. --- ## Appendix C — Sample programs (informative) These sample programs are **self-contained**: each takes no arguments and names its own subjects and values inline, so it runs exactly as shown — paste it, run it, read the result. Parameterised scripts (a signature with typed parameters, run with positional arguments over the wire) are specified normatively in Wire §4.2 and the grammar (§4); the samples here stay self-contained so they need no external invocation input. ### C.1 Trivial smoke ``` # smoke-trivial.dpy — a write, an exhaustive match, and a length read. def smoke_trivial(): remember(Cat.felix.color, "orange", "op1") cur = current(Cat.felix.color) match cur: case active_claim: print("color = " + str(cur.value) + " (per " + str(cur.source) + ")") case empty: print("no color claim") hist = get(Cat.felix.color) print("history has " + str(hist.length) + " claim(s)") ``` Run it as a one-shot with `run` (Wire §4.2). ### C.2 Audit walk ``` # audit-subject.dpy — read cluster + length composition. def audit_subject(): print("subject Cat.felix") attrs = list_attributes(Cat) print("attribute count = " + str(attrs.length)) cur = current(Cat.felix.color) print("current color inspected") hist = get(Cat.felix.color) print("history depth = " + str(hist.length)) ``` ### C.3 Try with refuse handling under a branch ``` # experimental write under a branch with explicit rollback. def try_paint(): with branch("experiment"): try: remember(Cat.felix.color, "tigret", "audit") after = current(Cat.felix.color) if after.value == "tigret": commit else: rollback except refuse as r: print("paint refused: " + str(r.reason)) rollback ``` ### C.4 Classes and methods (§13) ``` # classes.dpy — a class with a typed field, a void method, and a value # method; a def binds an instance and calls both. class Sensor: temp: string def record(self, v: string, src: string): remember(self.temp, v, src) # field write def label(self) -> string: return "sensor" # value method def demo(): s = Sensor("room-a") # instance binding s.record("21", "op1") # void method call name = s.label() # value method call reading = s.temp # field read match reading: case active_claim: print(name + " = " + str(reading.value) + " per " + str(reading.source)) case empty: print(name + ": no reading") ``` ### C.5 Datetime round-trip (§3.5.5, §5.6) ``` # datetime-round-trip.dpy — a datetime value keeps its type across write/read. def datetime_round_trip(): remember(Event.launch.at, datetime("2026-01-02T03:04:05Z"), "ops") cur = current(Event.launch.at) match cur.value: case datetime as d: print("launch at " + str(d)) case default: print("not a datetime") ``` ### C.6 Duration round-trip (§3.5.6, §5.6) ``` # duration-round-trip.dpy — a duration keeps its type and reads back canonical. def duration_round_trip(): remember(Task.build.budget, duration("PT90M"), "ops") cur = current(Task.build.budget) match cur.value: case duration as u: print("budget = " + str(u)) case default: print("not a duration") ``` ### C.7 Real round-trip (§3.5.7, §5.6) ``` # real-round-trip.dpy — a real keeps its type and reads back in canonical form. def real_round_trip(): remember(Sensor.a.reading, 3.5, "ops") cur = current(Sensor.a.reading) match cur.value: case real as r: print("reading = " + str(r)) case default: print("not a real") ``` ### C.8 Blob round-trip (§3.5.8, §5.6) ``` # blob-round-trip.dpy — a blob keeps its type and reads back as canonical hex. def blob_round_trip(): remember(Doc.d1.payload, blob("48656C6C6F"), "ops") cur = current(Doc.d1.payload) match cur.value: case blob as b: print("payload = " + str(b)) case default: print("not a blob") ``` ### C.9 Real arithmetic (§3.5.7, §8.3) ``` # real-arithmetic.dpy — reals compute; int/real promote; a computed real # writes through and reads back as a real. def real_arithmetic(): sum = 2.5 + 1.25 print("sum = " + str(sum)) # 3.75 print("half = " + str((7.0 / 2))) # 3.5 — int promotes, true division print("scaled = " + str((sum * 2))) # 7.5 — real * int promotes remember(Sensor.a.total, sum, "ops") cur = current(Sensor.a.total) match cur.value: case real as r: print("stored = " + str(r)) # 3.75, still a real case default: print("not a real") if sum > 3.0: print("above threshold") ``` ### C.10 Base64 blob input (§3.5.8) ``` # base64-blob.dpy — a blob written with the base64 spelling reads back as the # same canonical hex as the equivalent blob("…") hex form. def base64_blob(): remember(Doc.d1.payload, blob_b64("SGVsbG8="), "ops") cur = current(Doc.d1.payload) match cur.value: case blob as b: print("payload = " + str(b)) # 48656C6C6F — canonical hex case default: print("not a blob") ``` ### C.11 As-of read (§7.1) ``` # as-of-read.dpy — current/get take an optional datetime to read a value as of # another time. For an always-valid fact that is the present value; with a # validity window an interior time selects the value valid then. def as_of_read(): remember(Rate.usd.pct, "3.0", "src") past = current(Rate.usd.pct, datetime("2020-01-01T00:00:00Z")) print("rate as of 2020: " + str(past.value)) ``` ### C.12 Validity windows (§7.1) ``` # validity-window.dpy — two writes at one cell with non-overlapping validity # windows (distinct sources) model a value that changed over time; two as-of # reads at interior times select the two values. def validity_window(): remember(Sensor.room1.status, "cold", "reading-2019", datetime("2019-01-01T00:00:00Z"), datetime("2021-01-01T00:00:00Z")) remember(Sensor.room1.status, "warm", "reading-2021", datetime("2021-01-01T00:00:00Z"), datetime("2023-01-01T00:00:00Z")) past = current(Sensor.room1.status, datetime("2020-06-01T00:00:00Z")) print("status as of 2020: " + str(past.value)) recent = current(Sensor.room1.status, datetime("2022-06-01T00:00:00Z")) print("status as of 2022: " + str(recent.value)) ``` ### C.12.1 Reading back a scheduled commitment (§7.1) ``` # scheduled-commitment.dpy — a fact whose validity window has not yet opened is # not part of the present, so the traversal verbs report nothing about it until # they are given the time to answer as of. The same anchor that reads a cell # reads the enumerations leading to it, so the fact is reachable by walking # rather than only by already knowing where it is. def scheduled_commitment(): remember(Release.v2.ships, "2027-03-01", "roadmap", datetime("2027-01-01T00:00:00Z"), datetime("2027-12-31T00:00:00Z")) when = datetime("2027-06-01T00:00:00Z") subs = list_subjects(Release, when) print("subjects: " + str(subs)) attrs = list_attributes(Release.v2, when) print("attributes: " + str(attrs)) vals = list_values(Release.ships, when) print("values: " + str(vals)) ``` ### C.13 Aggregate query (§7.1.1) ``` # aggregate-demo.dpy — read-only summary statistics over a stored attribute. def aggregate_demo(): remember(Reading.r1.value, 10, "sensor") remember(Reading.r2.value, 20, "sensor") remember(Reading.r3.value, 30, "sensor") mean = avg(Reading.value) print("mean = " + str(mean)) n = count(Reading.value) print("readings = " + str(n)) # identity / positional folds (§7.1.1): distinct values, which subject holds # the max, and the earliest-recorded reading. kinds = distinct(Reading.value) print("distinct = " + str(kinds)) hottest = argmax(Reading.value) print("hottest subject = " + str(hottest)) oldest = first(Reading.value) print("first recorded = " + str(oldest)) ``` ### C.14 Computed field (§13.7) ``` # computed-field-demo.dpy — a field the engine derives and maintains. # Declaring `total` with an initializer installs a derivation: whenever an # Order's price and qty are known, total is price × qty. class Order: price: int qty: int total: int = price * qty def computed_demo(): remember(Order.o1.price, 10, "sales") remember(Order.o1.qty, 5, "sales") t = current(Order.o1.total) print("total = " + str(t.value)) ``` ### C.15 Standing rule (§14) ``` # standing-rule-demo.dpy — a named rule the engine applies automatically. # `needs_review` flags any order over 1000 with no shipment recorded; the # engine sets `review` on its own (and would withdraw it if a shipment were # later recorded). The demo writes one qualifying order and reads the flag. @rule def needs_review(): for o in Order: if o.total > 1000 and absent(o.shipment): o.review = True def rule_demo(): remember(Order.o1.total, 1500, "sales") r = current(Order.o1.review) print("review = " + str(r.value)) ``` ### C.16 Hypothesis (§15) ``` # hypothesis-demo.dpy — read a value under supposed facts, without committing. # The rule flags an order for review when it is over 1000 AND has shipped. One # supposition cannot satisfy a rule that needs two facts, so the second call # supposes both — recording nothing either way. @rule def needs_review(): for o in Order: if o.total > 1000 and o.shipment == "sent": o.review = True def hypothesis_demo(): remember(Order.o1.shipment, "sent", "ops") would = suppose(Order.o1.total, 2000, Order.o1.review) print("would review = " + str(would)) both = suppose(Order.o1.total, 2000, Order.o1.shipment, "sent", Order.o1.review) print("under both = " + str(both)) ``` ### C.17 A data module (Reference §9.1, §9.2) ``` # catalog.dpy — a module: a class schema and a data declaration. The body runs # on import (Reference §9.1); it declares no callable script (Reference §9.7). class Product: price: int remember(Product.widget.price, 500, "price-list") ``` Load it by name (service surface, Reference §9.3): ``` import catalog ``` ### C.18 Importing a module and a module-qualified read (Reference §9.3, §9.6) ``` # reporter.dpy — imports the catalog module (Reference §9.3) and reads one of its cells # with the module-qualified construction (Reference §9.6). import catalog def price_report(): p = catalog.Product("widget").price print("widget price = " + str(p.value)) ``` ``` import reporter ``` Invoking `reporter`'s script by its module-qualified address `reporter.price_report` (Reference §9.6) against a store that has imported `catalog` (§C.17). The response header names the script's own call frame (`price_report()`); the module qualifier is the *address*, not part of the frame: ``` OK script price_report(): 1 print print widget price = 500 ``` ### C.19 String slicing, search, and replace (§5.2, §5.3, §8.6) ``` # string-ops.dpy — char access, slicing, search, tests, case, and trimming. def string_ops(): email = " Merlin@Langsyn.org " trimmed = email.strip() at = trimmed.find("@") print("local = " + str(trimmed[:at]).lower()) print("domain = " + str(trimmed[at + 1:])) print("first char = " + str(trimmed[0])) print("length = " + str(trimmed.length)) print("upper = " + str(trimmed.upper())) print("masked = " + str(trimmed.replace("@", " at "))) print("is org = " + str(trimmed.endswith(".org"))) print("starts M = " + str(trimmed.startswith("Merlin"))) print("dots = " + str(trimmed.count("."))) print("has at = " + str(("@" in trimmed))) print("no spam = " + str(("spam" not in trimmed))) print("tidy = [" + str("**Merlin**".strip("*")) + "]") print("reversed = " + str(trimmed[::-1])) print("every 2nd = " + str(trimmed[::2])) print("last = " + str(trimmed[-1])) print("tld = " + str(trimmed[-3:])) print("digits only = " + str("12345".isdigit())) print("all caps = " + str(trimmed.isupper())) print("at index = " + str(trimmed.index("@"))) ``` Run it as a one-shot with `run` (Wire §4.2). --- ### C.20 Constructed lists, comprehensions, and split/join (§3.5.9, §5.1, §5.3, §8.6, §8.9) ``` # collections.dpy — list literals, indexing/slicing, membership, # comprehensions, and the split/join string bridge, all client-side. def collections(): nums = [3, 1, 4, 1, 5] print("nums = " + str(nums)) print("count = " + str(nums.length)) print("last = " + str(nums[-1])) head = nums[:2] print("head = " + str(head)) print("has 4 = " + str((4 in nums))) evens = [n for n in nums if n % 2 == 0] print("evens = " + str(evens)) words = "merlin,are,langsyn".split(",") print("words = " + str(words)) caps = [w.upper() for w in words] print("joined = " + str(" ".join(caps))) print("same = " + str(([1, 2] == [1, 2]))) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script collections(): 9 prints print nums = [3, 1, 4, 1, 5] print count = 5 print last = 5 print head = [3, 1] print has 4 = True print evens = [4] print words = ['merlin', 'are', 'langsyn'] print joined = MERLIN ARE LANGSYN print same = True ``` ### C.21 Tuples, dicts, and sets (§3.5.11, §3.5.12, §3.5.13, §5.1, §5.3, §8.1, §8.6) ``` # collections2.dpy — tuple, dict, and set literals with their reads, # all client-side. def collections2(): point = (3, 4) print("point = " + str(point)) print("x = " + str(point[0])) ages = {"ana": 30, "bo": 25} print("ages = " + str(ages)) print("ana = " + str(ages["ana"])) print("has bo = " + str(("bo" in ages))) print("same = " + str((ages == {"bo": 25, "ana": 30}))) print("names = " + str(ages.keys())) tags = {"red", "green", "red", "blue"} print("tags = " + str(tags)) print("size = " + str(tags.length)) warm = {"red", "orange"} print("shared = " + str(tags.intersection(warm))) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script collections2(): 10 prints print point = (3, 4) print x = 3 print ages = {'ana': 30, 'bo': 25} print ana = 30 print has bo = True print same = True print names = ['ana', 'bo'] print tags = {'blue', 'green', 'red'} print size = 3 print shared = {'red'} ``` ### C.22 Dict and set comprehensions (§8.9) ``` # comprehensions2.dpy — build a dict and a set by bounded iteration. def comprehensions2(): nums = [1, 2, 3, 4] squares = {n: n * n for n in nums} print("squares = " + str(squares)) parity = {n % 2 for n in nums} print("parity = " + str(parity)) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script comprehensions2(): 2 prints print squares = {1: 1, 2: 4, 3: 9, 4: 16} print parity = {0, 1} ``` ### C.23 zip, enumerate, and partition (§8.6) ``` # zipping.dpy — pair collections into tuples, and split a string once. def zipping(): names = ["ana", "bo"] scores = [90, 85] paired = zip(names, scores) print("paired = " + str(paired)) ranked = enumerate(names) print("ranked = " + str(ranked)) parts = "user@example.com".partition("@") print("parts = " + str(parts)) print("domain = " + str(parts[2])) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script zipping(): 4 prints print paired = [('ana', 90), ('bo', 85)] print ranked = [(0, 'ana'), (1, 'bo')] print parts = ('user', '@', 'example.com') print domain = example.com ``` ### C.24 Value scripts and value-calls (§4.2, §4.4, §9.2.8) ``` # value-scripts.dpy — value-returning scripts compose by expression: one is # nested inside another's arguments, and a branch-covered value script returns # a string on every path. def doubled(n: int) -> int: return n * 2 def summed(a: int, b: int) -> int: return a + b def classify(n: int) -> string: if n > 100: return "big" else: return "small" def value_scripts(): total = summed(doubled(10), doubled(11)) print("total = " + str(total)) print("nested = " + str(doubled(doubled(5)))) print("size = " + str(classify(total))) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script value_scripts(): 3 prints print total = 42 print nested = 20 print size = small ``` ### C.25 Inheritance, override, super, dispatch, and isinstance (§13.8, §13.9) ``` # inheritance.dpy — a subclass extends a base, overrides a method and calls # super, dispatches polymorphically through a base-typed parameter, and tests an # instance's class with isinstance and a class match. class Animal: sound: string def speak(self): remember(self.sound, "generic", "op1") def describe(self) -> string: return "an-animal" class Dog(Animal): breed: string def speak(self): super().speak() remember(self.breed, "collie", "op1") def describe(self) -> string: return "a-dog" class Cat(Animal): def describe(self) -> string: return "a-cat" def label(a: Animal): print("desc=" + str(a.describe())) def inheritance(): animals = [Dog("d1"), Cat("c1")] for a in animals: label(a) d = Dog("d2") d.speak() br = d.breed match br: case active_claim: print("breed=" + str(br.value)) case empty: print("breed=?") print("is-animal=" + str(isinstance(d, Animal))) c = Cat("c2") match c: case Dog: print("class=dog") case Cat: print("class=cat") case default: print("class=other") ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script inheritance(): 2 claims written, 5 prints print desc=a-dog print desc=a-cat remember Dog.d2.sound = "generic" remember Dog.d2.breed = "collie" print breed=collie print is-animal=True print class=cat ``` --- ### C.26 Temporal canonical form, equality, and ordering (§3.5.5, §3.5.6, §8.1) ``` # temporal.dpy — datetimes and durations read back canonical, compare by value # rather than by spelling, and order (chronologically for instants, by length for # spans). `PT90M` and `PT1H30M` denote one span, so neither is shorter. def temporal(): start = datetime("2026-01-02T03:04:05Z") end = datetime("2026-01-02T03:04:05.500Z") short = duration("PT90M") same = duration("PT1H30M") longer = duration("PT2H") print("end-canonical=" + str(end)) print("span-canonical=" + str(short)) print("earlier=" + str(start < end)) print("same-span=" + str(short == same)) print("neither-shorter=" + str(short < same)) print("shorter-than=" + str(short < longer)) print("ordered=" + str(sorted([longer, short]))) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script temporal(): 7 prints print end-canonical=2026-01-02T03:04:05.5Z print span-canonical=PT1H30M print earlier=True print same-span=True print neither-shorter=False print shorter-than=True print ordered=[PT1H30M, PT2H] ``` --- ### C.27 Temporal arithmetic (§3.5.5, §3.5.6, §8.3) ``` # temporal-math.dpy — shift an instant by a length, measure the length between # two instants, and scale a length. Subtracting forwards from backwards gives a # negative span, and a shift respects the calendar. def temporal_math(): start = datetime("2026-01-02T09:00:00Z") shift = duration("PT7H30M") finish = start + shift print("finish=" + str(finish)) print("elapsed=" + str(finish - start)) print("double=" + str(shift * 2)) print("back=" + str(start - finish)) print("leap=" + str(datetime("2024-02-28T12:00:00Z") + duration("P1D"))) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script temporal_math(): 5 prints print finish=2026-01-02T16:30:00Z print elapsed=PT7H30M print double=PT15H print back=-PT7H30M print leap=2024-02-29T12:00:00Z ``` ### C.28 Quotient and remainder, and reading backwards (§8.3, §8.6) ``` # quotient.dpy — split a division into its quotient and remainder in one call, # and walk a collection backwards. Both halves of divmod floor together, so a # negative dividend keeps the remainder positive. def quotient(): print("even = " + str(divmod(9, 3))) print("odd = " + str(divmod(7, 2))) print("negative = " + str(divmod(-7, 2))) minutes = 135 hm = divmod(minutes, 60) print("duration = " + str(hm[0]) + "h" + str(hm[1]) + "m") print("countdown = " + str(reversed([1, 2, 3]))) print("backwards = " + str(reversed("stressed"))) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script quotient(): 6 prints print even = (3, 0) print odd = (3, 1) print negative = (-4, 1) print duration = 2h15m print countdown = [3, 2, 1] print backwards = ['d', 'e', 's', 's', 'e', 'r', 't', 's'] ``` ### C.29 Type conversions and the spelling of a rendered bool (§8.13) ``` # conversions.dpy — every conversion §8.13 defines, in one script. The first # line is the one worth reading twice: a bool renders `True`/`False`, the # Python spelling, not the lowercase token the engine stores it under. def conversions(): print("bool = " + str(True) + " " + str(False)) print("int = " + str(int(3.9)) + " " + str(int(-3.9)) + " " + str(int(True)) + " " + str(int(" -7 "))) print("float = " + str(float(1)) + " " + str(float("2.5")) + " " + str(float(True))) print("str = " + str(42) + " " + str(2.5)) print("roundtrip = " + str(bool(str(True) == "True"))) ``` Running it as a one-shot with `run` (Wire §4.2) produces: ``` OK script conversions(): 5 prints print bool = True False print int = 3 -3 1 -7 print float = 1.0 2.5 1.0 print str = 42 2.5 print roundtrip = True ``` --- ## Appendix D — Glossary - **DKE** — the service that compiles and executes DKE Python. The target of DKE Python programs in production deployments at `dke.langsyn.net`. - **Canonical verb surface** — the wire-public verb vocabulary published with DKE; the in-language verbs in §7.1 are drawn from it. - **Class** — a declared grouping of typed fields and the methods that operate on them (§13.1); it takes no marker. - **Instance** — a typed handle to one named member of a class, written `Class(subject)` (§13.2). - **Method** — a `def` in a class body with an explicit `self` receiver; void or value-returning, resolved by static dispatch (§13.4). - **Class match** — a `match` whose scrutinee is a bare instance variable and whose cases name classes; closed and exhaustive (§13.5). - **Module** — a `.dpy` source file, whose body of declarations and statements runs once when the module is compiled or imported (Reference §9.1); a module is a namespace for the names it introduces (Reference §9.6). - **Compile** — the service-surface operation (Wire §4.1) that submits a module: it stores the module under a name and runs its body, so its scripts become callable by name. - **Import** — the in-language operation that loads an already-stored module by name, running its body and making its names available under its namespace (Reference §9.3). - **Run** — the service-surface operation (Wire §4.2) that executes a program and returns a transcript, either an inline `source` one-shot (not stored) or an already-stored script by name. - **Slot grammar** — the dotted-path notation `K.s.a` for addressing a store cell by kind, subject, and attribute. - **Discriminator type** — a type whose values carry a `.kind` string naming which case a `match` would dispatch to. - **Finite collection** — a type whose values have a determinable `.length` and whose `for … in` iteration runs that many times. - **Refuse** — a recoverable runtime outcome of a verb call, recoverable in source via `except refuse`. - **Engine error** — a runtime outcome from the target service layer, recoverable in source via `except engine_error`. - **Bounded termination** — the family-wide termination guarantee: bounded iteration over finite sets with no recursion (also called *bounded-terminating*). --- **End of DKE Python Spec (alpha · API 1).**