Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Arrays and Containers

Arrays

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

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

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

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

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

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

Growth Methods

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

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

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

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

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

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

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

Shapes and Dimensions

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

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

Dictionaries and Bidictionaries

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

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

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

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

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

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

Lookup

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

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

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

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

Mutation

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

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

Views and Combination

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

Representation

A dictionary is a compact hash table: dense entries in insertion order with their stored hashes, plus a sparse probe table using open addressing with CPython's perturbation sequence. Removal leaves a tombstone, iteration and growth compact entries lazily, and none of this is observable beyond the order and complexity guarantees. Keys and values are currently word-sized scalars or strings.

Bidirectional dictionaries and container 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.add("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.add(x) inserts a member. 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. Literal members must currently be constants (duplicates collapse at compile time), and 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 = ():>int64 => {
    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]
    return 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 = ():>int64 => {
    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]
    return 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.