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 the reference compiler emits internally is conforming as long as the observable behaviour matches: same input source plus same target store plus same arguments produces a transcript with the same shape and the same status discriminators across statements.

The conformance keywords MUST, MUST NOT, SHOULD, SHOULD NOT, and MAY in this document carry their RFC 2119 meanings.

1.2 Relationship to DKE

DKE Python is the contract between a tenant and the DKE service. The import/store/invoke lifecycle described in §11 is the wire-visible behaviour of the service. 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 a draft of the DKE Python Spec. 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), log(msg). The natural-language phrase form shared with the base member (remember K.s.a = v per src, current K.s.a) is an accepted alternative (§4.5); the two compile to the identical program.
• Bare assignment binds a read. cur = current(K.s.a) — there is no let introducer.
• match / case. Discrimination is spelled match <expr>: with case <discriminator>: arms (where the base member uses when).
• try / except … as. Handled blocks use Python’s except <kind> as <var>: shape.
• Script invocation is a plain call. audit_subject(K, s) — there is no invoke keyword (the wire-surface verb invoke <name>(<args>), §11.2, is unchanged).
• 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.
• The reference compiler’s error message text (only the error category is normative; message strings are quality-of-implementation).
• Operational characteristics: performance, latency, quotas, throttling.

1.5 Independence from a live service

This specification is forward-looking: it defines the conformance contract for any implementation of DKE Python and for the reference target service at dke.langsyn.net, independent of whether a given target service is reachable when this document is read.

Parser/checker conformance (§13.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 §13.2. Compiler/runtime conformance (§13.1) is claimed against whichever target service an implementation connects to.

3.1 Source encoding

DKE Python source MUST be valid UTF-8. A conforming implementation MUST reject ill-formed UTF-8 sequences with a parse_error that names the offending byte offset (and SHOULD name the invalid byte).

3.2 Whitespace, line terminators, and the off-side rule

DKE Python is indentation-significant. Line feed (U+000A) and the carriage-return / line-feed pair both end a source line. A block is introduced by a header line ending in : and is delimited by indentation:

def f(K: string):
    <statement>
    <statement>

• Indentation is measured in spaces; a tab in indentation is a lexical error (parse_error).
• A deeper indent opens a nested block (the lexer emits INDENT); returning to a shallower level closes as many blocks as needed (DEDENT). An indent that matches no open level is a parse_error.
• Blank lines and comment-only lines do not affect block structure.
• Inside ( and [, newlines are not significant: a bracketed expression may span lines.

3.3 Comments

A # begins a comment that runs to the end of the line. Comments are equivalent to whitespace and do not affect block structure.

3.4 Identifiers

DKE Python identifiers follow Unicode UAX #31 with the standard profile:

identifier := XID_Start XID_Continue*

An identifier starts with any codepoint having the XID_Start property (Latin letters, æ ø å, CJK ideographs, Arabic, Hebrew, Devanagari, Hiragana, Katakana, Hangul, Cyrillic, Greek, the _ underscore, and many more) and continues with any XID_Continue codepoint (the above plus decimal digits and combining marks).

A conforming implementation MAY approximate UAX #31 with block-level ranges covering at least the languages DKE serves at the natural-language tier. Identifiers are case-sensitive: Cat, cat, and CAT are distinct.

3.5 Literals

string-literal := '"' string-char* '"'
string-char    := any UTF-8 codepoint except '"', '\', and newline
                | '\\'                   # backslash
                | '\"'                   # double quote
                | '\n'                   # line feed        (U+000A)
                | '\t'                   # horizontal tab   (U+0009)
                | '\r'                   # carriage return  (U+000D)
                | '\x' hex hex           # one byte, two hex digits
                | '\u' hex hex hex hex   # one codepoint ≤ U+FFFF, UTF-8 encoded
hex            := '0'..'9' | 'a'..'f' | 'A'..'F'

int-literal := dec-int | hex-int | oct-int | bin-int
dec-int     := dec-digit ( '_'? dec-digit )*
hex-int     := '0' ( 'x' | 'X' ) hex-digit ( '_'? hex-digit )*
oct-int     := '0' ( 'o' | 'O' ) oct-digit ( '_'? oct-digit )*
bin-int     := '0' ( 'b' | 'B' ) bin-digit ( '_'? bin-digit )*

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

datetime-literal := 'datetime' '(' '"' rfc3339-utc '"' ')'
rfc3339-utc      := date 'T' time frac? 'Z'
date             := dec-digit dec-digit dec-digit dec-digit '-'
                    dec-digit dec-digit '-' dec-digit dec-digit   # YYYY-MM-DD
time             := dec-digit dec-digit ':' dec-digit dec-digit
                    ':' dec-digit dec-digit                       # HH:MM:SS
frac             := '.' dec-digit{1,9}          # 1..9 fractional-second digits

duration-literal := 'duration' '(' '"' iso8601-duration '"' ')'
iso8601-duration := 'P' days? ( 'T' hours? minutes? seconds? )?   # at least one term
days             := dec-digit+ 'D'
hours            := dec-digit+ 'H'
minutes          := dec-digit+ 'M'
seconds          := dec-digit+ 'S'

real-literal := dec-digit ('_'? dec-digit)* '.' 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 | '+' | '/' | '='

3.6 Operators and punctuation

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

The token = appears in bare assignment (§4.3), in the verb write phrase (remember K.s.a = v per src, §7), and in the class field-write statement (§14.3). The token : ends a block header and separates a parameter or field name from its type. Newlines terminate simple statements (§3.2); there is no ;. The word forms and / or / not are the logical operators (§8.2); there are no && / || / ! tokens.

3.7 Reserved words

The following identifiers are reserved and MUST NOT be used as user identifiers (declaration names, parameter names, loop variables, handler bindings, assignment targets):

(a) Structural keywords

def   class   return
match   case   if   else   for   in
try   except   as
branch   commit   rollback

(b) Logical operators

and   or   not

(c) Built-in

log

(d) Boolean literals

True   False

(e) Verb surface vocabulary. The verb head-words and prepositions of the shared verb phrases (§7) — remember, update, forget, assert, pin, checkpoint, restore, verify, current, get, why, caveats, dependents, conflicts, diff, subjects, list, categories, attributes, values, result, types, checkpoints, pinned, scripts, source, compile, of, where, since, per — are recognised in verb position. Programs SHOULD NOT use them as user identifiers. (compile is reserved by the service and is not available as a user identifier; like forget script and info script it is not executable inside a program body.)

A conforming implementation MUST treat the (a)–(d) identifiers as reserved at the lexical level. Contextual relaxation for dotted field access. After a . in a path expression, an identifier-shaped token is parsed as a field name (permitting claim.source, claim.value, and similar even though source is a verb-surface word); whether the field is meaningful for the base type is decided by the typechecker (§6). The type names of §5.5 (string, int, claim_list, …) are contextual identifiers, not reserved words; programs SHOULD nonetheless avoid them as user identifiers.

3.8 Token classes

3.9 Natural language

The natural language a source is written in — which keyword vocabulary its statements use, and the language its responses are rendered in — is set out of band, by the language parameter supplied when a source is submitted, not by the source. When the parameter is omitted, the language is English (eng).

eng is the default and, at this time, the only offered value; a request for another natural language is declined. The parameter is the forward-compatible surface for additional natural languages, which are not offered today.

A program’s meaning is independent of the language it is written in: the same program in any supported keyword vocabulary denotes the same thing. The natural language is therefore a property of how you are talking to the service — set per call — not a property stored in the program. A source has no header line and does not declare its natural language in-band.

4.1 Programs

source       := option-verb NEWLINE | module-body
module-body  := top-item+
top-item     := decl | class-decl | rule-decl            # decl §4.2, class-decl §14.1, rule-decl §15
              | import-stmt | statement                  # import-stmt §4.3, statement §4.3 (incl. the four writes) — see §17
option-verb  := '--' IDENT IDENT?

A source has no header line: it is the module body (§17) from its first line. Its body admits, at the top level, not only declarations but also import statements (§17.3), data declarations (write statements at module scope, §17.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 (§17.1); a file whose body is exactly one def is the common single-script case.

The natural language the source is written in — the language of the knowledge it names and of its authored text — is set out of band (§3.9), not in the source; it also selects the language in which the script’s own structured output — its invocation transcript (§11.2) — is rendered. It does not select the response language of the surrounding service surface, which remains a property of the calling channel; the two may differ.

Option verbs. A ---prefixed word in declaration position is an option verb — a compiler-directed verb, addressed to the implementation rather than the store. An option verb’s spelling involves no language keyword, so --help means the same thing in every context. The supported set is --help (§4.2), which takes an optional topic word; an unknown option verb is a parse_error whose diagnostic names the supported set. An option verb never compiles and never stores anything, by construction.

A source file may declare one or more scripts — a compile unit. Every declaration compiles and stores under its own name, in declaration order. Declaration order is compile order: a declaration may call only an EARLIER declaration of the same unit or an already-stored script (§6.8, §9.7, compile-before-call). Two declarations in one unit MUST NOT share a name. A unit need not declare a script at all: a module whose body only installs a schema, defines a rule, or writes data is valid (§17.1, §17.7).

A unit with an empty body — whitespace and comments only — is a parse_error. Except where an example shows a complete compile unit, program examples elsewhere in this document are fragments: a fragment omits the surrounding program scaffolding for brevity.

4.2 Declarations

decl    := 'def' IDENT '(' params? ')' ':' NEWLINE INDENT stmt+ DEDENT
params  := param ( ',' param )*
param   := IDENT ':' type-name

A declaration is the def keyword, a name, a parenthesised parameter list, a :, and an indented suite. A parameter is name: type where type-name is one of the type names enumerated in §5.5 — a primitive (string, int, bool) or a read-result type such as claim_list or handle. (empty names the absent arm of a match and is never a parameter type.) The declared objects are called scripts (§11’s wire verbs address them as such).

--help is the teaching option verb (§4.1) — the in-band way to learn the language from inside it. Bare --help yields the orientation lesson: the declaration shape, one complete example, and the topic index. --help <topic> yields one topic’s lesson; the topics are header, types, verbs, statements, and scripts. The lesson language follows the language parameter (§3.9). An unknown topic is a parse_error whose diagnostic names the topic index.

--help types

A unit whose body is a help form never compiles and stores nothing; on the wire it is classified parse_error, and its diagnostic message is the lesson. A conforming implementation whose surface faces a human directly (such as a CLI) SHOULD present the lesson without error framing and report success — asking for help is not a mistake.

4.3 Statements

A statement is either a simple statement, ending with a NEWLINE, or a block statement (if / for / match / try / branch), whose body is a :-headed indented suite.

stmt         := simple-stmt NEWLINE
              | block-stmt

simple-stmt  := assign-stmt
              | field-write-stmt
              | log-stmt
              | call-stmt
              | verb-call-stmt
              | commit-stmt
              | rollback-stmt
              | import-stmt

block-stmt   := match-stmt
              | for-stmt
              | if-stmt
              | try-stmt
              | branch-block

assign-stmt      := IDENT '=' expr
field-write-stmt := IDENT '.' IDENT '=' expr 'per' expr        # class field write, §14.3
log-stmt         := 'log' expr
call-stmt        := IDENT '(' arg-list? ')'
verb-call-stmt   := verb-phrase                                # see §4.5, §7
commit-stmt      := 'commit'
rollback-stmt    := 'rollback'
import-stmt      := 'import' module-name                       # load a module, §17.3
module-name      := IDENT ( '.' IDENT )*

match-stmt   := 'match' expr ':' NEWLINE INDENT case-clause+ DEDENT
case-clause  := 'case' IDENT ( 'as' IDENT )? ':' ( simple-stmt NEWLINE | NEWLINE INDENT stmt+ DEDENT )
for-stmt     := 'for' IDENT 'in' expr ':' NEWLINE INDENT stmt+ DEDENT
if-stmt      := 'if' expr ':' NEWLINE INDENT stmt+ DEDENT
               ( 'else' ':' NEWLINE INDENT stmt+ DEDENT )?
try-stmt     := 'try' ':' NEWLINE INDENT stmt+ DEDENT handler*
handler      := 'except' 'refuse' 'as' IDENT ':' NEWLINE INDENT stmt+ DEDENT
             | 'except' 'engine_error' 'as' IDENT ':' NEWLINE INDENT stmt+ DEDENT
branch-block := 'with' 'branch' '(' STRING ')' ':' NEWLINE INDENT stmt+ DEDENT

arg-list     := expr ( ',' expr )*

A bare assignment (assign-stmt) binds one name to an expression result; there is no let introducer, and the right-hand side MUST NOT be a statement-only verb (§7.4). A call statement whose head identifier is not a verb head-word is a stored-script invocation — the plain-call spelling of what the wire surface writes as invoke <name>(...). Resolution follows the compile-before-call rule (§6.8, §9.7).

Each case arm of a match may be an inline statement or an indented suite; the arms must be exhaustive over the scrutinee’s discriminator (§6.2). The optional as IDENT on a case label binds the matched content and is well-typed only on a value-match arm (§5.6, §6.2); elsewhere it is a type_error. Both try handler clauses are optional, in the fixed order shown (except refuse before except engine_error). 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 (§17.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.

4.4 Expressions

expr         := or-expr
or-expr      := and-expr ( 'or' and-expr )*
and-expr     := cmp-expr ( 'and' cmp-expr )*
cmp-expr     := add-expr ( cmp-op add-expr )*
cmp-op       := '==' | '!=' | '<' | '>' | '<=' | '>='
add-expr     := mul-expr ( ( '+' | '-' ) mul-expr )*
mul-expr     := unary-expr ( ( '*' | '/' | '%' ) unary-expr )*
unary-expr   := ( 'not' | '-' ) unary-expr
              | postfix-expr
postfix-expr := primary-expr postfix*
postfix      := '.' IDENT '(' arg-list? ')'   # method call (§14.4)
              | '.' IDENT                      # field access
              | '[' expr ']'                   # indexing
primary-expr := STRING | INT | 'True' | 'False'
              | IDENT '(' expr ')'             # instance constructor (§14.2)
              | IDENT
              | path-expr
              | '(' expr ')'
              | verb-phrase                    # see §4.5
path-expr    := IDENT ( '.' IDENT )+           # K.s.a slot-grammar dotted path

Prefix - (unary minus) is an int → int operator; its runtime semantics are 0 - a (§8.3), so negating the most-negative integer overflows and refuses rather than wrapping. The boundary between path-expr (a multi-segment dotted reference to a store cell) and postfix-expr with .field chains (field access on a value) is resolved by the typechecker (§6) using the type of the head identifier. The comparison operators do not chain grammatically (§4.6); a < b < c is not well-formed and must be written a < b and b < c.

4.5 Verbs

The built-in verb surface (§7) is written as function calls — a verb name and a parenthesized, comma-separated argument list: remember(K.s.a, v, src), current(K.s.a), list_attributes(K). The first argument is the dotted K.s.a slot path (or a name literal / handle, per the verb). Read verbs produce a value and may stand in expression position (bound by assignment or composed with operators); write verbs have no value and stand only as statements.

Representative forms, as they read in a program:

remember(K.s.color, "orange", "op1")          # write: (path, value, source)
update(K.s.color, "black", "op1")
forget(K.s.color)                             # path-scoped
assert(K.s.nickname, "op1")                   # absence assertion: (path, source)

cur   = current(K.s.color)                    # reads
hist  = get(K.s.color)
proof = why(K.s.color)

attrs = list_attributes(K)                    # K or K.s
subs  = list_subjects(K.color)
vals  = list_values(K.color)
hits  = subjects(K.color, "orange")

h       = checkpoint("pre_audit")             # name literal → handle
changed = diff(K.s.color, h)
deps    = dependents(h)
restore(h)

v = verify(K.s.color, "orange")               # optional: verify(K.s.a, v, src)

Natural-language phrase form (accepted alternative). The same verbs may also be written as natural-language phrases — a head-word, the slot path, and where needed the prepositions of / where / since / per (remember K.s.color = "orange" per "op1", current K.s.color, list attributes of K, checkpoint pre_audit). The two forms are interchangeable and compile to the identical program; the call form is the canonical surface and a source may mix both. §7.1 lists both spellings per verb.

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

Lowest to highest precedence; all binary operators are left-associative.

Comparison operators do not chain: a < b < c is not well-typed (the bool result of a < b fails the numeric-operand rule of §8.1). Combine with and instead (a < b and b < c).

5.1 The 17 types

The five finite collection types are exactly the types that may appear as the iterand of a for … in (§6.3). Three of them (subject_set, string_list, result_type_set) yield string elements; claim_list and proof_tree yield active_claim elements. A proof_tree is the collection of claims that participated in a why derivation — iterating it (or reading .length / [i], §5.3) yields those claims, each an active_claim carrying the same fields a claim_list element does (.value, .source, .trust, .created_at); a proof_tree additionally offers a .root accessor naming the queried claim (§5.2). match is meaningful over the discriminator types (active_claim with its empty case, and verify_result) and over the value tagged union, which a match destructures by the class of the stored content (§5.6, §6.2).

empty is never produced standalone; it is the second case of an active_claim discriminator. The typechecker recognises empty as a valid case label on an active_claim scrutinee, not as a standalone expression.

value (§5.6) is not a user-composed type — it is the single built-in union, carrying whichever primitive a claim’s content happens to be. There is still no subtyping, no generics, and no user-defined types.

The 17 types do not include an absence-of-value type. Absence is asserted through the assert verb (§7.1), which carries no value argument — so the absence semantic stays implicit in the verb head-word rather than being represented as a typed value.

5.2 Field access

The expression <value>.<field> is well-typed when the table below has a row for the value’s type and field; otherwise it is a type_error.

claim_id is a positional descriptor, not a persistent identity: the claim’s cell path followed by # and its 1-based position in the result that produced it (a get element reads Cat.felix.color#2); a claim obtained through current carries the designator current in place of a position. claim_id is not stable across mutations of the cell; programs that need a claim’s content use .value and .source.

created_at is the claim’s creation moment: the UTC wall-clock instant at which the claim was recorded, rendered as an RFC 3339 timestamp with microsecond precision and a literal Z suffix — e.g. 2026-07-04T09:15:42.123456Z. The value is fixed when the claim is created and is the same string no matter how the claim was obtained (current and get agree). A claim recorded before the service began stamping creation moments carries the empty string. Lexicographic comparison of two non-empty created_at values orders them chronologically (RFC 3339 UTC is sortable).

Universal accessors:

• <expr>.kind returns string for any discriminator value (active_claim, empty, verify_result, and the try-handler discriminators of §5.4) and for proof_tree. The returned string is the type name as written in §5.1.
• <expr>.length returns int for any string or any finite collection.

5.3 Indexing

The expression <value>[<int>] is well-typed when the value is a finite collection; the result type is:

Indexing out of bounds is a runtime refuse (§10.3), not a static error. The index expression MUST be of type int.

5.4 Try-handler discriminator types

A try statement’s except handlers each introduce one bound identifier, carrying a discriminator type the user cannot write as a type annotation:

• except refuse as r — r has fields reason, teaching_hint, discriminator, all of type string. r.kind returns the literal string "refuse_info".
• except engine_error as e — e has fields reason, code, both of type string. e.kind returns the literal string "engine_error_info".

These types are produced only by their corresponding handlers; they cannot be passed as parameters, returned by verbs, or written in a type annotation.

5.5 Type names in source

Eleven type names are valid as type-name tokens — in parameter annotations (§4.2) and as the field type in a class field declaration (§14.1): the three primitives (string, int, bool) plus the eight non-primitive types from §5.1 (active_claim, claim_list, proof_tree, subject_set, string_list, handle, verify_result, result_type_set).

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 datetime (§5.6) names a value class; a datetime arises from a datetime("…Z") literal (§3.5.5) or a case datetime as <var>: match arm (§6.2) and is likewise NOT writable as a type-name token. The names duration, real, and blob (§5.6) are value classes in the same way — each arising from its literal (duration("…") §3.5.6, 3.5 §3.5.7, blob("…") §3.5.8) or a case <class> as <var>: arm — and are likewise NOT type-name tokens. Type names are contextual identifiers, not reserved words (§3.7).

5.6 The value union

The .value field of an active_claim (§5.2) has type value: the stored content of a claim, carrying its own type. A value written as an integer reads back as an int; a value written as a boolean reads back as a bool; a value written as text reads back as a string; a value written as a datetime("…Z") datetime literal (§3.5.5) reads back as a datetime; a value written as a duration("…") duration literal (§3.5.6) reads back as a duration; a value written as a 3.5 real literal (§3.5.7) reads back as a real; a value written as an blob("…") blob literal (§3.5.8) reads back as a blob. The type is a property of the claim, fixed when the claim is recorded, and is the same however the claim is obtained (current and get agree, as for every other field).

value is a tagged union over its value classes:

value  =  int | bool | string | datetime | duration | real | null | blob

Seven of the eight classes are write-producible from DKE Python — a program writes an int, bool, string, datetime, duration, real, or blob and reads it back at that class. The remaining class, null (an explicit absent value), is read-only: it is asserted through the assert verb (§7.1), which carries no value argument, so no value literal produces it — but a claim carrying one is discriminable on read (see below).

A program consumes a value in one of three ways:

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

  c = current(Sensor.room.count)
  match c.value:
      case int as n:      log("next = " + (n + 1))     # n : int — arithmetic is well-typed
      case bool as b:     log("flag = " + b)           # b : bool
      case string as s:   log("text = " + s)           # s : string
      case datetime as d: log("time = " + d)           # d : datetime — renders RFC 3339
      case duration as u: log("span = " + u)           # u : duration — renders ISO 8601
      case real as r:     log("value = " + r)          # r : real — renders decimal
      case blob as b:     log("bytes = " + b)          # b : blob — renders hex
      case null:          log("an absent value")       # detect-only — no `as` binding

  A write-producible class (int, bool, string, datetime, duration, real, blob) supports a named case <class> as <var>: arm that binds <var> to the content at the arm’s class type, scoped to that arm, so arithmetic and other type-specific operators apply without a cast. This is the only way to recover an int (for arithmetic), a bool (for logical operators), or a datetime / duration / real / blob (to render or re-store, §8.4) from a claim’s content.

  The one read-only class, null, is written as a bare case null: arm — it discriminates the class but binds no payload; attaching as <var> to it is a type_error (an absent value has no content to bind).

• Render it directly. A value is expressible: log <value> appends its textual rendering (§8.7), and string concatenation coerces it ("count=" + c.value → string, §8.4). Rendering never requires knowing the class.

• Compare it with == / != against a scalar literal or another value (§8.1). The result is always bool; a class mismatch compares unequal rather than coercing (c.value == 41 is false when the content is the text "41").

A value match covers the eight named classes above, or any subset of them plus a case default: catch-all (§6.2). case default: keeps a match well-defined without enumerating every class, and also covers any class the service might add beyond this set in a later revision. A value cannot be written in a type annotation (§5.5) and is never constructed by a program — it arises only from reading a claim.

6.1 Scoping

DKE Python is lexically, function-scoped for variables. An assignment x = <expr> binds x in the enclosing script body, not in the :-headed suite that contains it: an assignment inside an if, for, match, except, or branch block updates the enclosing binding and its value persists past the block. A for loop body may therefore accumulate into an outer variable, and an if branch may conditionally reassign one. A re-assignment MUST keep the variable’s type — assigning a value of a different type to a name already in scope is a type_error (§6.4); a same-type re-assignment is permitted. A name first introduced inside a block is visible within that block and its nested blocks; to read a variable after a block, bind it in an enclosing scope first. Script parameters are in scope for the entire body.

Two bindings are block-local and do not leak past their block: the for loop variable and the except handler variable. Each is visible only within its own block; when the block ends the name is restored to whatever it held beforehand, or becomes unbound if it was not previously bound. match case clauses do not bind a new name; the scrutinee’s binding (if any) stays visible inside every case body.

A branch block rolls back the store on abort (§9.2.5), never variable bindings: a variable assigned inside a branch keeps its value whether the branch commits or rolls back — variables are not transactional.

A path segment that names an in-scope variable (current(k.s.a) with k, s parameters) is resolved to that variable’s value; a segment that is not an in-scope name at the point of the call is a literal kind/subject/attribute name. Because this is decided from lexical scope, a variable never captures a same-named literal segment introduced later — but a variable that shares a name with a literal attribute you address in the same scope will shadow it, so avoid naming a variable after an attribute you path into.

6.2 Match exhaustiveness

A match statement’s case clauses MUST cover the case set of the scrutinee’s type:

Any other scrutinee type is a type_error — except a bare instance variable, whose match is the distinct class match construct (§14.5), dispatching over class names. A missing case is a type_error (bad-nonexhaustive-match); a case label not in the set is a type_error; a repeated case label is a type_error. Case order is not significant.

Value match. When the scrutinee has type value (§5.6), the case labels are the eight value-classes int, bool, string, datetime, duration, real, null, and blob. Like a class match (§14.5), the arms MUST either cover all eight classes or provide a case default: catch-all; a value match that is neither exhaustive nor defaulted is a type_error. A write-producible class (int, bool, string, datetime, duration, real, blob) MAY bind the content with a named case <class> as <var>: arm — n : int inside case int as n: — scoped to the arm; the binding is optional (case int: with no as is well-formed). The one read-only class, null, is a bare case null: arm only: attaching as <var> to it is a type_error, because an absent value has no content to bind. A case default: arm likewise MUST NOT carry an as binding (it spans more than one class, so no single payload type exists). The bound identifier obeys the reserved-word rule (§6.6) and is visible only within its arm.

6.3 Bounded iteration

A for x in <expr>: statement MUST have <expr> of a finite collection type (claim_list, string_list, subject_set, or result_type_set). Any other iterand type is a type_error (bad-unbounded-for). The loop variable x carries the collection’s element type (§5.3) within the loop body. This rule, together with the absence of any recursion construct (§9.7), gives DKE Python its termination guarantee (§9.5).

6.4 Assignment type agreement

A bare assignment x = <expr> binds x to the initializer’s static type. Binding a statement-only verb (§7.4) is a type_error — the right-hand side carries no result value.

6.5 Name arguments

The name argument of checkpoint (and of the wire verbs import, forget script, info script) is a bare identifier whose form is identifier-shaped per §3.4: first codepoint XID_Start, remaining codepoints XID_Continue. The identifier is a name, not a string value; it denotes the checkpoint or script it names, verbatim. A violation is rejected at compile time (parse_error).

6.6 Reserved-word constraint

A user identifier (declaration name, parameter name, loop variable, handler binding, assignment target) MUST NOT be any of the reserved words in §3.7 (a)– (d). The reference compiler raises this at the lexer or parser; a conforming implementation MAY raise it at the typechecker.

6.7 Scope resolution for plain identifiers and paths

A bare identifier in expression position MUST resolve to a parameter, an assignment binding, a for binding, or an except handler binding visible in the current scope. An unresolved identifier is a type_error (bad-undeclared).

A dotted path H.<rest> is classified by the type of its head identifier H:

• If H is in scope with any non-string type, the path is a field-access chain on H’s value; each segment after H MUST be a field of the previous segment’s type (§5.2).
• If H is in scope with type string, the path is a slot-grammar reference addressing the store cell named by kind H and the following slot segments; slot-grammar references are meaningful only as verb-phrase arguments. A string-typed segment resolves to that binding’s value at invocation; otherwise the segment is taken verbatim as a slot name.
• If H is not in scope, the path is a type_error — the kind position of a verb path MUST be a string-typed identifier in scope.

6.8 Calls between scripts

A call statement <name>(<args>) whose head is not a verb head-word resolves as a stored-script invocation under the compile-before-call rule: the callee MUST be an EARLIER declaration of the same compile unit or an already-stored script. A forward reference to a LATER declaration of the same unit is rejected. The same-unit call graph is therefore acyclic by construction (§9.7). Argument count and types are checked against the callee’s declared parameters at compile of the unit.

7.1 The in-language verbs

The call form’s compound heads (list_attributes, list_values, list_subjects, list_categories, list_result_types, list_checkpoints, list_pinned, list_scripts) are single snake_case tokens. They are soft keywords: recognized as a verb only immediately before (, so the same spelling remains a usable ordinary identifier elsewhere.

branch, commit, and rollback are language constructs (§4.3, §9.2.5, §9.2.6), not verbs, and are spelled directly in DKE Python syntax.

As-of reads. current and get accept an optional datetime (§3.5.5) second argument. current(K.s.a, t"…") / get(K.s.a, t"…") read the cell as of that past time rather than now — current yields the single value that was active then, get the claims valid then. Omitting it reads the present. A fact carried without a validity window is valid at all times, so its as-of value is its present value.

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")) in call form, or remember K.s.a = v per src t"2019-…" t"2021-…" in phrase form. Either bound may be the literal null, leaving that side open — t"2024-…", null is valid from 2024 onward with no end, and null, t"2024-…" up to 2024 with no start; at least one bound must be given. Omitting the pair records an always-valid fact (the default). Both bounds are inclusive. A windowed fact is selected by an as-of read whose time falls inside its window (above), so two writes at one cell with non-overlapping windows — and distinct sources, since one source may not assert two different current values at a cell — model a value that changed over time.

Forget is path-scoped. forget takes exactly one path argument — K.s.a (one cell) or K.s (a whole subject). There is no value- or source-scoped forget form; retraction granularity is the path.

Absence-assertion verb carries no value. assert K.s.a per src asserts that the value at K.s.a is known to be absent per src — an assertion observably distinct from there being no claim at all.

One data-read script verb runs in-language; the rest are wire-only. The list scripts verb executes from inside a program, reading stored script data (list scripts → string_list of names). The remaining script-lifecycle verbs — forget script, info script, and invoke (§11) — are wire-only: using one inside a program body is rejected at compile time with a type_error that teaches the wire route. The service stores no source text, so there is no source-readback verb.

7.1.1 Aggregate query functions

An aggregate query computes a summary value over a whole column of stored data — the values of one attribute across every subject of a kind. It is a read-only expression: it never changes the store.

Three call shapes, by the function’s arity:

The available folds:

The two-column folds take two attributes of one kind (slope(Point.x, Point.y)); both columns are read over the same subjects. K, col, x, y follow the ordinary slot-grammar rules (§7.2) — each may be a literal name or a string parameter/variable resolved at runtime.

Result type. An aggregate query returns a value (§5.1). Its runtime class follows the column(s): a numeric column yields a number (int or real); over a datetime or duration column, a fold yields a datetime or duration as appropriate. Because the class is not fixed at compile time, bind the result to a name and destructure it with match (§9.2.3) to consume a specific class, or use it directly wherever a value is expressible (log, +, ==).

Position. An aggregate query reads the service, so — like current and the other reads — it is used in expression position bound to a name on its own line (m = avg(Reading.value)), then referenced; it may not be written as a bare argument to another call. An aggregate over a column with no data is a runtime refuse (§10.3). A numeric fold (sum, avg, min, max, stdev, and the rest) over a column whose values are not numbers — a text column, or one mixing numbers with non-numeric values — is likewise a runtime refuse: the fold declines rather than treating a non-number as zero. (count counts values of any class, so it never refuses on this ground.)

The fold names are soft keywords: recognized as an aggregate only immediately before (, so every name remains a usable ordinary identifier elsewhere.

7.2 Slot validity

Slot identifiers (kind, subject, attribute, source names) are strings under §3.4 (UAX #31). At runtime, an implementation MAY refuse a slot containing characters not in the target service’s identifier alphabet; this is a refuse, not a type_error.

Values (the v in remember, update, verify, and subjects where) are scalar literals — a string, an int, or a bool — and are NOT identifier-shaped; the two write verbs (remember, update) additionally accept a datetime literal (§3.5.5), a duration literal (§3.5.6), a real literal (§3.5.7), or a blob literal (§3.5.8). The value slot is type-checked against these types; a compound value (a claim_list, a path, and so on) is a type_error.

• A write verb (remember, update) records the value with its literal type: remember(K.s.a, 42, src) stores the int 42, remember(K.s.a, True, src) stores the bool true, remember(K.s.a, "42", src) stores the text "42", remember(K.s.a, datetime("2026-01-02T03:04:05Z"), src) stores a datetime, remember(K.s.a, duration("PT1H30M"), src) stores a duration, remember(K.s.a, 3.5, src) stores a real, and remember(K.s.a, blob("48656C6C6F"), src) stores a blob. The recorded type is a property of the claim and reads back through .value (§5.6).
• The two query verbs (verify, subjects where) 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 type-aware equality == follows (§8.1) — a class mismatch compares unequal rather than coercing — applied at the query boundary; no value is widened or narrowed to fit. datetime, duration, real, and blob are not query-slot types in this version: such a literal in verify / subjects where is a type_error. Compare one of these by reading it back and matching its value (§5.6).

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 (or, in the phrase form, is written after the per preposition) and MUST be a string. The source identifier’s content is subject to the runtime constraints of the target service (typically: XID-shaped, no @ / : / /); a non-conforming source is a runtime refuse.

7.4 Statement-position vs expression-position

A verb listed as stmt in §7.1 MUST appear only as a statement (not bound by an assignment, not embedded in a larger expression). Binding a stmt-position verb is a type_error (§6.4). A verb listed as expr produces a value of the named result type and may bind an assignment, be a match scrutinee (if a discriminator), be iterated (if a finite collection), or be composed with operators per §8. checkpoint may appear in either position; in statement position its handle result is discarded.

7.5 Write-verb semantics

• Writes are permissive. update K.s.a = v per src on a location with no active claim succeeds and establishes the claim — it does not require a prior remember.
• pin marks; it does not protect. forget on a pinned location succeeds and removes the claim (and its pin).
• Writes are durable as executed. A later statement’s failure does not undo earlier writes; transactional grouping is the branch construct’s job (§9.2.5).

8.1 Comparison

There is no string ordering. Comparisons do not chain (§4.6).

A value (§5.6) may be compared with == / != against a scalar literal or another value without first destructuring it; the result is bool regardless of the runtime class, and a class mismatch compares unequal rather than coercing (c.value == 41 is false when the content is text). This mirrors Python’s cross-type ==. Ordering (<, >, …) requires numeric operands (int or real), so a value must be destructured through match (§5.6) into a numeric arm before it can be ordered.

8.2 Logical

and and or are short-circuit. DKE Python uses the word forms; there are no && / || / ! tokens.

8.3 Arithmetic

The numeric operand set is N ∈ {int, real}. +, -, *, / promote: when both operands are int the result is int; when at least one is real the other is promoted to real and the result is real. Division is the sole place the promotion boundary is observable — int / int is integer division (truncating), but any real operand makes / true division (7 / 2 is 3, 7.0 / 2 is 3.5). % stays int × int; a real operand to % is a type_error.

Division by zero (integer or real) and modulo by zero are runtime refuses (§10.3). Integer overflow — any integer +, -, *, /, %, or prefix - whose mathematically correct result falls outside the signed 64-bit range — is a runtime refuse with a teaching message rather than wrapping. A real arithmetic result whose magnitude leaves the finite range is likewise a runtime refuse. Reals compute to the precision of an IEEE-754 double and render in the canonical decimal form of §3.5.7.

8.4 String concatenation

The + operator is overloaded for strings:

This overload supports common log "count = " + xs.length patterns without explicit conversion. It is the only implicit coercion in DKE Python. Whenever one operand is a string, the other may be any renderable primitive — including a value, which is rendered by whatever class it carries.

8.5 Field access

See §5.2 and §5.4 for the full table of well-typed field accesses. Accessing a field not in the table is a type_error.

8.6 Indexing

See §5.3. The index expression MUST be int; out-of-range indices refuse at runtime (§10.3).

8.7 The log statement

log(<expr>)          # canonical
log <expr>           # accepted alternative

Appends output to the script’s transcript. log is written as a call — log("temp=" + t.value) — or, equivalently, without parentheses (log <expr>); the two forms are identical. Evaluates <expr> and appends its rendering. The argument type MUST be a type for which a textual rendering is defined: string, int, bool, a value (§5.6, rendered by its class), or any discriminator type. Finite collections and proof_tree MUST NOT be passed directly to log; access a string-shaped field or build a string with + instead.

8.8 No I/O, no closures, no first-class functions

DKE Python has no I/O surface other than (i) verb phrases against the store and (ii) log. It has no closures, no anonymous functions, no first-class function values, and no captured environments. The only callable is a top-level stored script, via a plain call (§4.3, §9.7).

9.1 Evaluation order

Expressions evaluate strictly, left to right. The sub-expressions of a binary operator evaluate before the operator; the index expression of [] evaluates before the indexing; an argument list evaluates left to right before the call. The short-circuit operators and, or are the only exceptions: the right operand evaluates only if needed. Statements within a suite execute in textual order; an assignment’s binding becomes visible immediately after its initializer evaluates.

9.2 Control flow

try:
    S
except refuse as r:
    Sr
except engine_error as e:
    Se

with branch("<name>"):
    S

9.3 Refuses as control flow

A refuse is a recoverable runtime outcome of a verb phrase. Refuses arise from input that the store rejects (out-of-surface slot, incomplete slots, ambiguous match, invalid source slot, write conflict, …). The list of refuse reasons is defined by the target service; DKE Python guarantees only that a refused statement’s binding does not produce a value and that control transfers to the enclosing except refuse handler if present. A statement that would bind a value and refuses leaves the target identifier unbound; any subsequent reference within the same block is a refuse on the same path.

9.4 Engine errors

An engine_error indicates that the target service composed a well-formed request from the user’s source but the request failed at the engine layer. Engine_errors are distinct from refuses; they indicate a service-side issue, not a user-side correction opportunity. They are caught by except engine_error.

9.5 Termination guarantee

DKE Python guarantees bounded termination (it is bounded-terminating). Every well-typed program terminates on every input; this is the family-wide guarantee, identical across editions. The guarantee follows by structural induction:

• The only iteration construct is the for … in over a finite collection (§6.3). The collection’s length is determined at iterand evaluation; the loop runs that many times.
• There is no while, no unbounded loop, no goto, no continuation.
• There is no recursion. A stored-script call is inlined at compile time (§9.7); a direct or indirect call cycle between scripts is a compile error.
• All other control-flow constructs (if, match, try, branch) reduce body size, not increase it.

The reference implementation MAY additionally impose execution budgets (statement count, wall-clock time) for operational reasons; such budgets are NOT part of the language specification.

9.6 Determinism contract

Given (i) the same DKE Python source, (ii) the same target store state at invocation start, and (iii) the same argument values, two invocations of invoke <name>(args) MUST produce byte-identical transcripts. This holds across re-invocation, across implementation process restarts, and across implementation versions that share the same spec version (§12). Determinism applies to the response shape — the response header’s call frame (with its success verdict) and the ordered sequence of log outputs and store effects the body lists (§11.2); the exact prose of that human render is presentation, not a versioned contract (§11.2). Determinism does NOT constrain the wire encoding of the request or any internal representation.

9.7 No runtime recursion; inline expansion

DKE Python has no runtime function-call mechanism. A stored-script call <name>(args) (§4.3, §6.8) is compile-time inline expansion: each invocation site is replaced by the callee’s body with parameter bindings substituted. Consequently callees MUST be compiled before callers, cycles are forbidden (a compile error), and inlining is one-shot (recompiling a callee after the caller does not change the caller’s stored body until the caller is also recompiled).

10.1 parse_error

The source is not a well-formed token stream or does not match the grammar of §4. Examples:

• A tab in indentation, or a dedent that matches no open level (§3.2).
• Unterminated string literal.
• Codepoint outside XID at identifier position.
• A reserved word (§3.7) in user-identifier position.
• An empty compile unit — no declarations after whitespace and comments.
• A non-exhaustive match written with a missing arm (raised as type_error, §10.2) versus a malformed case header (parse_error).
• A name argument that is not an identifier-shaped bare word (§6.5).

A conforming implementation MUST report the line and column of the first offending token.

10.2 type_error

The source parses but violates a rule in §5 or §6. Examples:

• Use of an unbound identifier — including the kind position of a verb path (§6.7).
• A wire-only script verb in a program body (forget script, info script, invoke — §7.1).
• A match whose case set does not cover the scrutinee’s discriminator set, contains a case not in the set, or repeats a case (§6.2).
• A for … in over a non-collection (§6.3).
• Binding a statement-only verb by assignment (§6.4).
• <value>.<field> for a non-existent field.
• An operand-type mismatch outside the §8.4 string-concat overload — including a chained comparison (§4.6).
• A non-string source argument (§7.3).

A conforming implementation MUST report the line and column of the offending construct.

10.3 refuse

A runtime outcome of a verb phrase (or built-in operation) that the target service rejects with a teaching message. Examples:

• remember K.s.a = v per src where the cell already carries a different value under the same source.
• subjects where K.a = v where K is not a known kind.
• A verb path whose segment count does not match the verb’s slot shape (§7.2).
• Index out of bounds on claim_list[i].
• Division by zero; integer overflow.
• commit outside a branch.

A refuse carries a refuse_info (reason, teaching_hint, discriminator). When wrapped in try: … except refuse as r:, control transfers to the handler with r bound. The exact reason taxonomy is defined by the target service; a conforming implementation MUST surface whatever reason strings the service returns without altering them.

10.4 engine_error

A runtime outcome indicating that the target service composed a well-formed request from the source but the request failed at the engine layer. Carries an engine_error_info (reason, code). Caught by try: … except engine_error as e:.

10.5 Diagnostic format (informative)

The reference CLI prints diagnostics in the form

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

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

11.1 Submission (import)

import <name> from "<source>"

Source is submitted to the target service with import. A .dpy file is a module (§17.1): import <name> from "<source>" stores the module text under <name> and runs its body — executing its data declarations, installing its rules, and making its defs callable via invoke. The service MUST:

1. Lex, parse, and typecheck the source per §3–§6.
2. If any check fails, refuse the operation; no storage occurs.
3. Otherwise, store every declaration of the unit under its own declared name, atomically (all of the unit or none of it), each executable via invoke, and run the module body once (§17.1).

A unit that is exactly one def is just a one-declaration module — import submits it like any other; there is no separate single-script verb. The full submission semantics — name resolution (§17.4), re-import reconciliation (§17.5), namespacing (§17.6), and the as curated form — are specified at §17.3. The first character of <name> MUST be XID_Start.

11.2 invoke

invoke <name>(<arg-list>)

Executes the compiled script <name> with the supplied arguments against the target service’s current state. Arguments are evaluated in the caller’s scope before invocation; the argument count MUST match the declared parameter count; each argument’s type MUST be assignable to the corresponding parameter type (the only assignable relation is identity). The transcript of the invocation appears as the result of the invoke verb and renders in the natural language the script was compiled in (§3.9). Its call frame is the response header, not a body line: a successful run is headed OK script <name>(<args>): <verdict> and a failed one error: script <name>(<args>) failed — <reason>, so the header names the script, its arguments, the terminal status, and — on success — a verdict tallying what the run did (the count of store writes and log lines). The body then lists, in execution order, the run’s output (the values the script logs) and its store effects (the remember/update/ forget writes, each naming its target cell). Statements that change no state stay silent — assignment bindings, control flow (if/match/for), transaction verbs (branch/commit/rollback), and read/query or service-side calls — so the body carries the run’s outputs and durable effects, not its execution mechanics. This human-readable render is presentation, not a versioned contract: a conforming implementation MAY format the header, verdict, and effect lines differently. What §9.6 pins is that the render is deterministic (same source + same store + same args → byte-identical transcript) and that the machine-readable result carries the run’s terminal status and its log sequence. Invocation is not transactional: a failed invocation does not undo writes already executed by earlier statements; only a branch block groups writes transactionally.

invoke is the WIRE spelling. In-language, stored-script invocation is a plain call statement <name>(<args>) (§4.3, §6.8, §9.7); there is no invoke keyword in the language and no expression-position invocation that binds a value — scripts compose by writing to and reading from the shared store.

11.3 list scripts

list scripts

Lists every script currently compiled at the target service, one line per script carrying its full call signature — the name and its typed parameters in declaration order (ingest(id: int, payload: string, dry_run: bool)). Listing order is implementation-defined but MUST be stable across reads with no intervening import / forget script. In expression position inside a program, list scripts evaluates to a string_list of bare script names.

11.4 forget script

forget script <name>

Removes the script <name> and its compiled form. Idempotent: if no script with that name exists, the operation succeeds.

11.5 info script

info script <name>

Returns the script’s compile provenance as rendered text lines: the compiling authority, the natural language the source was compiled in, and the manifest version the compiled form was produced against. Invocations are not tracked — info script describes the compilation event, not any run. (For a data derivation, use the in-language why K.s.a, which returns a proof_tree; info script is wire-only and its response is text, not a typed value.)

The lifecycle verbs other than import are edition-neutral: invoke, list scripts, forget script, and info script take no edition tag. import is the sole exception — its submission form carries the edition (§11.1) to select the grammar for the submitted source.

12.1 Spec version

The DKE Python Spec is a draft; the published surface carries no release version number. A source carries no version marker: an implementation accepts a conforming source by its structure (§4), not by a version match. Were the specification to adopt numbered releases, revisions would be tracked as a MAJOR.MINOR document version:

• MAJOR increments on a breaking change (a previously accepted program becomes rejected) or an observable-behaviour change (e.g. a change to the invocation transcript, §11.2).
• MINOR increments on a backward-compatible addition or a backward-compatible revision that rejects no previously accepted program and changes no observable behaviour.

A document revision changes no source: an implementation accepts a conforming source by its structure (§4). Across a breaking change, source compatibility is not guaranteed; such changes are announced with a migration note published alongside this specification.

12.2 Reserved for future use

The following surface area is reserved in v4.x and MUST NOT be used:

• Escape sequences in string literals other than \\, \", \n, \t, \r, \xNN, \uNNNN.
• String ordering (<, >, <=, >= on strings; currently int-only).
• The names empty, refuse_info, engine_error_info as type-name tokens (§5.5).

(The 0x / 0o / 0b numeric prefixes, _ separators, and prefix unary minus are part of the language.)

12.3 Compatibility with the target service

A DKE Python program is portable across target services that implement DKE’s canonical verb surface verbatim. Behaviour differences caused by different target-service surfaces are not language differences; the language layer is the same.

13.1 Conforming implementations

An implementation MAY conform as one of:

• Parser/checker (static-only): accepts the language defined in §3–§6, rejects with the correct error class per §10.1 / §10.2, produces a typed AST. Sufficient for linters, formatters, syntax highlighters, and language servers.
• Compiler/runtime (full): in addition, implements the lifecycle (§11) against a target service and the dynamic semantics (§9), satisfying the determinism contract (§9.6) and the termination guarantee (§9.5).

A conforming implementation MUST document which class it implements and which spec version it claims.

13.2 Conformance suite (informative)

A minimal conformance suite for a parser/checker exercises:

• Every reserved word from §3.7 (a)–(d) in user-identifier position → parse_error.
• A tab in indentation and a bad dedent → parse_error.
• An empty compile unit (whitespace and comments only) → parse_error.
• An unterminated string → parse_error.
• A non-XID codepoint at identifier head → parse_error.
• A name argument that is not an identifier-shaped bare word → parse_error.
• An unbound identifier → type_error.
• A match on active_claim missing the empty case → type_error.
• A match on active_claim with an extra case, and one with a duplicate case → type_error.
• A for … in over an active_claim → type_error.
• Binding a statement-only verb by assignment → type_error.
• A chained comparison a < b < c → type_error.
• A <claim>.nonexistent → type_error.
• A forget script / info script / invoke in a program body → type_error.
• Every verb in §7.1 with its declared phrase form → accepted.
• A module body with a top-level data declaration and no def → accepted (a module need not declare a script; §17.1, §17.7).
• An import <module> statement at module scope → accepted (§17.3).
• A cross-module qualified read module.Kind(subject).field → accepted (§17.6).
• Re-importing an already-loaded module → accepted; it reconciles (§17.5).
• An import cycle (a module that imports itself, directly or transitively) → rejected when the module is loaded (§17.3).

The reference compiler ships with such a suite; third-party implementations are encouraged to share theirs.

14.1 Class declarations

class-decl   := 'class' IDENT ':' NEWLINE INDENT class-member+ DEDENT
class-member := field-decl | method-def
field-decl   := IDENT ':' type-name ( '=' expr )? NEWLINE

A class declaration is the keyword class, the class name, a :, and an indented body of field declarations and method definitions. A class takes no marker.

A field is name: type whose type is a primitive (string, int, or bool) — a stored value slot the customer writes and reads. Field names are unique within a class.

A field may instead carry an initializer — name: type = expr — making it a computed field whose value the engine derives from the class’s other fields and maintains automatically. A computed field’s type is int, real, or bool, and the customer never writes it directly. See §14.7.

class Sensor:
    temp: string
    # methods follow

Declaring a class introduces no storage and performs no action; it is a compile-time description the compiler uses to typecheck field access and method calls.

14.2 Instances

An instance names one member of a class, identified by a string:

instance-ctor := IDENT '(' expr ')'   # the class name applied to a name expression

Sensor(room) is an instance of Sensor, bound by assignment:

s = Sensor(room)

Constructing an instance records nothing — it is not a write; it yields a typed reference for reading and writing the instance’s fields and calling its methods. Reading a field that has never been written yields empty (§14.3).

14.3 Field access

Given an instance s of a class that declares a field f:

• Read — s.f yields the current claim for that field: an active_claim when the field has a value, or empty when it does not. Consume it with match (§6.2) or .value (§5.2).

  reading = s.temp

• Write — remember(s.f, <value>, <source>) records a new value for the field together with its provenance source (§7.3):

  remember(s.temp, "21", "op1")

Field access is available on an instance variable and, inside a method body, on the explicit receiver self (§14.4). Reading or writing a field the class does not declare is a type_error.

14.4 Methods

A method is a def inside a class body whose first parameter is the explicit receiver self. Inside the body, self.f names field f of the instance the method was called on.

method-def   := void-method | value-method
void-method  := 'def' IDENT '(' 'self' ( ',' param )* ')' ':' NEWLINE INDENT stmt+ DEDENT
value-method := 'def' IDENT '(' 'self' ( ',' param )* ')' '->' type-name ':' NEWLINE INDENT stmt* 'return' expr NEWLINE DEDENT

• A void method — def name(self, params): — declares no return type; it performs actions and yields no value, called as a statement.

  def record(self, v: string, src: string):
      remember(self.temp, v, src)

• A value method — def name(self, params) -> type: — declares a return type and ends with return <expr> of that type, called in expression position.

  def label(self) -> string:
      return "sensor"

A method is called on an instance with instance.method(args) — the self argument is supplied by the receiver, not written at the call:

s.record("21", "op1")           # void method, statement position
name = s.label()                # value method, expression position

The method is resolved at compile time from the receiver’s declared class (static dispatch): exactly one method body per call, with no runtime lookup. Methods obey compile-before-call exactly like scripts (§6.8); method recursion, direct or mutual, is not expressible, so the call graph is acyclic (§14.6). Argument count and types are checked against the method’s declared parameters.

14.5 Dispatch by class

When code must branch on which class an instance belongs to, it uses a match whose scrutinee is a bare instance variable and whose case arms name classes:

class-match := 'match' IDENT ':' NEWLINE INDENT class-case+ default-case? DEDENT
class-case  := 'case' IDENT ':' ( simple-stmt NEWLINE | NEWLINE INDENT stmt+ DEDENT )
default-case := 'case' 'default' ':' ( simple-stmt NEWLINE | NEWLINE INDENT stmt+ DEDENT )

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

A match whose scrutinee is a bare instance variable is a class match; a match over any other expression is an ordinary discriminator match (§6.2). Inside a case <Class>: arm the instance is treated as that class, so its fields and methods resolve to that class. The arm set is closed and exhaustive: it MUST cover the instance’s declared class or provide a case default: arm. A class match that is neither exhaustive nor defaulted is a type_error, and a case naming an unknown class is a type_error. Because the arm is selected from the instance’s compile-time class, a class match introduces no runtime dispatch and no unbounded lookup.

14.6 Termination

Classes preserve the termination guarantee of §9.5. Method dispatch — both direct calls (§14.4) and class matches (§14.5) — is resolved statically, so it introduces no runtime loop and no dynamic lookup; methods are non-recursive by construction; iteration remains the bounded for … in of §6.3. Every method body is therefore a finite, non-recursive program over bounded iteration.

14.7 Computed fields

A computed field is a field declared with an initializer:

field-decl := IDENT ':' type-name ( '=' expr )? NEWLINE

Its value is not written by the customer; the engine derives it from the class’s other fields and keeps it current as those fields change. A computed field’s declared type is int, real, or bool.

class Order:
    price: int
    qty: int
    total: int = price * qty        # a computed value
    big: bool = total > 1000        # a computed flag

Given Order.o1.price = 10 and Order.o1.qty = 5, reading Order.o1.total yields 50; writing Order.o1.price = 200 re-derives it. The customer writes only price and qty; total and big are maintained automatically. A computed field reads back like any field (current, §7.1) with a derived provenance in place of a source.

The initializer. Every identifier in the initializer must name another field of the same class declared earlier (a computed field may build on an earlier computed field), and the initializer must reference at least one such field. The form depends on the declared type:

• An int field is an arithmetic expression over int fields and integer literals using +, -, *, % (§8). Division (/) is not written in an int field — its result may be fractional; declare the field real.
• A real field is an arithmetic expression using +, -, *, / over int and real fields and numeric literals (% is integer-only, §8.3). Division that does not divide evenly yields a real value (§3.5.7).
• A bool field is a single ordered comparison — <, <=, >, >= — of one earlier field against a numeric literal or another earlier field. Its left side is a single field: to compare a computed value, declare that value as its own field first (total: int = price * qty, then big: bool = total > 1000).

Because every reference points at an earlier field, a class’s computed fields form no cycle. A computed field participates in match (§6.2) and expressions (§8) exactly as a written field of the same type would.

Termination. Computed fields preserve the termination guarantee of §9.5: a derivation is a finite, acyclic expression over the class’s own fields, evaluated once per change; it introduces no loop and no recursion.

15.1 The rule block

A rule is a def marked with the @rule decorator, named like any script, then a for clause naming the rows it ranges over, an if clause stating the condition, and an indented conclusion:

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

rule-decl   := '@rule' NEWLINE
               'def' IDENT '(' ')' ':' NEWLINE
               INDENT
                 'for' IDENT 'in' kind-name ':' NEWLINE
                 INDENT
                   'if' premise ( 'and' premise )* ':' NEWLINE
                     INDENT conclusion NEWLINE DEDENT
                 DEDENT
               DEDENT

The for clause names the kind the rule ranges over and the name it gives each row (for o in Order). Every name the rule uses — in a premise or in its conclusion — is that row variable. The @rule marker distinguishes a rule from an ordinary script; for, in, if, and and read here exactly as they do elsewhere in the language, and absent names the rule’s one negative premise (§15.2).

15.2 Premises

The if clause is one or more premises joined by and; the rule holds only when every premise holds:

premise    := comparison | absence
comparison := IDENT '.' IDENT cmp-op number      # o.total > 1000
absence    := 'absent' '(' IDENT '.' IDENT ')'   # absent(o.shipment)
cmp-op     := '<' | '<=' | '>' | '>='

• A comparison (o.total > 1000) holds when the field, read as a number, stands in the given order to the numeric literal.
• An absence (absent(o.shipment)) holds when the row has no value recorded for that field. This is the one negative premise, and it means the plain absence of information — not a field recorded as false or empty.

15.3 The conclusion

conclusion := IDENT '.' IDENT '=' literal         # o.review = True

Whenever the condition holds, the engine records the named field of the named row as the given literal. As with a computed field, the customer never writes that field directly.

15.4 What a rule does

Defining a rule takes effect immediately and continuously:

• Whenever the stored data comes to satisfy the condition — at definition time for data already present, or later as data is written — the engine records the conclusion, with a derived provenance (§7.1) in place of a source.
• Whenever the condition stops holding — including when a value is first recorded for a field an absent(...) premise required to be absent — the engine withdraws the conclusion it had recorded.

A derived field reads back exactly like any other field (current/get, §7.1); its value reflects the rules currently in force.

15.5 Well-formed rules

Two things make a rule usable; a rule that lacks either is rejected when you define it, with a message that names the rule.

• A rule must say which rows it applies to. A rule whose only mention of its row is an absence test never says which rows, so it has nothing to work over (for o in Order … if absent(o.shipment): … — which orders?). Give it at least one comparison, so it ranges over a definite set of rows.
• A rule’s outcome must settle. A rule — alone or together with others — must not chase its own tail: if recording its conclusion would remove the very condition that produced it, there is no answer to settle on, and the rule is rejected. You may build rules on stored data and on one another freely; the only thing ruled out is a set that cancels itself.

15.6 Termination

Standing rules preserve the termination guarantee of §9.5. A rule ranges over finitely many stored rows; its premises are tested, not iterated; and §15.5 rules out the one self-cancelling construction under which the outcome could fail to settle. Every set of rules therefore reaches a fixed set of derived facts in finite time.

17.1 A .dpy file is a module

A DKE Python source file is a module; its top level is the module body — a sequence of declarations and statements, read top to bottom. A module body may contain, in any order:

• declarations — def (a callable script, §4.2), class (a kind schema, including computed fields, §14.1, §14.7), @rule-marked def (a standing rule, §15);
• data declarations — the four write statements remember / update / forget / assert (each with its per <source> provenance), written at module scope (§17.2);
• statements — any statement legal inside a def body (§4.3): bounded for / if / match / try, reads bound by assignment, log, and commit / rollback;
• import statements (§17.3).

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

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

17.2 Data declarations at module scope

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

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

A data declaration is an ordinary write (§7.1) that happens to sit at module scope; it obeys every rule a write inside a def obeys, and it takes effect when the module is imported.

17.3 import

import <module>
import <name> from "<source>"
import <name> from "<source>" as curated

import loads a module: it makes the module’s names available under the module’s namespace (§17.6) and runs the module body once (§17.1).

• import <module> loads a module already stored under <module>, resolved along the search path of §17.4. This is the one form written in a program body — a module may import another module (§4.3); import is a contextual keyword recognised only at statement head.
• import <name> from "<source>" provides the module text inline: it stores <source> under <name> and loads it, so the module can be loaded again later by the bare import <name>. <source> is a string holding a complete compile unit (§4.1).
• import <name> from "<source>" as curated provides the module into the shared library on the search path (§17.4) rather than into the caller’s own namespace, so every caller resolves <name> to it unless the caller has a module of the same name (§17.4).

The two from "<source>" forms are managed from the service surface (§11.1); the bare import <module> is the form legal inside a program body.

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

A unit that is exactly one def needs no separate verb — it is a one-declaration module, and import <name> from "<source>" submits it like any other. import always runs the module body (§17.1), so a source with more than one declaration, a data declaration, a rule, or a top-level statement is submitted the same way.

17.4 Name resolution and shadowing

import <module> resolves <module> along a search path that spans, in order:

1. the caller’s own modules (provided into the caller’s namespace by an earlier import <name> from "<source>");
2. the shared library on the import search path — the curated modules the service ships, together with any module provided as curated (§17.3).

Resolution is by search-path order: a caller’s own module shadows a shared-library module of the same name. A shared-library name (say code) is therefore a default, not a reserved word — a caller who has provided their own module code resolves import code to theirs.

17.5 Re-import reconciles

Importing a module that is already loaded re-runs its body, and the re-run is a reconciliation:

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

Re-import therefore leaves the store reflecting the module’s current text — rewriting only the cells whose values changed — and is safe to repeat: edit the module text, import it again, and an unchanged cell is left as it is. (This is the one place import differs from a language whose import runs a module body only once — a DKE Python module is durable store state, not process memory, so re-import re-applies it.)

17.6 Namespacing

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

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

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

code.Function("f1").fanin names the fanin field of subject f1 of code’s Function; it reads like any field read (§14.3), and its result is an active_claim. The parenthesised subject distinguishes the module-qualified construction from an ordinary dotted path (§4.4). Because each module’s names are addressed under its own module name, two modules that both declare a Function never read or write each other’s cells.

17.7 Modules and single-def sources

• A module with no def is valid: a module that only installs a schema, defines a rule, or writes data declares no callable script and is loaded for its body’s effect (§17.1).
• A single-def source is just a one-declaration module: import <name> from "<source>" (§11.1, §17.3) stores the def and runs its (trivial) body, exactly as it stores and runs every declaration of a larger module — more than one declaration, or one bearing data, a rule, or a top-level statement. There is no separate single-script verb; import submits one def or many the same way.

C.1 Trivial smoke

# smoke-trivial.dpy — a write, an exhaustive match, and a length read.
def smoke_trivial():
    remember(Cat.felix.color, "orange", "op1")
    cur = current(Cat.felix.color)
    match cur:
        case active_claim:
            log("color = " + cur.value + " (per " + cur.source + ")")
        case empty:
            log("no color claim")
    hist = get(Cat.felix.color)
    log("history has " + hist.length + " claim(s)")

Invocation (wire surface, §11.2):

invoke smoke_trivial()

C.2 Audit walk

# audit-subject.dpy — read cluster + length composition.
def audit_subject():
    log("subject Cat.felix")
    attrs = list_attributes(Cat)
    log("attribute count = " + attrs.length)
    cur = current(Cat.felix.color)
    log("current color inspected")
    hist = get(Cat.felix.color)
    log("history depth = " + hist.length)

C.3 Try with refuse handling under a branch

# experimental write under a branch with explicit rollback.
def try_paint():
    with branch("experiment"):
        try:
            remember(Cat.felix.color, "tigret", "audit")
            after = current(Cat.felix.color)
            if after.value == "tigret":
                commit
            else:
                rollback
        except refuse as r:
            log("paint refused: " + r.reason)
            rollback

C.4 Classes and methods (§14)

# classes.dpy — a class with a typed field, a void method, and a value
# method; a def binds an instance and calls both.
class Sensor:
    temp: string
    def record(self, v: string, src: string):
        remember(self.temp, v, src)    # field write
    def label(self) -> string:
        return "sensor"                # value method

def demo():
    s = Sensor("room-a")               # instance binding
    s.record("21", "op1")              # void method call
    name = s.label()                   # value method call
    reading = s.temp                   # field read
    match reading:
        case active_claim:
            log(name + " = " + reading.value + " per " + reading.source)
        case empty:
            log(name + ": no reading")

C.5 Datetime round-trip (§3.5.5, §5.6)

# datetime-round-trip.dpy — a datetime value keeps its type across write/read.
def datetime_round_trip():
    remember(Event.launch.at, datetime("2026-01-02T03:04:05Z"), "ops")
    cur = current(Event.launch.at)
    match cur.value:
        case datetime as d:
            log("launch at " + d)
        case default:
            log("not a datetime")

C.6 Duration round-trip (§3.5.6, §5.6)

# duration-round-trip.dpy — a duration keeps its type and reads back canonical.
def duration_round_trip():
    remember(Task.build.budget, duration("PT90M"), "ops")
    cur = current(Task.build.budget)
    match cur.value:
        case duration as u:
            log("budget = " + u)
        case default:
            log("not a duration")

C.7 Real round-trip (§3.5.7, §5.6)

# real-round-trip.dpy — a real keeps its type and reads back in canonical form.
def real_round_trip():
    remember(Sensor.a.reading, 3.5, "ops")
    cur = current(Sensor.a.reading)
    match cur.value:
        case real as r:
            log("reading = " + r)
        case default:
            log("not a real")

C.8 Blob round-trip (§3.5.8, §5.6)

# blob-round-trip.dpy — a blob keeps its type and reads back as canonical hex.
def blob_round_trip():
    remember(Doc.d1.payload, blob("48656C6C6F"), "ops")
    cur = current(Doc.d1.payload)
    match cur.value:
        case blob as b:
            log("payload = " + b)
        case default:
            log("not a blob")

C.9 Real arithmetic (§3.5.7, §8.3)

# real-arithmetic.dpy — reals compute; int/real promote; a computed real
# writes through and reads back as a real.
def real_arithmetic():
    sum = 2.5 + 1.25
    log("sum = " + sum)                # 3.75
    log("half = " + (7.0 / 2))         # 3.5 — int promotes, true division
    log("scaled = " + (sum * 2))       # 7.5 — real * int promotes
    remember(Sensor.a.total, sum, "ops")
    cur = current(Sensor.a.total)
    match cur.value:
        case real as r:
            log("stored = " + r)       # 3.75, still a real
        case default:
            log("not a real")
    if sum > 3.0:
        log("above threshold")

C.10 Base64 blob input (§3.5.8)

# base64-blob.dpy — a blob written with the base64 spelling reads back as the
# same canonical hex as the equivalent blob("…") hex form.
def base64_blob():
    remember(Doc.d1.payload, blob_b64("SGVsbG8="), "ops")
    cur = current(Doc.d1.payload)
    match cur.value:
        case blob as b:
            log("payload = " + b)          # 48656C6C6F — canonical hex
        case default:
            log("not a blob")

C.11 As-of read (§7.1)

# as-of-read.dpy — current/get take an optional datetime to read a value as of
# a past time. For an always-valid fact that is the present value; with a
# validity window a past time can select an earlier value.
def as_of_read():
    remember(Rate.usd.pct, "3.0", "src")
    past = current(Rate.usd.pct, datetime("2020-01-01T00:00:00Z"))
    log("rate as of 2020: " + past.value)

C.12 Validity windows (§7.1)

# validity-window.dpy — two writes at one cell with non-overlapping validity
# windows (distinct sources) model a value that changed over time; two as-of
# reads at interior times select the two values.
def validity_window():
    remember(Sensor.room1.status, "cold", "reading-2019", datetime("2019-01-01T00:00:00Z"), datetime("2021-01-01T00:00:00Z"))
    remember(Sensor.room1.status, "warm", "reading-2021", datetime("2021-01-01T00:00:00Z"), datetime("2023-01-01T00:00:00Z"))
    past = current(Sensor.room1.status, datetime("2020-06-01T00:00:00Z"))
    log("status as of 2020: " + past.value)
    recent = current(Sensor.room1.status, datetime("2022-06-01T00:00:00Z"))
    log("status as of 2022: " + recent.value)

C.13 Aggregate query (§7.1.1)

# aggregate-demo.dpy — read-only summary statistics over a stored column.
def aggregate_demo():
    remember(Reading.r1.value, 10, "sensor")
    remember(Reading.r2.value, 20, "sensor")
    remember(Reading.r3.value, 30, "sensor")
    mean = avg(Reading.value)
    log("mean = " + mean)
    n = count(Reading.value)
    log("readings = " + n)

C.14 Computed field (§14.7)

# computed-field-demo.dpy — a field the engine derives and maintains.
# Declaring `total` with an initializer installs a derivation: whenever an
# Order's price and qty are known, total is price × qty.
class Order:
    price: int
    qty: int
    total: int = price * qty

def computed_demo():
    remember(Order.o1.price, 10, "sales")
    remember(Order.o1.qty, 5, "sales")
    t = current(Order.o1.total)
    log("total = " + t.value)

C.15 Standing rule (§15)

# standing-rule-demo.dpy — a named rule the engine applies automatically.
# `needs_review` flags any order over 1000 with no shipment recorded; the
# engine sets `review` on its own (and would withdraw it if a shipment were
# later recorded). The demo writes one qualifying order and reads the flag.
@rule
def needs_review():
    for o in Order:
        if o.total > 1000 and absent(o.shipment):
            o.review = True

def rule_demo():
    remember(Order.o1.total, 1500, "sales")
    r = current(Order.o1.review)
    log("review = " + r.value)

C.16 Hypothesis (§16)

# hypothesis-demo.dpy — read a value under a supposed fact, without committing.
# The rule flags an order for review over 1000. The hypothesis asks what review
# WOULD be if the total were 2000 — recording nothing.
@rule
def needs_review():
    for o in Order:
        if o.total > 1000:
            o.review = True

def hypothesis_demo():
    would = suppose(Order.o1.total, 2000, Order.o1.review)
    log("would review = " + would)

C.17 A data module (§17.1, §17.2)

# catalog.dpy — a module: a class schema and a data declaration. The body runs
# on import (§17.1); it declares no callable script (§17.7).
class Product:
    price: int
remember(Product.widget.price, 500, "price-list")

Load it by name (service surface, §17.3):

import catalog

C.18 Importing a module and a module-qualified read (§17.3, §17.6)

# reporter.dpy — imports the catalog module (§17.3) and reads one of its cells
# with the module-qualified construction (§17.6).
import catalog
def report():
    p = catalog.Product("widget").price
    log("widget price = " + p.value)

import reporter

Reading report back against a store that has imported catalog (§C.17):

OK script report(): 1 log
  log widget price = 500