Refinements, Effects, and Safety - Dewy Language Reference

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.

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

array<int64 length=3>

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

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

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

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

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

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

Array Contracts and Dependent Indices

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

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

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

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

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

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

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

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

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

Refined Parameters

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

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

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

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

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

Refined Results and Field Invariants

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

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

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

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

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

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

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

Type Facts

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

A boolean result states its facts per arm:

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

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

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

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

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

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

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

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

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

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

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

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

Prototyping Without the Proofs

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

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

The Length Cap

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

No Traps

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

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.
A value. If a failure is genuinely undecidable at compile time — arithmetic on 64-bit parts that may overflow, tan of an angle whose cosine may be exactly zero, reading a file that may not exist — the operation's type says so: rational | Overflow, fixed | DivisionByZero, T | none, and the caller handles that branch explicitly (is?, or_throw, a default).

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

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

Operation Preconditions

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

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

Assertions

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

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

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

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

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

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

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

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

Effects

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

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

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

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

`unsafe`

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

Provisional Boundary

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

Keyboard shortcuts

Dewy Language Reference