DKE Python — Language Reference

4.1 The 17 types

Three groupings drive the static rules:

• Primitives — string, int, bool.
• Finite collections — claim_list, string_list, subject_set, result_type_set, proof_tree. Exactly the types a for … in may iterate (§7.7) and the types with a .length (§10). claim_list and proof_tree yield active_claim elements; the other three yield string. A proof_tree additionally offers a .root accessor (§10.2).
• Discriminators — active_claim (+ its empty case) and verify_result. Consumed by a match, alongside the value union.
• The value union — the stored content of a claim (active_claim.value), one of eight classes: int, bool, string, datetime, duration, real, null, or blob. Seven are write-producible — int, bool, string, datetime, duration, real, blob (a program writes one and reads it back at that class). The remaining class, null (an explicit absent value), is read-only: it is asserted via assert (§5.1), no value literal produces it, but a claim carrying one is discriminable on read. Consume the union with a value match (§7.8) to recover the typed content, or render it directly. → Spec §5.6
• datetime — a UTC instant written with the datetime("…Z") literal (e.g. datetime("2026-01-02T03:04:05Z"), RFC 3339 with a required Z and optional 1–9 fractional-second digits). A write verb stores it typed and it reads back as the datetime class of value; it renders as its RFC 3339 text. → Spec §3.5.5
• duration — a length of time written with the duration("…") literal (e.g. duration("PT1H30M"), an ISO 8601 duration PnDTnHnMnS; calendar years and months are not accepted). A write verb stores it typed and it reads back as the duration class of value; it renders as ISO 8601 in a canonical form, so duration("PT90M") reads back as PT1H30M. → Spec §3.5.6
• real — a fractional number written as a decimal literal 3.5 (at least one digit on each side of the point; _ may separate digits as in 1_000.5; 3. and 3.name stay an integer 3). A write verb stores it typed and it reads back as the real class of value in a canonical decimal form (insignificant trailing zeros are dropped — 3.50 reads back as 3.5, while 5.0 reads back as 5.0); it renders as its decimal text. A case real as r: arm binds r : real. Reals compute: + - * / and the ordered comparisons accept them and promote int → real, and any real operand makes / true division (§8.3, §6.3). → Spec §3.5.7
• blob — an opaque byte string written as a hex literal blob("48656C6C6F") (an even count of hex digits) or a base64 literal blob_b64("SGVsbG8=") (RFC 4648; the same bytes) — two input spellings for one byte space; the empty blob("") / blob_b64("") is a valid zero-byte blob. A write verb stores it typed and it reads back as the blob class of value in a single canonical uppercase-hex form regardless of the input spelling (a value written blob_b64("SGVsbG8=") reads back 48656C6C6F); it renders as its hex text. A case blob as b: arm binds b : blob. → Spec §3.5.8

There is no absence-of-value type and no null literal. To assert that a value is known to be absent, use assert K.s.a per src (§5.1), which carries no value. A parameter may be annotated with any value type in this section (none of empty, value, datetime, duration, real, or blob is a parameter type — empty is a match arm only, value arises only from .value field access, and each value class arises only from its literal or a case … as …: arm: datetime from a datetime("…Z") literal or case datetime as d:, duration from a duration("…") literal or case duration as u:, real from a 3.5 literal or case real as r:, and blob from an blob("…") / blob_b64("…") literal or case blob as b:). → Spec §4.2, §5

4.2 Handler bindings

The except refuse as <var> / except engine_error as <var> handlers of a try (§7.9) bind a value exposing string fields (for a refuse, .reason and other string fields; for an engine error, .reason). These cannot be written as parameter types. → Spec §5.4

5.1 Write verbs (statement position)

remember(K.s.color, "orange", "op1")     # string
remember(K.s.count, 42, "op1")           # int — reads back as int
remember(K.s.rate, "3.0", "src", datetime("2019-01-01T00:00:00Z"), datetime("2021-01-01T00:00:00Z"))  # valid 2019–2021
remember(K.s.plan, "active", "ops", datetime("2024-01-01T00:00:00Z"), null)  # valid 2024 onward, open end

update(K.s.mood, "playful", "op2")

forget(K.s.mood)

assert(K.s.chip_id, "vet")

pin(K.s.color)

5.2 Read verbs (expression position)

cur = current(K.s.color)

hist = get(K.s.mood)

cav = caveats(K.s)

confs = conflicts()

vals = list_values(K.color)

hits  = subjects(K.color, "orange")     # text match
warm  = subjects(K.temp, 42)            # int match — not the text "42"

subs = list_subjects(K.color)

attrs = list_attributes(K)

cats = list_categories()

5.3 Provenance and reasoning

pt = why(K.s.color)
n  = pt.length                     # how many claims participated
r  = pt.root                       # the queried claim
first = pt[0]                       # a participating claim → active_claim
for c in pt:                        # iterate the derivation's claims
    log("via " + c.source)

v = verify(K.s.color, "orange")
if v.match:
    log("confirmed")

deps = dependents(h)

5.4 Checkpoints

h = checkpoint("before_cleanup")

restore(h)

changed = diff(K.s.color, h)

cps  = list_checkpoints()
pins = list_pinned()

5.5 Result-type introspection

rts = list_result_types()

5.6 Script-data reads (in-language)

Read-only, so they run inside a program. → Spec §7

names = list_scripts()

5.7 Wire-only verbs (not callable in a program)

Callable at the dke.langsyn.net wire surface but rejected in a program body — they mutate the script set or answer administrative provenance. → Spec §7

The lifecycle verbs are edition-neutral. import <name> from "<source>" is the submission form: it stores a module by name and runs its body — which matters for a module that writes data or installs rules at its top level (§7.11). → Spec §11.1, §17.3

5.8 Call form and phrase form, side by side

The call form is canonical; the phrase form is an accepted equivalent. Both compile to the identical program, and a source may mix them. → Spec §7.1

5.9 Aggregate query functions

A read-only fold over a whole column — one attribute across every subject of a kind — returning a value (§4.1). Bind it to a name on its own line, then use it; an aggregate may not be a bare argument to another call. → Spec §7.1.1

n     = count(Reading.value)          # single-column fold
p90   = percentile(Reading.value, 90)  # ranked fold, rank 0–100
slope_xy = slope(Point.x, Point.y)     # two-column fold (both columns of one kind)
mean  = avg(Reading.value)            # bind first, then use `mean`

• Single-column fn(K.col) — count, sum, product; avg, median, midpoint, mode, geomean, harmmean, rms; min, max, span, variance, stdev, iqr, mad, cv; skewness, kurtosis, entropy.
• Ranked percentile(K.col, <int>) — the <int>-th percentile (rank 0–100).
• Two-column fn(K.x, K.y) (both columns of one kind) — covariance, correlation, slope, intercept, rsquared.

The result’s class follows the column (a numeric column yields a number; a datetime / duration column a datetime / duration); destructure with match or use it wherever a value is expressible. Fold names are soft keywords — recognised only right before (, so they stay ordinary identifiers elsewhere. An aggregate over a column with no data is a refuse; a numeric fold over a column whose values are not numbers (a text column, or one mixing numbers with non-numeric values) is likewise a refuse — the fold declines rather than treating a non-number as zero. count counts values of any class, so it never refuses on that ground. → Spec §7.1.1, §10.3

6.1 Comparison

== != over (string, string), (int, int), (bool, bool), two discriminators (compares .kind), or a value against a scalar / another value (Python-faithful — a class mismatch is false, never a coercion; §4.1); < > <= >= over numeric operands (int or real, mixed allowed — compared numerically). No string ordering.

6.2 Logical

and, or (short-circuit), not, over bool.

6.3 Arithmetic

+ - * / over numeric operands (int or real); % (remainder) over int only; prefix - negates an int. The numeric operators promote: int × int stays int, and any real operand yields a real. Division is the one place the boundary shows — int / int is integer division (truncating toward zero), but any real operand makes / true division (7 / 2 is 3, 7.0 / 2 is 3.5). Reals compute to IEEE-754-double precision and render in canonical decimal form. Division / modulo by zero and out-of-range (including non-finite real) results refuse at runtime. → Spec §8.3

6.4 String concatenation

+ joins a string with a string, int, bool, or value (either order); the non-string operand renders (a value by its class). The only implicit coercion.

log("count = " + xs.length)

6.5 Field access and indexing

x.field (see §10) and xs[i] (zero-based; out-of-range refuses; index is int). → Spec §5.2, §5.3

7.1 Declaration

def audit(K: string, s: string):
    <suite>

The def keyword, name, typed parameters (name: type), :, indented body. Two declarations in a unit must not share a name; a unit compiles its declarations in order and a call may target only an earlier one (compile-before-call). → Spec §6.8

7.2 Assignment (bind a read)

hist = get(K.s.color)

Bare assignment — there is no let introducer. The right side must not be a statement-only verb (no value). → Spec §6.4

7.3 log

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

Appends <expr>’s rendering to the transcript, written as a call — log("temp=" + t.value) — or, equivalently, without parentheses; the two forms are identical. The argument is string, int, bool, or a discriminator. → Spec §8.7

7.4 Script call (invocation)

audit_subject(K, s)

A plain call of a stored script — there is no invoke keyword (a script is called like any function). Static, compile-time inline expansion; argument count and types must match; no recursion, no cycles; no value-returning invocation. → Spec §6.8, §9.7

7.5 Verb-call statement

A write verb (§5.1) in statement position:

remember(K.s.color, "orange", "op1")

7.6 if

if <cond>:
    <suite>
else:
    <suite>

<cond> must be bool; else is optional. → Spec §9.2.1

7.7 for … in

for c in hist:
    <suite>

Iterates a finite collection only; any other iterand is a type_error. The collection is snapshotted at entry. Bounded iteration is what gives DKE Python its termination guarantee. → Spec §6.3, §9.5

7.8 match (discriminator dispatch)

match cur:
    case active_claim:
        log("value = " + cur.value)
    case empty:
        log("absent")

The scrutinee must be a discriminator (active_claim, verify_result). Arms exhaustively cover the discriminator’s cases. Python uses case where the base member uses when. → Spec §6.2

(A match whose scrutinee is a bare instance variable is the distinct class match, §8.6.)

A match whose scrutinee is a value (a claim’s .value, §4.1) is a value match: the case labels are the eight value-classes int, bool, string, datetime, duration, real, null, and blob. The seven write-producible classes (int, bool, string, datetime, duration, real, blob) may bind the typed content with a named as <var> arm; the one read-only class, null, is a bare arm only — attaching as <var> to it is a type_error:

match cur.value:
    case int as n:      log("next = " + (n + 1))     # n : int
    case string as s:   log("text = " + s)
    case duration as u: log("span = " + u)           # u : duration
    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")       # bare — no `as`
    case default:       log("other class")

Arms cover all eight classes or provide case default:; a bound as <var> is typed at the arm’s class and scoped to that arm. → Spec §5.6, §6.2

7.9 try

try:
    <suite>
except refuse as r:
    <suite>
except engine_error as e:
    <suite>

Python’s own except … as …: shape. Both handlers are optional. A refused statement does not bind and transfers control to except refuse as; an engine error to except engine_error as. With no matching handler, the outcome propagates. → Spec §9.2.4

7.10 branch / commit / rollback

with branch("experiment"):
    remember(K.s.color, "tigret", "audit")
    if ok:
        commit
    else:
        rollback

A with branch("<name>"): block groups writes transactionally: clean exit commits; an uncaught refuse / engine error rolls back. Bare commit / rollback end the branch explicitly. Ordinary invocation is not transactional. → Spec §9.2.5, §7.5

7.11 import (module)

import catalog                       # in a program body: load a stored module

A DKE Python file is a module (Spec §17); import <module> loads one: it runs the module’s body once and makes its names available under the module’s namespace. import is a contextual keyword — the import statement only at statement head, an ordinary identifier elsewhere. A module may import another module; an import cycle is rejected when the module loads. Loading a module already loaded reconciles it: only the cells whose values changed are rewritten, so re-import is safe to repeat. → Spec §17.1, §17.3, §17.5

A module’s names are namespaced. A kind a module declares with class is addressed under the module name — catalog.Product — and a cell of it is read with the module-qualified construction module.Kind(subject).field:

p = catalog.Product("widget").price    # read catalog's Product widget, field price
log("price = " + p.value)

Two modules may each declare a Product without collision (catalog.Product, store.Product, distinct). → Spec §17.6

Provide a module from the wire. import <name> from "<source>" stores a module by name and runs it; import <name> from "<source>" as curated provides it into the shared library on the import search path, where a caller’s own module of the same name shadows it. These two forms are wire-managed (§5.7); the bare import <module> is the form written in a program. → Spec §17.3, §17.4

Data at module scope. A write verb (§5.1) written at a module’s top level — not inside a def — is a data declaration: it runs when the module is imported. A module that only declares a schema, installs a rule, or writes data defines no callable script and is loaded for its body’s effect. → Spec §17.2, §17.7

# in a module body, at top level:
remember(Rate.vat.pct, 25, "2026-finance-act")   # runs on import

8.1 Class declaration

class Sensor:
    temp: string                                 # typed field (primitive)
    def record(self, v: string, src: string):    # void method (explicit self)
        remember(self.temp, v, src)
    def label(self) -> string:                    # value method
        return "sensor"

Written class <Name>: — no marker. Fields are name: type with a primitive type; names unique within the class. Declaring a class stores nothing. → Spec §14.1

8.2 Instance construction and binding

s = Sensor(room)

Sensor(room) names one member of Sensor identified by the string room; bound by assignment, its type is the class name. Construction records nothing. Reading a never-written field yields empty. → Spec §14.2

8.3 Field read and write

reading = s.temp                    # read → active_claim or empty
remember(s.temp, "21", "op1")       # write value + provenance source

A read has type active_claim; consume with match or .value. Accessing a field the class does not declare is a type_error. Inside a method the explicit receiver self (the first parameter) names the instance (self.temp). → Spec §14.3, §14.4

8.4 Void method

s.record("21", "op1")               # statement position; self is supplied by the receiver

def name(self, params): — no return type; performs actions; called as a statement. The self argument is supplied by the receiver, not written at the call. → Spec §14.4

8.5 Value method

name = s.label()                    # expression position

def name(self, params) -> type: ending with return <expr> of that type; called in expression position. Static dispatch from the receiver’s declared class; compile-before-call; no recursion. → Spec §14.4

8.6 Class match (dispatch by class)

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

A match whose scrutinee is a bare instance variable dispatches over class names. Inside case <Class>: the instance is treated as that class. The arm set is closed and exhaustive — cover the instance’s declared class or provide a case default:. Non-exhaustive or unknown-class arms are type_errors. Resolved from the compile-time class — no runtime dispatch. → Spec §10.5

8.7 Computed fields

A class field declared with an initializer the engine derives from the class’s other fields and keeps current as they change. The customer writes only the inputs; the derived field reads back like any field, with a derived provenance in place of a source. → Spec §14.7

class Order:
    price: int
    qty: int
    total: int = price * qty        # int: an arithmetic expression (+ - * %) over earlier fields
    big: bool = total > 1000        # bool: one ordered comparison of an earlier field

An int field is arithmetic (+ - * %) over earlier fields; a real field may also use /; a bool field is one ordered comparison (< <= > >=). Every reference is to a field declared earlier, so computed fields never form a cycle, and writing an input re-derives every field built on it. why over a computed field lists the inputs it was derived from (§5.3). → Spec §14.7

8.8 Standing rules

A named top-level declaration — a sibling of class / def, not a class member — that derives a field automatically: whenever its condition holds the engine records the conclusion, and it withdraws the conclusion when the condition stops holding. The @rule decorator marks the def as a rule; absent names its one negative premise, inside a rule block only. → Spec §15

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

• for <var> in <Kind> — the rows the rule ranges over and the row variable.
• if <premise> (and <premise>)* — each premise is a comparison (o.total > 1000, a field against a number, < <= > >=) or an absence (absent(o.shipment), the row has no value recorded for that field).
• the conclusion <var>.<field> = <literal> is recorded with a derived provenance; the customer never writes it directly.

A rule must name which rows it applies to (at least one comparison, not an absence alone) and must not cancel itself out — either is rejected when the rule is defined. It ranges over finitely many rows; termination is preserved. A derived field reads back like any other (current / get). → Spec §15

8.9 Hypothesis

suppose(<field>, <value>, <field>) reads what the second field would be if the first were set to the value — letting standing rules and computed fields run under the supposition — then discards everything. Nothing persists. Returns a value; bind it and read it, or concatenate it into a log. → Spec §16

would = suppose(Order.o1.total, 2000, Order.o1.review)   # true, if a rule sets review over 1000

Supposes exactly one fact. If the read field has no value under the supposition, suppose produces no value — a catchable refuse (guard it with try / except). Safe for preview, comparison, and what-if exploration; termination preserved. → Spec §16

10.1 Universal accessors → Spec §5.2

• <expr>.kind → string — for any discriminator and for proof_tree.
• <expr>.length → int — for any string or finite collection.

10.2 Field access by type → Spec §5.2

10.3 Indexing element types → Spec §5.3