DKE Python — Language Specification

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 — 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 — 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 <expr>: with case <discriminator>: arms (where the base member uses when).
• try / except. Handled blocks use Python’s except <kind> [as <var>]: shape; the as <var> 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.

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

• 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

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)
                | <any string-char escape>   # 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

"long text "
"split over lines"     # same value as "long text split over lines"
"a" "b" "c"            # same value as "abc"

message = (
    f"hello {name} "
    "and welcome"
)

banner = """usage:
  run <name>"""            # 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

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

bool-literal := 'True' | 'False'

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

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

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

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 | '+' | '/' | '='

list-literal := '[' ( expr ( ',' expr )* ','? )? ']'

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

tuple-literal := '(' ( expr ( ',' expr )* ','? )? ')'

dict-literal := '{' ( expr ':' expr ( ',' expr ':' expr )* ','? )? '}'

set-literal := '{' expr ( ',' expr )* ','? '}'

scientific-literal := 'scientific' '(' '"' scientific-numeral '"' ')'
scientific-numeral := '-'? mantissa ( 'e' | 'E' ) '-'? dec-digit+
mantissa           := dec-digit+ ( '.' dec-digit+ )?    # a nonzero magnitude

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

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.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    := 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<T>, set<T>, dict<K, V>, or tuple<T, ...>, nestable (e.g. dict<string, list<int>>). 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 <expr> 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<int>, -> dict<string, int>, …); an empty-list return [] satisfies any concrete -> list<T>. 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<T, ...> (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<T, ...> — 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 <topic> 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 <expr> 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 <expr> 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 <name> 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 <module>) 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 <a> <b> 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 returns, 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)).

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.1 The base types

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<T>). 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<int>, ["a", "b"] a list<string>, [[1], [2]] a list<list<int>>. list<T> 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<T>; a literal mixing scalar value classes is a list<value>; the empty list is list<unknown> until context fixes T. An empty list<unknown> is compatible with any list<T>: 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<list<int>>), 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<T> 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<T>:

• tuple<T1, …, TN> — a fixed-length heterogeneous sequence built by a tuple literal (§3.5.11): (1, "a") is a tuple<int, string>. 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<T, ...> — 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<K, V> — 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<T> — 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<T>, 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 <value>.<field> is well-typed when the table below has a row for the value’s type and field; otherwise it is a type_error. <value> 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.)

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:

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

• <expr>.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.
• <expr>.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 <value>[<int>] selects one element. It is well-typed when the value is a finite collection or a string; the result type is:

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 <int> 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<T> (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 <string>[<start>:<end>] returns the substring from character position <start> up to (but not including) position <end>. Both bounds are optional: s[<start>:] runs to the end of the string, s[:<end>] 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<T> (result list<T> — 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 — <string>[<start>:<end>:<step>]. The step (an int, default 1) selects every <step>-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 <start> to the beginning and <end> to the end, while a negative step defaults <start> to the last character and <end> 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<T> 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<T>. 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<T> — the idiom behind starred unpacking.

String methods. A string value carries these built-in methods:

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<string> (§5.1) and join consumes one; join’s argument MUST be a list<string> (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 <name>, §9.2), carrying a discriminator type the user cannot write as a type annotation. When a handler omits as <name> 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 <ExcType>(…) (§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<T>, set<T>, dict<K, V>, tuple<T, ...> — 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 <class> as <var>: arm that binds <var> 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 <var> to it is a type_error (an absent value has no content to bind).

• Render it directly. A value is expressible: print(<value>) 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.1 Scoping

DKE Python is lexically, function-scoped for variables. An assignment x = <expr> 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):

class Box:
    label: string

def put(id: string, label: string):
    remember(Box.id.label, label, "op")   # rejected: `label` is both

def put(id: string, text: string):
    remember(Box.id.label, text, "op")    # writes Box.<id>.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.<s>.<field> and, where the bare name resolves to it (Reference §9.6), Class.<s>.<field> 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:

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 <class> as <var>: 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 <var> 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 <expr>: statement MUST have <expr> of a finite collection type (claim_list, proof_tree, string_list, subject_set, result_type_set, diagnosis, or a constructed list<T>, set<T>, or dict<K, V>) 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 = <expr> 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.<rest> 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 <name>(<args>) 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 <expr> 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.1 The in-language verbs

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 <module>.<Kind> — 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.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.1 Comparison

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 datetimes, two durations, 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<int> == list<real> 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<unknown> 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<T> 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 <var> in <set>: 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<string, int> == dict<string, real>) 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

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

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 durations 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 datetimes 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<T> * int yields a list<T>. 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<int, int> when both are int, tuple<real, real> 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=<value> 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:

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<int> + list<int> → list<int>), two lists of differing scalar element types box into list<value> ([1] + [3.5] → list<value>), and an empty operand takes the other side ([] + [1] → list<int>); 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<int, string> + tuple<bool> is tuple<int, string, bool>. 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<int>). 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<string>) and sep.join (a list<string> → string), and the collection-returning methods s.partition / s.rpartition (→ tuple<string, string, string>, splitting once at the first / last occurrence of the separator) and s.splitlines (→ list<string>, splitting at line boundaries) (§5.3). A constructed list<T> (§5.1) is indexed (xs[i], negative from-end permitted) and sliced (xs[a:b:c], yielding a new list<T>) 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<K, V> (§5.1) is projected with d.keys() (→ list<K>), d.values() (→ list<V>), and d.items() (→ list<tuple<K, V>>), 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<T> 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<T>. Two builtin functions pair collections into tuples: zip(a, b, …) → list<tuple<…>> pairs elements position by position up to the shortest input, and enumerate(xs [, start]) → list<tuple<int, T>> 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=<bool>]) returns a new list<T> 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<T> 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(<expr>)

Appends output to the script’s transcript. print is written as a call — print("temp=" + str(t.value)). Evaluates <expr> 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<T>, or any discriminator type. A constructed list<T> 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 <source> (any finite collection type, a constructed list/set/dict, or a string — by character, §6.3), binds each element to <var>, evaluates the optional <cond> (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 <result> → list<T> (T the type of <result>); a set comprehension collects <result> → set<T>, removing duplicates and sorting (the <result> must be hashable — a scalar or a tuple of hashables); a dict comprehension maps <key> : <value> → dict<K, V> in insertion order, last value winning on a repeated key (<key> must be hashable the same way). <result> (and <value>) 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 <result> (and a dict’s <value>) is evaluated only in the innermost scope. A later clause’s <source> 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 <var> of each clause is comprehension-local: it is in scope within the clauses to its right, the <cond>s, <result> (and a dict comprehension’s <value>), may shadow an outer or earlier binding of the same name, and does not leak to the enclosing scope. A list comprehension whose <result> is itself a comprehension nests naturally ([[y for y in row] for row in grid] is a list<list<T>>).

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<int>
uniq    = {n % 2 for n in nums}                 # set   → set<int> (deduped, sorted)
squares = {n: n * n for n in nums}              # dict  → dict<int, int>
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<value>
shouted = [w.upper() for w in text.split(" ")]  # compose with split → list<string>

The <source> 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 = <expr>) 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 = <expr> (or a, (b, c) = <expr>, 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<T>, 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 <iter>:) 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 = <expr> binds every target on the left to the one value of <expr>, 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:

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

• 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<T> 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<tuple<K, V>> is a type_error.

• tuple(x) collects the elements into a variadic homogeneous tuple tuple<T, ...> — a tuple of runtime length whose every element is T. Unlike a fixed tuple<T1, …, Tn> (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.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

for x in <iter>:
    S
else:
    Se

try:
    S
except refuse as r:
    Sr
except engine_error as e:
    Se
else:
    So
finally:
    Sf

with branch("<name>"):
    S

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 <name>(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.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).
• <value>.<field> 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

<class> <file>:<line>:<col>: <message>

where <class> is parse_error or type_error. The text after <class> is quality-of-implementation; a third-party tool MAY choose any format.

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.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 <claim>.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 <module> 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.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, <value>, <source>) 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 <expr> or a sequence of local name = <expr> bindings followed by a tail return <expr> 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 <Class>: 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().<name>(args) runs the base class’s version of <name> 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 <Class>: 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.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:

@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 (<field>__none<N>, numbered from 1 in the order the none(...) premises are written) — a rule concluding f.safe records f.safe__none1. It is 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:

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:

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 updateing or forgetting 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 <name>

Removes one standing rule and everything it derived. <name> 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:

Kinds are named in the addressable form (<module>.<Kind> 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:

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

Removes one standing constraint. <name> 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.1 Supposing a fact away

suppose_absent(<field>, …, <field>) 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 <field> 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 <field> 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.

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