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 customer 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 MCP Reference — 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 modules chapter of the Python Reference — 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 the DKE Python — Language Specification, version V, changed in rev R, at alpha · API 1.5 · rev N, as the Version line above states it: this document’s own version, which moves only when its text does, and the revision it last changed in; then the release it belongs to, an alpha release describing API version 1.2, at revision N — one number for the whole published surface, which every document, the web pages and the service wire state and which moves whenever any of them changes. §11.1 says what each promises, and Appendix E records the version and revision at which this document changed. 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).
• match / case. Discrimination is spelled match <expr>: with case <discriminator>: arms. One arm may name ALTERNATIVES, separated by | — case int | string: — and may carry a guard, case int as n if n > 0: (§6.2).
• 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) — a program reaches a stored script by importing its module and calling it qualified (MCP Reference §4.2, Python 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 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. A line feed (U+000A), a carriage return (U+000D) and the carriage-return / line-feed pair each end a source line; the pair ends one line, not two. Every line ending reads as a line feed, including inside a triple-quoted string, so a program means the same whichever of the three its file uses. 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 form feed (U+000C) is whitespace between tokens, as a space is. In a line’s indentation it is not counted: it sets the count back to zero, so only the spaces after it count. A line holding four spaces after a form feed is indented four, as CPython reads it, and a line holding a form feed after four spaces is not indented.
• 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.
• Only a header’s : opens a block, so a line indented deeper below a line that does not end in one is a parse_error, “unexpected indent”. It is answered where CPython answers it: at the line’s first token, with that token’s column counted from zero. The two lines x = 1 and y = 2 are a parse_error at line 2, column 4. A line holding only a \ after its indentation is answered on the line it continues onto.
• Blank lines and comment-only lines do not affect block structure.
• Inside (, [ or {, newlines are not significant: a bracketed expression may span lines.
• A trailing comma may follow the last item of a comma-separated list written inside (, [ or {: the arguments of a call (to a script, a builtin, a method, a verb or a class), the parameters of a def or a method, the base of a class, the elements of a literal (§3.5.9, §3.5.11–§3.5.13) and the elements of a sequence or mapping pattern (§6.2). It means nothing: f(1, 2,) is f(1, 2), so a list written one item per line may end every line with a comma. It never stands for an item. f(,), f(1,,2), [,] and [1,,2] are parse_errors, and f(1,) passes one argument. A subscript’s comma makes a tuple, as in Python. In two bracketed forms the comma makes a tuple of one: in a subscript, where d[1,] is d[(1,)] (§4.4), so xs[0,] is a type_error on a list, which is indexed by an int; and in (e,), rather than a parenthesized e (§3.5.11). The target list of a for header or a comprehension clause is not bracketed and takes one too: for a, b, in xs: is for a, b in xs:, and in for a, in xs: the comma makes a target list of one (§8.11), as it does in a, = t.
• A backslash immediately before a line ending 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, answered one past the \, where CPython answers it: x = 1 \ y is a parse_error at column 8. So is a \ the source ends after, with or without its line ending, since there is no line for it to join: it is refused one past the \, as CPython refuses it. Inside a bracket the bracket left open is the answer instead (§10.1).

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.

One comment is also read: a source’s first line, when it opens # dke:, is the source’s declaration of what it is written in (§3.9.1). It remains a comment, and changes nothing the program means.

3.4 Identifiers

DKE Python identifiers follow Unicode UAX #31 with the standard profile, as Python’s do:

identifier := XID_Start XID_Continue*     # read in NFKC

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 read in Normalization Form KC, as Python reads it, so every spelling of one form is one name. ｘ (U+FF58) is the name x, fi is fi, and e followed by U+0301 is é, so Ｃat and Cat are one class and one kind. Where the form does not compose, the marks are part of the name: بِسْم and बिल्ली carry their vowel marks, and U+0958 is read as क followed by the nukta U+093C. Whether a mark composes can depend on the letter before it: ا followed by U+0654 is أ, while the same U+0654 after a letter it does not compose with stays in the name.

A keyword is compared as it is written, before a name is read, as in Python. So ｉｆ = 1 binds the name if, and print(ｉｆ) reads it. A word this language reads only where its form stands is compared the same way, so ｍatch does not begin a match. The name of a built-in function is read like any other: ｐｒｉｎｔ("p") calls print.

A name that keeps a combining mark from U+0300 to U+036F with no letter to compose into, as x followed by U+0301 does, may name a local, a parameter or an alias. It cannot name what a store holds. A class, a field, a method, a script, a rule or a constraint so named is a parse_error naming the mark, and a kind, a subject or an attribute written so in a path is a refuse naming it at run time. A module’s name is what import reads: ｍ9 is refused, and the refusal says to write m9.

A string is not read, as Python’s getattr does not read one. A variable holding "ｘ" addresses ｘ where the path K.ｘ.v addresses K.x.v, and a script sent to the service by name is found under the name it reads as: ok9.f, never ok9.ｆ.

Two limits stand where Python answers otherwise. Ｔｒｕｅ, Ｆａｌｓｅ and Ｎｏｎｅ are names a program may bind, and where it has not, they are names nothing binds, told name 'True' is not defined, where Python finds its constants. A name does not contain U+00B7, U+0387, U+013F or U+0140, the code points CPython continues a name with; each is refused wherever a name would hold it, as an unexpected character that the message names by its code point.

Identifiers are case-sensitive: Cat, cat, and CAT are distinct. As kinds in one store they cannot all be held: a store holds one kind of any names that differ only in the case of a letter A to Z, and a write that would make another is refused naming the kind held, with nothing written. Letters beyond A to Z are not compared this way, so Øy and øy are two kinds.

3.5 Literals

string-literal := '"' string-char* '"'
                | '"""' triple-char* '"""'   # triple-quoted (may span lines)
                | raw-prefix '"' raw-char* '"'             # raw
                | raw-prefix '"""' raw-triple-char* '"""'  # raw, triple-quoted
raw-prefix     := 'r' | 'R'
raw-char       := <any UTF-8 codepoint except '"', '\' and a line feed>
                | '\' <any UTF-8 codepoint>   # both kept: the backslash escapes nothing
raw-triple-char := <any UTF-8 codepoint except '\' and the closing '"""'>
                | '\' <any UTF-8 codepoint>
triple-char    := <any UTF-8 codepoint except '\' and the closing '"""'>
                | <a line feed, U+000A>      # written as itself, not escaped
                | string-escape              # the escapes of string-char
string-char    := <any UTF-8 codepoint except '"', '\' and a line feed>
                | string-escape
string-escape  := '\\'                   # backslash
                | '\"'                   # double quote
                | '\' <a single quote>   # single 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 codepoint <= U+00FF, 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
                | '\' octal octal? octal?   # one codepoint, up to three octal digits
                | '\' <a line feed>      # nothing: the string goes on at the next line
                | '\' <any other character>   # both kept: the backslash escapes nothing
octal          := '0'..'7'
hex            := '0'..'9' | 'a'..'f' | 'A'..'F'
name           := ( 'A'..'Z' | 'a'..'z' | '0'..'9' | ' ' | '-' )+   # a Unicode character name, matched case-insensitively

"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 )*
dec-digit   := '0'..'9'
oct-digit   := '0'..'7'
bin-digit   := '0' | '1'

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

def blob_slice(b, start, stop, step):
    return b[start:stop:step]


def blob_join(b1, b2):
    return b1 + b2


def blob_byte(b, i):
    return b[i]

list-literal := '[' ( display-item ( ',' display-item )* ','? )? ']'
display-item := expr | '*' bitor-expr        # an element, or a spread (§8.15)

fstring-literal := fstring-prefix '"' ( fstring-char | replacement-field )* '"'
fstring-prefix  := 'f' | 'F'
                 | raw-prefix ( 'f' | 'F' ) | ( 'f' | 'F' ) raw-prefix   # raw, §3.5.1
fstring-char    := string-char (§3.5.1)   #  '{{' and '}}' denote literal '{' and '}'
replacement-field := '{' expr '='? ( '!' ('r' | 's') )? ( ':' format-spec )? '}'
format-spec       := ( fill? align )? sign? 'z'? '#'? '0'? width? grouping? ( '.' precision )? format-type?  # §8.13
fill              := <any one character>
align             := '<' | '>' | '^' | '='
sign              := '+' | '-' | ' '
width             := dec-digit+
grouping          := ',' | '_'
precision         := dec-digit+
format-type       := 's' | 'd' | 'x' | 'X' | 'o' | 'b' | 'c' | 'n'
                   | 'e' | 'E' | 'f' | 'F' | 'g' | 'G' | '%'

tuple-literal := '(' ( display-item ( ',' display-item )* ','? )? ')'   # a `*` item alone needs its comma (§8.15)

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

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

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

imag-literal := ( dec-int | real-literal ) ( 'j' | 'J' )

3.6 Operators and punctuation

( ) [ ]   . , : =
== != < > <= >=
+ - * / // % **
| & ^ << >> ~

The tokens |, & and ^ are the bitwise operators on two integers and the set operators on two sets (§8.3, §8.6), and | also separates the alternatives of a case label (§6.2). << and >> are the shifts, and the prefix ~ is bitwise inversion (§8.3). A @ that begins its line begins the decorator of a rule or a constraint. After anything on its line it is Python’s matrix product, which reads and which no value here answers (§8.3). 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. A newline or a ; ends a simple statement (§3.2, §4.3). 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, class, method and field names, parameter names, loop variables, handler bindings, assignment and unpack targets, and names a case pattern binds). They are Python 3.11’s keywords and the absence word null (§3.5.4). A conforming implementation MUST treat every one of them as reserved at the lexical level.

and        as         assert     async
await      break      class      continue
def        del        elif       else
except     False      finally    for
from       global     if         import
in         is         lambda     None
nonlocal   not        null       or
pass       raise      return     True
try        while      with       yield

This list is complete; no other word is reserved. Every keyword Python 3.11 reserves is in it. Compiling a module, forgetting a script and reading a script’s metadata are wire operations (MCP Reference §9.2), not statements of a program body.

This language’s own words are names. The head-words of the built-in verb surface (§7), match, case, branch, commit, rollback and script are ordinary names, as they are in Python, wherever the form each heads does not stand. A verb’s word is the verb immediately before its (. match heads a match statement at the head of a line that ends in :, and case an arm at the head of a line in that statement’s block. commit and rollback are the statement alone on a line or after a : or ;, and branch is the context manager before its (. So get = 1, def f(match: int):, case = 2, import list and xs.case(1) are all read as Python reads them. A def, a class or an import at the top level of a unit takes the word for the whole unit, so a call of it is a call of what the unit declares.

After a ., an identifier-shaped token is parsed as a field name; whether the field is meaningful for the base type is decided by the typechecker (§6). A word in the list above, which CPython reserves too — if, class, True, None and the rest of its keywords — names no field, method or path segment, as CPython’s grammar reads only a name after a .: xs.if, g(xs).class and remember(K.s.class, 1, "op") are parse_errors at the word (§10.1), and so is such a word beginning a path, current(class.s.a), bar lambda, which begins a lambda there as it does in Python and is answered where its header stops (§8.8). A kind, subject or attribute spelled as one is still addressed, through a string name that holds it (§6.7): k = "class", then remember(K.s.k, 1, "op"). 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

The typed values of §3.5.5–§3.5.8 and §3.5.14 — datetime("…"), duration("…"), blob("…") / blob_b64("…") and scientific("…") — have no token class of their own: each lexes as an IDENT, punctuation and a STRING, and becomes a literal in the grammar (§4).

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 by the language parameter supplied when a source is submitted. When the parameter is omitted, the language is the one the source declares (§3.9.1), and when it declares none, English (eng).

eng is the default. The parameter’s accepted values belong to the wire contract and are listed in the MCP Reference; a value outside that set is declined before the source is compiled.

This specification describes the English surface. Every keyword, verb and rendered response given here is the eng spelling.

The natural language is a property of how you are talking to the service, set per call, and the call decides it. A source may say what it was written in, so that a file read later carries that with it; the call is checked against what it says (§3.9.1), and it never decides in the call’s place.

# dke: edition=python.1 language=eng.1
def hello():
    print("written in English, at API 1")

declaration   := '#' decl-blank* 'dke:' decl-blank* decl-setting decl-blank+ decl-setting decl-blank*
decl-setting  := decl-key '=' decl-name ('.' decl-version)?
decl-key      := 'edition' | 'language'
decl-name     := ('a'..'z')+
decl-version  := ('1'..'9') ('0'..'9')*
decl-blank    := ' ' | <a tab>

4.1 Programs

source       := option-verb NEWLINE | module-body
module-body  := docstring? top-item+
docstring    := STRING NEWLINE                           # documents what it opens; nothing runs it
top-item     := decl | class-decl | rule-decl            # decl §4.2, class-decl §13.1, rule-decl §14
              | constraint-decl                          # constraint-decl §14.10
              | import-stmt | stmt                       # import-stmt §4.3, stmt §4.3 (incl. the four writes) — see Modules
option-verb  := '--' IDENT IDENT?

A source is the module body (Python Reference §9.1) from its first line. Its body admits, at the top level, not only declarations but also import statements (Python Reference §9.3), data declarations (write statements at module scope, Python 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 (Python Reference §9.1); a file whose body is exactly one def is the common single-script case. Because it runs again on every import, a module’s top level writes each cell once per source and period: a second write to one cell from one source over an overlapping window refuses (Python Reference §9.5).

The natural language the source is written in — the language of the knowledge it names and of its authored text — is set by the call’s language parameter, which the source’s first-line declaration may supply (§3.9.1); it also selects the language in which the script’s own structured output — its invocation transcript (MCP Reference §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. A declaration may call any other declaration of the same unit, above or below it, or an already-stored script, as long as no call leads back to its caller (§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 (Python Reference §9.1, §9.7).

A unit with an empty body — whitespace and comments only — is a parse_error.

A docstring is a string literal alone on the first line of a module, a class body (§13.1) or a def body (§4.2). It documents what it opens and is not a statement: nothing runs it, and a unit compiles exactly as it would with a comment in its place. A def whose body is only a docstring does nothing, as a body of pass does, and a module that holds only a docstring is still empty. A string standing alone anywhere else is an expression statement (§4.3).

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? ')' ( '->' return-type )? ':' NEWLINE INDENT ( docstring stmt* | stmt+ ) DEDENT
return-type := type | 'value' | 'None'              # `value`: a store fold's result, narrowed by the caller (§4.2); `None`: what no annotation says
params    := param-item ( ',' param-item )*             # which lists are read: §4.2
param-item := param | var-param
           | '/'                                        # what stands before it takes no keyword (§4.2)
           | '*'                                        # what follows it takes no position (§4.2)
param     := IDENT ':' param-type ( '=' const-expr )?   # a default value
var-param := '*' IDENT ':' binding-type                  # variadic: surplus positionals → tuple<type, …>
const-expr := expr                                      # a literal, or an operation over literals
param-type := binding-type
            | module-name '.' IDENT                     # a class an imported module declares (§13.2)
binding-type := type
type    := type-name
         | IDENT                                   # a class name (§13.1), in EVERY type position (§5.5)
         | 'list' '<' type '>' | 'set' '<' type '>'
         | 'dict' '<' type ',' type '>' | 'tuple' '<' type ( ',' type )* '>'
         | 'iterator' '<' type '>'                                          # §8.6
         | 'dict_keys' '<' type '>' | 'dict_values' '<' type '>'           # dict views (§5.1)
         | 'dict_items' '<' type ',' type '>'
         | collection-word '[' type ( ',' type )* ( ',' '...' )? ']'       # any of them in CPython's brackets, the same type (§5.5)
type-name := scalar-name
           | 'active_claim' | 'claim_list' | 'proof_tree' | 'diagnosis'   # read-result types (§5.1)
           | 'subject_set' | 'string_list' | 'verify_result' | 'result_type_set'
           | 'slice'                                                       # a slice value (§5.3)
           | 'range'                                                       # a range of ints (§5.3)
scalar-name := 'string' | 'int' | 'bool'                                 # primitives
             | 'datetime' | 'duration' | 'real' | 'blob' | 'scientific'  # value-class scalars (§5.5)
             | 'complex'
             | 'str' | 'float'                                           # CPython's names for `string` and `real` (§5.5)
collection-word := 'list' | 'set' | 'dict' | 'tuple' | 'iterator'
                 | 'dict_keys' | 'dict_values' | 'dict_items'

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, complex), 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. A class crosses it both ways, as a collection does. A parameter may name a class and receives an instance of it, and a return type may name one too (§13.2). (empty and null name absence and are never parameter types.) The declared objects are called scripts (the wire addresses them as such, see MCP Reference §9.2).

One name space. A compile unit declares four kinds of named thing — a script, a standing rule (§14.1), a standing constraint (§14.10) and a class (§13.1) — and they share one name space: no two declarations in a unit may have the same name, whatever their kinds. A second declaration of a name the unit already holds is a type_error (§10.2), reported at that declaration’s name, and its diagnostic names the kind of the declaration holding the name. Python also binds a class and a function in one module name space, and rebinds a name declared twice; DKE Python refuses the second declaration instead.

Void scripts and value scripts. A script with no -> type whose body holds no return <expr> 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 return [], return set([]) or return {} satisfies any concrete -> list<T>, -> set<T> or -> dict<K, V>. A script with no -> type whose body holds a return <expr> is a value script too, of the type its returns give, and behaves as one written with that type, wherever its call stands. The wider of two types one of which fills the other is that type, so a return of an int and one of a real give real. Two returns of types neither of which fills the other are a type_error, and so is a path that ends with no value, and a return no type is known for, such as an element of a list bound empty, which is told so, annotated or not, and the annotation it takes is on that name. So is a body whose type waits on the type of a body that may call it back: writing -> <type> on either settles what is no cycle (§9.7). The return statement itself is specified in §4.3 and §9.2.8.

-> value. A value script may also declare -> value, as a value method may (§13.4): Python has one construct for both. It is the return type of a script that hands on a store fold’s result, such as m = max(K.attr), whose class is whatever the cells hold. The caller narrows it with match (§6.2), and so does a script that would rather promise a narrower type: -> int, then match m: and case int as n: and return n. Only an expression whose type is value fills a -> value return, so return 1 is a type_error (§6.4), as it is in a method.

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 or fill it (§6.4): a bool default is accepted for an int parameter, and either for a real one. 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 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. 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: a signature names every keyword a call may pass, which is what lets a misspelt keyword be refused where it is written rather than collected as data. Use explicit named parameters — with defaults where useful — or a dict parameter.

Positional-only and keyword-only parameters. A / makes the parameters before it positional-only, and a bare * or a variadic parameter makes the parameters after it keyword-only, as in Python: def f(a: int, /, b: int, *, c: int = 3) is called f(1, 2) or f(1, b=2, c=4). A keyword naming a positional-only parameter is told f() got some positional-only arguments passed as keyword arguments: 'a', and a positional argument that would reach a keyword-only one f() takes 2 positional arguments but 3 were given. A keyword-only parameter takes a default as any parameter does, and one with no default may follow one with a default. A spread (§8.15) fills only what a position may reach. Each marker stands at most once and in that order, as §10.1 says of a list Python would not read.

The listing of scripts writes each parameter list as it was written, markers included.

--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, declarations, statements, expressions, types, verbs, 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 ;, or a block statement (if / for / match / try / branch / world), whose body is a :-headed indented suite. Where this grammar writes that suite, the simple statements of one line may stand after the header’s : instead, as in Python: if a: b = 1; c = 2, def f(): pass, class C: x: int. A block statement does not stand there, nor after a ;.

stmt         := simple-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
              | rebind-stmt                                  # changes a collection, §8.14
              | del-stmt                                     # §8.14
              | 'pass'                                       # a no-op
              | '...'                                        # a no-op, as `pass` is
              | expr-list                                    # an expression statement: it runs, and nothing keeps its value
              | 'break'                                      # loop control, §9.2.7
              | 'continue'

block-stmt   := match-stmt
              | class-match                                  # dispatch by class, §13.5
              | for-stmt
              | if-stmt
              | try-stmt
              | branch-block
              | world-block                                  # §9.2.9

assign-stmt      := IDENT '=' expr-list
                  | IDENT ':' binding-type                     # an annotation with no value; it binds nothing
                  | IDENT ':' binding-type '=' expr-list       # annotated assignment; the type must agree with the initializer, and only a name takes one (§6.4)
                  | chain-target ( '=' chain-target )+ '=' expr-list  # chained assignment; every target binds one value, left to right (§8.12)
                  | IDENT aug-op expr-list                     # augmented assignment on a bare name; `x op= e` is `x op e`, changed in place on a list or set (a field names a source, so it uses `remember(...)`, not `op=`)
                  | top-target ( ',' top-target )+ '=' expr-list                # unpacking a tuple or list; nested targets + one optional `*rest` (§8.11)
                  | target-group '=' expr-list                                  # a parenthesised or bracketed target list (§8.11)
expr-list        := display-item ( ',' display-item )* ','?     # a bare comma-list; holding a comma, it is a tuple (§3.5.11); a `*` item alone is none (§8.15)
top-target       := unpack-target | '*' unpack-target                           # a target, or THE single starred target (≤ one per list), which may be any target
unpack-target    := IDENT | element-target | target-group      # a name, an element or a slice, or a nested target list, which may hold its own star
target-group     := '(' top-target ( ',' top-target )* ','? ')'   # in parentheses; one target alone in them is that target
                  | '[' top-target ( ',' top-target )* ','? ']'   # in brackets; `[a]` is a list of one target (§8.11)
                  | '(' ')' | '[' ']'                           # a list of no targets; the value must hold nothing (§8.11)
chain-target     := top-target ( ',' top-target )* ','?        # a target or a target list, as an assignment takes one (§8.12)
element-target   := write-target subscript                      # an element or a slice, written as an element write writes it (§8.14)
                  | postfix-expr subscript                      # an element of what an expression answers, which no name holds (§8.14)
aug-op           := '+=' | '-=' | '*=' | '/=' | '%=' | '//=' | '**=' | '|=' | '&=' | '^=' | '@='
rebind-stmt      := write-target '.' rebind-method '(' arg-list? ')'  # changes the collection the target reaches; a statement, never an expression (§8.14)
                  | write-target '.' answer-method '(' arg-list? ')'  # changes the collection and discards what the call answers; the call is an expression too (§8.14)
                  | postfix-expr '.' ( rebind-method | answer-method ) '(' arg-list? ')'  # the same, on what an expression answers, which no name holds (§8.14)
                  | element-target '=' expr-list                # an element or slice write; changes the collection the target reaches (§8.14)
                  | element-target aug-op expr-list             # `c[k] op= e` is `c[k] = c[k] op e`, the target and `k` evaluated once
write-target     := IDENT ( subscript | '.' IDENT '(' arg-list? ')' )*  # a bound name, then any chain of subscripts and method calls; what it reaches is the collection changed (§8.14)
subscript        := '[' expr ( ',' expr )* ','? ']'             # an index or a key; a comma makes it a tuple, `d[1, 2]` is `d[(1, 2)]` (§4.4)
                  | '[' expr? ':' expr? ( ':' expr? )? ']'      # a slice; only a list's is written (§8.14)
rebind-method    := 'append' | 'extend' | 'insert' | 'remove' | 'sort' | 'reverse' | 'clear' | 'add' | 'discard' | 'update'
answer-method    := 'pop' | 'setdefault' | 'popitem'           # changes the collection and answers a value (§8.14)
del-stmt         := 'del' write-target subscript                # removes one element, entry or slice from the collection the target reaches (§8.14)
                  | 'del' postfix-expr subscript                # an element of what an expression answers, which no name holds (§8.14)
                  | 'del' '(' element-target ')'                # in parentheses, that element (§8.14)
print-stmt       := 'print' '(' ( print-arg ( ',' print-arg )* )? ')'
print-arg        := expr                                       # a value to render
                  | '*' expr                                   # each element of a collection, as an argument of its own (§8.15)
                  | ( 'sep' | 'end' | 'flush' ) '=' expr       # a keyword, read after the arguments
                  | 'file' '=' 'None'                          # the default, which is the line itself
                  | '**' dict-literal                          # its keys as keywords, each key a literal (§8.15)
raise-stmt       := 'raise' ( ( EXC-NAME ( '(' ( expr ( ',' expr )* ','? )? ')' )? | IDENT ) ( 'from' expr )? )?        # a catchable refuse; any other value after `raise` is read as a raise and is a parse_error at the value (§4.3)
assert-stmt      := 'assert' expr ( ',' expr )?                # Python assertion (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' import-item ( ',' import-item )*   # load each module, Python Reference §9.3; `math` and `cmath` name the built-in namespaces, §8.16, `vector` one more, §8.17, and `struct` one more, §8.18
                  | 'from' IDENT 'import' import-names         # bind names a module declares
                  | 'from' IDENT 'import' '(' import-names ','? ')'
import-names     := import-name ( ',' import-name )*
import-name      := IDENT ( 'as' IDENT )?                      # bind the name, or bind it as the name after `as`
import-item      := module-name ( 'as' IDENT )?                # bind the module, or bind it as the name after `as`
module-name      := IDENT ( '.' IDENT )*
return-stmt      := 'return' expr-list?                        # early exit / value, §9.2.8

match-stmt   := 'match' expr-list ':' NEWLINE INDENT case-clause+ DEDENT   # two or more items, or one and a comma, are the tuple written without its parentheses (§3.5.11), as CPython reads a subject
case-clause  := 'case' class-label ( 'if' expr )? ':' arm-body            # §6.2
              | 'case' elem-pattern ( 'if' expr )? ':' arm-body           # structural: an alternative is a `pattern`, §6.2
              | 'case' value-pattern ( 'if' expr )? ':' arm-body          # value patterns, §6.2
              | 'case' 'default' ':' arm-body                             # never guarded, §6.2
class-label  := IDENT ( '|' IDENT )*                    # alternatives, §6.2
              | IDENT 'as' IDENT                        # `as` binds ONE class, never across `|`
value-pattern := value-alt ( '|' value-alt )* ( 'as' IDENT )?
value-alt    := case-literal | '_' | IDENT | class-pattern   # IDENT: a capture, a name that is no
                                                       #   class label, and alone; `_` last
class-pattern := IDENT ( '.' IDENT )? '(' ( elem-pattern ( ',' elem-pattern )* ','? )? ')'   # a class tested, §6.2
case-literal := '-'? ( INT | REAL ) | STRING+ | 'True' | 'False'
              | '-'? IMAG | '-'? ( INT | REAL ) ( '+' | '-' ) IMAG      # a complex, §3.5.15
arm-body     := simple-stmt NEWLINE | NEWLINE INDENT stmt+ DEDENT
pattern      := seq-pattern | map-pattern               # a SHAPE label, §6.2
seq-pattern  := '[' ( elem-pattern ( ',' elem-pattern )* ( ',' '*' IDENT )?
                    | '*' IDENT )? ']'                  # a `*` MUST be last
map-pattern  := '{' ( case-literal ':' elem-pattern ( ',' case-literal ':' elem-pattern )* )? '}'
                                                       # no key named twice, §6.2
elem-pattern := elem-alt ( '|' elem-alt )* ( 'as' IDENT )?   # the same names bound by
                                                       #   each; only the last may match every
                                                       #   value; IDENT is not `_`
elem-alt     := IDENT | '_' | case-literal | pattern | class-pattern   # one per §6.2 element row, plus
                                                       #   `'*' IDENT` above, whose position
                                                       #   is constrained, and the `|` and the
                                                       #   `as` above
for-stmt     := 'for' top-target ( ',' top-target )* ','? 'in' expr ':' NEWLINE INDENT stmt+ DEDENT   # a target list unpacks each element — the SAME list an assignment takes (§8.11)
#            (an element target among them is written each iteration; `top-target` is defined with `assign-stmt` above)
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
world-block  := 'with' 'world' '(' expr ')' ':' NEWLINE INDENT stmt+ DEDENT   # `world` is a soft keyword here

arg-list     := arg ( ',' arg )*
arg          := expr                             # positional
              | '*' expr                         # a spread: each element a positional argument of its own (§8.15)
              | IDENT '=' expr                   # a keyword argument

# several statements on a line, and a body on its header's line
def tally(a: int, b: int):
    c = a + b; d = a - b;
    if c > d: print(c); print(d)

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 positional argument may not follow a keyword argument or a ** argument, and a * argument may not follow a ** argument. Each is a grammar error, as it is in Python, and is answered where Python answers it (§10.1). So is a * that no expression follows, written after another argument. 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, told in Python’s words and in its order: each keyword as written, a keyword no parameter takes, too many positional arguments, a positional parameter left unbound, then a keyword-only one. A method’s count holds its receiver, and it is named by the class whose body holds its def. A positional argument written *xs is a spread: each element of xs is a positional argument of its own, in its place. Where a spread’s length is known only as the program runs, or the call has a ** argument, or no type is known for what the statement reads, those errors are found as it runs (§8.15), and a line that does not run is told nothing.

A bare assignment (assign-stmt) binds one name to an expression result; 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 (MCP Reference §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). A builtin there, where no script of that name resolves, is an expression alone: it is evaluated and its value dropped, so len(xs) runs and next(e) reads an element and discards it, since reading changes the iterator.

An augmented assignment (IDENT aug-op expr) computes the plain form: x op= e is x op e, with x evaluated once, and binds it to x — except on a list or a set, below. 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. On a list, += and *= change the list the name holds in place to x + e or x * e (§8.4), and on a set |=, &=, -= and ^= change the set in place (§8.6), as Python’s do — so every other name holding that list or set sees the change (§8.14). On a number, a string or a tuple, which do not change, the name is bound to the new value and another name keeps the old one, as in Python.

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

An augmented operator after what Python does not augment — anything but a name, an attribute or a subscript, in any parentheses around it whole — is a parse_error where that target begins, as in Python, naming what it is: f() += 1 is a parse_error at column 1, “‘function call’ is an illegal expression for augmented assignment”, and (a, b) += 1 one naming a ‘tuple’. A comma, a : or a ** in a lambda‘s header is no part of what its bracket holds, so (lambda x, y: k) += 1 names the ’lambda’, at column 2, and {lambda: 1} += 1 a ‘set display’. Python reads the value after the operator before it answers, so a grammar error there is answered first: f() += a if b is a parse_error at column 8, a conditional with no else. The value need only begin, as 1 + does; where none begins, as in f() +=, the answer is at the operator, at column 5. A lambda begins one only where Python reads its header, so f() += lambda x=1 y: 1 is answered at the operator too. True, False and None are refused as the reserved words they are.

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. Outside a script return is refused, in Python’s words (§10.1). 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 or fill it (§6.4) — a bool satisfies a -> int return and either satisfies a -> real one. 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.

The subject of a match statement (match-stmt) is an expr-list: two or more items, or one item followed by a comma, are the tuple written without its parentheses (§3.5.11), so match d, e: is match (d, e): and a * item spreads into the tuple as it does in a parenthesized one. A * item alone is no tuple and no value, and is a parse_error at the : after it, as it is in CPython.

Each case arm of a match may be an inline statement or an indented suite; over a type with a case set the arms must be exhaustive (§6.2). A case label is one discriminator, or two or more separated by | — an alternation, matching if the scrutinee’s discriminator is any one of them (§6.2) — and may be followed by if <expr>, a guard the arm must also satisfy to be taken (§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), and only where that arm names a single class; elsewhere it is a type_error. The try handler clauses are optional and may appear in any order and any number, and where more than one handles the same category the first of them runs (§10). 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 (Python 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. An import naming a module the store does not hold fails when control reaches it, with no module named <module>. A program that uses such a module, or has a type_error below a top-level import of it, is refused when it is compiled, at that import, in the same words — as CPython stops at the import before reaching either (Python Reference §9.3).

from <module> import <name>, … loads the module as import <module> does and binds each named script or class, so a later area(2, 3) means geo.area(2, 3) and compiles to the same program. from is contextual too. A name the module does not declare is refused at the import, used or not, as CPython refuses it. Like import, it runs the module’s body each time control reaches it (Python Reference §9.3), where CPython runs a module once. Only the names are bound: <module>.<name> needs an import <module> of its own, as in CPython. A bound name holds one thing, so assigning to it, taking it as a parameter or a for target, declaring a script or class under it, or importing it from another module with from is refused; Python would rebind it. Naming it in an annotation, as in item: Site = b, uses it and binds nothing. A diagnostic names a bound script or class as the unit binds it, Site rather than geo.Site, so a form it offers compiles as written. import a, b loads each module in turn. as binds another name, so after import geo as g a use of g means geo, and after from geo import area as ar a use of ar means geo.area, each exactly as if the module’s name had been written; geo itself is not bound by either, as in Python. A name an import bound is refused if it is bound again to something else, since every later use already reads as the first. A wildcard (from m import *), a dotted module and a relative import are refused, each naming the form to write.

from __future__ import <feature>, … loads nothing and binds nothing. Python’s features are all accepted and change nothing here. It stands where Python requires it, at the top of a unit, with only a docstring and other such imports above it. Anywhere else, and for a feature Python does not know, it is refused in Python’s words (§10.1).

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. A positional argument written with * spreads a collection: each of its elements is an argument of its own, so print(*xs) writes the elements of xs joined by sep (§8.15). sep and end are optional keyword arguments, each any expression that gives a string, and are read after the positional arguments, in the order written. None written as the whole of either is its default. One that gives anything else is a catchable refuse (§10) when the line is composed, “sep must be None or a string, not int”. flush is read in its turn, may hold anything, and changes nothing. file may be given None alone, which is its default, the line itself; given anything else it is a parse_error. A keyword print does not take is a type_error in Python’s words, the first one written, 'x' is an invalid keyword argument for print(), followed by the keywords it takes. A ** before a dict display gives these keywords as its keys (§8.15): print("a", "b", **{"sep": "-"}) is print("a", "b", sep="-"). A ** before any other dict, such as a name that holds one, gives them as the line is composed, and a name written beside it that print does not take is refused then, once its keys are merged (§8.15). 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 reserved (§3.7), as it is in Python: it is a statement and names nothing, so x = pass is a parse_error at column 5.

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 its argument (rendered to its text form) on r.reason. Several arguments are held as CPython holds them, and the reason is the text of their tuple: raise ValueError("a", 1) gives ('a', 1). 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 reserved (§3.7), as it is in Python: a statement head before any value.

raise alone raises again the exception being handled: in an except body, in a finally body while one is pending, and in a script either of them calls. It keeps its category, its r.reason and its r.discriminator. With nothing being handled it is a RuntimeError whose reason is No active exception to reraise, as the program runs, as in Python. A handler that ends restores the one around it.

raise e raises what the name e holds, which is an exception an except caught: the name it bound, or another name bound to that. A name holding anything else, or nothing, is a type_error teaching the exception names at the name.

from gives a cause, which is None or an exception an except caught. Any other value is a type_error in Python’s words, exception causes must derive from BaseException. Nothing here reads a cause back, so a cause changes nothing a program can observe; it is evaluated after the message, and one that fails fails in the raise’s place. An exception name is no value in this language (§10), so a cause written ValueError("a") is the same refusal it is anywhere else.

A value that is not a built-in exception name or a name alone, as raise 1 or raise (e), is a parse_error at the value, teaching the exception names, and a grammar error inside or after the value is answered where CPython answers it, as raise not c d is at column 13. It names nothing, so where it is assigned, read or written after a ., the parse_error is where Python answers it: raise = 1 is one at column 7, and x.raise = 1 one at column 3.

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 statement form of assert, and a condition may begin with a bracket: assert (x), assert (x), "m" and assert (x) == 1 are all this statement. The same word heads the absence-assertion verb (§7.1) in its call form assert(path, source), which records an explicit-absent claim. The verb is read where the bracket ends the statement and holds a first argument ending in a dotted name, and then a comma, and where it ends the statement holding one dotted path whose first name the program binds nowhere. So assert (x.y, "m"), which Python reads as a tuple and never fails, is the verb here.

A rebinding statement (rebind-stmt) and a del statement (del-stmt) change the list, set or dict a name holds, or one it reaches through subscripts and method calls, in place, so every name holding it sees the change: xs.append(v), d[k] = v, m[i][j] = v, xs[i:j] = ys, del d[k]. Each answers nothing and is a statement of its own, never an expression. The exceptions are pop, setdefault and popitem (answer-method), which change the collection and answer a value: a call of one is an expression, and as a statement its answer is discarded. Their semantics, typing and refusals are §8.14. del is a reserved word (§3.7), and heads a statement immediately before a name, or before the element or slice of a value no name holds that it removes, as in del (xs)[0] or del [xs][0][0] (§8.14). Parentheses around a name or an element at the head of a statement are that name or element, as in Python: (xs).append(v), (c).hi() and (f)() are the statements without them.

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     := bitor-expr ( cmp-op bitor-expr )*
cmp-op       := '==' | '!=' | '<' | '>' | '<=' | '>=' | 'in' | 'not' 'in' | 'is' | 'is' 'not'
bitor-expr   := bitxor-expr ( '|' bitxor-expr )*    # set union, §8.6
bitxor-expr  := bitand-expr ( '^' bitand-expr )*    # set symmetric difference
bitand-expr  := add-expr ( '&' add-expr )*          # set intersection
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
              | '[' display-item ( ',' display-item )* ','? ']'   # indexing (string / collection, §5.3); a comma or a `*` makes the index a tuple (§8.15)
              | '[' 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)
              | namespace-member               # math / cmath (§8.16), vector (§8.17), struct (§8.18)
              | IDENT '(' expr ')'             # instance constructor (§13.2)
              | module-name '.' IDENT '(' expr ')'   # module-qualified construction (Python Reference §9.6)
              | value-call                     # value-script invocation (§6.8)
              | hypothesis                     # suppose (§15)
              | absence-hypothesis             # suppose_absent (§15.1)
              | 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 := '[' ( display-item ( ',' display-item )* ','? )? ']'          # list literal (§3.5.9); a spread, §8.15
              | '[' expr ( 'for' IDENT 'in' expr ( 'if' expr )* )+ ']'   # list comprehension (§8.9)
brace-display := '{' ( dict-item ( ',' dict-item )* ','? )? '}'      # dict literal (§3.5.12)
              | '{' display-item ( ',' display-item )* ','? '}'              # 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)
              | '(' ( display-item ( ',' display-item )* ','? )? ')'   # tuple literal (§3.5.11); a `*` item alone needs its comma
builtin-call := ( 'zip' | 'enumerate' | 'reversed' | 'range' | 'abs' | 'round' | 'divmod' | 'str' | 'int' | 'float' | 'list' | 'set' | 'dict' | 'isinstance' | 'issubclass' ) '(' ( ns-arg ( ',' ns-arg )* )? ')'   # zip/enumerate/reversed/range §8.6, abs/round/divmod §8.3, conversions §8.13, isinstance §13.9, issubclass §13.10; a spread §8.15
namespace-member := ( 'math' | 'cmath' | 'vector' | 'struct' ) '.' IDENT ( '(' ( ns-arg ( ',' ns-arg )* ( ',' IDENT '=' expr )* )? ')' )?   # §8.16–§8.18; a constant takes no call, a function takes one
ns-arg           := expr | '*' expr                           # a value, or a spread of its elements (§8.15)
path-expr    := IDENT ( '.' IDENT )+           # K.s.a slot-grammar dotted path

Prefix + takes what prefix - takes and changes no number, and any other operand is a type_error; a bool gives the int it is, so +True is 1. Prefix - (unary minus) negates an int, a real or a duration, and any other operand is a type_error. Negating an int has the runtime semantics of 0 - a (§8.3), so negating the most-negative integer overflows and refuses rather than wrapping; negating a real keeps the sign of zero, so -a is -0.0 when a is 0.0, as in Python. 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, with b evaluated only once.

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 the program has not bound 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 name the program has bound comes first, as Python’s lookup finds it first. A def of the unit is what a call of its name finds in any body and in any statement below it, whatever built-in shares the name, print included, while a statement above it still reaches the built-in. A name holding a value is not called, whatever else carries the name: max = 3; max(1, 2) is a type_error at the call, 'int' object is not callable, as x = 3; x(1) is and as get = 3; get(1) is, and Python raises that TypeError as the program runs. A body that names a built-in which the statements above its def have bound to a value is refused too, since no body reads a name from outside it (§4.2), and so is one that names a built-in the statements below it bind. A class holds its name ahead of a built-in of that name in every body of the unit, and from its own line at the top of the unit, so a statement above it still reaches the built-in. A method’s name is its class’s and takes nothing from the built-in. A name a body binds anywhere is that body’s from its first line. An assignment binds one, and so do a for, a capture in a case, an import and an as. A call or a read of it above the binding is a type_error, cannot access local variable 'max' where it is not associated with a value, where Python raises that UnboundLocalError as the program runs. A comprehension’s variable takes the name through the comprehension but for its first source, which is read outside it, and holds it from there on: a later source or an if that reads a name a later clause binds is that type_error too, whatever an outer scope holds under the name. Read from inside a comprehension, a body’s name or an outer comprehension’s is a free variable, and the words are cannot access free variable 'q' where it is not associated with a value in enclosing scope, where Python raises that NameError. A module is no callable: a call of one is a type_error, 'module' object is not callable, where Python raises that TypeError as the program runs. An except’s name holds through its handler, and at the top of a unit the built-in is found again past it, since Python deletes the name there. __debug__ reads as True, as it does in Python, and nothing may bind it or delete it. A call to a void script (§4.2) in expression position is a type_error; call it as a statement (§4.3) instead.

A subscript that holds a comma indexes by a tuple, as Python reads it: d[1, 2] is d[(1, 2)], and d[1,] is d[(1,)]. That holds for a write and a del through one too (§8.14). A slice beside another index, as in xs[1:2, 0], is a parse_error at the slice’s :, since no value is indexed by a tuple that holds a slice. Every part of the subscript is read first, so a grammar error anywhere in it is the answer 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 or a claim, per the verb). Read verbs produce a value and stand in expression position as the whole right side of an assignment or the whole value of a return (§7.1.1), not inside a larger expression; 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
prem    = premises(cur)                       # claims that one was concluded from

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 11). The bitwise operators and the shifts sit between comparison and + / -, in Python’s order, so c <= a | b compares c with the union, a | b & c is a | (b & c), a - b | c is (a - b) | c, and 1 + 2 << 3 is 24. ** binds more tightly than the prefix - and ~, 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, a range, a string, and a tuple whose elements all have one type (§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. The proof_tree a why yields is the derivation alone, the conclusion and then the claims it rests on; the earlier, superseded values of the cell are no longer elements of it, and remain readable through get. 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).

Listing order is part of this contract. Each of the six has a defined order. claim_list has two, because a read within one cell and a read spanning several answer different questions:

Ascending name order is the order sorted() gives (§8.6) — codepoint order, not locale collation — the same deterministic sorted order a constructed set<T> is presented in, and, like that one, a defined refinement of Python rather than a promise Python makes. So xs == sorted(list(xs)) holds for every row that says ascending, and sorting such a read again is dead code.

This is stronger than the stability §9.6 already guarantees: it fixes not only that the order does not vary between runs but what the order is. The two structural rows are as binding as the sorted ones — a proof_tree leads with its conclusion, and a diagnosis reads top to bottom as written.

result_type_set sorts by type name, in the ascending name order above.

list_result_types() has a published membership — these nine, in this order:

active_claim, claim_list, diagnosis, empty, proof_tree,
result_type_set, string_list, subject_set, verify_result

They are the result types a program can hold. Eight of them are also type names you may write in an annotation; empty is the ninth member and is not one — it is the sentinel case of an active_claim (below), and it is listed because a program can hold it, which is the question this verb answers.

These names are canonical. They are the same strings .kind yields and the same case labels a match compares against.

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. Classes (§13) remain the only user-defined types, and a class’s bases the only subtyping.

Constructed lists (list<T>). Separately from the store-derived finite collections above, a program may build a finite list 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> (holding numbers when they are all ints and reals, §5.6); 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]), an annotated binding (xs: list<int> = []), 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. The empty set (set([]), a set<unknown>) and the empty dict ({}, a dict<unknown, unknown>) are compatible the same way with any set and any dict, at the same sites: seen = set([]) then seen |= {"a"} binds seen as a set<string>, and d = {} then d = {"a": 1} binds d as a dict<string, int>. An annotation supplies an unknown element type at any depth, and for the empty dict too: ys: list<list<int>> = [[]] and d: dict<string, int> = {} bind the annotated 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 exists only while the program runs and is never stored; it is shared and changed in place (§8.14). 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 values alongside list<T> — a tuple immutable, a dict and a set shared and changed in place as a list is (§8.14):

• 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, which a constant index reads; a tuple is sliced by constant bounds (t[1:] → a sub-tuple, §5.3), repeated by a literal int count into the repeated position list ((1, 2) * 2, §8.3), and compared with ==/!= or ordered with </>/<=/>= against a tuple of any length (§8.1). When every position holds the same type it also iterates (§6.3), converts (list/set/tuple, §8.13) and is indexed and sliced at a computed position, as a list of its elements is. So does a tuple whose positions are all scalars, whose element is a value (§5.6), and one whose positions are all class instances, whose element is their nearest common base (§13.8). A tuple holding a collection beside a value of another type does none of these, since there is no single element type to bind or collect.
• 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 unpacks as a list does, its length checked when the statement runs (§8.11); it is repeated by any int count, literal or not, since it has no arity in its type to name (§8.3); it compares (==) against any tuple whose elements agree with T. It is homogeneous by construction, so it always iterates (§6.3). A fixed tuple whose positions all agree with T is one, a tuple being immutable, so it fills a declared tuple<T, ...> wherever one is written: as a value, inside a collection literal written at that declaration (ts: list<tuple<int, ...>> = [(1, 2)]), by an element write (ds[k] = (1, 2)), and by append / insert / extend. A collection a name already holds is not widened into a second name: a list is shared (§8.14), so its element type stays the one that name has. Fixed tuples of different lengths whose elements all share a type T are held together as tuple<T, ...>, as a type checker joins them: the display [(1, 2), (3, 4, 5)] is a list<tuple<int, ...>>, so it fills that annotation as each of its tuples does on its own. Tuples of one length keep their fixed type, and tuples whose elements share no type are not held together.
• 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>, exist only while the program runs and are never stored, and none is one of the base types. A key or set element is hashable: a scalar value class (every class a cell value has, §5.5), a value, or a tuple whose positions are recursively hashable. A list, dict or set is unhashable and is not itself a key or set element. Writing one where a key or an element is held is told in Python’s words, unhashable type: 'list', and a tuple is asked of what it holds. Looking one up is told the same as the program runs, whatever the dict or the set holds, since Python hashes first: [1] in d, d.get([1], 0), d.pop([1], 0), d[[1]], del d[[1]], s.discard([1]), s.remove([1]). A set asked after in a set is read as the frozen set it spells, so {1} in {1} is False. A range is hashed by the integers it denotes, as CPython’s is, so it may be a key or an element.

Iterators. iterator<T> is one further type former: a one-pass reader over a collection, returned by zip, enumerate, reversed and iter (§8.6), which states what reads one. It gives each element once, has no length and no position, and is equal only to itself. Like the three above it exists only while the program runs, and is not a base type. It is not a key or set element either, where CPython hashes an iterator by its identity. A key or set element here is held by its value, and an iterator has none to hold it by, since it is equal only to itself: a set is walked in sorted order (§3.5.13), where an iterator has no place, and CPython prints a set or a dict of iterators with each one’s address, which no other run repeats.

Dict views. dict_keys<K>, dict_values<V> and dict_items<K, V> are the views a dict<K, V> answers from .keys(), .values() and .items() (§8.6), as CPython’s are. A view reads its dict when it is read, not when it was made: after ks = d.keys() and d["b"] = 2, ks holds "b". It walks the dict’s keys, its values or its tuple<K, V> pairs in insertion order — for for (§6.3), a comprehension, a conversion (§8.13) and every builtin that reads a collection — has a length (len, .length) and a truth value (§8.2), and tests membership (§8.1). It has no position: d.keys()[0] is a type_error, and list(d.keys())[0] returns the first key. A keys view and an items view are set-like: each equals a set holding the same elements, takes the set operators beside any collection, on either side, and takes the inclusion order beside a set or another such view (§8.1, §8.3). A values view is equal only to itself. A view prints as CPython’s does, dict_keys(['a', 'b']). Like an iterator it exists only while the program runs, and is not a base type, and it is not a key or set element, where CPython hashes a values view by its identity, for the reason an iterator is not one.

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. Since a name holds one type (§6.1), no name can hold “a value or nothing” either, which is why DKE Python has no None (§3.5.4).

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

Every number has the two parts CPython gives it. A number is its own real part, a bool read as the int it is, so True.real is 1; its imaginary part is a zero of its class, 0 for an int or a bool and 0.0 for a real. A claim’s value (§5.6) has neither until it is narrowed: it may hold a string, and what takes only a number takes a value only once a match or a test has said it holds one.

Two types in the table are ones 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 names the claim: its cell path followed by # and a code of twelve lowercase hexadecimal digits (Cat.felix.color#3f09c1a27b44). The code is made from what the claim shows — its value and its type, where it came from (source, or the rule that concluded it), its validity window, its qualifiers and its created_at — so a claim carries the same claim_id on every read that returns it, and writing, revising or removing another claim leaves it unchanged. A claim recorded anew has a claim_id of its own: the new claim of a revision (the claim it supersedes keeps its id), a conclusion a rule draws again, and a value in force the restore tool brings back — an older version it puts back into the history keeps its claim_id, since it keeps its created_at. Two claims at one cell that agree on all of those fields share a claim_id. dependents, premises, forget and would_forget (§7.1) take a claim_id in place of the claim it names.

written_by names the store 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. A store 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",
             datetime("2020-01-01T00:00:00Z"), datetime("2022-12-31T00:00:00Z"))
    remember(Emp.e1.dept, "eng", "hr",
             datetime("2021-01-01T00:00:00Z"), datetime("2023-12-31T00:00:00Z"))
    remember(Emp.e2.ongoing, "yes", "hr", datetime("2021-01-01T00:00:00Z"), null)
    a = current(Emp.e1.dept, datetime("2021-06-01T00:00:00Z"))
    show("dept", a)
    d = current(Emp.e1.flagged, datetime("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" valid_from=datetime("2020-01-01T00:00:00Z") valid_to=datetime("2022-12-31T00:00:00Z")
  remember Emp.e1.dept = "eng" valid_from=datetime("2021-01-01T00:00:00Z") valid_to=datetime("2023-12-31T00:00:00Z")
  remember Emp.e2.ongoing = "yes" valid_from=datetime("2021-01-01T00:00:00Z")
  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.

qualifiers reports the facts the writer stated about this claim when it wrote it — how the value was obtained, how sure the writer is of it, what it was measured with: whatever the writer chose to say, as a dict from name to value. They are written with the qualifiers= argument of remember and update (§7.1), and they belong to the one claim they were written with. Another source’s claim at the same attribute carries its own, and a claim written with none reports an empty dict. The store keeps them with the claim, returns them on every read that returns the claim, removes them with it, and never acts on one. A qualifier named confidence is what its writer said about its own value, not a judgement the store has made: the store’s account of how a claim arrived is trust, and no qualifier changes it.

Each value keeps its class (§5.6), exactly as value does — a qualifier written as 0.8 reads back as a real and one written as datetime("…") as a datetime — and the names come back in name order.

# claim-qualifiers.dpy — a writer states facts about its own claim, and every
# read that returns the claim gives them back.
def qualifier_report():
    remember(Reading.r1.temp, 21, "lab",
             qualifiers={"method": "observed", "confidence": 0.8})
    remember(Reading.r1.temp, 23, "forecast", qualifiers={"method": "predicted"})
    remember(Reading.r2.temp, 19, "lab")
    readings = get(Reading.r1.temp)
    for r in readings:
        q = r.qualifiers
        print(r.source + " says " + str(r.value) + ", " + str(q["method"]))
    plain = current(Reading.r2.temp)
    none = plain.qualifiers
    print("r2 carries " + str(len(none)) + " qualifiers")

OK script qualifier_report(): 3 claims written, 3 prints
  remember Reading.r1.temp = 21 qualifiers={"confidence", "method"}
  remember Reading.r1.temp = 23 qualifiers={"method"}
  remember Reading.r2.temp = 19
  print lab says 21, observed
  print forecast says 23, predicted
  print r2 carries 0 qualifiers

The two sources disagree about r1, and each claim still says how it was reached. That is the point of putting the account on the claim rather than beside it: a program weighing the two reads both values and both accounts from one place, and nothing about either was lost when the other was written.

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 nor a matter of preference (§7.6), 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 with derived_by the two fields separate the three cases a reader meets:

derived_by names what concluded a derived claim. A rule (§14) reads as the name list(target = rules) lists it under (§14.7) — heat.comfy for the rule comfy in the module heat, warm for a rule compiled on its own — and a computed field (§13.7) as its class and its field, qualified by its module the same way — heat.Box.area. It is the empty string on a claim someone recorded. premises(c) (§7.1) returns the claims the conclusion was drawn from. rule_kind is the kind of relation the concluding rule states, when its author said (§14.1) — "causal" for a rule written @rule(kind="causal") — and the empty string otherwise: on a claim someone recorded, on a computed field’s conclusion, and on a conclusion of a rule written without one.

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 eight 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 recorded as absent (assert), a condition recorded with a value that has no order under an ordered test (a blob, or a recorded absence), a condition recorded with a value that has an order and compared under an ordered test with one that has none, a condition required to be absent that is present, and a condition whose sources disagree. A recorded absence holds no value, so a rule that only reads the field is told it is absent, not that it failed a comparison. A condition comparing two fields (o.qty > o.limit) is stated with both, as it was written. A value with no order is not a value that failed, on either side of the test: no value of its type passes <, <=, > or >=, so what it needs is a different value, or ==. The value compared with is named when the rule read one value for it. 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. When a rule has every condition it needs and still concludes nothing — a fold of the rule cannot take the values it reads (§14.9, declined), the comparison it concludes cannot rank the values it reads, or the arithmetic it computes has no answer for them (a divisor of zero, say) — both verbs say so of that rule, the last with the operation over the values it read and the fields they came from, and what_needs says it before the conditions it lists as recorded. A condition whose cell already holds a value is named as recorded, with the case why_not would give it (out of its window, failing its test, recorded as absent, without an order, compared with a value without one, or disagreed on), rather than as a fact to supply. A condition required to be absent whose field holds a value is named as present, never as a fact to supply. The move is removing the value or narrowing its window where the caller recorded it, and changing what the concluding rule reads where a rule concludes it, since a conclusion forget removes is drawn again while its premises hold (§14.4). The walk does not go through the rules that would conclude such a field, since what they need would make it hold, and a condition required to be absent that is absent is listed as held. 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, datetime("…")) 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 — by match, whose case set for a proof_tree is { proof_tree, empty } (§6.2). 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 without its # and code. It is most useful for the reads whose claims live at cells the call site did not name: dependents and premises (the cell each claim they return lives at) and conflicts (each conflicting cell). path and claim_id are spelled the way a program addresses the cell, so a kind a module declares reads back qualified by its module — inventory.Item.i1.qty — as §7.1’s listings name it.

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 with no recorded creation moment 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, proof_tree, empty, verify_result, and the try-handler discriminators of §5.4). The returned string is the type name as written in §5.1.
• <expr>.length returns int for any string, any blob or any finite collection. For a string the result is the number of characters (Unicode characters, not bytes); for a blob it is the number of 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 none of these).

5.3 Indexing and slicing

Indexing. The expression <value>[<int>] selects one element. It is well-typed when the value has one of the types in this table, and the result type is the one the table gives:

A set does not index. A set has no positional index, in Python or here, so s[i] and s[a:b] are refused before the run, in Python’s words: 'set' object is not subscriptable. A set’s elements are read with a bounded for, which walks them in sorted order (§3.5.13), and one is tested with in (§8.1).

Tuple indexing. A tuple’s positions may differ in type, so t[i] with a compile-time constant integer i (a literal, an optional leading minus, or a constant +/- of such) has the type of that position: t[0] the first, t[-1] the last. A computed index reads what a for over the tuple binds (§5.1): the positions’ one type, value over scalars of several (§5.6), or the nearest common base of class instances. Over a tuple holding a collection beside a value of another type a computed index is a type_error, which costs no function, every position being reachable by a literal index. An index past either end compiles, and refuses when it runs, catchably, as Python raises its IndexError there (§10.3), so t[9] on a pair is a catchable refusal at run time, saying tuple index out of range. A constant one is typed as an element of the tuple read as a list, the positions’ one type or value over scalars of several (§5.1), so what reads it is checked as it would be against such an element. This is one application of a general rule (§8.3, Value-dependent typing), not a rule of its own.

Dict indexing. d[k] looks a value up by key, comparing k with the keys as == does, and the result is V. A key absent at run time is a catchable refuse (§10.3), and so is a key of another type, which no key equals ({1: 2}["a"] refuses as 'a'). 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. An index of another type is a type_error, told in Python’s words over a string, a list or a tuple, naming the index’s class: list indices must be integers or slices, not str for [1]["a"], and string indices must be integers, not 'float' for "ab"[1.5]. A del or a write through such an index says the same, and a list’s pop given one says 'str' object cannot be interpreted as an integer. An index of a type only this language has keeps this language’s words.

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, which a change to the source does not reach, §8.14); 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). With constant integer bounds (t[1:], t[:2], t[1:-1], t[::-1]) the result type is the sub-tuple of the selected positions. With a computed bound it is a variadic tuple<T, ...> of what a computed index reads, and over a tuple holding a collection beside a value of another type a computed bound is a type_error, as a computed index is (§5.3). list(t[a:b]) (§8.13) then converts the result to a list<T> — the idiom behind starred unpacking.

A slice as a value. slice(stop), slice(start, stop) and slice(start, stop, step) build a value of type slice (§5.1) that holds three bounds. Each argument is an int, a bool (kept as written, as CPython keeps it) or None (§3.5.4), which leaves that bound open, and a bound not given is open too, so slice(5) is CPython’s slice(None, 5, None). A slice indexes as its bounds written in brackets do: xs[s] answers what xs[a:b:c] answers on a string, a list<T> and a variadic tuple. A zero step is refused there as the bracketed form refuses it. On a fixed-length tuple a slice is a bound the compiler does not see, so t[s] reads as a computed bound does: a variadic tuple of what a computed index reads, and a type_error over a tuple holding a collection beside a value of another type. On a list, xs[s] = c, xs[s] op= c and del xs[s] change what the bracketed slice would (§8.14).

A slice carries:

A slice prints as CPython prints it, slice(1, 5, None), through print, str, repr, an f-string hole and inside a collection. Two slices are == when their three bounds are, so slice(1, 2) == slice(True, 2) holds as it does in CPython. A slice is not ordered, since CPython orders slices by their bounds and fails wherever one is None. It is always true and has no .length, and it is not hashable, as in CPython 3.11, so it is neither a set element nor a dict key. It is a value a program builds rather than a fact: no field and no verb stores one.

One difference from CPython: an open bound read back prints null, as an open window bound does (§3.5.4), where CPython prints None. print(slice(3).start) writes null, while the slice itself prints slice(None, 3, None).

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

Arguments by name. A string method takes by name exactly the arguments CPython lets a caller name, and places each in the position it names, as a built-in function does (§8.13): sep and maxsplit on split and rsplit, keepends on splitlines and tabsize on expandtabs, so s.split(sep=",", maxsplit=1) splits as s.split(",", 1) does. A separator left out is Python’s None, which has no spelling here, so naming maxsplit alone is how a whitespace split is bounded: " a b c ".split(maxsplit=1) is ['a', 'b c '], the rest kept whole after the whitespace that follows the last piece, and " a b c ".rsplit(maxsplit=1) is [' a b', 'c'], its pieces taken from the right. A dict’s update takes any name as a key and sort takes key and reverse (§8.14). Every other method of a string, a list, a tuple, a set, a dict, a dict view or a number takes no argument by name, as in Python, and a name given to one is a compile-time error in Python’s words, naming the receiver’s Python class, such as str.center() takes no keyword arguments. A receiver without the method is told that instead, since Python finds the method before it reads an argument.

Arguments of a type a method does not take. An argument of a type a string’s method does not take is a compile-time error in Python’s words, which follow how the method is written in C, and so differ by method for one fault: "abc".find(1) is refused with must be str, not int, "abc".replace("a", 1) with replace() argument 2 must be str, not int, "abc".startswith(1) with startswith first arg must be str or a tuple of str, not int, "abc".split(1) with must be str or None, not int, "abc".strip(1) with strip arg must be None or str, "abc".center(5, 1) with The fill character must be a unicode character, not int, and "abc".zfill("a") with 'str' object cannot be interpreted as an integer. A search’s bounds are read as a slice’s: "abc".find("a", 2.5) is refused with slice indices must be integers or None or have an __index__ method, and [1, 2].index(1, "a"), over a list or a tuple, with slice indices must be integers or have an __index__ method. A list’s insert position and a slice’s indices argument are integers, so xs.insert("a", 2) is refused with 'str' object cannot be interpreted as an integer. An argument of a type Python has no class for, such as a claim’s value, is told instead which type the method takes.

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 reads any iterable of strings as for reads it, as Python does — a string, a list, a tuple, a set (in its order, §3.5.12), a dict’s keys, a dict view or an iterator, which it reads to the end: "-".join("abc") is "a-b-c". An iterable whose elements are not all strings is a type_error, in Python’s words where the first that is not is of a class Python has: "a".join([1]) is refused with sequence item 0: expected str instance, int found, and "a".join(1), over what is no iterable, with can only join an iterable. These are the only method calls the language defines on a built-in value.

upper() and lower() apply the full case mapping stated above: a character whose case change needs more than one character maps to all of them, so "straße".upper() is "STRASSE" and len("ß".upper()) is 2. 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

The type names valid as type-name tokens are the primitives (string, int, bool), the value-class scalars (datetime, duration, real, blob, scientific, complex), and the read-result types from §5.1 (active_claim, claim_list, proof_tree, diagnosis, subject_set, string_list, verify_result, result_type_set). A parameter or return annotation (§4.2) additionally admits a parameterized collection type — list<T>, set<T>, dict<K, V>, tuple<T, ...> — nestable to any depth, and an iterator type iterator<T> (§8.6), which typing.Iterator[T] is taught to write, and the three dict view types dict_keys<K>, dict_values<V> and dict_items<K, V> (§5.1). A collection type is built from these names or from a class name, so list<Animal> is a type.

CPython’s spellings are read beside these. str and float are string and real, on the surface whose words are CPython’s, and a class the program declares by either word is that class; another surface has its own word and teaches it. A collection type takes CPython’s brackets as well as angle brackets, so list[int] is list<int>, dict[str, int] is dict<string, int> and tuple[int, ...] is tuple<int, ...>. They are one type, and a diagnostic renders it with angle brackets. A collection word with nothing after it, as in x: list = [], says nothing of what it holds and is refused, teaching list[int], and so are typing’s capitalised names, List[int] among them, which have no module here to come from. bytes is refused, teaching blob, since a blob prints otherwise. A return annotation of None alone, as in def f() -> None:, says what no annotation says; None as any other annotation is refused.

A class name the program declares (§13.1) is a type too, and is valid in every position a type is written: a parameter, a binding annotation, a collection’s element type, a script’s return and a value method’s return. It is not a type-name token — it enters the grammar at type, as an IDENT (§4.2) — so the list above remains the list of names the language itself reserves for types, and is not the list of everything writable where a type goes. What a class name means in those positions is §13.8: a subclass instance stands where its base class is named.

A parameter (§4.2) may be typed by any of them. 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), a complex as the text it renders as, with or without its parentheses (§3.5.15) — and refuses if the text is malformed. A complex is given as 3+4j, (3+4j) or -2.5j.

A class field (§13.1) must be a primitive or a value-class scalar — a scalar-name, a type the engine stores as a cell value (string, int, bool, datetime, duration, real, blob, scientific, complex) — 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; a value written as a complex number (§3.5.15) reads back as a complex. 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 | complex

Every class but one is write-producible from DKE Python — a program writes an int, bool, string, datetime, duration, real, blob, scientific or complex 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 four ways:

• Destructure it with a match (§6.2) to obtain the typed content:

  c = current(Sensor.room.count)
  match c.value:
      case bool as b:     print("flag = " + str(b))           # b : bool
      case int as n:      print("next = " + str((n + 1)))     # n : int — arithmetic is well-typed
      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 complex as z:  print("size = " + str(abs(z)))      # z : complex — arithmetic is well-typed
      case null:          print("an absent value")       # detect-only — no `as` binding

  A write-producible class (int, bool, string, datetime, duration, real, blob, scientific, complex) 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 and a test (below) recover an int (for arithmetic), a bool (for logical operators), or a datetime / duration / real / blob / scientific / complex (to render, compute with 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).

• Narrow it with a test. Where a test has shown what a name holding a value holds, the name is read at that class: in the branch an isinstance test takes (§13.9), after the test in an and, after a comprehension’s if making it, in a conditional expression’s first branch, in an arm of a match naming its class (§6.2), and in the body of an arm whose guard tests it, as CPython runs each. isinstance(v, int) reads v as an int, and so does a test of int beside bool, since a bool is one; a test of either beside real reads it as a value holding a number, and an or of two tests reads it as what the two join to. Only a name is narrowed, not a field read such as c.value.

  A value built from scalars holds their classes and no other: [1, "a"] holds an int or a string, and so does an element read from it, a loop variable over it and a join of two such values. Where a test fails, a name holding one is read at the classes left to it: in the else of an isinstance test, in the branch a negated test takes, in a conditional expression’s second branch, after the test in an or, and in an arm of a match below arms naming classes (§6.2). A value whose classes are not known, such as a claim’s, may be any class, so a failed test leaves it a value; so does the else of an and, whose left test may have held. A branch no value can take is never run and is not read: a test of types no value has (isinstance(v, list)), two tests no class passes both, or the else of a test of object. An operator meeting a value of known classes runs where it takes each class beside the other operand, and answers what their answers join to, so x * 2 over a value holding an int, a real or a string is a value of the three; a name read on both sides meets only a class with itself.

  for e in (1, 2.5, "a"):
      if isinstance(e, int):
          print(e + 1)                       # e : int
      elif isinstance(e, str):
          print(e.upper())                   # e : string
      else:
          print(e * 2)                       # e : real

• 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 any value — a literal of any of its classes, another value, a collection (§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 every class named 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). Reading a claim is not the only way to get one: the element of a collection mixing scalar value classes is a value ([1, "a"], §3.5.9), and so is whatever is read from it — an index, a loop or comprehension variable — and so is an or or and over two value classes (1 or "yes", §8.2).

A value that holds a number. When every element a mixed collection can hold is an int, a real or a bool — [1, 2.5], {1, 2.5}, [True, 2.5], the values of {"a": 1, "b": 2.5}, the positions of (1, 2.5) — its value is known to hold a number, and the numeric operators and built-ins take it as one: arithmetic (§8.3), ordering, == and membership against numbers (§8.1), sum / min / max (§8.3), sorted (§8.6), and abs, round, divmod, int and float (§8.3, §8.13). Each element keeps its own class, so [1, 2.5][0] is 1, [1, 2.5][1] + 1 is 3.5 and min([1, 2.5]) is 1, as in Python. Its type is still written value — in a diagnostic, and wherever it meets a declared type — so it does not satisfy an int or real parameter, return or annotation; convert it with int(…) or float(…) (§8.13).

An operation over it is typed by the classes that can reach the result. Where the rules of §8.3 give a real whichever class the value holds — a real other operand, /, a negative literal exponent — the result is a real; otherwise it is again a value holding a number, because its class is the element’s. So is sum over such a collection: sum([1, 2.5]) is 3.5, and sum([x for x in [1, 2.5] if x < 2]) is 1.

The property composes, and is lost wherever a value that is not a number could arrive:

• it is kept through reading (xs[i], for x in xs, a comprehension, a generator expression, list / set / tuple of the collection), through arithmetic, through + of two collections that each hold numbers ([1, 2.5] + [3]), and into the keys of a dict, which are matched by value (§3.5.12): sum({1: "a", 2.5: "b"}) is 3.5;
• where one expression may produce either of two values — a conditional expression, and / or, the re-binding of a variable, a loop variable left over from a loop, min / max of separate values or with default= — the result holds a number only when both sides do, so ys = [1, 2.5] if c else ["a", 1] is a list<value> that sum refuses;
• the inner lists of a nested literal unify the same way, so the lists [[1, 2.5], ["a", 1]] holds are not lists of numbers;
• a bool is the int it is, as in Python (§8.1), so [True, 2] is a list<int> and [True, 2.5] a list<value> holding numbers: sum([True, 2.5]) is 3.5, and True in [1, 2.5] is True. It keeps its class, so max([True, 0]) is True, the element itself.

A value that holds a magnitude. When every element a mixed collection can hold is a number or a scientific — [scientific("2.0e0"), 1], the keys of {scientific("2.0e0"): "a", 1: "b"} — its value is known to hold a magnitude, and it orders as a scientific does, by magnitude (§8.1): against a number, a scientific or another such value, in sorted, min and max, and inside two lists or tuples being ordered. It is not a number, so arithmetic, sum and the numeric built-ins refuse it, as they refuse a scientific. It composes as a value holding a number does, and a number has a magnitude too, so [1, 2.5] + [scientific("3.0e0")] holds magnitudes, and min of a scientific and a number holds one.

6.1 Scoping

DKE Python is function-scoped for variables, as Python is. 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, try, except, or branch block binds the script’s variable, 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. Script parameters are in scope for the entire body.

A name is read only where every path that reaches the read has bound it — the definite-assignment rule, which the compiler checks, so that no run reads a name unbound. A name first bound inside a block is readable within that block and its nested blocks, and after the statement holding the block when every path through that statement that completes binds it:

• both arms of an if/else, and every arm of an if/elif/…/else chain;
• every arm of a match with an unguarded catch-all (case _:, a capture, or case default:), and every arm of a match over an instance of a class, whose arms must cover every class the instance can hold;
• a try body, which runs on into its else, so the else reads what the body bound, and each except handler present; a name the finally binds is bound on every path;
• a branch block’s body, which runs in full (§9.2.6).

A path ending in return, raise, break, or continue reaches nothing after the statement, so it need not bind the name. Every path must bind the name to one type: paths binding it to two types compile, and a read after them is a type_error naming both. A name bound on some paths only — after an if with no else, a match with no catch-all, or a try with a handler that does not bind it — or in a for body, which may run zero times, or in the for’s else, which a break skips, is readable within its block only; a read after is a type_error saying it is not bound on every path. Bind it before the statement to read it after. Where CPython raises NameError on a run that reaches such a read with the name unbound, DKE Python refuses the read before any run. A finally reads none of its try’s bindings, since it also runs when the body did not complete.

The except handler variable is block-local and does not leak past its block: it is visible only within its own block, and when the block ends the name is restored to whatever it held beforehand, or becomes unbound if it was not previously bound. The for loop variable is not: the loop assigns each element to it in the enclosing scope, so after the loop, and in its else body, it holds the last element bound, as in Python, and a loop that runs zero times binds nothing and leaves the name as it was. Being an assignment, a loop over a name that is already a variable keeps that variable’s type (§6.3). A comprehension’s variable, by contrast, is local to the comprehension (§8.9). match case clauses bind no name of their own; the scrutinee’s binding (if any) stays visible inside every case body. A class arm’s as binding is local to its arm (§6.2), while a value pattern’s capture and as bind as assignments do (§6.2).

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. A value whose one fault is a combining mark — "cafe" followed by U+0301, which renders as café — is refused naming the mark by its codepoint, since the mark draws onto the letter before it and nothing on screen shows it. A held value is not read as a written name is (§3.4), so the mark stays and does not compose. Reading the cell and writing it are refused alike.

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 (Python 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 over a value Python has is Python’s: a number, a text, a collection, a slice, a view, an iterator or a class instance. Every arm is a test, tried in the order written, and when none holds none runs. What only this language has dispatches by CLASS, and such a match MUST cover the case set of the scrutinee’s type:

Any other scrutinee type is a type_error. Over a type with a case set, a missing case is a type_error; a case label not in the set is a type_error; a repeated case label is a type_error, and the order of class labels is not significant. Value patterns are tried in the order written. A class instance the compiler follows to its class also takes the class match (§13.5).

Value match. When the scrutinee has type value (§5.6), the case labels are the value classes int, bool, string, datetime, duration, real, null, blob, scientific and complex. Like a class match (§13.5), the arms MUST either cover every class or provide a case default: catch-all; a value match that is neither exhaustive nor defaulted is a type_error. That holds where an arm writes a label of this language’s own, a class named with no parentheses (case int:, case int as n:, case null:). Where every arm naming a class writes Python’s parentheses instead, the match is Python’s, as over a value Python has: every arm is a test, tried in the order written, and none is required. In an arm naming classes, a scrutinee written as a name is read at the class they join to (§5.6), in the arm’s guard and body, and in an arm below them at what their tests failing leave it. A bool is an int (§8.1), so an arm naming int takes a bool too, as Python’s class patterns do, and covers it: the classes are all covered without an arm naming bool. An arm naming bool below an unguarded arm naming int could never run and is a type_error; to tell the two apart, write the bool arm first. A write-producible class (int, bool, string, datetime, duration, real, blob, scientific, complex) 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). case int():, Python’s class-pattern spelling, tests what case int: tests for every write-producible class, as case <Class>(): does for a declared class (§13.5), and case str(): and case float(): are the string and real arms, the names isinstance reads for them. In a match that is Python’s, a type Python has holding one pattern binds the value to it, as Python’s does: case int(n): binds n, and a capture binds it too. Beside a label of this language’s own, a type with a pattern inside its parentheses is a type_error, as is a type only this language has holding one; bind the content with as. A label that is no class, null, default or empty, takes no parentheses: case null(): is a parse_error. 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.

Alternation. A case label MAY name two or more discriminators separated by | — case int | string: — and the arm is selected when the scrutinee’s discriminator is any one of them. An alternation is a spelling, not a widening: it covers exactly the classes it names, and the arms of the match must still be exhaustive or defaulted by §6.2’s table. case int | string: and the two arms case int: / case string: with the same body are equivalent; which to write is a matter of style.

# match-arms.dpy — one arm may name ALTERNATIVES, and a guarded arm may be
# followed by a second arm naming the same class.
def describe_reading() -> string:
    remember(Sensor.roomA.count, 42, "demo")
    c = current(Sensor.roomA.count)
    match c.value:
        case int as n if n > 100:
            return "high"
        case int as n:
            return "count " + str(n)
        case string | datetime:
            return "not a number"
        case default:
            return "other"

Four rules constrain it, each a compile-time error:

The third rule is the case default: restriction above, generalised: a label spanning more than one class has no single payload type, and default is that same condition reached by a different spelling.

| is the alternation separator between the labels of a case. In an expression, a guard’s included, it is the set union (§8.6), so case int as n if {n} <= allowed | extra: reads it there, and on two integers it is the bitwise or (§8.3).

Guards. A case label MAY carry a condition: case <label> [as IDENT] if <expr>:. The arm is taken when the scrutinee’s discriminator matches AND the condition holds; when the condition is false the arm is not taken and the next arm is tried. The condition is any expression with a truth value (§9.2.2’s rule for if, unchanged), and the arm’s as binding is in scope in it — case int as n if n > 0: is the form guards exist for. The body reads a name holding a value at the class its guard has shown, as a branch reads its test’s (§5.6).

A guarded arm does not satisfy exhaustiveness, and this is the rule the rest of the construct rests on. Its guard may be false, so the arm cannot be counted as covering its class: a match with no case default: must name every class of §6.2’s table in an arm with NO guard. One consequence is worth stating plainly, because it is what the rule buys: an exhaustive match always runs exactly one arm, and no program can make it fall through. A match with no class set — over a value Python has, or over a value naming no class — is not exhaustive, and runs no arm when no pattern matches, as Python’s does (value patterns, below).

Two rules follow from it, both compile-time errors:

Because a class may be named more than once, arm order is significant for guarded arms: the first arm whose label matches and whose guard holds runs. Where no guards are involved no class can repeat, so order remains immaterial.

Sequence and mapping patterns. A case label MAY be a SHAPE rather than a class: case [a, b]: matches a sequence of exactly two elements, and case {"id": i}: a mapping containing the key id. A sequence pattern matches a list or a tuple and a mapping pattern a dict; over any other value Python has, it compiles and never matches, at any depth. As one alternative of several it is left out of its arm, unread, and the arm stands on the alternatives left, taking its names from the one that matched: over x = 1, case 1 | [2]: is taken and case [1] | 2: is not. Over what only this language has, a shape label is a type_error.

A sequence pattern is a bracketed list of element patterns:

Without a * the pattern matches a sequence of EXACTLY that length; with one, of AT LEAST the fixed length. case []: is the empty sequence. A * that is not the last element is a compile-time error: matching one requires counting the fixed elements from the end, which this surface does not do. The elements after it are still read as Python reads them, so a syntax error among them is the answer over this refusal (§10.1): case [*y, 1 +]: is a parse_error at the ].

Alternatives separated by | are an element pattern too, in a sequence and as a mapping’s value: case [1 | 2, b]:, case {"k": "a" | "b"}:. Each alternative binds the same names, and a name is bound from the one taken, so case [[1, a] | [2, a, 0]]: binds a from either. Two compile-time errors, each answered below a syntax error after it (§10.1): an alternative that matches every value — _ or a capture — before the last, as case [a | 1]:, since the alternatives after it could never match; and alternatives binding different names, as case [1 | a]:, since a name could be left unbound. An element pattern MAY end in as IDENT, which binds the value it matched, alternatives included: case [1 | 2 as k, w]: binds k to the 1 or the 2.

A case label MAY be an element pattern itself when one of its alternatives is a sequence or a mapping pattern, and it is then a shape label: case [1] | [2]:, case 1 | [b, 2]:, case {"k": 1} | {"j": 2}:, case [1, _] as z:. The rules for alternatives and as above are its rules. When its last alternative is _ or a capture and it carries no guard, it matches every value, and it is a catch-all with a catch-all’s rules: case [1] | _: must be the last arm, and it covers the match.

A mapping pattern is a braced list of <literal>: <element pattern> entries. It matches when every named key is PRESENT, and says nothing about keys it does not name — a mapping pattern is a subset test, never an exact one. The key MUST be a literal as a value pattern writes one — a text, a number, a complex, True or False — and is found as in finds a key, so case {1.0: v}: matches {1: "a"}. A key that were itself a pattern would be a lookup by an unknown value, which is a search rather than a test, so a name or a bracket where a key goes is a parse_error, as in Python, and a dotted name, Python’s value pattern, is refused as it is wherever a pattern holds one. A pattern MUST NOT name one key twice: case {1: a, 1.0: b}: is a compile-time error, as in Python. Keys that are equal are one key, as 1, 1.0 and True are.

A match over a value Python has takes any expression, evaluated once, whatever its arms, and needs no catch-all. Its arms are tried in source order. Shape labels, value patterns and class patterns may stand in one match, and each MAY carry a guard — case [a, b] if a > b: — with the pattern’s own bindings in scope in it.

Class patterns. case <Class>():, case <module>.<Class>(): and case <type>(): test the class, as isinstance does (§13.9): an instance is of its class and of each base, a bool is an int, and object takes every value. A class pattern over what can never be of that class compiles and never matches. Python’s types that read as themselves, int, bool, float, str, list, tuple, dict and set, MAY hold one pattern, over the same value: case int(n): binds n, case int(1): takes only 1, and case list([a, b]): is case [a, b]: over a list. Anything past that count, or anything inside the parentheses of a declared class, complex, slice or object, raises a catchable type_error in Python’s words once the class has held: int() accepts 1 positional sub-pattern (2 given), C() accepts 0 positional sub-patterns (1 given). A keyword, as case C(n=1):, reads a field while the match dispatches, and a read stands on its own line (§7.1.1), so it is a parse_error, as it is on a type: read the field inside the arm. A class pattern MAY stand inside a sequence or a mapping pattern, or beside a literal as an alternative: case [int(), C() as c]:, case 1 | str():. A guard and a body read the name the match holds, and the name after as, as the one class an arm tests.

A class named with no (), as case C: or case int:, is a label of this language, and Python reads it as a capture. Over an instance the compiler follows to its class it is the class match of §13.5; over any other value Python has it is a compile-time error, naming case C():, as null and empty are, which label what a value or a read holds.

Value patterns. A case label MAY be a VALUE PATTERN, Python’s own:

A name is a class label when it is a type name (§5.5), empty, or a class the unit declares; every other name after case is a CAPTURE. _ MAY end an alternation of literals (case 1 | _:), which then matches anything. Value patterns take guards like any label. The name after as is never _, which binds nothing: case 1 as _: is a parse_error at the _, and so is an as _ inside a sequence or a mapping pattern. A pattern binds each name once: case a as a: is a compile-time error at the pattern’s start, and a name bound twice inside a sequence or a mapping pattern is one at the pattern binding it the second time, as case [a, a]: at the second a. An as binds once the pattern before it has matched, so a name it binds twice is answered at the last pattern read before it: case [a] as a: at the inner a. A pattern in parentheses is the pattern it holds, here and inside a sequence or a mapping pattern, as Python’s group pattern is: case (1 | 2) as z:, case [(1 | 2), b]:. Parentheses that hold a comma, or hold nothing, are a sequence pattern instead, as square brackets are: case (1, b): is case [1, b]:, case (1,): is case [1]: and case (): is case []:, here and inside another pattern, as case [(1, 2)]:. A sequence pattern MAY also be written with no brackets at all, as Python’s open sequence pattern, when commas outside every bracket separate its elements: case a, b: is case [a, b]:, case a,: is case [a]: and case 1, *rest: is case [1, *rest]:, and it ends at the : or the guard’s if. The case-clause grammar above does not write these forms; this paragraph defines them.

A literal is read as Python reads one, here and inside a sequence or a mapping pattern. A sign after a number begins a complex literal, so an imaginary number follows the sign: case 1 +: is a parse_error at the :, case 1 + 2: at the 2, where an imaginary number is required, and case 1j + 2j: at the 1j, where a real one is. A - begins a negative number, and what follows it when that is no number is answered there: case -x: is a parse_error at the x.

Where each is admitted:

Arms are tried IN THE ORDER WRITTEN, class arms and value patterns alike, and the first whose label matches and whose guard holds runs; no other arm runs. A literal matches exactly when == would say the scrutinee equals it, so case 1: matches 1.0, case 1.0: matches 1 and case 1: matches True, compared exactly at every magnitude (§8.1). True and False are the exception, as in Python (PEP 634): they match by IDENTITY, so case True: takes True and not 1, and case False: takes False and not 0. A literal of a type the scrutinee can never equal compiles and never matches, and neither does one over an instance. A literal of one class does not match a value of another, whatever the two render as: over a value holding the integer 7, case "7": does not match and case 7: does. A capture and an as binding over value patterns are ASSIGNMENTS: they are made once the pattern has matched and before the guard is evaluated, and the name keeps the value when the guard is false, as in Python. They follow §6.1 like any assignment, so a name first bound in an arm is not readable after the match. _ and an unguarded capture satisfy exhaustiveness as case default: does, where a match requires it.

Over an int, a literal, an alternation, a guarded capture and _:

# value-match.dpy — a value pattern compares a scalar, as Python's does.
def sizes():
    said = []
    for n in [0, 2, 7, 40]:
        match n:
            case 0:
                said.append("none")
            case 1 | 2:
                said.append("a couple")
            case m if m < 10:
                said.append(str(m) + " is a few")
            case _:
                said.append("many")
    print(said)                             # ['none', 'a couple', '7 is a few', 'many']

A CATCH-ALL MUST BE THE LAST ARM. _, an unguarded capture, and case default: in a match with any value pattern each take every value that reaches them, so an arm after one could never run. One before another arm is refused at the _, the capture or the default itself, a pattern’s last alternative included, which is where Python refuses the first two. Each rule below is a compile-time error:

A match over a datetime, a duration, a blob or a scientific remains a type_error: only this language has them, and an if compares them.

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>), a string, a tuple whose elements all have one type, a dict view (§5.1), or an iterator (§8.6), which the loop reads one element per pass. Iterating a diagnosis binds its report lines, each a string (§5.1). Iterating a dict binds its keys; iterating a dict view binds what it views, the keys, the values or the (key, value) pairs, reading a value when the loop reaches it; 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 iterates exactly when its elements all have one type: always so for a variadic tuple<T, ...>, and true of a fixed tuple<T1, …, TN> when T1 … TN are the same type, or are all int and real, when the loop variable is a value holding a number (for x in (1, 2.5), §5.6). A fixed tuple whose positions differ in type otherwise is not iterable — one loop variable cannot hold values of two types — so index it by a constant instead (§5.3), and the type_error says which property is missing rather than citing this rule. That refusal is about ELEMENT TYPES and never about termination: a fixed tuple’s length is a compile-time constant, which makes it the most obviously bounded iterand in the language. The tuple may be written without its brackets, as in Python: for x in 1, 2: iterates (1, 2), and for x in 1,: the one-element tuple, a trailing comma included. It is held to the same rules, and an element written with * spreads a collection into it, as it does in a bracketed tuple (§8.15), so for x in *a, 3: walks the elements of a and then 3. Any other iterand type is a type_error. The loop variable x carries the collection’s element type (§5.3) within the loop body, and stays bound after it (§6.1). So a for over a name that is already a variable assigns every element to that variable and is held to the rule for a re-assignment (§6.1): the element type must be the variable’s type, or give an empty list its element type (§5.1). After x = 1, the loop for x in ["a"]: would leave a string in an int variable. Python allows that and fails at the variable’s first use as an int; DKE Python refuses the loop itself, with a type_error that names it. 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). A counting loop is for i in range(n): — range (§8.6) returns a range, which the loop walks without building it, so a count costs no more to hold than its bounds.

An iterand whose element type nothing has supplied is iterable too, and the loop runs zero times, as in Python. That is [] or {} which no context refined (§5.1), a name bound only to one, and a collection or an iterator derived from one whose element is a tuple with such a position (enumerate([]), {}.items()). The loop variable then has no type, so what reads it cannot be checked, and is not: a statement that reads the loop variable, or a name bound from it, is not type-checked. An if whose condition reads it and a for whose source reads it lose only that expression, and their bodies are checked; a match on it is skipped with its arms. In a comprehension the same holds for a filter, the result, and a dict’s key and value (§8.9). Everything else in the body is checked as usual, and a target list over a tuple element must still match its arity (§8.11). No element is ever bound, so the loop leaves its variable as it found it.

The checker relies on those zero iterations, so a program where they may not hold is a type_error. They may not hold when the source reads a name and a loop around the iteration also gives an empty list, set or dict binding its element type, by a re-binding such as xs = xs + [1] or seen = seen | {1} (§5.1): on that loop’s next pass the source could hold elements. Declare the element type where the binding starts instead, as in xs: list<int> = [], seen: set<int> = set([]) or d: dict<string, int> = {}.

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.

A declared type. An annotated assignment (x: T = e), an argument for a declared parameter, a parameter’s default and a return agree with the type they declare when the value’s type IS that type or fills it. A bool fills an int, as in Python, where bool is a subclass of int, and an int or a bool fills a real. The value keeps its class: x: int = True binds True, and print(x) prints True. A tuple fills position by position, since nothing can change one, so (True, 2) fills a tuple<int, int>. A list, set or dict does NOT: a list<bool> does not fill a list<int>, because a collection is shared (§8.14), and a name holding it as list<int> could write a 5 where another name reads a bool. That is the variance mypy gives each. A written collection is held to the same rule where mypy would type it from the name it fills, so ys: list<int> = [True, False] is a type_error. A literal that holds an int beside its bools is a list<int> itself (§5.6). Where a program names an int without declaring one — an index, a slice bound or step, a repetition count, a string method’s count, width or bound, and the int arguments of range, enumerate, chr, round and int — a bool is taken as the int it is.

An annotation with no value binds nothing. x: int on its own line does nothing, in CPython and here, and x is still to be bound. ... alone on its line does nothing either, as pass does.

An expression alone is a statement. It runs, and nothing keeps its value, as in CPython, so what it would raise is raised and a store it would read is read and billed: alone, f() + 1 calls f, and an index past a list’s end stops the program. A construction alone, K("a"), reads its subject and keeps nothing.

Only a name is annotated. An annotation declares the type of the name it binds, so one written on any other target Python’s grammar reads, an attribute or an element, is refused at its :, with a value or without one: xs[0]: int = 1 is written xs[0] = 1. A name in parentheses is the name, so (x): int = 1 binds x. A target list, x, y: int or [x]: int = 1, is not annotated in Python either, and is a parse_error at its first target.

An annotation names a type. CPython reads any expression as an annotation and evaluates it. Here one that begins with a value no type begins with — x: 5 = 1, x: -int = 1, x: (int) = 1, def f(x: [int]): or def f() -> 5: — is a parse_error at its first token, in each place an annotation stands. It is a refusal, read past as CPython reads the expression, so a grammar error later on its line or below it is the answer.

A type may be written as a string. def f(x: "int") -> "K":, x: "int" = 1, n: "int" as a field and list["K"] read as the type the string spells, in names, dots, brackets and commas, and a run of strings reads as one. CPython keeps any string in that place and never reads it, so x: "a b" runs there. Here a name keeps the type it declares, so a string that spells no type is a parse_error at the string, in words saying so, and one naming no type this unit knows is told it as x: Nope is.

6.5 Name arguments

The name argument of a wire tool addresses what it names with identifiers, each identifier-shaped per §3.4: first codepoint XID_Start, remaining codepoints XID_Continue. A module is addressed by its bare name — by compile (MCP Reference §4.1) and the module tools (MCP Reference §9.4). A script, a rule or a constraint is addressed qualified, as module.name: its module’s name and its own, joined by a dot (MCP Reference §9.2, §9.3). The name is a name, not a string value; it denotes what it names, verbatim. A name of the wrong shape is refused, and nothing is compiled or removed.

6.6 Reserved-word constraint

A user identifier (declaration, class, method or field name, parameter name, loop variable, handler binding, assignment or unpack target, or a name a case pattern binds) MUST NOT be any of the reserved words in §3.7. 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.

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, it is a literal kind name and the path is a slot-grammar reference addressing the cell named by that kind and the following slot segments. This is the ordinary form — remember(K.s.a, 1, src), count(Order.customer), avg(Reading.value) — and it is why the kind position does not require a binding: a kind is a name in the store, and a program that names one need not have declared it.

An out-of-scope head is therefore not an error in the kind position, and IS one in expression position, where the first rule of this section applies and an unresolved identifier is a type_error. The classification is keyed on POSITION, and one consequence follows that is worth stating rather than discovering: a typo in a kind position is indistinguishable from a deliberate literal and cannot be diagnosed, so it writes to a cell nobody reads instead of being refused.

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 a declaration of the same compile unit, above or below the caller, or an already-stored script, and the unit compiles a callee before its caller, whichever is written first. A call that leads back to its caller is a type_error naming the cycle, so the same-unit call graph is acyclic (§9.7). A module’s own statement runs where it stands, so one that reaches a def below it, directly or through what it calls, is told name 'g' is not defined when the unit compiles, whether or not the program would reach that statement. Argument types are checked against the callee’s declared parameters at compile of the unit, and so is the argument count, unless a spread whose length is known only as the program runs stands among the arguments. The count is then checked as the program runs (§8.15).

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 return type, written or given by its returns, and naming a void script — or a script neither declared nor stored — 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, and a body whose returns give its type is read before a body that calls it.

6.9 Exhaustive return

A value script (§4.2) MUST return a value on every path through its body. A conforming implementation checks this conservatively: a suite definitely returns iff one of its statements definitely returns, what follows that statement never running, where

• a return <expr> definitely returns, and so does a raise;
• an if/else with a non-empty else definitely returns iff both its then and else suites do;
• a match with a case set (§6.2) definitely returns iff every arm does, and any other match iff, besides, one of its arms takes every value;
• a try definitely returns iff its finally does, or iff its body or its else does and every handler it has 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 (§4.2) 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, create_world, merge_world, discard_world, list_worlds, compare_worlds) are single snake_case tokens. They are soft keywords, as every verb’s word is (§3.7): recognized as a verb only immediately before (, so the same spelling remains a usable ordinary identifier elsewhere.

Keyword arguments. A verb takes the keyword arguments its row above writes, and no other. A keyword argument it does not take is a parse_error at the keyword that names the keywords the verb takes, or says it takes its arguments by position: current(K.s.a, a=1) names known_at=, and pin(K.s.a, a=1) says pin takes its arguments by position. A keyword argument the verb takes comes after the arguments it takes by position, and a call writes one. Written before them, it is a parse_error at the keyword that says they come first: remember(K.s.a, 1, qualifiers={}), which has no source, is one at column 20. Written after another keyword argument, it is a parse_error at the keyword that says the verb takes one keyword argument in a call: forget(K.s.a, recorded_before=t, valid_before=u) is one at column 34. Python reads such a call, so a grammar error later in it, or below it, is the answer instead (§10.1). A positional argument after a keyword argument is a grammar error, as it is in any call (§7): y = current(K.s.a, known_at=t, b) is a parse_error at column 33, the ).

Arguments by position. A verb takes as many arguments by position as its row above writes, and a fold (§7.1.1) and the literal factories (§3.5) as many as their forms write. An argument after them is a parse_error at that argument that says how many the call takes: y = current(K.s.a, t, u) is one at column 23, “current takes 2 positional argument(s) here, and this is one more”. A * or ** argument there may spread nothing, and is refused (§10.1). A call short of an argument it takes is a parse_error at its ) that says how many the call takes: remember(K.s.a) is one at column 15, “remember takes at least 3 positional argument(s), and this call gives 1”. Python reads such a call and leaves its arity to run time, so a grammar error later in it, or below it, is the answer instead (§10.1). len, isinstance and issubclass are built-in functions, and a count one does not take is answered as any built-in function’s is (§8.13).

A path argument. Where a verb’s row above writes a path (K.s.a, K.s, K.a or K), the path is the whole argument. An argument that goes on past a path as an expression is a parse_error at the argument that says so: y = current(K.s.a + 1) is one at column 13, “current takes a path here, and this argument goes on past the path as an expression — the path is the whole argument”. So is a call in the path’s place: y = current(f(x)) is one at column 13. An argument there that is no path at all is a parse_error at it that says what a path there wants: y = current("s") is one at column 13, “expected a path such as K.s.a”. An instance written where a path names one of its fields, without the field, is one where the field was wanted. Python reads such a call, so a grammar error in the argument, later in the call, or below it, is the answer instead (§10.1).

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. So is the world block (§9.2.9), where world is a soft keyword: recognised only immediately after with, and an ordinary identifier everywhere else.

Walking a derivation. dependents(c) returns the claims concluded from c, one step down, and premises(c) the claims c was concluded from, one step up: the claims the rule read, or the fields a computed field reads. The operand is a claim bound to a name — read with current or get, or an element of a proof_tree or of dependents — or a claim’s claim_id (§5.2), which names the claim whatever has been written since it was read; an operand that is neither is a type error. A claim_id that names no claim the store holds is refused (refuse, catchable), as is one that two claims share; a string that is not a claim_id is an error. An element of dependents is the dependent claim itself, so a chain can be walked a step at a time in either direction. dependents(c, transitive=True) goes the whole way down in one read: the claims concluded from c, the claims concluded from those, and so on, each listed once, in name order. It answers in full on every store, one where two conclusions each rest on the other included. transitive= is a keyword, takes a bool and is given at most once; transitive=False is the one-step read. Both verbs answer for the store as it stands. A claim someone recorded has no premises. A claim the store no longer holds is refused (refuse, catchable) by both verbs, whether it is passed as the claim or as its claim_id, as forget and would_forget refuse it (§10.3). That covers a conclusion withdrawn since it was read, and one a known_at= read worked out again, which the store never recorded. An empty answer there could not be told apart from a recorded claim’s true lack of premises. A conclusion whose validity window does not cover the present still names its premises: they are read at a time inside its window. Where two rules conclude different values at one cell, each claim answers its own premises.

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, datetime("…")) yields the single value active then, get(K.s.a, datetime("…")) the claims valid then, and why(K.s.a, datetime("…")) 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, datetime("…")) the subjects of the kind, list_values(K.a, datetime("…")) the values at the attribute, list_attributes(K.s, datetime("…")) 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.

Reads as of what the store knew. The same six reads accept one keyword argument, known_at=, a datetime naming a moment on the other time axis: not when a fact was true of the world, but what the store had been told by then. get(K.s.a, known_at=datetime("…")) returns the claims the store held at that moment. A claim written later is not among them, and a claim later revised or replaced is, with the standing it had then, so a disagreement the store held at that moment reads as one, and current refuses over it as it does over a disagreement now. why and the three enumerations answer the same way. The positional time and known_at= are independent and may be given together: current(K.s.a, datetime("T1"), known_at=datetime("T2")) is the value the store, as of T2, held to be in force at T1. A read without known_at= answers over everything the store holds now, and one whose known_at= is later than every write answers the same.

forget is retroactive: what was forgotten was never known, as far as any read can tell. A conclusion is answered as it stood at that moment: what the rules, as they read then, concluded from what the store had been told by then, including a conclusion withdrawn since and leaving out any that only a rule written later concluded. A conclusion in such an answer may carry an empty .created_at, since when it was recorded is not kept once what it rests on has changed. The read refuses, catchably, in three cases (§10.3). The answer rests on a rule that was changed after that moment, or on one whose text at that moment the store holds no record of, so its text then is not known; the reason is derived_field, and the remedy is to read without known_at= or as of a moment after the change. A rule whose earlier text the store holds no record of takes part once it is compiled again, unchanged, for a read as of any moment from then on. Or a value the answer rests on, at the address or at one a rule reads to reach it, was replaced by one that has since been forgotten, so when it stopped being in force is no longer recorded; the reason is not_recorded. Or the answer rests on more of the store than a read as of an earlier moment may work over; the reason is limit_exceeded, and the same read over the same data refuses the same way every time.

A read that finds nothing says why, when the reason is an import. A read naming a kind the store does not know refuses (§10.3). Where a missing import is the reason, the refusal says so instead, in the two cases one produces. This holds for current, get, subjects and the list_* reads, and for forget, which a missing import would otherwise turn into a removal of nothing that reports success:

• 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 a read of a kind that exists still answers empty, or a collection with no elements, where that kind holds nothing; and a name no module declares refuses as a kind the store does not know (§10.3), naming no import.

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 (Python 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. The same holds for an address: list_pinned() names each pinned cell in the form pin and unpin take, so an address it returns, written back into unpin, lifts that pin.

list_attributes(K) and list_categories() take no as-of argument, because neither answers about an instant. The first gives the attribute names recorded for a kind and the second 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 — datetime("2024-…"), null is valid from 2024 onward with no end, and null, datetime("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 model a value that changed over time, whether one source writes both or two sources write one each. Where a window overlaps one the same source already gave at the cell, remember refuses a second value, and refuses the same value too unless the window is the same: moving a window is a revision, which is update’s. update supersedes only that source’s claims whose windows overlap the new one (§7.5).

Qualifiers. remember and update accept one keyword argument, qualifiers=: a dict (§3.5.12) from name to value stating facts the writer wants the claim to carry about itself — remember(K.s.a, v, src, qualifiers={"method": "observed", "confidence": 0.8}). It follows every positional argument, the window included, and is keyword-only because the positions after the source are the window’s. Each name is a name in the sense a path segment is — it starts with a letter or _ and continues with letters, digits, _ or - — and each value is one value a claim could hold: a string, int, bool, real, datetime, duration, blob, scientific or complex. A claim carries at most 16. An empty dict writes none. They are read back through the claim’s qualifiers field (§5.2).

A claim’s qualifiers are written with it and stay with it. The same source restating the same value with the same qualifiers is an ordinary no-op restatement; restating it with different qualifiers is refused as a conflicting write (§10.3), exactly as restating a different value is, and update is how a source revises its claim — value, qualifiers or both.

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, blob, scientific or complex — 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 claim can also be named by the claim itself: forget(c) removes the one claim c and leaves every other claim at its cell standing. The operand is the one dependents takes — a claim bound to a name, read with current or get or bound as an element of what they return, or a claim’s claim_id (§5.2). It tells apart the two claims the value-and-source form cannot: one source’s value recorded for two periods is two claims with one value and one source, and forget(K.s.a, v, src) removes the first of them, while get(K.s.a, datetime("…")) at an instant inside the second period returns the claim that forget then removes alone. The claim is looked for in the store as it stands. A claim removed since it was read, or written inside a branch that rolled back, is refused (refuse, catchable), as is a claim_id two claims share, and nothing is removed; a superseded claim is still recorded and is removed like any other. The claim is the whole address, so nothing follows it, and a claim’s field in the place of a path, forget(c.claim_id), is a compile error naming forget(c).

A fourth form is time-scoped: forget(K.s.a, datetime("…")) 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=datetime("…")) 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=datetime("…")) 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. With an address the bound is required; there is no bare form. would_forget(c) previews forget(c): it returns 1 while the store holds the claim, and refuses as forget(c) would when it does not.

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, as forget(c) removes the claim c; forget(K.s.a, datetime("…")) removes the values in force at that instant and leaves the rest. Nothing is retained in history that a read can reach, and nothing in this language reinstates what it removed. Removal means what it says.

One qualifier, and it is not part of this language: while a checkpoint stands, a removed value stays recoverable outside every read, so the restore tool of the MCP Reference can bring it back: a value that was in force as a new claim at the current instant, and an older version into the history where it stood. That is a re-assertion and not a rewind — the removal still happened and the claim was still reclaimed. With no checkpoint standing at the moment of removal, nothing is kept.

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. Compiling a module the store holds removes what an earlier text installed and this one no longer declares — a def, a method, a rule, a computed field or a constraint (Python Reference §9.5) — and that is a removal too. Under a read-write key such a compile is refused with scope_forbidden before any statement runs: the answer names what would go, and the store is left as it was. A compile that removes nothing, changes a declaration in place or drops only the module’s body is an ordinary write.

Adding without revising takes the read-add grant. A key scoped read-add reads, and writes only what adds to the store: a value where none is in force, a restatement of a value its source holds, a value from a source that holds none there, and an assert where nothing is recorded. An update over a value its own source holds is a revision, whether it changes the value, the window or the qualifiers, and it is refused when it runs, with scope_forbidden. The program ends at that statement, try does not catch the refusal, and what the program wrote before it is kept. Committing a branch is refused in the same way when the commit would replace a value the store holds, and the branch stays open. What a standing rule concludes from an added fact changes as it does under any key. A read-add key cannot remove, cannot pin, unpin, prefer or unprefer, cannot restore a checkpoint or drop one, and cannot compile over a module the store holds; each of these 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.

Script data in a program. list_scripts() executes from inside a program and returns the stored script names as a string_list. Forgetting a script and reading its metadata are the wire’s forget and info tools (MCP Reference §9.2), not statements of a program body. The service stores no source text, so there is no source-readback verb.

7.2 Slot validity

Slot identifiers (kind, subject, attribute) are strings under §3.4 (UAX #31); a source is a label rather than an identifier (§7.3). 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), a blob literal (§3.5.8), a scientific literal (§3.5.14), or a complex (§3.5.15). 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, remember(K.s.a, blob("48656C6C6F"), src) stores a blob, and remember(K.s.a, scientific("1.5e3"), src) stores a scientific, and remember(K.s.a, 3 + 4j, src) stores a complex. 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, real and bool 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, verify(K.s.a, 5) matches a stored 5.0, and subjects(K.a, 1) selects a subject holding True, as True == 1. 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. This is what makes a query verb and a rule premise answer “which subjects have K.a == 5” the same way (§14.2). datetime, duration, real, blob, scientific and complex are not query-slot types: 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 store 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.

A source is a label, not an identifier: any non-empty text naming where the content came from — a citation ("2026 finance act"), a register, a URL. It is stored and read back exactly as written, with no normalization, so two texts that differ in any character are two sources: "2026 finance act" and "2026-finance-act" are not one, and agreement counts them twice.

A source MUST NOT be empty, and MUST NOT hold one of the few characters the implementation reserves. A literal source that breaks either rule is a type_error. One that arrives at run time — from a parameter, a row, a computed expression — is a refuse (§10.3), so a loader can catch it per row and keep the rest. Either refusal names its fault; a reserved character is named by its code point (U+XXXX) and byte, never echoed back.

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.
• update revises the writing source’s own claim. update(K.s.a, v, src) supersedes the claims src holds at K.s.a whose windows overlap the new one, and no other claim. A value another source holds there stands beside the new one, so a revision never settles a disagreement (§7.6); to replace another source’s value rather than stand beside it, remove that claim with forget(K.s.a, v, src). A superseded claim stays readable through get and why. Restating exactly what src holds there — the same value, the same qualifiers and the same window — writes nothing. The same value over a different window that overlaps the old one is a revision, and the new window is the one in force. A claim src holds in a window the new one does not overlap stands, so one source records a value that changed over time by writing each period with update.
• update inside a branch or world block revises a claim src recorded before the block as it would outside one. Inside the block that claim no longer reads, at any instant, and a later remember there is judged against the new claim. The earlier claim itself is not changed: a rollback, or leaving a world, leaves the store as it was (§9.2.5, §9.2.9), and a commit or a merge leaves it as the same update written outside the block would. Of two such claims the later stands, in the block as after the commit or the merge: where the store is revised after a world wrote, the store’s revision reads in the world in place of the world’s own. What the store’s rules concluded from the earlier claim, and anything concluded from that in turn, no longer holds inside the block either, as after the commit or the merge; the store keeps it. A conclusion the rules still reach from what the block reads holds there as it would outside.
• A fact written inside a branch or world block where the store’s rules concluded something from that fact’s absence: the conclusion, and anything concluded from it in turn, no longer holds inside the block, as after the commit or the merge. The store keeps it, so a rollback, or leaving a world, reads it again (§9.2.5, §9.2.9).
• pin protects. At runtime, forget(K.s.a) at a pinned location refuses, and so does forget(K.s) for the subject above it and every removal of one claim there, forget(c) included, until unpin(K.s.a) lifts the pin (§10.3).
• pin, unpin, prefer and unprefer never change nothing. Each refuses a call that names something the store does not hold — pin or prefer at a location with no value, prefer naming a source that recorded no value there, unpin or unprefer where there is neither the mark it lifts nor a value — with the reason not_recorded. Each refuses a call asking for a state that already holds — a location already pinned, or not pinned, a source already preferred, no preference standing there — with the reason already_in_effect. A program making sure of a state catches that one and carries on. unpin and unprefer lift any pin or preference that stands, whatever the location holds now.
• 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(c) removes the claim c a read returned, which is how one of two claims with one value from one source is chosen. forget(K.s.a, datetime("…")) 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, whether the second is written with remember or with update: update revises only its own source’s claim (§7.5). 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.
• The two sides are never one recorded value and one derived value. A disagreement is between two recorded values, or between two values rules derived. A field a rule or computed field derives cannot also be written (§13.7, §14.3), so a recorded value is never added beside a derivation at one location.
• A disagreement ends when the claims change. forget one of them, or have one source update its claim to the value the other holds, 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 names a source that is there. prefer(K.s.a, src) refuses at a location holding no value, and when src recorded no value at that location — a preference over nothing is a mistyped address or source, not a judgment (§7.5). A location with one value is not in disagreement, and you may still prefer its source there.
• 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 — which may be the same source again: stating it over the new set is a new judgment, and is refused as already in effect only while the preference still covers every source there. 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.

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). A complex has no order: <, >, <= and >= with one on either side is a type_error, stated as Python states it ('<' not supported between instances of 'complex' and 'int'), and so is everything that ranks its operands — sorted, min, max, a list or tuple ordered against another. Compare one with == and !=, or order by a part or the magnitude: sorted(zs, key=abs). Comparisons chain (a < b < c is (a < b) and (b < c) with b evaluated once, §4.6).