Dewy Language Reference

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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.

Fresh compiler examples and target-scoped acceptance results belong to Implementation Compatibility. Those implementation notes do not redefine the source language.

Conventions

• Dewy source conventionally uses the .dewy suffix.
• 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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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 micro sign µ and Greek mu μ name the same binding. ASCII and Greek letters remain distinct: A is not Α.

An underscore followed by decimal digits spells subscript digits; an overline ‾ (U+203E) followed by decimal digits spells superscript digits. Adjacent runs combine, and the ordinary Unicode spelling names the same binding:

let x_12 = 42       # also x_1_2 or x₁₂
let x‾12 = 7       # also x¹²; distinct from x₁₂ and x12
let foo_2_bar = 3  # also foo₂_bar; foo_bar stays unchanged

This rule applies only to digits. Write letter decorations directly (xᵢ, xᵀ); x_i remains a different name. Superscripts in identifiers are labels, not exponentiation. Normalization does not change string contents or the source spans used in diagnostics.

The full Unicode repertoire and additional equivalences remain open. A doubled marker as an escape is still a design question.

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.

The names extern, intrinsic, none, void, end, and new are reserved. They cannot name variables, parameters, fields, methods, loop bindings, type aliases, or import aliases. Their existing expression and type roles remain: none is the absence value/type, void is a no-value result, and xs[end] uses the last valid index. <none> in a match arm tests the type and does not introduce a binding. untyped is not reserved; the compiler's internal inference marker does not reserve a source name. Reserving new does not yet implement the planned singleton-axis indexing operation.

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. Whitespace always separates expressions. At head(...), the head's type decides once between a call and a juxtaposed multiplication (see Operators and Precedence); no alternative parses are kept.

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

Literals

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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. Bidictionary and multidimensional literal details are catalogued in Arrays and Containers and the design appendix.

Source Files and Execution

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

Current command line

Use dewy file.dewy to run, dewy check file.dewy to check without output, or dewy build file.dewy --release -o program to save a native executable. In a checkout use ./tools/dewy in place of dewy. build --target wasm32 emits a browser page. See installation and target-scoped coverage.

Source-language rules

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 = ():>void => {
    printl"running"
}

main returns void or the errors that reach it: void | E, an ordinary result type, declared or inferred. It gives no exit code: success exits 0, and a script that needs a particular code calls exit(n). An error reaching main is printed on standard error and ends the program with its kind's code, assigned 1, 2, 3, … in the order the kinds are declared (a declared result fixes the order), below 126; an error type may pin its own with an exit_code member. dewy build --exit-codes prints the table. 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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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.

Local Read-Only Views

Inside a function, const name = @route demands a read-only view of an existing stored value. The compiler must prove that the storage stays valid and stable; it cannot silently replace this request with a copy.

Box:type = [value:int64]
read = (boxes:array<Box length=1>):>int64 => {
    const box = @boxes[0]
    return box.value
}

A conflicting write is diagnosed at that write. Use .copy() when an independent snapshot is intended. Reading a view through an ordinary value boundary, such as returning it or storing it in another record, still supplies an independent value; this does not create a first-class reference.

The normal inference proof keeps the owner stable throughout the function. A required view can also use a shorter interval ending at the last use of all its dependent aliases, including return edges and loop backedges. Private, uncaptured storage may change outside that interval. Captured owners and exposed addresses still need stronger lifetime evidence. It supports bindings, fields, and array elements, including scalars, records, arrays, strings, unions, dictionaries and sets. Scalar views retain the source width and signedness; they make the same stability demand as a view of aggregate storage.

let cursor = @xs[i] creates a mutable local place. Writes through cursor update the selected element; i is evaluated once at the declaration. A place may also select a named binding, a record field, or a proven dictionary entry (let entry = @table[key]). A dictionary key is evaluated once; the entry must already be known present when the place is declared. The selected storage must remain available until the last use, including uses by derived aliases. Replacing or resizing its owner in that interval is rejected. A local place retains the selected storage's write contract and const barriers, and its reads/writes retain the owner's effects and facts. It is not a first-class reference: captured or escaping places still require further lifetime support. Writes through the selected alias keep the containing dictionary’s keys present, while invalidating changed value facts. Earlier value snapshots remain independent. Ordinary value reads can still produce independent snapshots.

let xs:array<int64> = [40]
let cursor = @xs[0]
cursor += 2
$assert xs[0] =? 42

The explicit @ form is an escape hatch while inference improves; ordinary read-only locals already borrow when the compiler can prove it safe.

A required view introduces no allocation permission: a function that only inspects ordinary by-value input through such views can state no_effects. The storage proof still has to succeed. A view of a place parameter retains its external read effect; binding a local name does not hide that access.

Requiring Explicit Copies

The file-level $explicit_copies directive rejects an implicit copy of runtime-sized storage when the compiler cannot prove a borrow or move. It applies to that module, including when it is imported. Only copies that cost something count. Sharing an immutable string never duplicates its bytes, so keeping, passing or storing a string is not a copy under the policy. A string still counts when it leaves an $allocator block, which copies it for real. This distinction applies recursively: a fixed record or fixed array of strings can share its immutable bytes, while a runtime-length array still has an unbounded mutable-storage copy. Backend placement copies remain visible in analysis reports without changing which programs the source policy accepts. $explicit_copies = false disables the policy; a file may set it once.

Use .copy() when an independent value is intended, or const view = @source when stable borrowed storage is required. For example, a function that needs a mutable working array can copy it explicitly:

$explicit_copies
changed = (source:array<int64>):>array<int64> => {
    let working = source.copy()
    working.push(42)
    return working
}

The check includes nested storage and fields added by concrete child types. A fixed-size record can contain a runtime-length array; a single grapheme can contain arbitrarily many bytes. Copy-on-write sharing does not satisfy the requirement by deferring those copies. Fixed-size copies remain allowed ; this directive is not a no-allocation contract.

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.

Minted types can declare compiler-only, zero-argument members tagged $__drop__, $__copy__, and $__move__. Drop returns void and runs before automatic field cleanup; copy and move return the same nominal type. The compiler supplies a borrowed receiver. A drop hook without a copy hook makes the resource move-only: proven last uses transfer it, proven read-only uses borrow it, and independent ownership requires a copy hook. Hooks participate in effect and fact checking. Copy/move elision can change whether an optional hook invocation occurs.

Cleanup supports nested records, arrays and optional/union owners, including recursive records linked through optional fields. A parent's hook runs before its fields are cleaned up in reverse order; arrays clean up elements in reverse order. Resource dictionaries clean up live values and transfer ownership on removal; independent snapshots invoke the component copy hooks.

Conditional transfers follow the path that executes. An owner created outside a loop can move on a path that exits with break, including a labeled exit, when no later use or live alias needs it. A path that continues the loop still needs the owner for later iterations. For example, an owning consume(owner) immediately followed by break can move; following it with continue cannot. Mutable entry places can replace resource values: the replacement is evaluated first, then the old value drops once. General field transfers remain conservative.

The broader typed allocation capabilities remain provisional; see Design Maturity.

Scoped Allocators

$allocator(@scratch) expression requests allocation from an Arena for the whole next expression. Braces group several statements under the same request:

let scratch = Arena[]
let summary = $allocator(@scratch) build_summary(input)
scratch.reset()

Results leave the scope with independent storage, so resetting the scratch arena does not invalidate summary. The arena itself cannot be used while it is lent to the expression. Cross-allocator copies remain subject to $explicit_copies, including immutable strings whose bytes must leave the arena.

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.

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.

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.

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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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. 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. A numeric parent can be written as follows in the design:

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 = ():>void => exit(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 = ():>void => {
    let words:array<string> = ["hi"]
    let w = first(words)          # T = string
    let s = swap(1 "one")         # T = int64, U = string
    exit(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.

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 = ():>void => exit(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 = ():>void => {
    let m:Mode = "slow"
    exit(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 = ():>void => {
    let q = safe_div(6 3)             # int64
    let e = safe_div(6 0)             # DivZero
    if e is? DivZero { exit(q) }     # 2
}

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

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<(>? 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 illustrate this model.

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 = ():>void => {
    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
    exit(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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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 on them is exact, like int; the width is a storage property plus facts. Storing a result into an intN or uintN binding, field, parameter or return is the proven narrowing: free when the facts prove it fits, otherwise a compile error with fix-its (a guard, an overflow policy, or $runtime_checks). The overflow policy is a keyword type parameter: uint32<overflow='wrap'> wraps modulo 2^32 and uint8<overflow='saturate'> clamps.

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 exact sum that needs a proof before it is stored in an int64. 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.

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

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 belong to the language design. 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.

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 is exact and narrows only when stored, so let w:nat64 = end - start computes the exact difference followed by the proven cast.

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

Fixed-width expressions use sufficiently wide machine words, including statically sized multiword values, without bigint allocation. Unproven stores retain runtime checks under the current default; $no_hidden_costs rejects them. Use uint32<overflow='wrap'> for modular arithmetic or overflow='saturate' for clamping. Provisionally, if facts cannot bound an intermediate's width, compilation fails with suggestions to guard the count/exponent, use explicit int, or choose an overflow policy.

Expressions and Evaluation

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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.

no is a prefix used only in function effect contracts, such as :> int64 & no reads<Filesystem>. It is not Boolean negation.

Juxtaposition

Adjacent expressions written without whitespace can form several operations:

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

Multiplication by juxtaposition is restricted and type-directed. The eligible forms are a numeric literal before a name, member term or parenthesized group (2x, 2sin(x), 3(a+b), 2x^2); a named numeric value or field route before a parenthesized group (a(x), material.k(T), n(n+1)/2); and a parenthesized scalar before a parenthesized group ((a+1)(a-1)). The left side must be a statically known, non-callable numeric scalar or quantity; having __mul__ alone does not qualify. In this multiplication the group holds exactly one value: for a number a, a(x y) is an error (write a * (x * y)).

At head(...) the head is classified once, before any implicit zero-argument call: a callable is a call, an eligible number is a multiplication at coefficient precedence, and a union of callable and numeric, an unresolved category, or a value that is both requires narrowing or an explicit operator. A failed call never falls back to multiplication.

Whitespace always separates expressions, so a b is never a product (write *). A call result (f(x)g(x)), an indexed element (xs[i](j)) and a tensor (A(x)) are never coefficients; write f(x) * g(x), xs[i] * j and A*x (or A[x] to index). Partial application @a(x) requires a callable, and a string literal after a name (printl"hi") is always a call.

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 = ():>void => {
    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 }
    exit(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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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.

Effect Contracts

Effects describe what evaluation may do, independently of the returned value or error alternatives. Attach the row to the result with &:

Filesystem = type of any
forward = (f:():>int64 & reads<Filesystem>):>int64 & reads<Filesystem> => f()
read_value = (@value:int64):>int64 & reads<value> => value
set_value = (@value:int64):>void & mutates<value> => {value=42}

Named resources use nominal type identity. Aliases and imports preserve that identity; another mint with the same name does not. A place subject identifies a parameter's caller-owned storage, optionally followed by stored fields. Ordinary by-value reads and private scalar assignments have no external read/write effects. Compound assignment requires both reading and mutation.

A positive row is an upper bound on all effects. no_effects (also spelled Effect<>) is the empty bound. no reads<Filesystem> excludes that read; no reads excludes the entire read family. Without a positive bound, negative clauses leave other effects open. Callback calls preserve these guarantees. reads<> and no reads<> are rejected to avoid confusing an empty subject set with a family-wide exclusion.

Current checking covers scalar computation, read-only value access, place reads and scalar place writes, direct calls, and constrained callbacks. Unmodeled operations and allocations remain unknown and cannot satisfy an empty row or negative promise. In particular COW deferral is not proof of no allocation. A function literal with an omitted row now carries its inferred body effects when used as a callback:

answer = ():>int64 => 42
use = (f:():>int64 & no_effects):>int64 & no_effects => f()
checked = ():>int64 & no_effects => use(@answer)

An omitted row on an unknown callback parameter still admits unknown behavior: there is no body from which to infer a narrower contract. Recursive calls, generic calls, conditional callback choices and callback reassignment retain possible effects; inferred rows also include synthesized lifecycle operations. Inferred wrappers preserve open negative guarantees; unknown operations still remove unproved exclusions. Generic row substitution preserves the guarantees shared by every contributing callback. Scoped place-row inference and the full allocation/failure vocabulary remain in progress.

Effect rows have their own generic kind:

let apply = <E:Effect>(f:():>int64 & E):>int64 & E => f()

The callback's contract determines E; repeated callback constraints combine by union. Ordinary types and rows may coexist in a generic parameter list, but an effect parameter cannot be an argument type, return value type, or runtime value. Omitted callback contracts infer unknown effects, not purity. Generic instances retain their row arguments in cache identity.

The initial inference supports one free row remainder in each callback bound. Two unconstrained remainders cannot be split uniquely. Callback-relative place subjects are not inferred into an outer row: their slots belong to the callback, not the enclosing signature. Such routes need an explicit scoped representation before this case can be supported. Negative-only callback rows infer an open row with their exclusions. Combining callbacks keeps only shared guarantees; adding a permission can remove an incompatible inferred exclusion. Written exclusions remain obligations on the complete result. Effect-polymorphic type aliases are also pending.

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.

Control Flow

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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<(<? 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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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.

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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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<(<=? 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. Refinement facts 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<(<? 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.

Nested range bounds compose with the enclosing loop's facts. For example, inside loop i in [0..xs.length), a loop j in [0..i) can index xs[j] without restating a guard. The counters retain abstract-integer semantics. To represent an unbounded counter as a word, the compiler verifies its first value and every advancing path, including continue, against the word range. Breaks and returns do not advance. This also permits inclusive conditions when the bound leaves room for the next step, and descending counters. An unproved storage invariant is discarded, not assumed; arbitrary-precision iterator lowering remains required for counters that cannot use a word.

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<(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<(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 = ():>void => exit(percent(1 4) + share(3 4))   # 25 + 75

Refined Results and Field Invariants

A result may be refined — let positive = (n:int64):>int64<(>=? 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<(<=? 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<(<=? 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< (<=? 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 = ():>void => {
    let r = Ratio(84 2)
    let q:rational<int64> = 1 / 3                        # the word rational declares the same invariant
    exit(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<(<=? 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 = ():>void => {
    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  exit((n transmute int64) - 11) }   # 0
    exit(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<(<=? 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<(<=? 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 runtime result :> void & <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):> void & <ok =? true> => { if not ok { printl"{msg}"  exit(1) } }
let ensure_nonempty = (@xs:array<int64>):> void & <xs.length >? 0> => { if xs.length =? 0 { xs.push(0) } }
let must_be_word = (tok:Token):> void & <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 outside a $proof 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<(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. 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). Each target is analyzed against its own address-space 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 = ():>void => {
    loop i in 0..2 { $assert i <? 3 }
    exit(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, process failure, 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.

Omitted function rows are inferred from bodies and checked callable assignments. Each call translates effects on the callee's place parameters into the caller's actual arguments. Reordering parameters or passing a field does not change the identity of the storage being described. Inferred callback rows retain this mapping until their behavior is known, including through reassigned handles.

Negative guarantees retain their scope: no mutates<box.field> does not promise no mutates<box>. Unknown behavior cannot establish a missing guarantee. Generic row parameters carry nonlocal effects, including nominal resource permissions and negative guarantees. Place permissions stay explicit in each signature, for example:

let forward = <E:Effect>(f:(@x:int64):>void & mutates<x> & E @y:int64):>void & mutates<y> & E => f(@y)

Here the call translates mutates<x> to mutates<y>. A callback-local place effect cannot instead be inferred into E: its parameter number would have a different meaning in the wrapper. Local exclusions remain at the callback boundary and are omitted from the nonlocal remainder. A more general syntax for rows carrying/remapping place identities remains a separate design item.

Type aliases can also take row parameters. Each argument is checked against its parameter's kind; a row cannot become a value type or runtime value. Aliases preserve nominal resource identities, negative guarantees and nested binder scope, including through imports.

Action:type = <E:Effect>(():>int64 & E)
let invoke = <E:Effect>(f:Action<E>):>int64 & E => f()
quiet = ():>int64 & no_effects => 42
main = ():>int64 & no_effects => invoke(@quiet)

Action<no_effects> supplies a concrete empty row; Action<E> forwards an existing row parameter. Type and row parameters can occur in the same alias. A negative-only argument such as no mutates<Filesystem> keeps an open row with that exclusion; it does not promise that every other effect is absent.

noreturn is a control-flow guarantee that a function cannot return to its caller. It is kept separate from the may-effect row: permitting fewer possible effects does not imply that a call never returns.

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.

Allocation contracts use bare allocates and no allocates:

snapshot = (xs:array<int64>):>array<int64> & allocates => xs.copy()
inspect = (xs:array<int64>):>int64 & no allocates => xs.length

The positive row permits allocation and bounds other effects; the exclusion forbids allocation while leaving other behavior inferred. Neither permits an unrelated external read or mutation. allocates<> and allocates<Resource> are rejected: resource markers do not select an allocator. Normal row subtyping and <E:Effect> forwarding apply.

The measurement rule counts logical storage work remaining after proven borrows, moves and static/stack placement. Deferring a copy through COW does not establish no allocates.

answer = ():>int64 & no_effects => {
    let xs:array<int64> = [40 2]
    xs[0] = xs[0] + xs[1]
    return xs[0]
}

A bounded temporary record passed to a read-only helper can also lend stable array descriptors and inline record fields. The root lives in frame storage; its fields keep their original owners. Known helper chains may forward this root when every use ultimately projects fields. A helper that owns or returns the complete record keeps the ordinary ownership boundary. Scalar union fields pack directly into the root, without a temporary allocation.

Closed literal initializers of startup const bindings supply stable storage, and reading those immutable values has no external effect. Mutable globals and captured bindings need their own stability proof. Exact array-length facts do not change the declaration's storage representation.

Storage effects apply to built-in array growth, removal, reservation and joining, and to dictionary/set lookup, membership, stores, removal, entry snapshots and built-in array iteration. They conservatively require allocates: dictionary reads may build or compact an index, and mutations may detach shared storage. Reads and mutations of a place parameter also require its corresponding permissions; private value parameters do not introduce external resources. For example:

append = (@items:array<int64> value:int64):>void
    & reads<items> & mutates<items> & allocates => items.push(value)

Selectors, inserted values and eager lookup defaults retain their own effects. Taking a dictionary entry's address still reads its dictionary to find the key; it cannot promise no reads<table> merely because the callee only writes the payload. Lifecycle hook effects are checked after their calls are inserted. Sort callbacks remain conservative until their implicit calls are included in the public call equations.

Numeric range iterators use allocation-free word counters when their finite extent fits or the bounds checker proves every advancing edge stays within the word range. A guard alone does not establish that proof: an unbounded continue path can defeat it. The loop body retains its own effects, including allocation and external writes. Lowering's full placement/move proofs are not yet shared with this checker, so it can require permission even for a boundary the backend later removes. Unsupported operations and unconstrained callbacks remain unknown, and cannot satisfy a closed row or an unproved exclusion. This initial allocation vocabulary does not settle allocation-failure policy or promise that the underlying allocator cannot fail.

unsafe

$unsafe_assume condition [, message] introduces an assumption without a runtime check. The condition is a pure fact condition with an optional compile-time string literal. It does not turn off unrelated checking. Writes and calls invalidate its facts normally, and a checked $proof body cannot use it.

read_at = (xs:array<int64> i:int64):>int64 => {
    $unsafe_assume 0 <=? i and i <? xs.length, 'validated by the producer'
    return xs[i]
}

The condition is not evaluated at runtime. Its truth is the programmer's responsibility; a false assumption can invalidate bounds or representation safety. Conditions the compiler can prove false are rejected with assertion refuted; unknown conditions are accepted and audited.

Provisional Boundary

The complete proposition grammar and qualifier inference still need work. The reviewed effect rules are: positive rows are upper bounds, omitted rows are inferred, no_effects is the explicit empty row, and no reads<resource> excludes one effect while no reads excludes the family. Empty family forms such as reads<> are rejected by the design; Effect<> is the desugared empty row. Error-value propagation has its own settled core and provisional surface details; see Errors and Forwarding and Design Maturity.

Checked proof statements

A $proof declaration establishes a fact without producing a value. Its fact-only result, :> <P>, is reserved for proofs; an ordinary runtime procedure uses :> void & <P> and retains its runtime behavior.

$proof
ordered = (a:int64 b:int64<(>=? a)> c:int64<(>=? b)>):> <a <=? c> => {
    $assert a <=? b
    $assert b <=? c
}
ordered(1 2 3)

Every normal exit must establish the result fact. Proof bodies initially permit static assertions, conditional branches, returns without a value, and direct calls of other proofs. The proof-call graph must be acyclic; loops, runtime calls, global reads, default arguments and place parameters are outside this initial finite subset. $prototype cannot defer proof obligations or checks on erased arguments.

Only direct statement calls of statically known proofs are supported, including imported proofs. A proof cannot be stored, passed as a callback, or used as a value: both let x = ordered(1 2 3) and @ordered are errors. Arguments must be pure fact terms such as names, literals, trusted lengths, and supported arithmetic over those terms. Definitions and calls erase only after validation. Returned facts refer to current argument values; subsequent mutation invalidates them normally.

Sort invokes its key callback, so the callback's effects contribute to the sort's contract in addition to reading, mutating and allocating storage for the receiver. Selecting a callback can have separate effects. The key and reverse options evaluate once, in source order, even when the array is empty; the key itself is then called for each element. Unknown callback effects remain unknown.

Testing

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

Current project tests

Mark a module-level function with $test on the line before it and state what it checks with $expect, as in adds_numbers = () => $expect 20+22 =? 42, then run dewy test file.dewy. A condition the program itself relies on is $assert (decided at compile time) or $runtime_assert (checked when it runs). See the project testing guide. The sections below describe the design, with coverage reported separately.

Design test functions

In the language design, tests are ordinary functions marked $test. The test driver 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

For the current compiler, use the project-test guide. The $test model above specifies test discovery and per-case expectations; its runner behavior is part of the design rather than a promise about the current command. Historical driver details are retained in the archive.

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 design can express a subprocess-based compiler test as follows:

$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("dewy" ["build" source.path "-o" binary.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 further design includes: 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

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

Current compiler and editor

Use dewy build hello.dewy -g -o hello-debug, then debug the executable with a native debugger. The VS Code extension uses CodeLLDB; configure dewy.core.path to the standalone bin/dewy-core or the checkout launcher. See tools and the extension guide.

The following directive describes the language design. Its behavior is not certified by the command above; consult generated coverage.

$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 (a native debugger 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.

Strings and Graphemes

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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 = ():>void => exit(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 = ():>void => {
    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
    exit(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 Missing (the prelude's search exception, neither none nor -1; xs.index_of(x) too); 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 = ():>void => {
    let line:string = "  key: value  ".trim
    match line.find": " {
        i:int64 => printl"key ends at {i}"
        <Missing> => printl"no separator"
    }
    let parts = line.split": "
    exit(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, 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 = ():>void => {
    let letters:array<string> = []
    loop i in [0x41..0x44) { letters.push(chr(i)) }
    exit(letters.join.length)      # "ABC": 3
}

Arrays and Containers

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

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

Equality

xs =? ys compares arrays by value: they are equal when they have the same length and their elements are pairwise =?, recursively through nested arrays, records and unions. Arrays whose static lengths differ are simply unequal. not =? is the negation. Storage is never compared: two arrays built separately with the same elements are equal. An array of dictionaries or sets has no =? yet.

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

Bidirectional dictionaries and dictionary equality remain provisional.

Sets

set[...] constructs a set; set<T> names its type. Members are distinct, and a set remembers first-seen order for iteration and s.values (a fresh array<T>).

let permissions = set["read" "write"]
permissions.push("execute")
let present = "read" in? permissions
let taken = permissions.pop("read")

set"0123" is the set of a string's graphemes and set(values) the set of an array's elements (set(xs) also drops duplicates). s.push(x) inserts a member, using the same operation name as arrays; inserting an existing member preserves its position. x in? s tests membership. s.pop(x) removes a proven member and yields it; s.pop(x default=v) removes x if present and yields it, else v (default=none makes the result T | none). s.clear empties the set; s.length counts members. Sets are not indexable and have no keys.

Set operators produce new sets: |/or union, &/and intersection, - difference, xor symmetric difference. Operands must have the same element type. A set must not be mutated by a loop that iterates it.

Set equality, ordering, and compound operator forms remain provisional.

Arrays, sets, and dictionaries print — and convert to string — as their literal syntax; see Printing.

Loop Capture

An array literal whose only item is a loop collects the values the loop body expresses, in order — one per iteration, or none when the body expresses nothing on that path, so an if without an else filters. Nested loops flatten into the one array.

let main = ():>void => {
    let squares = [loop i in [1..5) i * i]                     # [1 4 9 16]
    let evens = [loop n in [0..10) if n % 2 =? 0 n]            # [0 2 4 6 8]
    let pairs = [loop a in [1..3) loop b in [1..3) a * 10 + b]  # [11 12 21 22]
    exit(squares.length + evens.length + pairs.length)         # 13
}

set[loop …] collects into a set, and a loop whose values are key -> value pairs collects into a dictionary (a later pair with the same key replaces the value, as a store does):

let main = ():>void => {
    let odds = set[loop n in [0..10) if n % 2 =? 1 n]          # set[1 3 5 7 9]
    let lengths = [loop w in ["a" "bb" "ccc"] w -> w.length]   # ["a" -> 1 "bb" -> 2 "ccc" -> 3]
    exit(odds.length + lengths.length)                         # 8
}

The element (or key and value) type is the values' type, or the annotation's (let xs:array<string> = [loop …]); values of different types are an error, as is mixing pairs with plain values. The container is a runtime-length one declared and filled just before the statement that contains the literal, so the loop's break and continue work as usual. A capture must sit in a block body ({ … }), not in an expression-bodied function or a default; a loop whose body is all statements is an error.

Literal Classification

At the top level of []:

• positional values form an array;
• named = fields form an object;
• -> pairs form a dictionary;
• <-> pairs form a bidictionary.

set[...] constructs a set from positional values. Mixed top-level forms must satisfy the rules of the selected container rather than silently switching interpretation element by element.

Structural Objects

Language design. Generated coverage names measured programs and target restrictions; examples here illustrate the design.

An object is a structural value containing named fields in source order. Field names, field types, and order participate in its structural type.

let Pair:type = [left:int64 right:int64]
let pair:Pair = [left=20 right=22]

A type alias names the structure; it does not create a runtime class object or give the structure nominal identity.

Structural Intersections

Intersecting object types combines their field requirements. Unique fields are retained; a field required by both sides receives the intersection of its two types.

const Located:type = [line:int64 column:int64]
const Labeled:type = [label:string]
const LabeledLocation:type = Located & Labeled

# equivalent requirements:
# [line:int64 column:int64 label:string]

Matching fields must have the same mutability. Choosing the stricter-looking declaration would be unsound: code accepting the mutable contract is allowed to write the field, while the const contract prohibits that write. Incompatible field types normalize the containing intersection to never.

Intersection never creates nominal identity. A structurally stronger alias remains the same nominal kind as any nominal component it already contains.

Fields and Mutation

Member access uses .. A mutable object binding permits assignment to its mutable fields. Ordinary object copies remain independent:

let original = [name="draft" saved=false]
let copy = original
copy.saved = true             # original.saved remains false

Nested array and object fields recursively follow the same value rule.

Equality

a =? b compares records by value: field by field with =?, recursively. Records of different branded types are unequal, and a record in a family compares the fields of its own concrete type. As for arrays, storage is never compared.

Immutable Records

const [...] in a type position is an immutable record: a runtime value whose contents never change after it is built. It is not a compile-time value, and it is not the const binding declaration: the binding may still be replaced whole. Nothing writes through such a value — not a field, not a member changed in place (an array's push, a dictionary's store or pop), not a place taken of a field (@info.radix), and not a method of the record that assigns a field (refused where the method is declared). The barrier holds through copies, containers, unions, and function boundaries, because the qualifier is part of the type: const [x:int64] and [x:int64] are different types. A writable record of the same shape may be used where the immutable one is expected (the value is copied there), never the reverse, so a writable contract cannot be handed an immutable value. A copy of a member taken out with let is an ordinary value again. type of any & const [...] mints an immutable nominal type, and a child of an immutable parent is immutable.

What cannot change stays proven, which is what the qualifier is for: a field of an immutable record may relate to an earlier sibling — radix:uint8<radix =? alphabet.length> — and the relation is checked when the record is built (for the default and for an explicit value; a wrong explicit value is refuted) and known wherever the record is read afterwards. A writable record refuses such an invariant: either field could be assigned later.

BaseInfo:type = const [
    alphabet:string<2 <=? length <=? uint8.max>
    case_sensitive:bool
    radix:uint8<radix =? alphabet.length> = alphabet.length     # a sibling invariant, with its default
]
let hex = BaseInfo['0123456789abcdef' false]                   # radix defaults to 16, proven equal to the length
let bin = BaseInfo['01' true 2]                                # an explicit radix is checked the same way
let last_digit = (info:BaseInfo):>string => info.alphabet[info.radix - 1]   # in bounds: radix is the alphabet's length
let main = ():>void => {
    let current:BaseInfo = bin
    current = hex                                              # the binding is replaced whole; its contents never change
    if last_digit(current) =? 'f' and bin.radix =? 2 return
    exit(1)
}

info.radix = 8, info.alphabet = "01", or bump(@info.radix) in last_digit would each be refused as a write through an immutable record; BaseInfo['01' true 3] is refuted at construction.

Constructors

Calling an object type constructs a value of it. The field list is the constructor's signature, read exactly like a function's: positional arguments fill fields in declaration order, keyword arguments name them, and a field declared with a default (name:type = default) may be left out — a default may refer to earlier fields by name.

Other names in a default come from the scope where the type was declared, including that module's namespace imports. Importing the type does not require repeating those imports. Earlier fields use the values supplied to this particular construction; explicit arguments are evaluated in the caller's scope.

let Span:type = [start:int64 stop:int64 = start label:string = "span"]

let a = Span(1 9)                      # positional
let b = Span(stop=5 start=2 label="b") # keywords, in any order
let c = Span(7)                        # stop = start, label = "span"