Dewy Language Reference

This reference defines the intended syntax and semantics of the Dewy programming language. It is organized by language construct and is meant for answering exact questions rather than teaching the language in sequence.

For a guided introduction, read Learning Dewy.

Normative Language and Current Implementations

The main reference describes Dewy itself. A rule does not become less normative merely because the current compiler has not implemented it yet.

Language-design maturity is recorded in Design Maturity and Open Questions:

• settled behavior is documented directly;
• provisional behavior is documented only as far as decisions have been made;
• unspecified behavior is identified without inventing a default.

Current compiler coverage, target restrictions, and µDewy compatibility belong to Implementation Compatibility. Those implementation notes do not redefine the source language.

Conventions

• Dewy source conventionally uses the .dewy suffix.
• µDewy source conventionally uses .udewy; suffixes do not select Dewy semantic rules.
• Code labelled provisional illustrates a design whose stated portions are decided but whose surrounding rules may change.
• T | none denotes an optional value.
• exception is the nominal parent of values forwarded by safe navigation; both error and none descend from it.
• intN and uintN denote fixed-width signed and unsigned integer families when a rule applies uniformly across widths.
• “Produces” describes the value or values expressed by a construct. void means that no value is produced.
• “Place” means a mutable storage location selected explicitly with @; it is not an accidental alias created by an optimization.

Unless a section explicitly says otherwise, evaluation proceeds from left to right within the order established by grouping and operator precedence.

Lexical Structure

Source Text

Dewy source is Unicode text. Source-file suffixes are conventional and do not alter tokenization or semantic rules.

Case

Dewy is case-sensitive. Keywords (let, loop, if), word operators (and, or, not, in?, is?), the booleans true and false, and symbols are matched exactly as written: True, AND, and Loop are ordinary identifiers, distinct from each other and from true, and, and loop. Case does not matter in two places, both where the strict reading would silently mean something else: inside a numeral, the alphabetic digits of a based integer (0xff and 0xFF) and the exponent marker (1e5 and 1E5) may be written either way, while the base prefix itself is lowercase (0x, 0b; 0X is not a prefix); and the two string escapes that take digits, \u/\U (a scalar, \u{1F600}) and \x/\X (a hex byte escape, which Dewy rejects), are recognized in either case. Every other escape is lowercase (\n), and a backslash before any other character is that character itself (\N is N).

Identifiers

An identifier contains at least one base character. Decorations may appear before or after that base character, and decimal digits may follow it.

The current base repertoire contains ASCII Latin letters, the ordinary Greek alphabet, _, ‾, !, °, and selected mathematical letter symbols such as ℂ, ℕ, ℤ, ℚ, and ℝ. Decorations include the supported Unicode superscript and subscript letters and digits, prime marks, and ℠, ™, ©, and ®.

Identifiers are case-sensitive. The exact Unicode repertoire and its normalization/security policy remain provisional; implementations must document the repertoire they accept and must not silently normalize two distinct source spellings into one binding.

Reserved operator words such as and, or, not, in, as, and transmute tokenize as operators in their grammatical contexts. A word operator cannot simultaneously be used as an ordinary identifier in that context.

Whitespace and Juxtaposition

Whitespace separates tokens. Dewy does not generally use commas to separate arguments, parameters, or array elements.

Spacing can also determine whether expressions are juxtaposed with a punctuation operator. Range endpoints are the clearest example:

first..last    # both endpoints
first ..last   # no left endpoint
first.. last   # no right endpoint
first .. last  # no endpoints

Newlines normally behave as whitespace. A construct may assign additional structural meaning to line boundaries only where its grammar explicitly says so. One does: return and yield take a value only from their own line, so at a line end they return nothing — if done return followed by a statement on the next line returns, and the statement is not the returned value. A value that needs several lines starts on the keyword's line (return ( … )). A ; ends a bare return on the same line.

Comments

# begins a line comment. #{ and }# delimit a nestable block comment.

# one line
#{ outer
   #{ nested }#
   outer again
}#

Comment markers inside strings are string contents.

A documentation string is an ordinary call of the prelude's doc with a string — usually a """ block — at the top of a module, a function body, or a type. The compiler keeps nothing from it yet, so the call is a no-op:

doc"""
Tokenizer framework.
"""

Tokens and Ambiguity

Tokenization chooses the longest valid token subject to explicit lexical rules. Parsing may preserve several structurally valid interpretations—most notably call, indexing, and multiplication juxtaposition—until types and context resolve them.

See Literals for literal tokens and Operators and Precedence for expression grouping.

Literals

A literal introduces a value directly in source. Literal syntax may preserve more exact type information than the eventual context requires. In a type context the same literal is a singleton type — see Literal Types.

Booleans and Absence

true and false are the two bool values. none is a storable value used in unions such as T | none. void describes the absence of a produced value and is not interchangeable with none.

Integers

Decimal integers require no prefix. Integer numerals support the following bases; the prefix is lowercase (0x, never 0X) and the alphabetic digits after it are case-insensitive:

42
0b101010
0t1120
0q222
0s110
0o52
0d42
0z36
0x2a

An integer literal initially has an exact value type. Context may place it in int, uint, or a compatible fixed-width integer type. A literal outside the destination range is rejected rather than truncated.

Underscores may group digits without affecting the value: 1_000_000.

Prefixes for bases above 16 are available only on quoted packed data. An unquoted higher-base digit sequence is rejected rather than silently tokenized as a different value.

Decimal and Exponent Literals

A numeral with a fraction or a decimal exponent — 9.8, 1.25e2, 5e-1 — is an exact rational (49/5, 125, 1/2), never a floating-point approximation. Binary exponents and non-decimal bases in such literals are not yet supported.

Integer numeral prefixes and packed based-string prefixes are related spellings with different results. An unquoted 0x2a is an integer; quoted 0x"2a" is packed data.

Strings

Single and double quotes delimit strings. Both forms have the same string semantics.

'short text'
"text with {interpolation}"

Escape syntax may insert code points. Interpolation braces contain ordinary Dewy expressions. See Strings and Graphemes.

Packed Based Strings

Power-of-two based strings encode digit sequences densely as exact bytes:

0b"11110000"
0x"deadbeef"

The supported packed prefixes are 0b, 0q, 0o, 0x, 0u, and 0g, contributing 1, 2, 3, 4, 5, and 6 bits per digit respectively. Bits are appended in source order from each digit's most-significant bit to its least-significant bit. A final partial byte is padded with zero bits on the right.

Whitespace and comments may separate digits. Base 64 uses the ordered alphabet 0–9, a–z, A–Z, +, /; - aliases +, _ aliases /, and trailing = is explicit padding that contributes no bits. _ is therefore a digit in a base-64 string rather than a visual separator.

Non-power-of-two dense packing remains a provisional design because the width of concatenated subsequences is not generally compositional.

Container and Object Literals

Square brackets use the top-level contents to determine the constructed form:

[1 2 3]                       # array
[name="Ada" active=true]     # object
["Ada" -> 1 "Grace" -> 2]   # dictionary
set[1 2 3]                    # set

Array, object, dictionary, and set forms are settled; a dictionary or set literal may appear in any expression, and an empty one needs a dict<K V> or set<T> context. Postfix ... spreads an existing container into a literal: [xs... 0 ys...] builds an array from the elements of arrays (or the members of sets) and written elements, with an exact length when every operand's length is known; [base... c=3 other...] builds an object from the fields of objects and written fields, a later entry winning over an earlier one with the same name (at the first one's position), as in Python. This is how containers combine — + never concatenates. Operands are named values (bind a computed value first) with a non-union type; spreading into dictionary and set literals is not implemented yet. Bidictionary and multidimensional literal details are catalogued in Arrays and Containers and the design appendix.

Source Files and Execution

A source file is a compilation unit. Its executable top-level expressions run once in source order after imported dependencies have initialized.

A program does not require main. When a zero-argument function named main exists in the entry module, the program invokes it after top-level initialization.

printl"initializing"

let main = ():>int64 => {
    printl"running"
    return 0
}

main may return void or an integer exit status. Additional standardized entry parameters such as command-line arguments and environment access are provisional.

An explicit top-level call to main() is an ordinary call and does not suppress automatic entry invocation.

Imported modules initialize once in dependency order. Import cycles and colliding names are errors unless a future construct explicitly defines a valid cycle or disambiguation.

Bindings, Initialization, and Scope

Declarations

let creates a mutable binding. const creates a binding that cannot be reassigned after initialization.

let count = 0
const limit = 10

An assignment to a name with no visible binding implicitly declares a mutable binding. Otherwise it updates the visible mutable binding:

message = "hello"     # implicit let
message = "welcome"   # reassignment

Type annotations follow ::

let count:int64 = 0
const Name:type = string

Declarations and assignments produce void.

An unpacking target [a b] on the left of = (with or without let/const) binds each name. An object source is unpacked by field name: each target names the field it takes, in any order and any subset. An array, dictionary, or set source is unpacked by position (insertion order for dictionaries and sets), and its exact count must be known: the target count must equal it, _ discards a value, a nested […] unpacks an element further, and a dictionary entry is unpacked as [key value]. Each name follows the ordinary declaration rule: let/const declare, and a bare target declares a new name or assigns an existing one. The source value is evaluated once.

Lexical Identity

Each declaration creates a distinct lexical binding. A child scope may shadow an outer binding without changing the outer value.

{} creates a child lexical scope. () groups expressions in the surrounding scope.

let value = 1
{
    let value = 2
    printl"{value}"    # 2
}
printl"{value}"        # 1

Initialization

An eager expression cannot read a binding before that binding is initialized on every reachable path.

A binding is assigned only within the module that declared it. The prelude's bindings and a module's imports are read here but not written: run = … or A = … at the top of a module is an error naming where the binding belongs and suggesting let — let run = … declares a new run that shadows the prelude's within this module.

Function bodies may refer to declarations that occur later in the same enclosing scope — whether the later function is declared with let or by a bare name = (…) => … (a first name = value in a block declares; a later one assigns). The relevant requirement is that each reachable call occurs after every eagerly read captured binding has been initialized. This permits mutually recursive and forward-declared function relationships without permitting an uninitialized runtime read.

Captures

A function body may refer to bindings in enclosing lexical scopes. If the function escapes the lifetime of those bindings, its closure must preserve the captured state according to Dewy's value and place semantics.

The complete representation and identity rules for escaping closures remain provisional. This does not change lexical name resolution.

Values, Copies, and Places

Value Semantics

Assignment, argument passing, and return supply an independent value. Mutating the destination cannot change the source merely because an implementation reused backing storage.

let original = [1 2 3]
let copy = original
copy[0] = 9                  # original remains [1 2 3]

The compiler may realize that semantic copy through physical copying, a move, ownership transfer, borrowed reading, shared immutable storage, or another representation whose differences are unobservable.

Scalar, array, object, string, and container values all follow this rule. A field whose own type has explicit handle semantics retains those semantics when its containing value is copied.

Places

@ explicitly selects the place occupied by a mutable value. A parameter that accepts a place also carries @, making caller-visible mutation explicit at both boundaries:

let update = (@xs:array<int64 length=3>):>void => {
    xs[0] = 9
}

let values = [1 2 3]
update(@values)

Passing values without @ supplies an ordinary value. Passing @values to a non-place parameter is likewise a type error.

Projected Routes

A leading @ selects the place at the end of the complete field-and-index route:

set(@pair.left)
set(@values[i])
set(@box.rows[row][column])

The parser groups @pair.left as (@pair).left, but the language does not expose @pair as a separate reference value before applying .left. The whole expression refers to the place occupied by left. Putting the route inside the prefix, @(pair.left), selects the same place. Grouping the completed selection, (@pair.left), ends the @ chain; this distinction matters when a following argument group calls a selected function. There is no pair.@left form. A computed index in a place route evaluates once before the call.

Type and Aliasing Rules

A mutable place is invariant in its value type: a callee must not reinterpret the caller's storage through a broader or narrower place contract.

Two mutable place arguments in one call must be proven disjoint. Sibling object fields and distinct constant indices are disjoint. Prefix-related routes overlap. Dynamic indices are potentially overlapping unless analysis proves otherwise.

A const binding does not provide a mutable place.

Escaping Places and Identity

Nonescaping place calls have settled semantics. Storing or returning a place, sharing it across concurrent work, and defining lifetime-bearing place types require the provisional ownership and escape design.

There is no place-identity test: places are borrows rather than first-class values, and the ownership model never exposes storage sharing between independent values, so the once-reserved @? was retired (see Operators and Precedence).

Function handles build on the same root-and-route interpretation of @; see Functions and Calls.

Provisional User-Managed Handles

The future systems escape hatch builds on, but does not change, the rules above. A library-defined shared-ownership type such as Rc<T> is intended to remain an ordinary Dewy value. Copying the handle retains its explicitly shared payload; copying an object containing such a handle does the same recursively. This does not make ordinary arrays or objects reference-semantic values.

@rc selects the place occupied by the handle, allowing a callee to replace that handle in the caller's binding. It does not select the allocation behind the handle. Payload access will instead use lifetime-bounded places supplied by the handle type: read-only while shared, and mutable only after unique ownership is established or through a separate checked-mutation abstraction.

The required userland lifecycle and allocation hooks are provisional and not implemented. The current design direction is recorded in the compiler's user_managed_storage.md note.

Storage and Escape Copies

Where a value's bytes live is the implementation's business, but it is observable in one way: cost. A string may be static (a literal), arena-backed (decoded bytes, a join), owned by a container (an array element, an object field), frame-backed (an interpolation, or a call result copied into the calling frame), or a parameter's (the caller's, unknown to the callee). Storing a string where it outlives the current evaluation — into a growable array, an object field, a union cell — stores a static literal as it is, takes over a fresh arena string nobody else holds (a join or a decode stored directly), and copies everything else into the arena, so every stored string has exactly one owner. dewy analyze file.dewy lists every such escape copy with its reason, so the copies a program pays for are never a mystery; the ownership model's later steps (moves by liveness, borrowed parameters) will remove the ones that proofs can.

A transfer at a value's last use is a move: return xs, [items = xs], box.items = xs, or return box for a local built here, when nothing uses the local afterwards (and the store is not inside a loop the local outlives), adopts the arena storage instead of copying it. Transfers of a value that is used again copy, as value semantics require. dewy analyze lists every transfer of an owned array as a move or a copy with its reason.

An array of strings owns its elements: when a local array's scope ends (or the binding is rebound), the element strings are released with the buffer — so building and dropping string arrays in a loop runs in constant memory. It follows that element strings never alias: reading an element out and storing or returning it copies it, and a copy of a string array (let copy = parts) gets its own element strings. dewy analyze reports each of these copies too.

Objects own their runtime-sized members the same way. When a local object's scope ends, its string fields, its array fields (with their elements), and the string payloads of its union cells are released; a copy of an object (let two:Point = one) owns copies of its own; assigning over a string field (two.name = "changed", through a nested object or an element too — o.inner.name = …, pts[0].name = …, xs[0] = …) releases the value it held; an exact-length local array releases its element strings and element objects with it; and a literal or call result stored into an array or returned moves its members into the new owner rather than cloning them. Dictionaries are objects of arrays, so a local dictionary releases its keys and values too. Building and dropping objects, arrays of objects, and dictionaries in a loop runs in constant memory.

String storage that never leaves a function — slices, decoded bytes, joins that no return reaches (stores copy such strings into the arena as described above) — comes from the function's frame region, a scoped arena created on entry and released whole at every exit, so string work in a loop does not accumulate. Strings a return may hand out, and their sources, stay in the process arena.

A loop body gets a region of its own: a string it builds that stays within the iteration — no assignment carries it to a binding declared outside the loop — is given back at the end of every iteration (continue and break included), so string work inside a long loop runs in constant memory rather than accumulating until the function returns. A string assigned to an outer loop's variable lives in that loop's region; one assigned to a variable of the function lives in the function's. Stores into arrays, fields, and dictionaries copy, as before.

String locals own their values. A local whose every value is a function's result, a literal, a view, an interpolation, or a join releases it when its scope ends; return s moves it to the caller instead; a return that only reaches it (return s.trim) copies; assigning over it releases the old value first. Every string a function hands back belongs to the caller: a parameter (or a module variable) returned as it is comes back as a fresh view of the same bytes, and a call result that nothing keeps — an argument (printl(f(x))), a receiver, the element copies of a [a b].join literal — is released after its statement. A local that holds a view of another local (let t = pick(s true)) is safe because the viewed local outlives it, and returning such a view copies. The same rules cover a runtime-length array a call returns that nothing keeps (text.split" ".length: released after its statement), the strings a loop's condition builds (the loop's region), and an optional or union local — or a match temporary — that holds a call's string payload: it is released at scope exit, return maybe moves it to the caller, and a return that reaches it through another local clones it. Building strings through calls in a loop therefore runs in constant memory.

Runtime-sized storage is released when its owner is done with it. A growable array's old buffer is given back the moment growth relocates it, and a local that owns an array releases it at every exit of its scope — the end of the block, a return (after the returned value is computed; a returned array is copied out first), a break or continue. A loop that builds and drops a 1000-element array 10 000 times therefore runs in constant memory. Only storage the arena owns is released (a literal's static data and a borrowed parameter's are not); nothing is freed twice, because a released descriptor forgets that it owned anything.

Types and Conversions

Dewy statically checks values and expressions. Types describe semantic values; implementations may select any representation that preserves those semantics.

Type Values and Aliases

A type is a compile-time value of type type. A binding may name it explicitly or infer a type-valued expression:

const Name:type = string
const Index = <int64>
const MaybeIndex = <int64 | none>

<> groups a type-valued expression where ordinary expression context would otherwise treat it as a runtime value. Alternatives inside use the normal type operators: <int64 | string>, not whitespace-separated alternatives.

A type alias does not create nominal identity unless its defining construct explicitly requests generativity.

Nominal Identity

type of Parent evaluates to a fresh nominal child of Parent — so a value of type of any & Info also satisfies an Info parameter, the structure's fields leading the child's. Implemented today: error types (type of error, alone or & [...] for an error carrying fields) and object types, where the operand may be an object type, any alone (an empty marker type), or an intersection of any with object types (& contributes structure, never identity):

let NotFoundError:type = type of error
let Name:type = type of any & [text:string]
Punct = type of any & [text:string]     # same structure, distinct type
let Vec = type of [x:int64 y:int64  length_squared = ():>int64 => x*x + y*y]

type of Parent where Parent is itself a minted type mints a nominal child: a subtype of the parent (a Whitespace value satisfies a Token parameter, and t is? Token holds for every child in a union), distinct from the parent and from its siblings. A minted value carries its brand at runtime, so a value seen through the parent still says which child it is: ctx is? Root on a Context tests the brand, match ctx { r:Root => … <StringBody> => … } selects by it and binds the child with its own fields, and a child stored where the parent is expected — a Context variable, an element of array<Context>, a Token | none member — is stored whole (a parent-typed slot is sized for the largest child). The parent's fields lead the child's, and the operand may add more (type of Token & [text:string]); one nominal parent per mint.

Conversion to string follows the brand too: a value seen through its parent — or through the structure the mints were minted from — converts as what it is, so an array<TokenProtocol> prints each element as its child. A parent's __as__ applies to every child (a child may override it), and can name the child through typename, read bare inside a method like any field: the minted name a value carries, or a plain object's structural spelling.

let Protocol:type = [
    eat:<(src:string):>int64>
    __as__ = ():>string => "<{typename}>"
]
Whitespace = type of Protocol & [eat = (src:string):>int64 => 1]

describe = ():>string => {
    let table:array<Protocol> = [Whitespace]
    return "{table}"                    # "[<Whitespace>]"
}

Types as Values

The types minted under a family are runtime values. type<Token> is the type of those values — Token itself when it is not $abstract, and every type minted under it — and a value of it is carried as the brand id an instance carries. It is stored, compared (kind =? Whitespace), tested (kind is? Whitespace: the type it names is Whitespace or minted under it), and matched, exhaustively by the same closed-world rule as an instance; kind.typename is its name. typeof(value) reads the type a minted value carries as such a value.

A method that reads no field of its type — and calls no method that does, transitively — is static: it is called off the type's name (Whitespace.eat(src ctx)), off a type value (kind.eat(src ctx), which dispatches to the named type's method), and off an instance alike. A method that reads a field needs an instance, and saying Whitespace.width for one is an error. Calling a type value constructs the type it names, with the family's own required fields: kind(src=… idx=…) — a type under the family may add fields only with defaults, and fills every function-typed slot with a method.

Token = $abstract type of any & [
    src:string  idx:int64
    eat:<(src:string):>int64?>                     # a slot every kind fills
    width = ():>int64 => src.length                # reads a field: an instance method
]
Whitespace = type of Token & [eat = (src:string):>int64? => if src.startswith(" ") 1 else none]
LineComment = type of Token & [eat = (src:string):>int64? => if src.startswith("#") src.length else none]

next_token = (src:string):>Token | none => {
    let kinds:array<type<Token>> = [Whitespace LineComment]
    loop kind in kinds {
        match kind.eat(src) {
            n:int64 => { if 0 <? n <=? src.length return kind(src=src[0..n) idx=0) }
            <none> => {}
        }
    }
    return none
}

A match over a minted type is exhaustive when its arms cover every brand the whole program mints under it — the parent itself included unless it is $abstract. $abstract is written on the mint and says the type has no values of its own, only its children's: constructing it is an error at that site, it is no unit inhabitant even without fields, and its children alone make a match exhaustive. A child minted in a module compiled later still counts (the program is one closed world), so a match without an else reports it; with an else, later children take that branch.

Context = $abstract type of any & [depth:int64]
Root = type of Context & [base:string = '0d']
StringBody = type of Context & [quote:string]

describe = (ctx:Context):>int64 => match ctx {
    r:Root => r.base.length + r.depth
    s:StringBody => s.quote.length            # exhaustive: Context is abstract
}

A minted type with no fields is both the type and its single inhabitant — written with its name where a value is wanted, as an error type is: [Whitespace Name(text='x')], return Whitespace, let w = Whitespace (Whitespace() constructs the same value). The same holds for a minted type every field of which has a default: its bare name is the construction Name(), as a callable with no required parameters is called by its name. A method declared in a mint under the name of an inherited function-typed field is that field's value — the child implements the protocol's slot — so Whitespace = type of Protocol & [eat = (src:string):>int64 => …] is fully defaulted and [Whitespace LineComment] is an array<Protocol>.

let Token = type of any
let Whitespace = type of Token
let Name = type of Token & [text:string]

A minted object type is structurally its operand but distinct from every other type, including a structurally identical one: Name | Punct is a two-member union that match distinguishes, and a Name value does not satisfy a Punct annotation. The type prints by its name. Values are constructed by calling the type (Name(text='hi'), positionally Vec(3 4)) or by an object literal in the minted type's context (let n:Name = [text='hi']); methods and &= constructor overloads work as on any object type. Numeric parents such as type of int are not implemented yet:

const UserId:type = type of int

Each evaluation of type of creates a distinct identity. Referring to or aliasing the resulting binding preserves that identity. <T of Bound> in a generic parameter is a bound declaration and is not this generative expression.

An alias is declared by any of Name = <type expr>, let Name = <type expr>, Name:type = <type expr>, or let Name:type = <type expr>. Intersecting object types strengthens structure without minting: Root = Context & [tag:string='root'] has Context's fields plus tag (and stays Context's nominal kind when Context is minted — a Root satisfies a Context parameter); a same-name field must fit the inherited one and replaces it, so a mint may narrow an inherited default (type of Report & [severity='error']). A field written name = value takes the default's widened type; construction is by calling the type (defaults fill omitted fields).

type of is the only generative type operation. Intersection does not mint nominal identity:

const ContextError:type =
    (type of error) & [context:string code:int64]

const DetailedContextError:type =
    ContextError & [source:string]

ContextError has one fresh identity beneath error. DetailedContextError is the same nominal kind with a stronger structural requirement; it does not add another node to the nominal tree. Consequently, ContextError | DetailedContextError simplifies to ContextError.

Intersections

A & B requires both operand types and is non-generative, including when an operand carries nominal ancestry. Re-evaluating equal intersections produces equal types.

Structural-object intersections merge requirements by field name. A field found on only one side is retained. Matching fields intersect their required types:

const T1:type = [a:int | bool b:string c:bool | none]
const T2:type = [a:bool b:int]

# a requires (int | bool) & bool, which simplifies to bool
# b requires string & int, which simplifies to never
const Impossible:type = T1 & T2  # compile-time error

A required never field makes the complete object intersection uninhabited; presenting that result as a constructible declared type is a compile-time error. Matching fields must also agree on mutability. A mutable requirement and a const requirement are incompatible because neither contract can safely stand in for the other.

These rules keep & associative, commutative, idempotent, and independent of declaration identity. Because object field order otherwise participates in structural types, normalization of a merged intersection must choose the same semantic field order independently of operand order; the exact canonical ordering and layout remain representation-design work.

Inference and Context

Literals retain exact information until context requires a broader type. An unannotated mutable integer binding widens from its literal singleton to int; a fixed-width annotation accepts the literal only when it fits.

Function parameters, returns, container elements, object fields, assignments, and operator overloads all provide type context.

Optional Sugar

T? in a type position is T | none: let word:string? = none, a parameter (v:string?), a result :>int64?, an element dict<string int64?>. ? does not appear in value positions; narrowing an optional is the ordinary is?.

Unions and Narrowing

A | B accepts a value belonging to either alternative. T | none is an optional value. Type and literal tests such as is? and isnt? narrow the tested value along control-flow paths.

General runtime unions are tag-and-payload cells; none, when present, is always member 0, so an optional is the two-member case of the same layout. A union whose members include several concrete types together with none (Node | int64 | none) is an ordinary union, including as a parameter or result.

Narrowing applies to member routes as well as bindings: after if node.next is? Node, node.next reads as Node until the field or its object is assigned. A store into a union field always accepts the field's declared type, and forgets any narrowing of that route.

A type test against a union of string literals is a membership test when the value is a runtime string: head is? BasePrefix with BasePrefix:type = '0b' | '0t' | '0x' compares head with each member, and narrows it to the union where the test passes. A test the static types settle is decided while checking (a three-grapheme string is never a two-grapheme member; see Generic Functions).

let BasePrefix:type = '0b' | '0t' | '0x'

let classify = (text:string):>string => {
    if text.length >=? 2 {
        let head = text[..2)
        if head is? BasePrefix { return head }
    }
    return "none"
}

let main = ():>int64 => classify("0x1f").length     # 2

Recursive Types

A type alias may refer to itself, but only as a union member of one of its fields:

let Node:type = [value:int64 next:Node|none]
let Tree:type = [value:int64 left:Tree|none right:Tree|none]

The recursive member is stored behind a handle, which is what makes the object finite. A field typed exactly Node (no union) is rejected as an infinite value, and an alias whose every union member is itself has no base case and is rejected too. Values keep value semantics: copying a Node | none deep-copies the chain it points to, and narrowing a recursive member (cur.next is? Node) yields the object itself, so cur.next.value reads and writes through the handle.

An alternative belonging to the nominal exception family receives special receiver-navigation behavior. Member access operates on every ordinary alternative that supports the member and forwards every exception alternative. Both error and none descend from exception; arbitrary union alternatives do not become skippable. See Errors, Exceptions, and Forwarding.

Parameterized Types

Parameterized types apply compile-time arguments:

array<string>
array<int64 length=3>
Duration<uint64>

User type aliases take parameters the same way: let Box:type = <T>[value:T], then Box<int64>.

Generic Functions

A generic function declares its type parameters before the parameter list and must declare its result type:

let first = <T>(xs:array<T>):>T | none =>
    if xs.length >? 0 xs[0] else none

let swap = <T U>(a:T b:U):>[x:U y:T] => [x=b y=a]

let total = <T of int>(a:T b:T):>T => a + b

let main = ():>int64 => {
    let words:array<string> = ["hi"]
    let w = first(words)          # T = string
    let s = swap(1 "one")         # T = int64, U = string
    return total(20 22) + s.y     # 43
}

Type arguments are inferred from the arguments (and a contextual result type), structurally through arrays, objects, and function types; a literal argument binds its ordinary type (1 is int64, "one" is string). T of Bound restricts the arguments a call may supply. The body is checked per instantiation with the type parameters bound to the inferred types — an operation the instance's types do not support is reported at that use, as it would be in a plain function — and each distinct instantiation is compiled as an ordinary function (first__string). A generic function is declared with let at module level, is called by name, and cannot be used as a value. Generic type aliases that refer to themselves, and generic local functions, are not implemented yet.

A type test the static types settle is decided while checking — v is? string is true when v's type is string and false when it cannot be — and only the live arm of an if on it is checked. In a generic, that is how a body varies by type parameter: each instance keeps the arm written for its type, which may use members the other arm's type lacks.

let size = <T>(v:T):>int64 => if v is? string v.length else 1

let main = ():>int64 => size("abc") + size(true)   # 4

Literal Types

In a type context a literal denotes its singleton type: x:5 admits only 5, d:0 only 0, s:"one" only "one", and a packed literal 0x"6869" only those bytes. Type contexts are annotation positions (name:T, :>T), the right-hand side of name:type = …, and an explicit type block <…>; anywhere else a literal is a value, and <…> is the way to write a type expression where the context alone would read it as values (<1 | 2 | 3> is a type — as values 1 | 2 | 3 would be or between numbers).

Unions of literals are enumerations, mixed freely with other types, and is? narrows them:

let Mode:type = <1 | 2 | "fast" | "slow">

let describe = (m:Mode):>int64 =>
    if m is? 1 10 else if m is? 2 20 else if m is? "fast" 30 else 40

let main = ():>int64 => {
    let m:Mode = "slow"
    return describe(m) + describe(2)    # 60
}

A literal-typed parameter specializes an overload — dispatch picks the most specific applicable method, and each call has the selected method's result type:

let DivZero:type = type of error
let safe_div = ((n:int64 d:0):>DivZero => DivZero)
             & ((n:int64 d:int64 & ~0):>int64 => n // d)

let main = ():>int64 => {
    let q = safe_div(6 3)             # int64
    let e = safe_div(6 0)             # DivZero
    if e is? DivZero { return q }     # 2
    return 0
}

The literal method wins exactly when the divisor is the literal 0; int64 & ~0 — the intersection of int64 with the negation of the literal type 0 — is the structural spelling of the refinement int64<d not=? 0>, so the two methods partition int64, the general method's n // d is proven, and a call with a runtime divisor must establish d not=? 0 first (a guard, or a $runtime_assert). Boolean literal types (true, false) are not implemented; use bool.

Refined Types

Refinements attach facts that values must satisfy. On a named declaration the declared name is the value — d:int64<d not=? 0>, xs:array<int64 xs.length >? 0> — while the lambda form names it where there is no name (Positive = int64<i => i >? 0>), and length>?0 alone still means the sequence's length. An object value can be refined by an integer field (r:Ratio<bottom >? 0>), and length on an array is the same idea for the one measure arrays expose today. Excluding literals has a structural spelling: int64 & ~0 and int64 & ~(0 | 1) are int64<d not=? 0> and int64<d not=? 0 and d not=? 1>. On a binding they are proven at the declaration; on a parameter at every call site and assumed inside the body (see Refined Parameters). The exact general refinement proposition language and proof interfaces remain provisional; value comparisons against constants and length facts use this model today.

as

as requests a meaning-preserving conversion defined for the source and destination types:

value as string
text as array<uint8>

Conversions may change representation and may invoke overloadable conversion behavior. Lossy or fallible operations require an interface whose type exposes that possibility rather than silently discarding information.

A declared type says how its values convert with a conversion method: __as__ = ():>T => … serves x as T, and — for T = string — string interpolation ("{x}"). The target type is the method's result type; nothing about a type's name or shape is special to the compiler. The prelude's Path converts to its text this way, which is why p"{root}/{name}" joins paths:

let Point:type = [
    x:int64
    y:int64
    __as__ = ():>string => "({x}, {y})"
]

let main = ():>int64 => {
    let pt = Point(3 4)
    let text:string = pt as string      # "(3, 4)"
    printl"{pt} and {p"a/b.c".parent}"  # (3, 4) and a
    return text.length
}

A type, a function, or an overload set has no runtime representation; where a value is needed — T as string, an interpolation field "{T}", printl(T), a generic's value parameter — it is its spelling ('0b' | '0t', <(a:int64):>int64>), which makes such things printable while debugging. A container, or an object whose type declares no __as__ to string, converts to string as its literal syntax ([1 2 3], [x=1 y=2]; see Printing). Any other value whose type has no fitting __as__ is an error where it is converted (unsupported value conversion, or no string conversion for this value). A type converts to several targets by adding conversions with &= — __as__ &= ():>int64 => x * 100 + y after the first — and x as T picks the one whose result fits T.

transmute

transmute reinterprets a compatible representation without performing a semantic conversion. It is valid only where source and destination layouts satisfy the transmute contract. It must not be used as an implicit substitute for numeric or textual conversion.

See Numeric Types, Strings, and Design Maturity.

Numeric Types

Integer Semantics

int is an arbitrary-precision signed integer type. uint is its nonnegative counterpart. Their semantics do not silently change to machine-width overflow because a compiler chooses a compact representation.

Fixed-width types use intN and uintN names such as int8, int32, and uint64. Arithmetic and bitwise operations on a fixed-width value remain at that width and roll over according to its bit representation.

The natural numbers, nat and natN (nat8 … nat64), are the non-negative integers of a signed width: nat64 is int64 & <(>=? 0)>, an int64 carrying the fact that it is never negative. It is what a count is; a size is the addr below. Being an int64 underneath, a nat64 takes part in int64 arithmetic without conversion (src.length - i), and stores into a uint64 by its own fact; storing an int64 into a nat64 is the proven conversion described below (let n:nat64 = a - b after if a >=? b), never a wrap. A nat64 may carry further facts (nat64<(<=? src.length)>). Use uint64 for what is genuinely a bit pattern — hashes, masks, wrapping arithmetic — not for sizes.

addr is the natural that fits the target's address space: a nat64 carrying one more fact, that it is a position — below 2^bits, where bits is the target's address width (48 on x86_64, arm, riscv, and c; 32 on wasm32), so it is [0, 2^48) on a 64-bit target and [0, 2^32) on wasm32. It is what .length is, and what an offset or an index is. Two positions in one address space add and subtract without leaving it — the same axiom that lets a length grow one element at a time — so s.start + by, end - start after if start <=? end, and i + 1 under i <? src.length are addr values with no further proof, where a nat64 + nat64 is an int64 sum that may wrap. Storing an arbitrary nat64 or int64 into an addr is the proven conversion: it passes when the facts bound the value by a length (i <=? src.length after a guarded loop, an index fact, a :>addr<(<=? src.length)> result) or by a constant below the cap, and is otherwise an error naming the obligation (value is a position in the address space); a product or an unbounded sum is not a position. A constant at or above the cap is refuted. An addr is a nat64 wherever one is wanted, and a record field or binding made from an addr keeps the name ([length=result] from an addr is [length:addr]). Spans and offsets in the standard reports are addr.

let count:int = 10
let byte:uint8 = 255
let offset:int32 = -12

An integer literal is admitted to a numeric context only when its exact value belongs to that type.

Representation and bigint

The compiler chooses how an int is stored. Range analysis proves most values fit a 64-bit word, and those lower to machine integers. A value it cannot prove word-sized — an oversized literal, a product of unbounded operands, a loop accumulator without a bound — takes the arbitrary-precision representation automatically, and every binding it flows into follows. The semantics are the same either way; only the cost differs, and dewy analyze reports each place a big integer was chosen and the range that forced it.

bigint names that representation explicitly: a bigint binding is always arbitrary precision, and any integer converts to it.

let seed = 3000000000
let cube = seed * seed * seed      # 2.7e28: stored as a big integer
let big:bigint = 5                 # explicitly arbitrary precision
let f = 2^100                      # constant, folded exactly

A big value cannot silently cross a word-sized boundary. Returning it from a function whose result type is int or int64, passing it to a word-sized parameter, or storing it in a fixed-width binding is a compile error unless a comparison proves the range or the boundary is annotated bigint; int in a signature is a 64-bit word, so functions that carry big values say bigint.

An explicit bigint can cross a fixed-width boundary after a range guard; as uses the same proof as an annotated binding or result. Both signed and unsigned limits are inclusive, and widening a uint64 to bigint preserves all 64 bits.

let byte = (n:bigint):>uint8 | none => {
    if n >=? 0 and n <=? 255 return n as uint8
    return none
}

A bigint converts to decimal text with as string and in interpolation. The retained text uses the same digits and sign as printing, including zero; optional big integers render none when absent. Integer values also retain the required conversion when stored in bigint | none: a present machine word becomes a big integer, and absence remains absence.

Arithmetic, comparisons, //, %, ^, and / (an exact rational) apply to big integers. A bigint is 0 | [sign:-1|1 limbs:array<uint64 length >? 0>]: zero is its own case rather than a sign value, so no negative zero and no zero with limbs is representable (canonical limbs — no leading zeros — remain the constructors' convention). if x =? 0 / x not=? 0 narrow between the two cases like is?, bigint & ~0 names the nonzero form, and a big divisor must have it: a // b, a % b, and a / b need if b not=? 0 { … } or a b:bigint & ~0 parameter (cannot prove the divisor is nonzero otherwise); a word divisor is proven the way any int64 & ~0 argument is.

let ratio = (n:bigint d:bigint & ~0):>rational => n / d
let half = (n:bigint):>bigint => n // 2          # a constant divisor proves itself
let big:bigint = 2^128
if big not=? 0 { let q = ratio(1 big) }          # `big` is `bigint & ~0` here

Shifts

Shift counts are unsigned. A negative literal count is therefore a type error.

For a fixed-width value, shifting by at least its width reaches the continuation bits of that shift:

• left shift produces 0;
• unsigned right shift produces 0;
• signed right shift produces 0 for a nonnegative value and -1 for a negative value.

Operands are evaluated once.

Rationals

rational is an exact fraction, kept normalized: a positive denominator and coprime parts. Like bigint it is 0 | [numerator:bigint & ~0 denominator:bigint<sign =? 1>] (the positive denominator is a type fact) — zero has no parts, so q.numerator and q.denominator are read behind if q not=? 0 { … }, which is also what a rational divisor needs. a / b on integers yields a rational (// is floor division and stays integral); a decimal literal such as 9.8 or 1.25e2 is an exact rational. +, -, *, /, negation, and the ordered comparisons apply, and an integer operand promotes to a rational. Constant rational expressions fold at compile time; a constant zero divisor is a compile error. Rationals print as n/d, or as an integer when the denominator is one. A decimal literal is a rational unless fixed is requested explicitly — by an annotation (let x:fixed = 0.1) or a fixed operand — and that coercion is the one lossy step: the constant rounds to the nearest Q32.32 value there (a constant outside the fixed range is a compile error).

The runtime representation is a pair of int64 parts; overflow beyond that range is currently unchecked, and a runtime zero divisor is an open error-value question.

Fixed-Point

fixed is a signed fixed-point number with 32 integer and 32 fraction bits. Conversions from integers and rationals round to nearest; multiplication and division truncate toward zero. A fixed operand absorbs integer and rational operands, so mixed arithmetic yields fixed. Trigonometric functions produce fixed values. Fixed values print in decimal with trailing zeros trimmed.

Powers

base ^ exponent is right-associative. An integer base with a constant non-negative exponent, or an unsigned runtime exponent, yields an integer; a negative constant exponent yields a rational; a rational base takes any integer exponent. Dimensioned quantities raise their dimension to the same power and require a constant exponent.

Floating Point

First-class IEEE floating-point types and arithmetic are planned. The initial focus is on making the numeric types people reach for without specialist mathematical or engineering knowledge work intuitively: integers, exact rationals, and fixed-point values. This sequencing does not limit the eventual numerical scope of Dewy; conventional scientific computing, including the kinds of array and tensor operations supported by NumPy and PyTorch, is an intended use case.

Floating-point arithmetic is not implemented yet. It is expected to arrive alongside the full matrix math system, although that sequencing is tentative. Supported formats, conversions, mixed-type promotion, exceptional values, and numerical execution policies remain design work; floats are not restricted to host interoperability.

Numeric Hierarchy

The intended hierarchy places int below rational, both below real and number, with complex numbers and quaternions as further domains whose rules remain provisional.

Representation Selection

Semantic type and storage representation are separate. A value with int semantics uses a 64-bit machine representation when compile-time range analysis proves every reachable value fits; the analysis validates every abstract-integer arithmetic result and every narrowing (an int meeting int64, printing, a fixed-width parameter). When the proof is unavailable, the compiler reports the obligation — the value is only known to lie in some interval — rather than silently choosing overflow; the program annotates a fixed width or narrows the value with a comparison.

min(a b) and max(a b) are the smaller and larger of two values, for int64 and uint64 (a call on integer literals alone takes int64, unless the expected type says uint64). Their results carry type facts: min(k src.length) is at most k and at most src.length, so src[..min(k src.length)) slices without a guard; max(a b) is at least either.

Meeting Another Width

A value of one integer width meeting another — an abstract int or an addr length stored into a uint64, an int8 widened to int64 — is a conversion the bounds analysis must prove in range from the facts it has: the type's own range (widening always passes), a comparison, a length (never negative), or a loop guard. An unproven narrowing is a compile error naming the known range (let b:int8 = w for an arbitrary w:int64), never a silent wrap. The same holds when the target is a union with one fixed-width integer member such as uint64?: the integer becomes that member, with that member's proof. Spelling the conversion explicitly (src.length as uint64, n as int8 after if n <=? 127) is the same proven cast, not a reinterpretation: an unproven as reports the same obligation. Comparisons between different widths (i:uint64 <? s.length) compare in the left operand's width — the right operand takes the same proven cast, so no value is ever reinterpreted.

first_over = (xs:array<int64> limit:int64):>uint64? => {
    loop i in 0.. and i <? xs.length {
        if xs[i] >? limit return i      # `i` lies in [0, int64.max]: a `uint64`
    }
    return none
}

An abstract-integer counter stepped inside a guarded loop needs no annotation: in i = 0 loop i <? src.length { i += 1 } the analysis first widens i to [0, ∞] and then narrows it back to what the guard admits, [0, cap], so the comparison and the steps fit a word (a counter that can genuinely pass the word, loop true { i += 1 if i >? n break } for an arbitrary n:int64, is still reported).

A comparison between two terms — bindings, fields, lengths — is also kept as a fact about their difference, the one relational fact the analysis holds: under i <? src.length the value src.length - i is at least 1, under start <=? end the value end - start is at least 0, and after a =? b the difference is exactly 0. So let rest:nat64 = src.length - i proves inside the guarded loop, and a span width proves after if 0 <=? start <=? end (the lower bounds also keep the subtraction within int64). A slice's length is its endpoints' difference read the same way — src[i..] under loop i <? src.length has length at least 1, so it satisfies a string<length >? 0> parameter. The fact drops when either side is assigned (except i += c / i -= c by a constant, which moves the difference by c and keeps the fact while it stays nonnegative — i <? src.length then i += 1 leaves i <=? src.length), when the sequence shrinks, and at a join where only one path established it — unless the other path implies it from its intervals (i = 0 before a loop implies i <=? src.length, so a counter that steps by one is within the length at the loop's exit); arithmetic on fixed widths stays at the operands' width and meets the annotated width afterwards, so let w:nat64 = end - start is int64 - int64 followed by the proven cast.

remaining = (src:string):>nat64 => {
    i:int64 = 0
    total:nat64 = 0
    loop i <? src.length {
        let rest:nat64 = src.length - i    # at least 1 while the guard holds
        total += rest
        i += 1                              # the fact drops here, and returns with the next test
    }
    return total
}

Expressions and Evaluation

Every executable construct in Dewy is an expression. An expression may produce one value, several values for a surrounding collector, void, or never when it cannot complete.

Produced Values

Literals, value-returning calls, exhaustive conditionals, and value-producing blocks can supply surrounding expressions. Declarations and ordinary assignments produce void.

An attached postfix semicolon evaluates an expression and suppresses the values it would otherwise produce:

operation();

An unattached semicolon is reserved for array-dimension selection and does not act as generic statement punctuation.

Blocks

{} is a scoped block. () groups expressions without introducing a child lexical scope.

A block evaluates its expressions in source order and expresses each non-void result. A context requiring one value rejects a block that can produce an incompatible number of values.

let circumference = {
    let diameter = 2 * radius
    pi * diameter
}

Only the final calculation produces a value because the declaration is void.

Evaluation Order

Within the expression tree established by grouping and precedence, operands and call arguments evaluate from left to right. A construct documented as evaluating an operand once must preserve that behavior even if lowering expands it into several primitive operations.

Boolean short-circuit expressions evaluate only the operands required by their truth rule. Flow alternatives evaluate conditions in order and execute only the selected body.

Assignment

Assignment evaluates its destination place and source, updates the binding or selected field/element, and produces void. Combined assignment loads the old value, applies the selected typed operator, and stores the result while evaluating the destination route only once.

See Operators and Precedence, Bindings, and Values, Copies, and Places.

Place Projection

The prefix @ must begin a place route and selects the location at the end of the complete member-and-index route:

@pair.left
@values[i]
@box.rows[row][column]

The parser groups the prefix before the selectors, but that grouping does not make the root place an independently observable intermediate value. @(pair.left) selects the same final place as @pair.left; Dewy has no pair.@left form.

Function handles extend the same whole-route rule with a grouping boundary between selection or partial evaluation and an ordinary call. See Function Handles.

Operators and Precedence

Operator tokens resolve to typed operations. An operator's spelling determines parsing precedence; operand types and available overloads determine its meaning.

Main Operator Families

• arithmetic: +, -, *, /, //, %, ^;
• shifts: <<, >>, <<<, >>>;
• comparisons and tests: =?, not =?, <?, <=?, >?, >=?, is?, isnt?, in? (the tests bind like comparisons, so a is? T and b in? s needs no grouping; comparisons chain one direction, see below);
• symbolic composition: &, |, ~ — the same operations as and, or, not, binding above the comparisons (see below);
• Boolean logic: and, or, xor, nand, nor, xnor, not, binding below the comparisons (not x =? y is not (x =? y));
• conversion: as, transmute; propagation: postfix or_throw, below as ("this expression, or throw");
• type relationships and construction: of, has, and the prefix type of Parent, which binds above & and |;
• call pipes: |> and <|;
• construction and binding: :, :>, =>, ->, <->, =;
• suppression: an attached postfix ;.

English Boolean operators short-circuit according to their truth rules. Explicit calls to the corresponding implementation functions are ordinary eager calls.

Most infix operations have a combined-assignment spelling such as +=. Combined assignment has assignment precedence, not the precedence of its inner operation.

Juxtaposition

Adjacent expressions can form several operations:

function(argument)
values[index]
2distance
values...

Parsing retains the meaningful call, index, and multiplication alternatives. Semantic analysis resolves the operation from the operand types and context. General juxtaposition multiplication is still a provisional implementation area, but its place in the expression grammar is settled.

Precedence

The following table is ordered from highest to lowest. “Fail” means an ungrouped repetition at that level is rejected rather than given an arbitrary associativity. “Flat” produces one n-ary sequence.

Symbolic and Word Composition

& and and are the same operation, as are | and or and ~ and not: both spellings dispatch to the same builtin, so on booleans they agree, on integers both are bitwise, on sets both are algebra, on types both compose. They differ only in precedence, the way * and multiplication juxtaposition do. The symbolic forms bind above the comparisons and the word forms below them, because each spelling is idiomatic for a different kind of operand:

• symbols compose types, overload sets, sets, and masks — x is? A|B, d:int64 & ~0, Rational|Overflow, @print_int & @print_string, keys & other_keys, flags & MASK =? 0 — where the composed thing is then compared or tested as a whole;
• words are boolean logic over comparisons — x >? 0 and y <? n, k in? d or default — where the comparisons are the operands.

The cost is the one expression that mixes them the wrong way round: x >? 0 & y >? 0 parses as x >? (0 & y) >? 0, not as a conjunction. That spelling is unidiomatic — it works directly on boolean values, which is what and is for — and the checker rejects the misparse in nearly every case (a boolean compared with an integer). Write x >? 0 and y >? 0.

else attaches flow alternatives outside these operator levels. Grouping with () or a scoped {} is required when the precedence table does not express the intended tree.

Word-not sits just above and, below the comparisons — the same symbol/word split — so not x =? y is not (x =? y) and not a and b is (not a) and b, while ~flags =? 0 is (~flags) =? 0. x not =? y is still the one inverted comparison.

Chained Comparisons

a <? b <? c is a chain: consecutive comparisons joined by and, each interior operand evaluated once (0 <? x <? 10 is 0 <? x and x <? 10; 0 <=? f(x) <? n calls f once — a hidden local holds the value, in front of the statement or, in an expression-bodied function, in front of the chain; a name, a literal, or a route of member reads such as loc.stop or src.length is simply reused, so the facts a chain establishes are about that term). A chain is one monotonic statement: its operators are rising (<?, <=?) or falling (>?, >=?), and =? may appear in either without changing direction. Mixing directions is an error, and not =?, is?, isnt?, and in? do not chain — write and. Parenthesizing the left comparison ((a <? b) =? c) compares its boolean instead.

let x = 5
$assert 0 <? x <? 10
$assert 10 >? x >=? 0
$assert 0 <? x =? 5 <=? 5

Partial Operators

A binary operator applied to only its right operand, in parentheses, is a partial operator: a one-parameter function of the missing left operand. (<? n) is i => i <? n, (* 2) is i => i * 2, (in? 1..3) is i => i in? 1..3, (.length) is x => x.length, (as string) is x => x as string. Only that form exists, and only for operators that have no prefix form — the comparisons and tests (=?, not =?, <?, >?, <=?, >=?, is?, isnt?, in?, not in?), ., as, transmute, *, /, //, ^, %, and \ — so (- 1) remains negative one and (+ 1) is just one. (*, /, and // have no prefix form; x ^/ 2 for a root is an opchain compound, its own operator.) The operand is everything to the closing parenthesis ((<? a + b) is i => i <? a + b). A partial operator is an ordinary function value: it is typed like an unannotated lambda, from the function type it is checked against (a sort key, a slot, an annotation — whose parameter name it takes), and it is a fact wherever a lambda is: uint64<(<? src.length)>.

let main = ():>int64 => {
    let names:array<string> = ["bb" "a" "ccc"]
    names.sort(key=(.length))
    let small:<(x:int64):>bool> = (<? 10)
    let text = "hello"
    let k:uint64<(<? text.length)> = 3
    let digit:uint64<(in? 0..9)> = 7
    if small(3) and names[0] =? "a" { return 0 }
    return 1
}

type of, as, and or_throw

type of is a prefix that binds above & and |, so type of Parent & Structure mints the parent and then strengthens it — (type of Parent) & Structure without the parentheses; a generic bound <T of A & B> uses the infix of, which stays loose, so the bound is the whole right-hand side.

as sits below | so that bytes as string | none converts to the union. The cost is that x as int64 + 1 is x as (int64 + 1): write (x as int64) + 1.

or_throw is a postfix just below as: it applies to the whole expression on its left, so f(x) * 2 or_throw is (f(x) * 2) or_throw, bytes as string | none or_throw is (bytes as (string | none)) or_throw, and lookup(id) or_throw and f(x) or_throw * 2 read as they look. Scaling a fallible call before propagating needs parentheses: 2 * (f(x) or_throw).

This table lists source-language forms whose place in the expression grammar has been selected. Token spellings reserved by the parser for future operations—such as left division, expression-producing assignment, compile-time assignment, and additional shift forms—do not acquire language semantics merely by being tokenizable.

Retired Operators

Three test operators were reserved early and removed on 2026-08-28; the symbols are free.

• of? — a value-level "is this of type T?". It duplicated is?.
• has? — a value-level "does this value have this structural binding?", meant to pair with the reserved type-level has (the binding side) the way is? pairs with of. Held back with has until structural binding is designed; today the question is a compile-time fact about the value's type.
• @? — "do two place expressions designate the same place?". Places are borrows (@x parameters, @ routes), not first-class values, and the ownership model gives every value one owner and never exposes storage sharing, so no program can observe the answer.

Functions and Calls

A function literal consists of a parameter contract, an optional return contract, =>, and a body expression:

let add = (left:int64 right:int64=2):>int64 => left + right

One bare parameter name may omit parentheses: x => x + 1. Here x is always the local parameter name, never an anonymous argument whose type happens to be named x. Whether the body can infer a generic contract without other type context depends on the provisional generic-function design. Annotated parameters use (x:int64), and zero parameters use ().

Argument Binding

Each explicit argument binds one currently unset parameter. Arguments are processed from left to right.

• A positional argument binds the first parameter still available by position.
• A named argument binds the unset parameter with that name.
• After explicit arguments are processed, each unset defaulted parameter evaluates its default for that completed call.
• A required parameter still unset after binding is an error.

Defaults are fallbacks, not values bound when the function is defined. They retain their positions:

let combine = (
    left:int64
    scale:int64=2
    right:int64
):>int64 => left + right * scale

combine(10 3 16)       # left=10, scale=3, right=16
combine(10 right=16)   # left=10, scale=2, right=16
combine(scale=3 10 16) # scale=3, then left=10 and right=16

combine(10 16) binds left and scale; it does not skip scale, and therefore reports missing right.

Default expressions evaluate independently for every completed call that omits them. Mutable objects created by a default are not shared accidentally between calls.

Parameter Kinds

Positional or keyword

An ordinary named parameter before the positional divider may be bound by position or name:

let subtract = (left:int64 right:int64):>int64 => left - right
subtract(7 2)
subtract(right=2 left=7)

Keyword-only

A bare ... ends the positional run. Parameters after it require names:

let offset = (value:int64 ... amount:int64):>int64 => value + amount
offset(40 amount=2)

Position-only

Wrapping the name and type in <> preserves the local name but removes it from the keyword interface:

let increment = (<value:int64>):>int64 => value + 1
increment(41)

increment(value=41) is an error. A default inside the wrapper remains a per-call fallback.

Types and names share identifier syntax, so a bare identifier in a function literal is a parameter name, not an anonymous argument whose type happens to have that spelling.

Rest Parameters and Spreading

The direction for ...rest is to capture arguments not claimed by earlier parameters and allow the resulting bundle to be forwarded with .... Exact bundle types and all interactions with named arguments remain provisional.

Function Contracts

A function type records its parameter and return contract:

let callback:<(value:int64):>int64> = increment

Position-only function contracts use <name:type>, just like function literals. The name describes the parameter inside the contract but is absent from the keyword-call interface. A bare identifier is always a parameter name, so Dewy does not infer an anonymous type-only parameter from its spelling.

A function value is an ordinary value of its contract type: @name selects a named function instead of calling it, and such values are stored in arrays and dictionaries (let table:dict<string <(x:int64):>int64>> = ['double' -> @double]), chosen by a flow (let op = if fast @double else @triple), and called through whatever holds them (table['double'](4), op(3)). A call whose callee's origin is not tracked — a table entry, a reassigned function binding — is checked for initialization order against every function of that type in the program. A function that reads enclosing locals cannot be a value yet (it needs a closure record); it is called directly or given what it needs as parameters.

A function value fits a slot of a wider contract by the usual rules — parameters contravariant, the result covariant — and a narrower union result needs no adapter: a function returning uint64? is stored where uint64? | TokenError is expected and called through it, because a union value carries its member's identity rather than a position in one particular union. The one result difference that is rejected is a bare value against a tagged one (a function returning none alone, or int64, in a slot returning int64?): those are different runtime forms.

let TokenError:type = type of error
let TokenProtocol:type = [eat:<(src:string):>uint64? | TokenError>]
Whitespace = type of TokenProtocol & [eat = (src:string):>uint64? => if src.startswith(" ") 1 else none]

count = ():>uint64 => {
    let table:array<TokenProtocol> = [Whitespace]
    return match table[0].eat(" x") { n:uint64 => n  <none> => 0  <TokenError> => 0 }   # `Whitespace.eat` returns `uint64?`; the slot reads it
}

Expected failures appear as direct error alternatives in the return contract. Public functions should normally declare a stable set of returned errors even where an unexposed helper could infer them.

Calls and Pipes

Parenthesized or juxtaposed arguments call a callable expression. |> supplies values to the callable on its right; <| supplies right-hand values to the callable on its left according to their associativity. The callable operand of a pipe is an ordinary expression, not a call position: a named function is written @name (3 |> @square), and a function literal or any other function-valued expression pipes as written.

Argument expressions evaluate from left to right before the function body begins, except that omitted defaults evaluate as part of completing the call. A defaulted parameter may be optional — (message:string? = none) — and the default fills the cell when the argument is omitted.

Record and container parameters may also have defaults, such as (seen:set<int64> = set[]). An omitted default is evaluated for each call; mutating that value does not affect the next call. An explicitly supplied record or container follows ordinary value-copy semantics, and its default is not evaluated.

Overloads

& combines compatible functions into an overload set. The call contract selects a unique applicable alternative:

let describe = ((value:int64):>string => "integer")
             & ((value:string):>string => value)

Ambiguous or unmatched calls are errors. Runtime multifunction values remain part of the provisional dynamic-dispatch design; ordinary overload resolution is static.

Function Handles

A bare function name is always a call: a function whose parameters all have defaults is called with none, and mentioning a function with required parameters without its arguments is an error rather than a reference. @fn selects the function binding as a first-class value instead:

let sum = (a:int64 b:int64) => a + b
let reference = @sum
let add5 = @sum(5)

Selectors use the ordinary whole-route place rule: @worker.on_event selects the function-valued place at the end of the route, and it cannot be written worker.@on_event. Although parsing groups the leading prefix first, @worker is not the semantic result of that complete expression.

A leading @ suppresses calls at every function-valued node in its complete ungrouped selector-and-application chain. The route still selects only its final place; intermediate nodes are not separately observable place values. Argument groups within that chain partially evaluate functions. A grouping boundary ends the @ chain, so an argument group outside it performs an ordinary call.

@worker.on_event.metadata     # metadata belonging to the function value
worker.on_event().metadata    # call on_event, then read result.metadata
(@worker.on_event)(5).metadata # select on_event, call it, then read result.metadata

An ordinary call resolves the callable at that node without automatically calling it first. @sum(5) saves 5, while (@sum)(5) invokes the selected function. Repeated argument groups do not implicitly end the chain:

@sum(1)(2)       # two stages of partial evaluation
(@sum(1))(2)     # partially evaluate with 1, then call with 2
@sum(1)()        # empty second partial evaluation; still a function
(@sum(1))()      # call the partially evaluated function with no arguments

An empty partial evaluation does not invoke the function or evaluate its signature defaults. If code needs a place within a returned value, it must bind that result and select a place from the stable binding; @ does not make a temporary call result into an escaping place.

Partial evaluation also works when the selected function is an object member:

let on_item = @worker.on_event(5)

This selects on_event at the endpoint of the route, preserves its receiver, and saves 5; it does not call either worker or on_event. When the object must first be produced by a call, bind that result before selecting its function member:

let worker = make_worker()
let on_item = @worker.on_event(5)

@make_worker() means an empty partial evaluation of make_worker, not an explicit call followed by place selection. A temporary call result is not a valid root for a place route.

Partial evaluation binds explicitly supplied values immediately. Defaults remain fallbacks evaluated when the resulting function is eventually called.

Handle identity, explicit function copying, escaping captures, and closure storage remain provisional.

Implemented today: a local function may read enclosing locals and parameters (it observes their current values at each call, since the compiler lambda-lifts them into hidden trailing parameters); writes to captured bindings and capturing functions used as values (escaping closures) are rejected with a message naming the binding.

Control Flow

Conditionals

if, else if, and else form an ordered flow expression. Conditions evaluate from left to right until one succeeds; only the selected body evaluates.

let label = if count =? 0
    "empty"
else if count =? 1
    "one item"
else
    "{count} items"

An exhaustive conditional may produce a value when its alternatives have a compatible result type. A nonexhaustive conditional produces void unless its context collects another well-defined result form.

Facts established by a condition narrow values inside the corresponding body and along later paths where earlier alternatives are known false.

A chain whose arms are all is? tests on one union binding is exhaustive when the alternatives excluded by every arm leave no member; such a chain needs no else for return coverage or for producing a value, and a value-producing chain that misses a member reports which member is unhandled. Statement-form chains may remain partial.

match

match <scrutinee> <arm | { arms }> is a member of the flow chain, so else (and else if, else match) attaches outside the arms. An arm is <signature> => <body>, and it matches when the scrutinee satisfies the signature, exactly as a call satisfies a parameter list:

let describe = (v:bool|int64|string):>string => match v {
    <bool>              => "a flag"          # a type: narrows, binds nothing
    answer:42           => "the answer"      # a singleton
    small:int64<small <? 100> => "small"     # the refinement is the arm's guard, and a fact in the body
    n:int64             => "large"           # binds `n` at `int64`
    s:string            => s
}
let sign_of = (b:bigint):>int64 => match b {
    <0>                 => 0
    [sign:1 limbs]      => limbs.length      # an object shape: the member with those fields, fields bound
    [sign:-1 limbs]     => -limbs.length
}
let sum = match (x y) (a:int64 b:int64) => a + b   # a sequence scrutinee; `(<T1> b:T2)` mixes anonymous and named

The scrutinee is evaluated once; a bare identifier is matched in place, so the arms narrow it. Arms are tried top to bottom and the first that matches wins. A bare name matches everything and binds the value, shadowing what the name meant, as a parameter would; _ is the idiomatic catch-all, and any other bare name warns (saying whether it shadows a type or a value) — write name:T to bind with a type or <T> to match one. An anonymous refined type, <int64<i => i <? 100>>, is a guard without a binding.

A chain that contains a match must be total: the arms must cover every member of the scrutinee's type, or the chain must end in else. Coverage is computed on value sets, so guards count where the type is known: a:int64<a <? 0> and b:int64<b >=? 0> cover int64; over -1|0|1, guards <? 0 and >? 0 leave 0 unhandled and the error says so. An arm that cannot match anything the earlier arms left (unreachable match arm) is an error. Value-producing arms combine like conditional branches: the result is the union of the arm types, so a match whose arms are 'A' and 'B' produces the enum 'A' | 'B'. An enum — a union of string and/or integer singletons — is one word at runtime, the member's index: c =? 'A', c is? 'A', and match arms compare that word, no string is built or compared, and the text exists only where the value meets a string.

Loops

loop condition body reevaluates its condition and executes its body according to the condition's Boolean or iterator behavior.

loop connected
    receive_message()

loop item in items
    process(item)

See Ranges and Iteration for iterator conditions and multiiterator formulas.

Exits

break exits a loop. continue begins its next condition evaluation. return exits the current function, optionally supplying its result.

An exit may target an enclosing labeled loop through Dewy's scope metatag mechanism. Exiting more loop levels than exist is an error.

never is the type of a path that cannot complete normally. It is distinct from void, which represents normal completion without a produced value. A function may declare it — exit(code:int64):>never ends the process, and a wrapper propagates the divergence:

let panic = (msg:string?=none):>never => {
    if msg isnt? none printl(msg)
    exit(1)
}

A :>never body must diverge (a body that completes is an error), a call to one is never wherever it appears — an else panic(…) arm contributes no type, and code after if v is? none panic(…) sees v narrowed — and main may end in one.

Postfix or_throw propagates an exception value from an expression through the current function. Its ordinary alternatives continue locally; its exception alternatives must be accepted by the enclosing return contract.

Related Provisional Control Flow

Cleanup/finally behavior and transformed error-propagation forms are provisional designs (match is settled; see above and dewy/semantic/match.md). Their eventual forms must compose with expression results and flow-sensitive narrowing rather than creating separate statement-only semantics.

Errors, Exceptions, and Forwarding

Dewy models expected failures as values belonging to nominal error types. A function exposes those values directly as alternatives in its return type rather than wrapping its result in a runtime Result<T, E> object.

Automatic forwarding is defined by the broader nominal exception family. Errors are one kind of exception; none is another. The direct-union model, exception classification, receiver-forwarding rule, explicit treatment of arguments, and separation of errors from effects are settled semantic direction. The surface forms called out as provisional below are not yet normative.

Implemented today: error types minted with type of error, unit-like or carrying fields, error alternatives in return unions and other unions, is? handling (including is? error for the whole family), postfix or_throw, and forwarding member access (safe navigation, reads only). Not yet implemented: forwarding through method calls and the fallback operators. Examples marked as compiler examples below compile with the current compiler; the rest are design.

Errors are the second half of Dewy's no-trap rule (see No Traps): what cannot be proven safe at compile time is returned as a value, never raised, never aborted.

The exception Family

The built-in hierarchy contains:

exception
├── error
└── none

Any value whose type descends from exception is a forwarding value. Programs may define additional exception types. A type that does not descend from exception remains an ordinary union alternative even if programmers conventionally use it as a sentinel.

“Exception” names a type category here. Exception values remain ordinary values; forwarding does not imply stack unwinding.

Declaring Error Types

An error type descends from the nominal base type error, which itself descends from exception. type of error creates a fresh nominal error type:

const MyCustomError:type = type of error

A unit-like nominal error has one canonical inhabitant, written with the type's name. The question of whether that inhabitant is literally the type value itself remains open, but there is no separate MyCustomError() spelling:

let MyCustomError:type = type of error

let maybeNumber = (flag:bool):>int64 | MyCustomError => {
    if flag { return MyCustomError }
    return 42
}

Minted names are nominal: two type of error aliases are distinct types even though both descend from error, and a value of one is never a value of the other.

Intersect the fresh nominal type with an object type when an error carries fields. The result is constructed, matched, and read like any minted object (Report's methods included when the structure is Report), sits in the error family for is? error, or_throw, and forwarding, and — being a fresh nominal child of its structure — satisfies a parameter of that structure:

let TokenError:type = type of error & [message:string offset:int64 = 0]

let count = (src:string):>int64 | TokenError => {
    if src.length =? 0 return TokenError(message='empty input')
    return src.length
}

describe = (n:int64):>string => match count("abc") {
    e:TokenError => e.message
    v:int64 => "{v} characters"
}

type of error mints the identity; & only adds the structural requirement. Further structural extension therefore reuses the existing nominal ancestry:

const MyMoreComplexError:type =
    MyComplexError & [metadata:string]

MyMoreComplexError is structurally stronger but is not a separate nominal error variant. See Nominal Identity.

Error Return Unions

let loadCustomer = (id:CustomerId)
    :> Customer | NotFoundError | DatabaseError
=> {
    # ...
}

Customer, NotFoundError, and DatabaseError are direct alternatives. Union normalization flattens errors in the same way as other alternatives, while nominal membership in error prevents an error from collapsing into a structurally similar success type. No Ok or Err constructor is implied.

An exposed function should ordinarily declare a stable error set. The compiler may infer error alternatives for an unexposed helper.

Forwarding Member Access

Let a receiver have type:

V1 | ... | Vn | X1 | ... | Xm

where each Xi descends from exception and no Vi does. For receiver.member:

1. Every ordinary alternative Vi must support member. Otherwise the expression is a type error.
2. When the runtime receiver is a Vi, the member operation is performed normally.
3. When the runtime receiver is an Xi, member lookup is not performed and that exception value is forwarded.
4. If the member results have types R1 through Rn, the result type is R1 | ... | Rn | X1 | ... | Xm.

let UserError:type = type of error
let Address:type = [city:string]
let User:type = [name:string address:Address|none]

let load_user = (id:int64):>User | UserError | none =>
    if id >? 0 [name="ada" address=[city="paris"]] else UserError

let city_of = (id:int64):>string | UserError | none => {
    let user = load_user(id)
    let city = user.address.city      # city: string | UserError | none
    return city
}

Each successive route segment applies the rule again. This gives exception-bearing receivers safe navigation without a separate ?. spelling. Ordinary union alternatives never forward merely because they lack the requested member.

The rule with no exception alternatives is plain common-member access: when every alternative of an ordinary union has the member, the access reads it without narrowing, at the union of the member types (one type when they agree):

let Customer:type = [name:string id:int64]
let Organization:type = [name:string members:int64]

let find = (id:int64):>Customer | Organization =>
    if id >? 0 [name="ada" id=id] else [name="acme" members=3]

let who = (id:int64):>string => find(id).name    # both alternatives have `name`

find(id).id is a type error there — Organization has no id — and so is assigning through any union route; narrow with is? first.

Forwarding applies at the receiver's current type; it does not recursively search inside containers. An array<int64 | ParseError> is an array value, not a top-level ParseError. Code that wants to combine or reject exceptions among its elements must do so explicitly.

Calls and Arguments

Selecting a member on an exception-bearing receiver follows the forwarding rule. Arguments to a call do not forward implicitly.

let service:Service | ServiceError = connect()
let request:Request | ParseError = parseRequest(text)

service.send(request)            # type error: request is still a union
service.send(request or_throw)  # explicit propagation

The first call is invalid unless send actually accepts Request | ParseError. Receiver forwarding does not change the argument contract.

or_throw

Postfix or_throw is the intended spelling for passing exception alternatives out of the current function.

For an expression of type V | X, where X contains its exception alternatives, expression or_throw:

• evaluates expression once;
• returns the encountered X value from the enclosing function; or
• produces the corresponding non-exception V value locally.

The enclosing return contract must accept every propagated exception alternative. This includes none and user-defined exception kinds as well as errors.

let NotFound:type = type of error

let lookup = (id:int64):>int64 | NotFound => {
    if id >? 100 { return NotFound }
    return id * 2
}

let twice = (id:int64):>int64 | NotFound | none => {
    let first = lookup(id) or_throw      # first: int64
    let second = lookup(first) or_throw
    if second =? 8 { return none }
    return second
}

or_throw is a postfix just below as in precedence, so it applies to the whole expression on its left: lookup(id) or_throw propagates the call's result, and f(x) * 2 or_throw propagates from the product (see operators and precedence). The propagated alternatives must each be accepted by the enclosing function's declared result type; a function without a declared result type cannot use it. Forms that replace or transform the propagated exception are part of the design direction, but their exact syntax and evaluation rules remain provisional.

Explicit Handling

Type tests narrow error unions through ordinary control flow:

let result = loadUser(id)

if result is? NotFoundError
    useGuest()
else if result is? DatabaseError
    report(result)
else
    greet(result.name)

The general pattern-selection syntax and type-directed recovery helpers remain provisional. Any recovery operation must remove only the alternatives it actually handles and preserve every unhandled error in the result type.

Forwarded values do not become false in Boolean context. If user.isAdmin has type bool | UserError | none, it is not a valid if condition until every exception alternative is propagated, handled, or otherwise narrowed away.

The current fallback direction keeps absence and failure distinct: ?? would replace none while preserving any error alternative. Under that proposal, applying a default to Address | DatabaseError | none produces Address | DatabaseError, not just Address. The final operator split between absence and error recovery is still provisional.

Mutation

Safe navigation is a read and receiver-selection rule. An assignment through an exception-bearing route must not silently become a no-op:

user.profile.name = "Ada"  # invalid if user may be UserError or none

The program must first narrow or propagate every exception alternative so the destination is a definite place.

Exceptions Versus Ordinary Sentinels

Only alternatives descended from exception receive forwarding behavior:

User | Missing         ordinary domain alternatives
User | NotFoundError   value or propagatable failure
User | none       value or forwarding absence

Code should use an ordinary domain type when both outcomes are meant to participate normally in later operations. It should use an error subtype for a forwarding failure, none for ordinary forwarding absence, or another exception subtype when neither built-in category expresses the contract.

Errors Versus Effects

Errors are return values. Effects describe observable behavior or requirements of evaluation. They occupy separate parts of a function contract and must not be mixed as alternatives of one union.

let loadInvoice = (id:InvoiceId)
    :> (Invoice | NotFoundError | DatabaseError) & reads<database>

Here the union describes what the caller receives. reads<database> describes what evaluating the call does. General effect syntax remains provisional; see Refinements, Effects, and Safety.

Provisional Boundaries

The following details remain open:

• pattern-selection and concise recovery syntax;
• transformed or_throw forms;
• whether pipes automatically forward exceptions, and the exact rule for broadcast pipes whose elements may be exceptions;
• fallback operators for absence and errors; and
• runtime layouts for general heterogeneous unions.

Until those questions are settled, programs should not infer behavior for them from an experimental compiler lowering. See Design Maturity and Open Questions and Implementation Compatibility.

Ranges and Iteration

Range Forms

A range contains ... Endpoints immediately juxtaposed with .. supply its anchors:

first..last
first..
..last
..

Square and round boundaries independently include or exclude an endpoint:

[first..last]
[first..last)
(first..last]
(first..last)

An unbracketed first..last includes both endpoints.

A first pair determines a step:

1,3..9       # 1 3 5 7 9
5,4..0       # 5 4 3 2 1 0

The step is second - first and cannot be zero. A descending range requires a negative step; 5..0 is empty rather than implicitly descending.

Iterability

A range with a first element may be consumed from that element onward. A left-unbounded range is a valid range value but cannot be iterated because it has no starting value.

Right-unbounded iteration continues until surrounding control flow or a finite companion iterator stops it.

Membership

value in? range tests whether the value belongs to the range, respecting open bounds and step alignment. Each runtime operand is evaluated once.

Sequence Slices

A range used as an index selects a slice. end refers to the last valid index of the selected axis:

text[3..12)
values[..end-1]
matrix[row][1..end]

Iterator Conditions

In a loop condition, name in iterable requests the next value, binds it to name, and reports whether a value was produced:

loop item in items
    process(item)

Iterator clauses may be combined with Boolean operators. Leaves advance from left to right once per condition evaluation:

loop index in 0.. and item in items
    printl"{index}: {item}"

For and, iteration ends when a required leaf is exhausted. Operators such as or may allow one leaf to continue after another is exhausted; an exhausted leaf's bound value is then optional.

The exact truth and exhaustion formulas for and, or, xor, nand, nor, and xnor follow their Boolean meanings applied to the per-leaf step results.

Provisional Boundaries

The following remain under design:

• advancement and short-circuit behavior when iterator clauses mix with ordinary Boolean predicates (settled, see below);
• stored generators and some dynamic iterator sources; and
• result types, normalization, empty-span behavior, and representation for arbitrary runtime range arithmetic.

See Design Maturity and Open Questions.

Iterators with Boolean Predicates

A loop condition may join iterator clauses and ordinary Boolean predicates with and. The iterators advance first, then the predicates are tested with the targets bound; the loop ends at the first false predicate, and inside the body the predicates are known to hold — so i <? src.length proves the index in src[i]:

const whitespace = set[' ' '\t' '\n' '\r']
leading = (src:string):>int64 => {
    let n:int64 = 0
    loop i in 0.. and i <? src.length and src[i] in? whitespace { n += 1 }
    return n
}

loop x in xs and x <? 4 { … } visits the prefix of xs below 4 (it stops at the first element that fails, it does not filter — put an if in the body to filter). Predicates may sit anywhere in the chain; only word-and joins them to the iterators, and or/xor chains stay multiiterator formulas.

Runtime Range Ends

A loop range's end may be a runtime value: loop i in [0..argv.length) visits each index, and the bare loop i in 0..n includes n (ranges are inclusive unless the bracket says otherwise). The end becomes a per-iteration guard on an open counter, so it composes with the mixed conditions above and bounds the counter the same way. A runtime start still needs the general runtime range representation.

In a dictionary loop the value target may unpack an object element by field name: loop [prefix [digits case_insensitive extra]] in BASE_SPECS declares each name as a copy of the field of that name (any subset, in any order).

Refinements, Effects, and Safety

This area has a settled semantic direction and a provisional general syntax. The rules below constrain the eventual design; they do not authorize arbitrary expressions as refinements or effects.

Refinements

A refinement combines a base type with facts every value of that type satisfies. Exact array length is a concrete instance:

array<int64 length=3>

A parameterize block may attach conditions to any type. An entry is a condition when it is a one-argument lambda about the value (int< i => i >? 0 >), a ?-comparison on length (array< length >? 0 >), or a length=N assignment; every other entry is a type parameter. A refined array type may leave its element open and receive it on application (NonEmptyArray<int>). A condition — a fact — compares against an integer literal, a fixed-width type's min/max (uint64.max), or — as an upper bound on a result — the length of one of the function's parameters (:>uint64<n => n <=? src.length>, see refined results and type facts); in? a range of integer literals is its two bounds (i => i in? 10..20, length in? [1..8)); a partial operator is the lambda it abbreviates (uint64<(<? src.length)>, uint64<(in? 0..9)>); and a condition may be a one-direction comparison chain — 0 <? length <=? uint64.max is the two conditions length >? 0 and length <=? uint64.max, i => 0 <=? i <=? 100 likewise — following the chaining rules. A refined type is named like any other:

nonemptystring = string<0 <? length <=? uint64.max>
let eat_whitespace = (src:nonemptystring):>uint64? => {
    loop i in 0..uint64.max and i <? src.length {
        if src[i] not =? ' ' return i
    }
    return src.length
}

Checking a value against a refined type yields one of three outcomes: proven, refuted (a compile error), or unknown (reported as unproven, never as false). A binding declared with a refined type carries the base type together with the proven facts: integer bounds feed range analysis and length intervals feed bounds proofs. The supported predicates apply to bindings, parameters, results, and object fields.

Refinement facts may arise from annotations, literals, ordinary control-flow conditions, successful explicit checks, and trusted interfaces. The facts the compiler tracks today include exact and minimum array lengths, i <? xs.length index guards, the difference two compared terms keep (start <=? end makes end - start nonnegative), integer intervals, narrowed union members, and proven dictionary and set keys.

if index >=? 0 and index <? values.length
    use(values[index])

Inside the body, the index relationship is available to prove the access valid. Mutation and calls invalidate any fact they may falsify.

Array Contracts and Dependent Indices

A mutable declaration let xs:array<int64> = [1] retains array<int64> as its assignment contract. Its initial length of one is a fact about the current value, so indexing xs[0] is valid, and assigning [40 2] later is also valid. An explicit array<int64 length=1> annotation instead requires every assigned value to have that length. Immutable bindings can retain their exact shape.

Length inequalities are storage contracts too. Growing an array<int64 length <=? 3> must leave at most three elements; shrinking an array<int64 length >=? 1> must leave at least one. These checks apply to named arrays, place parameters, and array fields. A guard such as if xs.length <? 3 { xs.push(value) } proves bounded growth. Reassignment checks the replacement and retains the declared length bounds for later operations.

The bound can also name another array's length, for example (limit:array<int64> @xs:array<int64 length <=? limit.length>). Growth then needs a guard such as xs.length <? limit.length. Shrinking preserves that upper-bound relationship. More precise index guards can also survive a removal: an index known to be below xs.length - 1 remains in bounds after one pop. This describes bounds, not which element occupies the index.

A result can relate an index to an array passed as a mutable place. The contract below is checked against the updated array at each return:

let append = <T>(@xs:array<T> value:T):>addr<i => i <? xs.length> => {
    let i = xs.length
    xs.push(value)
    return i
}

let example = ():>int64 => {
    let xs:array<int64> = []
    let i = append(@xs 42)
    return xs[i]
}

The result uses ordinary refinement syntax. Growth preserves this bounds evidence; a value copy preserves the corresponding evidence for the copy. Truncation, replacement, or passing the array to another mutable call can invalidate it. The fact says that the index is in bounds for that array's current value; it does not establish provenance for an unrelated array, or promise that insertion has preserved which element occupies an index.

Array membership similarly carries a result fact: after if value in? xs, xs is known to be nonempty. A failed search promises nothing about length.

The general proposition language must be a deliberately bounded, decidable fragment. Unsupported Dewy expressions produce an unknown proof result or a diagnostic; they do not silently enter refinement checking as trusted predicates.

Refined Parameters

A parameter may carry a refinement: (n:int64 d:int64<d not=? 0>), (xs:array<int64 xs.length >? 0>) — inside the annotation the parameter's own name is the value, so no lambda is needed (the lambda form int64<i => i not=? 0> remains for aliases). int64 & ~0 spells the same exclusion structurally. An object value may be refined by an integer field: r:Ratio<bottom >? 0> (also r:Ratio<r.bottom >? 0> or q => q.bottom >? 0) — proven from a literal's field, from a guard on the field (if r.bottom >? 0 { value(r) }), and assumed for r.bottom inside the body. Dispatch applies on the base type; the refinement is an obligation at every call site, proven the way $assert is — from constants at check time, otherwise by the bounds analysis from guards (if d not=? 0 { f(n d) }, $runtime_assert d >? 0), intervals (a loop variable over 1..3), and length facts (xs.length >? 0). A refuted obligation and an unprovable one are both errors (refinement refuted, cannot prove refinement), with a note on what the analysis knew. Inside the body the refinement is a fact: n // d is proven with d:int64<i => i not=? 0>, xs[0] with length>?0.

Two related spellings make invalid states unrepresentable rather than merely checked. A union of integer singletons — sign:-1|1 as a field, s:-1|1 as a binding or parameter, :>-1|1 as a result — is a word whose value set is its invariant: storing into it is an obligation (sign = -a.sign is proven from a.sign's facts) and reading it yields the facts; s is? 1 on such a word is the comparison s =? 1, and s is? -1|1 an or of comparisons (| binds above is?). A union that mixes literals of different kinds (1 | 2 | "fast") remains a tagged union tested with is?. A field may also carry a length invariant, limbs:array<uint64 length >? 0>, proven at construction and assumed on every read (v.limbs[0] needs no guard). And a literal beside an object type, 0 | [sign:-1|1 limbs:…], is a tagged union that x =? 0 / x not=? 0 narrow like is?; T & ~0 on such a union names it without the literal member — the nonzero object — so a parameter d:bigint & ~0 is satisfied by a binding narrowed with if d not=? 0 { … }. A field may also be refined by a field of its own type — start:Point<x >=? 0> — proven where the enclosing value is built (from a literal, or from a guard such as if p.x >=? 0 { [start = p …] }) and a fact wherever s.start.x is read; on a 0 | [...] type the same spelling refines the object member, so bigint<sign =? 1> is a positive big integer, nonzero by construction (the abstract rational's denominator is one).

let percent = (part:int64 whole:int64<whole >? 0>):>int64 => part * 100 // whole

let share = (part:int64 whole:int64):>int64 => {
    if whole >? 0 { return percent(part whole) }   # the guard proves the obligation
    return 0
}

let main = ():>int64 => percent(1 4) + share(3 4)   # 25 + 75

Refined Results and Field Invariants

A result may be refined — let positive = (n:int64):>int64<i => i >=? 1> => … — in which case every return (and the body's value) is an obligation, and every call is a fact: n // positive(n) is proven, and let g = positive(n) carries the fact on g.

A result may also be bounded by a parameter's length: (src:string):>uint64<n => n <=? src.length> (or <?) promises that the result never passes the end of src. The function proves it at every return from what it knows of src — return i under i <? src.length, return i + 1 under the same, return src.length, return n - 1 after n =? src.length — and a call turns it into a fact about the argument: let n = f(text) gives n <=? text.length, so text[0..n) proves; let length = f(src[i..]) gives length <=? src.length - i, so src[i..i+length) proves. That last fact follows the value where it goes — into a record field, an array of records, through .sort, out of matches[0] and an unpack — until i, src, or the value is reassigned (an element that does not satisfy it drops the fact from the array). A function type may carry the promise for its implementations: with eatfn = (src:nonempty):>uint64<n => n <=? src.length> | none, a type of Token & [eat = (src:nonempty):>uint64? => …] implementing the slot eat:eatfn has the promise as its own contract (its returns prove it), and a k.eat(src[i..]) through a type<Token> value has it as a fact. The promise is about the argument, not a name: a function whose own parameter is src cannot discharge n <=? src.length with other(text), however other names its parameter.

let nonempty:type = string<length >? 0>
let eatfn:type = (src:nonempty):>uint64< n => n <=? src.length > | none
let Tok:type = $abstract type of any & [eat:eatfn]
let Spaces = type of Tok & [
    eat = (src:nonempty):>uint64? => {
        if src[0] not=? ' ' return none
        loop i in 0..uint64.max and i <? src.length { if src[i] not=? ' ' return i }
        return src.length
    }
]
let Word = type of Tok & [
    eat = (src:nonempty):>uint64? => {
        if src[0] =? ' ' return none
        loop i in 0..uint64.max and i <? src.length { if src[i] =? ' ' return i }
        return src.length
    }
]
let tokenize = (src:string):>array<string> => {
    let out:array<string> = []
    let kinds:array<type<Tok>> = [Spaces Word]
    let i:uint64 = 0
    loop i <? src.length {
        matches = [loop k in kinds { length = k.eat(src[i..])  if length isnt? exception [length=length k=k] }]
        matches.sort(key=m=>m.length reverse=true)
        if matches.length =? 0 break
        [length k] = matches[0]
        out.push(src[i..i+length))          # proven: length <=? src.length - i
        i += length
    }
    return out
}

A field may declare an invariant: let Ratio:type = [top:int64 bottom:int64<bottom >? 0>]. It is proven wherever a Ratio is made — Ratio(1 2), a literal, or a plain object flowing into the type — and wherever the field is stored (r.bottom = z needs z >? 0), and it is assumed wherever the field is read, so r.top // r.bottom is proven for any Ratio. The prelude's rational<int64> (Rational) declares denominator:int64<denominator >? 0> this way.

let Ratio:type = [top:int64 bottom:int64<bottom >? 0>]
let scale = (r:Ratio):>int64 => r.top // r.bottom      # the invariant proves the division

let main = ():>int64 => {
    let r = Ratio(84 2)
    let q:rational<int64> = 1 / 3                        # the word rational declares the same invariant
    return scale(r) // 42 * (9 // q.denominator)         # 3
}

Facts about an object's integer field (if r.bottom >? 0 { r.top // r.bottom }) are tracked by member route, like array lengths, until the field or its object is reassigned; and a loop over an array or dictionary literal of constants that is never mutated bounds the loop variable by those constants.

Type Facts

A fact is one condition of a refinement: length >? 0, i => i <=? src.length, bottom >? 0, tok is? Word. A block of them, <facts>, is a type in its own right — the values the facts hold of — and T & <facts> intersects it with T, distributing over a union member by member. T<facts> is the same thing spelled as a parameterize block (which can also take type arguments; & <…> takes facts only). Inside a fact block a name resolves to a member of the value when the value has one (length, a field), and otherwise to a binding in scope — in a result type, the function's parameters. So a result may carry facts about the parameters: what the function establishes about its inputs by the time it returns.

A boolean result states its facts per arm:

let has_prefix = (src:string prefix:string):> true & <prefix.length <=? src.length> | false => {
    if prefix.length =? 0 return true
    if prefix.length >? src.length return false     # the guard is the proof of the `true` arm
    let last:uint64 = prefix.length - 1
    return src[0..last] =? prefix
}

A true result establishes prefix.length <=? src.length; the bare false arm promises nothing. Every return in the body is an obligation for the arm it returns — return true must prove the fact, from a guard (if prefix.length >? src.length return false before it) or the facts of the value returned — and a call is that fact wherever the result is known: if src[i..].startswith("[[") { i += 2 } keeps i within src, because a true startswith establishes prefix.length <=? text.length and the argument was the tail src[i..]. The prelude's startswith and endswith are declared this way. A proposition in type position is the type of its truth value, both arms at once — a type predicate:

let is_word = (tok:Token):> tok is? Word => tok is? Word

if is_word(t) narrows t to Word and the else branch away from it, exactly as if t is? Word does; the body must return precisely that truth value — return tok is? Word is its own proof, and written as two returns, if tok is? Word return true then return false, the fall-through remembers that tok is not a Word (there is no type for "a Tok that is not a Word", so the exclusion is a fact rather than a narrowed type). An expression-bodied function whose body is one such proposition about its parameters — a type test, or a comparison of lengths — is inferred to be a predicate, so let is_word = (tok:Token) => tok is? Word is the same declaration; :>bool opts out.

let Tok:type = $abstract type of any & [text:string]
let Word = type of Tok & []
let is_word = (tok:Tok) => tok is? Word

# the offset past a `[[ … ]]` block, within the source — no guard: `startswith` proves the steps
let eat_block = (src:string):>uint64<n => n <=? src.length> | none => {
    if not src.startswith("[[") return none
    let depth:int64 = 0
    let i:uint64 = 0
    loop i <? src.length {
        if src[i..].startswith("[[") { depth += 1  i += 2 }
        else if src[i..].startswith("]]") { depth -= 1  i += 2 }
        else { i += 1 }
        if depth =? 0 return i
    }
    return none
}

let main = ():>int64 => {
    let t:Tok = Word[text="hi"]
    let n = eat_block("[[a[[b]]c]] rest")
    if is_word(t) and n is? uint64 { let w:Word = t  return (n transmute int64) - 11 }   # 0
    return 1
}

The facts a result may state about a parameter are type tests (tok is? Word, tok isnt? Word), bounds on its length (prefix.length <=? src.length, against another length or a number, in either direction), and bounds on its value — against a number (true & <n >? 0> | false) or another parameter ((a:uint64 b:uint64) => a <=? b is a predicate whose true arm makes b - a a proven uint64 at the call). The value's own facts may likewise bound it by a parameter's length in either direction (n >=? src.length, n =? src.length) or by a parameter's value (n => n <=? limit). A length term may also appear on a parameter's own annotation, naming a sibling — (src:string n:uint64<v => v <=? src.length>) makes src[0..n) proven inside and n <=? src.length an obligation on the arguments at every call (the term names the argument passed for src, which must be a binding) — and on a local's, naming a binding in scope: let n:uint64<v => v <=? src.length> = 3 is proven where it is declared and at every assignment to n, holds wherever n is read, and requires that src is never reassigned in that function. A function that returns nothing may still establish facts: a result of only facts, :> <facts>, is owed at every return and at the end of the body, and holds for the caller after the call — the shape of a checking or fixing procedure. A boolean parameter promised =? true establishes the argument's own condition, so a library can write what $runtime_assert does; an @ place argument gets the facts the call establishes about it, the only facts that survive passing it by place; a type fact narrows the argument:

let require = (ok:bool msg:string):> <ok =? true> => { if not ok { printl"{msg}"  exit(1) } }
let ensure_nonempty = (@xs:array<int64>):> <xs.length >? 0> => { if xs.length =? 0 { xs.push(0) } }
let must_be_word = (tok:Token):> <tok is? Word> => { if tok isnt? Word { exit(2) } }

ensure_nonempty(@xs)  let first = xs[0]                 # proven
require(i <? text.length "i out of range")  let c = text[i]
must_be_word(t)  let w:Word = t

Facts may sit on any member of a union result — true & <…> | false & <…> is the case where the members are the two booleans. Ok & <tok is? Word n <=? src.length> | Trouble says what holds when the result is Ok: each return Ok owes those facts, and a caller that narrows the result to that member (if r isnt? exception, if r is? Ok, =? none) has them, until the result binding is reassigned. A bare fact block anywhere but a result — a parameter's or a local's annotation — is an error that says which type is missing (T & <facts>).

What a caller learns follows the argument: a fact about a parameter's length becomes a fact about the argument's length, about src.length - i for a tail src[i..], about j - i for a window src[i..j) (or j - i + 1 for src[i..j]) — so let k = take(text[i..j)) then text[i..i+k) proves under i <=? j <=? text.length — or a bound on a known length. Facts are never assumed from a type: a function type that states them (a slot eat:eatfn) makes them the contract of every implementation.

Prototyping Without the Proofs

$prototype in the entry module defers the program's unproven proof obligations to runtime: an unproven index, integer narrowing, or refinement obligation compiles anyway, wrapped in a runtime check that — if it fails — reports Runtime Panic with the violated requirement stated concretely (e.g. array index out of bounds, value does not fit `int8` , requirement violated), pointing at the same source span the compile error would have, with the observed values (observed: the index was 5 and the length was 1), then exits with status 102. The rigor is unchanged in kind, only in time: no-traps stays the language rule, and the metatag is the program writing the traps, wholesale, the way $runtime_assert writes one. Each deferral prints as a compile-time warning (prototype: …, silenced by $prototype_warnings = false). Type errors, arity errors, and structural rules are not proofs and still reject the program; a site whose check cannot be built (an operand with effects) also stays a compile error. $prototype is for development — remove it and the warnings show exactly what remains to prove.

$prototype
half = (n:int64 d:int64<i => i not=? 0>):>int64 => n // d
main = (argv:array<string>) => {
    printl(half(10 argv.length))    # warned at compile time; checked at runtime
    return 0
}

The Length Cap

One assumption sits under every length fact: no array or string holds more elements than the target's address space has bytes. An unknown length is therefore [0, 2^bits) rather than [0, ∞), where bits is the target's address width — 48 on x86_64, arm, riscv, and c; 32 on wasm32 (ADDRESS_BITS in dewy/targets.py). It is an axiom the analysis trusts, not something a program proves, and it is what lets s.length <=? uint64.max hold for any string on a 64-bit target, or a.length + b.length fit a word, without a guard; a bound below the cap (length <=? uint16.max) is a real obligation. The type addr is this axiom as a value: a natural that is a position in the address space, closed under sums and differences of positions (see Numeric types). dewy analyze names every proof in a program that rests on the axiom (address-space cap, with the target's width) and ends with the length cap report. Compiling one program for several targets is a question for later; each target is analyzed against its own cap.

No Traps

Dewy is a trap-free language. A compiled program never aborts, panics, or crashes on a path the programmer did not write: the only exits are the ones spelled out in the source — return, a failed $runtime_assert, an explicit call to exit. Every operation that could fail is handled in one of two ways, and never a third:

1. A compile-time proof. If the precondition is provable — an index within a proven length, a divisor a guard or refinement makes nonzero, a refinement an obligation discharges — the operation compiles to the bare instruction, with no check at runtime. If it is not proven, that is a compile error, and the fix is more facts (a guard, a refined type, an assertion), not a runtime check inserted by the compiler.
2. A value. If a failure is genuinely undecidable at compile time — arithmetic on 64-bit parts that may overflow, tan of an angle whose cosine may be exactly zero, reading a file that may not exist — the operation's type says so: rational | Overflow, fixed | DivisionByZero, T | none, and the caller handles that branch explicitly (is?, or_throw, a default).

The compiler therefore never emits a fallback that changes an operation's meaning, and the library never contains one: no silent wrap-to-zero, no clamping, no "unreachable" abort. The rule follows from proofs-over-exceptions — whatever raises in Python must in Dewy be proven safe or return a value — and it is what makes the proofs worth trusting: a program that compiles has no hidden exit.

The same holds for code written for others. It is unidiomatic for a library to exit the process on its own account: an explicit exit is a decision about the whole program, which only the program's author can make. A library that cannot prove a precondition moves the proof to its caller (a refined parameter — divide = (a:int64 b:int64 & ~0)), and one that meets a failure it cannot rule out returns it (:> T | Overflow). Exits and $runtime_assert belong in applications, at the points their authors chose. The standard library is written this way throughout.

Operation Preconditions

An ordinary partial operation is valid when its precondition is proven. Examples include indexing within bounds, dividing by a nonzero value, narrowing a number into a smaller representation, and satisfying a function's refined input contract. Integer // and % require the divisor proven nonzero: an interval that excludes zero (d >? 0, a loop variable over 1..3), a d not=? 0 guard (or a failed d =? 0), a refined parameter, or a $runtime_assert; otherwise cannot prove the divisor is nonzero is reported with the divisor's known range.

When a fact cannot be proven statically, the program chooses an explicit checked operation, establishes the fact with control flow, supplies a checked proof, or crosses an explicit unsafe boundary. The compiler must not insert a hidden semantic fallback that changes the operation's type.

Assertions

$assert condition states a fact the compiler must prove; $assert condition, message adds a string literal to the diagnostic. It has the three refinement outcomes: proven (nothing is emitted), refuted (assertion refuted), or unknown (cannot prove assertion — the fact is neither proven nor refuted). Facts come from the checker's folding and from the bounds analysis: constants, exact and minimum lengths, integer intervals, and index facts from guards.

A refuted or unproven $assert underlines the condition, uses the message as the pointer text, and explains in note: lines what the analysis knows about each operand and what that decides for each comparison (`i` is 3, `xs.length` is 3 (the array has exactly 3 elements), so `i <? xs.length` is false).

$runtime_assert condition and $runtime_assert condition, message evaluate the condition at runtime. When it fails, the program writes the same report shape to stderr through library/reporting.dewy — the excerpt with the condition underlined, the message (which may interpolate values) as the pointer text, and note: lines with the value of each non-literal comparison operand (re-evaluated on the failure path) — and exits with status 101. The failure path diverges, so the code after the assertion holds the condition's facts exactly as code after an early-return guard does. A runtime assertion whose condition the analyses refute is still a compile-time error.

let xs:array<int64> = [1 2 3]
$assert xs.length =? 3, "three elements"

let get = (ys:array<int64> i:int64):>int64 => {
    $runtime_assert i >=? 0 and i <? ys.length, "index {i} out of range"
    return ys[i]                      # proven by the assertion
}

let main = ():>int64 => {
    loop i in 0..2 { $assert i <? 3 }
    return get(xs 1)                  # 2
}

$expect condition, message is the assertion form for tests: a failure is recorded and returns from the enclosing function instead of exiting, a refuted condition is a warning rather than an error, and the code after it holds the condition's facts like the code after an assertion. See Testing.

The assertion directives are forms with their own argument grammar, like if cond body or return expr, not operators: $assert expr [, expr]. The directive owns the top-level comma of its argument — it separates the condition from the message — so the comma's operator precedence (tighter than the comparisons) never applies there, and x <? 3, "message" is the condition x <? 3 with the message "message". A condition that is itself a tuple comparison is parenthesized, $assert pair =? (1, 2), as a form's argument would be anywhere. A compile-time message must be a string literal.

Effects

An effect describes observable behavior relevant beyond a function's return value. The intended effect model covers at least mutation, allocation, blocking, I/O or host capability access, failure, nonreturning control flow, and escape of storage or handles.

Effects propagate through calls. A caller may preserve a refinement or borrow storage only when the callee's effects prove that behavior safe. Unresolved indirect calls require a conservative effect contract.

noreturn is a settled effect used by a function that cannot return to its caller. It is distinct from the never result type.

Expected failures remain error alternatives in the return type, not members of the effect set. A contract may contain both a returned error union and effects, but | combines the returned alternatives while the effect syntax describes evaluation behavior separately.

unsafe

unsafe identifies a proof or memory-safety obligation the compiler has not established. It is an auditable trust boundary, not a request to turn off unrelated checking.

Provisional Boundary

The complete proposition grammar, qualifier inference, proof-value form, effect vocabulary, effect polymorphism, and surface syntax for unsafe remain provisional. Error-value propagation has its own settled core and provisional surface details; see Errors and Forwarding and Design Maturity.

Testing

Tests are ordinary functions marked $test. dewy test finds them, builds each module with a generated runner as its entry, runs the runners, and adds up the failures. Nothing about a test function is special to the compiler beyond the annotation: it is checked, callable, and compiled like any other function, and a module keeps its own main for ordinary runs.

$test and $expect

$test on the line before a module-level function declaration marks it as a test. $expect condition (or $expect condition, message) states what the test checks:

let identity = (x:int64):>int64 => x

$test
let identity_is_itself = () => {
    $expect identity(42) =? 42, "forty-two isn't itself"
}

$expect has the same shape as $assert and $runtime_assert — a condition, an optional message that may interpolate values — and, like $runtime_assert, it is checked at runtime when the compiler cannot decide it. It differs in what a failure means:

• A failed expectation is recorded and returns from the enclosing function. The test stops at its first failure and the runner reports it; other tests still run. Because execution never continues past a false expectation, the code after one may assume it — $expect v is? int64 narrows v exactly as an assertion does.
• The report is the assertion report (the condition underlined in its source line, the message, a note: with each operand's value), written to stderr as expectation failed; the test's stdout continues afterwards.
• An expectation the compiler refutes is a warning, not an error: the module still builds and the test fails when it runs. $fail "not reached" is the deliberate "fail here" (a literal false condition is not warned about either). An expectation the compiler proves costs nothing.
• Expectations live in void functions: the test itself, or a helper it calls (the helper returns on failure; the test goes on). A function that returns a value cannot contain one — it returns the value to the test that checks it.

$fail message (or a bare $fail) is an expectation that always fails — the deliberate "this must not be reached" of a test, and the honest placeholder for a test not written yet.

$assert and $runtime_assert keep their meaning inside tests. A $assert that fails is a compile error before any test runs; a failed $runtime_assert exits the test binary (the runner reports the file as aborted), so it is for invariants a test cannot sensibly continue past.

Cases

$test(cases=…) runs the test once per case. A tuple or array of values passes each element as the single argument; an array of object literals passes each object's fields by name; a computed array (a module constant) is looped over with each element as the single argument:

let identity = (x:int64):>int64 => x

$test(cases=(1 2 3 4))
let identity_holds = (x:int64) => $expect identity(x) =? x, "identity of {x} is not {x}. got {identity(x)}"

$test(cases=[
    [a=1 b=2]
    [a=5 b=7]
    [a=(-3) b=4]
])
let addition_commutes = (a:int64 b:int64) => {
    $expect a + b =? b + a
}

Each case is reported as name[index]. A test that takes parameters must be given cases, and one that takes none cannot be.

Running tests

dewy test is the one command, a subcommand like dewy analyze:

• dewy test file.dewy runs one module's tests. The module is built with a generated entry that calls each test (per case), printing a green . for each pass and a red F for each failure as it goes; everything a test prints — its expectation report included — is captured and shown only if it fails, under a --- FAIL name[case] header after the marks, followed by the summary (1 failed, 10 passed). The exit status is the failure count (at most 100), or 101 when a $runtime_assert aborted the binary, 102 when the module did not build, 128+n for a signal. The binary is <stem>.test beside the module's ordinary one, and the module's own main is untouched.
• dewy test [directory] (default .) runs every .dewy file under the directory with a line beginning $test — hidden entries and __dewycache__ are skipped — by running dewy test on each (one line per file: tests/dewy/expectations.dewy .................) and adding up the failures. The runner itself is a Dewy program (tools/dewy_test.dewy). Output of child processes a test starts is not captured; run_silent discards it.
• --json on either form switches every line to a JSON object (per test, per file, and a summary).

Each module's tests run in their own process, so a test cannot disturb another module's, and an aborted binary is reported without hiding the others.

Whole programs

A program's behaviour is tested the same way as anything else: a test that builds an executable, runs it, and checks the result. The compiler's own fixture programs are tested like this (tests/dewy/programs.dewy), by running the host compiler and then the binary:

$test(cases=[
    [name="overload_calls.dewy" expected=42]
    [name="file_io.dewy" expected=42]
])
let program_exit_status = (name:string expected:int64) => {
    let source = p"dewy/tests/{name}"
    let binary = p"__dewycache__/dewy/tests/{p(name).stem}"
    if not binary.exists {
        match run_silent("/usr/bin/env" ["python3" "-m" "dewy" "--compile" source.path]) {
            status:int64 => $expect status =? 0, "compiling {name} failed ({status})"
            <SpawnError> => $fail "could not start the compiler"
        }
    }
    match run_silent(binary.path []) {
        status:int64 => $expect status =? expected, "{name} exited with {status}"
        <SpawnError> => $fail "could not run {binary.path}"
    }
}

Once the compiler is written in Dewy, compile is a library function and the spawn disappears; the same goes for testing the compiler's own stages — tokenize"…", parse"…", typecheck"…" are ordinary functions whose results (result is? UnterminatedString) a test inspects, so invalid source is a string passed to them, never the body of a test.

Planned

The design continues past what is implemented (see dewy/status.md): fixtures ($test(fixtures=[db=temporary_db]), passed before the case arguments, with lifecycle hooks for teardown), $test.case introspection inside a test, documentation tests (examples in doc strings and in these books), generated and guided cases (cases=Generated) with shrinking of failures, and parallel execution.

Debugging

Dewy compiles to native code, so debugging is a conversation with the compiled program: stop it, look at its values, step it. Two things make that conversation speak Dewy rather than assembly — a $breakpoint directive that stops the program and shows the live bindings, and debug line information that lets a native debugger (gdb or lldb) set breakpoints and step by .dewy source lines.

$breakpoint

$breakpoint is a statement (a metatag directive, like $assert; it takes nothing). When the program reaches it, it prints a banner naming the site and then every live binding of the enclosing function — its parameters and locals declared so far, innermost shadowing outer — one per line in the value's literal form (a string quoted, a container or object as its literal, a value that has no printable form as name : type):

── breakpoint at t0.dewy:222 ──
  src = "# just a comment\n"
  i = 0
  matches = [[length=17 token_cls=LineComment]]
  longest_match_length = 17

At module level it shows the module's bindings. Functions, types, modules, ranges, and the compiler's hidden bindings are not shown.

Then the program stops. Without a debugger it waits at a >>> prompt reading stdin. Commands start with a backslash, so that a plain expression stays free for evaluation later:

The end of input (a pipe that runs dry, /dev/null) continues, so a program with breakpoints left in still runs unattended.

Under a debugger (dewy debug, or any gdb/lldb attached to the process) the same directive traps into the debugger instead — the program stops on the $breakpoint line in your function, with the debugger's prompt and the snapshot already printed. The program decides at runtime by asking the kernel whether it is being traced, so one build serves both uses.

dewy debug

dewy debug file.dewy args… makes a debug build of the program and runs it under a native debugger — gdb if installed, else lldb (--debugger chooses). Every emitted statement carries its Dewy source position and every variable its Dewy name and type, so the debugger's own commands work on .dewy files and show Dewy values:

(lldb) b t0.dewy:222          # a breakpoint by Dewy line
(lldb) run
(lldb) n                       # step to the next Dewy statement
(lldb) bt                      # the call stack, by Dewy function names
(lldb) frame variable          # the live bindings, as Dewy prints them
(array<Hit>) hits = [Hit[length=3 name="a"] Hit[length=10 name="b"]]
(string) label = "run"
(int64 | none) maybe = none
(int64) total = 9
(Hit) h = Hit[length=3 name="a"]
(lldb) p total                 # or one value
(int64) 9

A variable is visible from its declaration on, a parameter throughout its function (gdb's info args, and frames print as describe (hits=[…], label="run")), and a loop variable under its own name. Values print exactly as "{value}" would — a string in its literal form, a container or object as its literal, a union as its member. The debugger sees Dewy function names (describe, __dewy_user_main for the program's main); the prelude's functions appear under their module-mangled names, and its variables as words. gdb and lldb are both supported, with the same view.

The debug build is a separate artifact (<name>.debug beside the ordinary binary): the value display costs compile time and size, so dewy file.dewy builds without it. An ordinary binary still has the line information — $breakpoint traps into an attached debugger, breakpoints and stepping work — but its variables show as raw words.

In an editor

Cursor, VS Code, and VSCodium debug Dewy through their stock native-debugger extensions — CodeLLDB (lldb, on Open VSX too) or C/C++ (cppdbg, gdb) — since the program carries DWARF for its Dewy source and the dewy_lldb.py / dewy_gdb.py scripts give the Variables pane, hovers, and the Debug Console Dewy values. The Dewy extension registers .dewy files for gutter breakpoints and offers two launch configurations under "Add Configuration…", both running the file in the active editor: Dewy: debug current file, and Dewy: debug current file with arguments, which asks for the program's command line each run (the prompt offers the last one again, and the extension splits the line like a shell — quotes for a path with a space — into the debugger's argument list; this is the way to run the bootstrap tokenizer on a file). Written out, with a task that builds the debug executable first (dewy debug --build file.dewy prints its path, __dewycache__/<path>/<name>.debug, and launches nothing):

// launch.json
{
    "name": "Dewy: debug current file with arguments",
    "type": "lldb",
    "request": "launch",
    "program": "${workspaceFolder}/__dewycache__/${relativeFileDirname}/${fileBasenameNoExtension}.debug",
    "args": "${command:dewy.programArguments}",
    "cwd": "${workspaceFolder}",
    "preLaunchTask": "dewy: build debug",
    "initCommands": ["command script import ~/.dewy/runtime/tools/dewy_lldb.py"],
    "sourceLanguages": ["c"]
}
// tasks.json
{
    "label": "dewy: build debug",
    "type": "shell",
    "command": "dewy",
    "args": ["debug", "--build", "${file}"],
    "options": { "cwd": "${workspaceFolder}" },
    "problemMatcher": []
}

${command:dewy.programArguments} is the extension's prompt (a ${command:…} can only yield a string, which is why the extension, not the debugger, does the splitting); "args": [] (or a fixed list, "args": ["tests/sample.dewy"]) is the configuration without one.

The gdb form is the same with "type": "cppdbg", "MIMode": "gdb", and "setupCommands": [{ "text": "source ~/.dewy/runtime/tools/dewy_gdb.py" }]. (CodeLLDB is the one exercised by the compiler's own tests, through its debug adapter.) In a checkout of the compiler the scripts are ${workspaceFolder}/tools/… and the command python -m dewy (the repository's own .vscode/launch.json is exactly this). Gutter breakpoints, stepping, the call stack, and the Variables pane then behave as for any native program, with Dewy names, lines, and values; a $breakpoint in the program pauses the editor on its line. The >>> prompt of a program run without a debugger belongs to the terminal, not the editor.

How the debugger sees Dewy

Positions: the compiler marks each statement of the µDewy it emits with a # @loc path:line:column comment naming the Dewy position it came from; the µDewy compiler turns each into a DWARF line-table row (a .loc for the assembler) for whatever it emits next, and a µDewy file compiled on its own reports its own lines the same way.

Variables: each declaration is marked # @var name shown formatter type; the µDewy compiler records every variable (a fixed slot in the frame) with the name it is shown under and its type, in a lexical block that starts at the declaration, as DWARF variable information. Values: for each type of a variable in a debug build, the compiler adds a function __dewy_debug_show_N = (v:T):>int64 that renders a value the way "{v}" does into a static text block; the variable's DWARF type is named after it, and the debugger scripts dewy debug loads (tools/dewy_lldb.py, tools/dewy_gdb.py) call that function on the stopped frame's word and read the text back. A type the module cannot spell or print (a function, a bigint under a unit) gets no formatter and shows as a word.

All of it is metadata: a program compiled with or without it is the same program, and a µDewy implementation that ignores the markers is still a correct one — though both µDewy compilers, the Python one and the bootstrap one written in µDewy, emit it (a parity test keeps their assembly identical). Evaluating typed-in Dewy expressions at a stop, and an IDE front end, come next.

Strings and Graphemes

Semantic Model

A string is an immutable sequence of Unicode extended grapheme clusters. A grapheme is a string whose length is one; char is an alias for the same semantic type.

Length, indexing, slicing, and default iteration operate in grapheme-cluster units rather than UTF-8 bytes or Unicode scalar values.

let text = "café 👨‍👩‍👧‍👦"
text.length
text[4]

The exact scalar sequence is preserved. Canonically equivalent spellings are not implicitly normalized, and exact equality compares the preserved spelling. Normalization-aware operations are a separate API design.

Indexing and Slicing

text[i] is the grapheme at i and text[a..b] a slice; both are proven in bounds, never checked at runtime. A string with a known length (a literal, or a binding initialized from one and not reassigned) is checked against that length. A runtime-length string is indexed from facts, exactly like a runtime-length array: a guard i <? text.length (or a failed i >=? text.length) proves text[i] for that binding, a proven minimum length (text.length >? 0) proves constant indexes and text[text.length - k], and a slice needs both endpoints proven the same way. Reassigning the binding drops its facts. Inside an index, end is the last index — text.length - 1 — and may take part in any expression: text[end], text[end - 1], text[2..end] (each proven the same way, so text[end] needs text.length >? 0).

let first_word = (text:string):>string => {
    let i:int64 = 0
    loop i <? text.length {
        if text[i] =? " " { return text[0..i) }
        i += 1
    }
    return text
}

let main = ():>int64 => first_word("héllo world").length   # 5

Interpolation

Braces inside a string literal evaluate an ordinary Dewy expression and convert its value to string:

let message = "item {index}: {value}"
let combined = "{left}{right}"

A field's value converts the way value as string does: numbers, booleans, and strings directly, a declared type through its conversion method __as__ = ():>string => … (see as) — user-defined formatting participates in the general conversion protocol rather than a string-only hook — and a container or an object without one as its literal syntax (see Printing). A field whose type cannot convert is an error. Big integers have a decimal string form, including inside optional values and containers.

An implementation may stream the literal chunks and converted fields directly to a consumer such as printl, or materialize a string value when the surrounding context needs one. That representation choice is not observable.

Printing

print writes a value; printl writes it and a newline. Both are ordinary generic functions of the prelude (library/io.dewy): a string, an integer, a boolean, or one of the number objects (Rational, BigInt, …) prints through its own arm — the arms are type tests decided per instance — and anything else prints as its as string text. So every value with a string conversion prints: a container as its literal syntax ([1 2 3], set["a" "b"], ["a" -> 1]), an object through its __as__ = ():>string when its type declares one and otherwise field by field ([x=1 name="q"]), members the same way, so nesting is arbitrary. A string inside a structure is quoted, with the escapes of its literal syntax ("a\tb"); a string printed on its own prints bare.

let Point:type = [x:int64 y:int64]

let main = ():>int64 => {
    printl(5)
    printl([1 2 3])                  # [1 2 3]
    printl(set["ab" "c"])            # set["ab" "c"]
    printl(["k" -> Point(1 2)])      # ["k" -> [x=1 y=2]]
    printl'{[true false]} and {[name="q"]}'
    let text:string = [1 2 3] as string
    return text.length               # 7
}

Because printing is as string, an array of graphemes prints as the text they form (printl(["a" "b"]) writes ab), as as converts it. A value that cannot convert — a member of an optional type, a container whose members are containers, or a rational/fixed number object inside a structure (those print, but have no string form yet) — is an error where it is printed. An interpolated argument is written part by part rather than built into one string first; that representation choice is not observable. Printing a structure is for looking at values: its exact text is not a stable format.

Searching, Splitting, and Trimming

Strings have methods, written in Dewy in the prelude's strings.dewy; positions and lengths are graphemes, like indexing. text.contains(x), text.startswith(x), text.endswith(x); text.find(x) and text.rfind(x) yield the first or last position or none; text.split(sep) yields the pieces between separators (adjacent separators give empty pieces; an empty separator splits into graphemes); text.lines the lines without their breaks (a final break adds no empty line); text.trim, text.trim_start, text.trim_end drop spaces, tabs, and line breaks; text.replace(old new) replaces every occurrence. Zero-argument methods are called without parentheses.

let main = ():>int64 => {
    let line:string = "  key: value  ".trim
    match line.find": " {
        i:int64 => printl"key ends at {i}"
        <none> => printl"no separator"
    }
    let parts = line.split": "
    return parts.length                    # 2
}

text.casefold is the Unicode full case folding (CaseFolding.txt, statuses C and F): the form for case-insensitive comparison, not a lowercase for display — "Straße".casefold is "strasse", "İ".casefold is "i̇". Compare a.casefold =? b.casefold; a test like head is? BasePrefix narrows to the union member (see Unions and Narrowing).

Joining and Building

xs.join concatenates the elements of a string array (array<string>, array<grapheme>) into a new string; xs.join(sep) — or, juxtaposed, xs.join", " — places the separator between neighbours. The result is re-segmented, so clusters may span the joins. join reads its receiver: it applies to any array value, of any length, and is not a mutation.

Loop-built strings use an array<string> as the builder: push each piece (an interpolation such as "{value}" converts anything printable), then join:

let render = (values:array<int64>):>string => {
    let pieces:array<string> = []
    loop v in values { pieces.push"{v}" }
    return pieces.join", "
}

+ is not string concatenation; two strings combine by interpolation ("{left}{right}"), many by join.

Decoding Bytes

bytes as string requires a proof that the bytes are valid UTF-8, which the compiler cannot make for runtime data. The checked form is bytes as string | none: it validates the bytes (RFC 3629 — no overlong forms, no surrogates, nothing above U+10FFFF, no truncated sequences) and yields the decoded string, or none for invalid input, so the program decides what to do at that point:

let text = read_text(path)          # `string`, or a file error, or `InvalidUtf8`
if text is? string { printl(text) } else { printl"not readable text" }

read_text is read_bytes followed by this decode, with none reported as the InvalidUtf8 error alongside the file errors (FileNotFound, FileAccessDenied, IsDirectory, FileError); a decode of bytes you already hold is bytes as string | none.

Including Files

$include_bytes(p"path") embeds a file's bytes at compile time. The path must be known when compiling — a path literal today, resolved against the source file — and the result is a binary literal (array<uint8> of a known length), usable like 0x"…": .length, indexing, as string | none. $include_bytes(p"path") as name is the statement form, declaring name. The generated program does not spell the bytes out; the target embeds the file itself, which is how the compiler's Unicode tables travel.

let table = $include_bytes(p"data/table.bin")
$include_bytes(p"data/notes.bin") as notes
let text = $include_bytes(p"data/notes.txt") as string | none

Representation Views

Explicit array views expose lower-level representations:

• array<uint8> contains UTF-8 code units;
• array<uint32> contains Unicode scalar values;
• array<grapheme> contains grapheme values.

Converting a grapheme array to string concatenates its contents and segments the result again, so boundaries between adjacent inputs need not remain grapheme boundaries.

Conversions from arbitrary integers to string representations require proof that the input is valid UTF-8 or valid Unicode scalar data; array<uint8> has the checked form as string | none described above.

Character Ranges

A range whose unannotated anchors are one-grapheme strings advances in Unicode scalar order when each anchor contains exactly one scalar. Iteration skips the surrogate interval. Enumerating multi-scalar graphemes or natural-language collation order is unspecified.

chr(scalar) is the one-scalar string of a Unicode scalar value (chr(0x1F600) is "😀"). The scalar's range, 0 to 0x10FFFF, is a proof obligation at the call — a loop over [0x41..0x5B) proves it — and a surrogate code point, which no string can hold, yields the replacement character U+FFFD.

let main = ():>int64 => {
    let letters:array<string> = []
    loop i in [0x41..0x44) { letters.push(chr(i)) }
    return letters.join.length      # "ABC": 3
}

Arrays and Containers

Arrays

An array is an ordered homogeneous value. Array indexing is zero-based.

let names:array<string> = ["Ada" "Grace"]
let triple:array<int64 length=3> = [10 20 30]

array<T> specifies the element type. Growable arrays hold word scalars, strings, and objects; an object element is stored as an independent copy, so the array never aliases the value pushed into it, and a popped element remains valid. Inside an index, end is the last index (xs.length - 1) and composes freely: xs[end], xs[end - 1], xs[2..end], proven from the same facts. Iterating an array of objects (loop s in spans) binds the loop variable as a read-only borrow of each element — assigning it, its fields, growing its arrays, or passing it as a place is rejected; copy it (let mine:Span = s) to change it. array<T length=N> additionally refines the length. Array values follow Dewy's value semantics: binding, assignment, argument passing, and return produce an independent value unless the program explicitly passes a place.

let original = [1 2 3]
let copy = original
copy[0] = 9                  # original remains [1 2 3]

The compiler may implement an unobservable copy as a move, borrowed read, shared immutable backing storage, or another equivalent representation.

.length reports the length. Integer indexes select elements, and range indexes select slices. The compiler must prove an ordinary index valid; operations that perform explicit runtime validation are separate checked interfaces.

Growth Methods

An array whose type has no exact length (array<T>) may change length through methods on the value. xs.push(v) appends; xs.pop removes and yields the last element and xs.pop(idx) the element at idx, shifting later elements down; xs.insert(v idx) inserts before idx (idx may equal the length); xs.truncate(n) keeps the first n elements; xs.clear empties; xs.reserve(n) requests capacity; xs.sort orders integer elements ascending in place.

Each partial operation carries a proof obligation: pop requires a proven positive length, and pop(idx)/insert(v idx) require 0 <= idx < length (<= for insert). Proofs come from literal lengths (an exact length is retained as a fact until a length-changing operation steps it), from push/pop stepping known lengths, and from guards such as xs.length >? 0 or idx <? xs.length. A binding declared with an exact length (array<T length=N>) cannot change length.

Length-changing methods also preserve declared minimum and maximum lengths, including contracts on array fields. xs.push(v) must prove it stays below an annotated maximum, and pop, truncate, or clear must preserve an annotated minimum. See array contracts. The count passed to truncate must be proven nonnegative, including when it is only known at runtime.

Container mutation is reached only through the container value; free functions are reserved for genuinely global operations.

A let with a runtime-length annotation and an empty initializer, let buffer:array<uint8> = [], is a growable array from the start (an empty exact array would be useless), and a callee may grow it through a place parameter: fill(@buffer 5). Passing @name makes the compiler forget what it knew about the binding — an exact length, a refinement — since the callee may have changed it.

A loop inside [] is loop capture: the collector receives each non-void value the loop expresses and produces an array.

A trailing ... after a sequence inserts its elements into a surrounding array literal. Fixed elements and spreads may mix: [heads... tails...], [0 xs... 1].

Shapes and Dimensions

Arrays are also the intended foundation for vectors, matrices, and tensors. Shape belongs in array type information rather than requiring unrelated matrix classes.

The exact general multidimensional literal and type syntax remains provisional. In particular, nested array<array<T>> must remain a valid array-of-arrays construction and must not prevent a contiguous representation such as an array whose length or shape is a sequence of dimensions.

Dictionaries and Bidictionaries

A dictionary literal uses -> pairs; a bidictionary uses <-> pairs and supports lookup in both directions:

let scores = ["Ada" -> 10 "Grace" -> 12]
let names = [1 <-> "one" 2 <-> "two"]

Dictionaries retain insertion order, and iteration yields key/value pairs in that order:

let scores = ["Ada" -> 10 "Grace" -> 12]

loop [name score] in scores
    printl"{name}: {score}"

dict<K V> names a dictionary type; a dictionary literal in a dict<K V> context adopts those entry types, and an empty literal requires such a context. K may be a union of string literals ('0b' | '0t', an enumeration of allowed keys — such a union is a string at runtime), and V may be an object type, an optional (int64 | none), or a union of objects, words, and strings (Number | Name | Punct, a token); arrays likewise hold string-literal unions, optionals, and such unions as elements — a loop over them binds each element for match. V may also be an array (dict<string array<Op>> — a table of handler lists); nested array elements are handles released one level deep. An abstract int or uint in an element position — array<int>, dict<string int | none>, set<uint> — is the 64-bit word, as int in a signature is. Unions containing arrays are not container elements yet. Dictionaries are values with the ordinary value semantics: they are passed, returned, stored, and compared by value, and copies are independent.

Lookup

d[key] is valid only when the key is proven present and then has type V. A key is proven when it is a constant entry of the literal that initialized the dictionary, was stored by d[key] = value, is the key bound by loop [key value] in d, or was tested by a guard if key in? d. Facts are path-sensitive (a key proven on every branch stays proven after the branches join) and are invalidated when the dictionary or the key binding is reassigned. A guard's search result is reused by the guarded lookup, so a proven lookup performs no second search. An unproven d[key] is a compile error.

d.get(key) is the lookup that may miss, with type V | none. d.get(key default) yields default when the key is absent and has type V.

A dictionary whose key type is finite — a union of literals such as '0b' | '0o' | '0x' — and whose literal has an entry for every value of it is total: d[k] is then proven for any k of the key type, not only for a constant key. Totality is inferred from the literal (a const keeps it everywhere; a let keeps it until a pop or clear), or declared with totaldict<K V>, which makes a missing entry an error at the literal (naming the missing keys) rather than at some later lookup, and refuses pop and clear, so the type is an invariant: a totaldict<K V> parameter proves table[k] without any fact at the call site. A total dictionary passes where a totaldict is expected; a dict<K V> that may be partial does not. totaldict needs a finite key type.

const BasePrefix:type = '0b' | '0o' | '0x'
const RADIX:totaldict<BasePrefix int64> = ['0b' -> 2 '0o' -> 8 '0x' -> 16]   # forgetting `'0x'` is an error here
let radix_of = (base:BasePrefix):>int64 => RADIX[base]                       # proven: every `BasePrefix` is a key

Mutation

d[key] = value replaces the value of an existing key in place or appends a new entry. d[key] += value (any compound operator) updates a proven key in place: it reads like d[key], so an unproven key is the same compile error, and the counting idiom is if word in? counts counts[word] += 1 else counts[word] = 1. d.pop(key) removes a proven key and yields its value; d.pop(key default=v) removes the key if present and yields its value, else v, without a proof. d.clear removes every entry. d.length is the number of entries.

A dictionary must not be mutated by a loop that iterates it; stores, pop, and clear inside such a loop are compile errors.

Views and Combination

d.keys is a fresh set<K> of the keys and d.values a fresh array<V> of the values, both in insertion order. d1 | d2 (equivalently d1 or d2) is a new dictionary containing every entry of d1 followed by the entries of d2 whose keys are new; for shared keys the right value replaces the left value at the left position. Other operators do not apply to dictionaries; combine key sets instead.

Representation