Wheeler

WIP-0012: Wheeler standard library

FieldValue
StatusDraft
OwnersWheeler language, library, compiler, runtime, quantum, proof, package, and documentation maintainers
Created2026-07-17
Updated2026-07-28
AreaStandard library, types, collections, quantum resources, host capabilities
Depends onWIP-0002, WIP-0005, WIP-0007, WIP-0009
SupersedesNone
Superseded byNone

Summary

Wheeler will have a standard library written in Wheeler. It provides the values, collections, text, bytes, arithmetic, reversible operations, quantum resources, hybrid workflows, proofs, capabilities, packages, and test tools needed by applications. The self-hosted compiler, runtime, and package manager use the same library.

The library has three layers. wheeler.core works without heap allocation or host effects. wheeler.alloc adds owned bounded storage. wheeler.std adds capability-scoped host services and higher-level packages.

Quantum modules expose affine logical Qubit and Qreg values, disjoint borrowed views, circuits, parameters, observables, results, and target requirements. They do not expose provider objects or physical qubit pointers.

Every public operation declares its type, ownership, effects, failures, allocation, limits, and reversibility. A method is rev only when its inverse is valid under the stated contract. Coherent lifting requires an exact finite permutation with no hidden allocation, history, measurement, or host effect. Unitary operations keep their semantic regions and adjoints. Logged containers, transactions, compensation, and replay records are never described as intrinsic inverses.

The standard library ships as locked Wheeler packages under WIP-0009. The self-hosted compiler builds it, wheeler doc documents it, and the native recovery graph includes it. Java, JVM collections, provider SDK types, and host serialization are outside the contract.

Motivation

Self-hosting needs more than syntax and bytecode. A compiler needs source text, UTF-8 decoding, byte builders, spans, records, tagged variants, deterministic maps, queues, arenas, diagnostics, paths, and result values. A package manager needs canonical manifests, hashes, graph algorithms, archive readers, capabilities, and atomic output. A proof kernel needs immutable terms, bounded recursion, exact arithmetic, and canonical encodings.

Quantum applications need equally strict types. Treating a qubit as an integer or provider object loses affine ownership, register identity, disjointness, target requirements, and measurement transitions. Using general classical collections for live qubits would allow copies and aliases that Wheeler must reject.

Importing Java's standard library would make Java object identity, exceptions, hash order, Unicode behavior, threads, serialization, and allocation part of Wheeler in practice. Thin wrappers would hide the dependency without removing it. Wheeler needs small, explicit abstractions that its VM and native runtime can implement and its proof system can reason about.

Goals

Non-goals

Package layers

The library graph is acyclic and divided by trust and capability.

wheeler.core

wheeler.core requires no allocator, filesystem, network, clock, randomness, target, or operating-system service. It contains:

The compiler, verifier, native transition kernel, and proof kernel can depend on this layer.

wheeler.alloc

wheeler.alloc depends on core and an explicit allocator capability. It contains:

Allocation failure returns a typed error or declared trap. It never silently invokes a host collector.

wheeler.std

wheeler.std depends on core, selected alloc packages, and explicit host capabilities. It contains:

Importing std grants no capability. Values enter through an application entry point or embedding host.

Fundamental types

Scalars

The standard scalar set includes:

Signed checked arithmetic, unsigned modular arithmetic, and bit-vector arithmetic are distinct APIs. Source operators resolve to a declared model. Coherent lifting never guesses that checked arithmetic means modular arithmetic.

Floating-point APIs specify NaN, infinity, signed zero, rounding, comparison, and conversion behavior. Proof code uses explicit finite, rational, algebraic, interval, or symbolic types when mathematical semantics require them.

Products and variants

Records have named fields and structural value semantics unless declared opaque. Tagged variants are exhaustive and carry bounded payloads. WIP-0041 Slot<T> represents explicit presence without ambient null. Result<T, E> carries ordinary recoverable failure. Done represents successful generic completion without a payload, while void means no value crosses a call boundary.

A variant tag and record layout have canonical .wbc type metadata. Native layout remains derived and cannot change value equality or serialization.

Ownership classes

Types participate in explicit capabilities such as:

WIP-0028 owns affine owners, structural ownership derivation, must-consume values, second-class shared/exclusive loans, deterministic memory-only drop, and bounded regions. WIP-0029 owns generic values and collections. WIP-0030 owns coherent compile-time classes for ordinary protocols plus certified evidence admission. WIP-0031 owns callable kinds and effect rows. External resources close, commit, abort, release, or return explicitly. Drop never becomes a user finalizer. The distinctions remain mandatory, but duplicate trait/interface dialects do not.

Collections

Arrays and slices

Array<T, N> owns exactly N elements. Slice<'a, T> is a shared bounded view. SliceMut<'a, T> is exclusive. Indexing is checked. Iteration order is increasing index.

Splitting a mutable slice proves disjoint ranges. Joining requires matching origin, adjacency, ownership, and lifetime. Quantum register slicing follows related affine rules but does not reuse copyable classical slice semantics blindly.

Vector and deque

Vec<T> and Deque<T> own bounded growable storage. Capacity and allocator are explicit construction inputs or policy defaults recorded in the value's execution context. Growth failure is typed.

Iteration, equality, hashing, encoding, and debug output are deterministic. Spare capacity and native addresses do not affect value identity.

Ordinary insertion and deletion are not automatically rev: allocation, moved values, and overwritten positions matter. Reversible variants require caller-provided clean storage or return enough owned information to run an exact inverse.

Maps and sets

The standard deterministic map provides canonical iteration independent of randomized host hash state. Initial implementations may use insertion order with canonical construction or ordered keys. Any hash table separates lookup hashing from semantic iteration.

Map APIs distinguish:

Set<T> follows the same identity and ordering rules.

Bit vectors and permutations

BitVec<N> and dynamically bounded bit vectors support exact bit operations, rank/count operations, endian conversion, and explicit width. Permutation<N> validates bijection at construction, composes, inverts, and can become a coherent operation when its encoding fits target and resource bounds.

These types drive arithmetic oracles, packet codecs, bytecode flags, proof finite domains, and state-vector basis mappings.

Arenas and regions

Arena owns a bounded region and returns scoped handles. Dropping an arena releases all its storage as one effect. It is not an intrinsic inverse for arbitrary mutations inside the region.

Compiler phases use immutable values or phase-owned arenas so self-hosting does not require a general tracing collector initially. Values that escape a region are copied, moved to a longer-lived owner, or rejected.

The current language substrate has bounded affine regions, fixed-length mutable word and byte buffers, validated UTF-8 owners, and signed maps. Hard byte and object limits apply. Access is checked, drop is explicit, and parameters may use nonescaping immutable UTF-8 borrows, exclusive region allocation borrows, or exclusive mutable word, byte, and map borrows.

Reversible data structures

The library provides reversible structures only where inverse ownership is explicit.

Reversible cell

RevCell<T> supports swap, exchange with a known clean value, and transformations carrying a proved inverse. Direct overwrite either returns the old owned value, records bounded history through an explicit logged type, or is unavailable.

Reversible vector operations

A reversible push consumes an owned element and known spare clean slot. Its inverse pops and returns that same element. A reversible pop returns both value and structural witness needed to invert. Reallocation is excluded unless an explicit allocator transaction and inverse contract cover it.

Reversible map operations

Insertion requires proof or checked evidence that the key is absent and returns an insertion witness. Removal consumes that witness or returns the complete entry and structural information under a representation-independent theorem. Callers cannot infer intrinsic reversal from an implementation's retained node pointer.

Logged and transactional containers

Logged<T> and Transaction<T> own bounded history and expose checkpoint, abort, commit, horizon, and exhaustion. They are effectful library types. Their API uses WIP-0001 and WIP-0004 terminology and never marks a logged overwrite as an intrinsic inverse.

Reversible algorithms

Library algorithms include swap, rotate, reverse, permutation, stable partition with explicit workspace, sorting with a permutation witness, and reversible graph or tree updates where all discarded information has an owner.

Contracts and WIP-0011 certificates state inverse laws, frame conditions, clean workspace, and complexity bounds.

Text and bytes

UTF-8

Utf8 decoding has one specified malformed-sequence policy: strict decoding returns a source-located error. Lossy replacement is a separate named operation. Overlong encodings, surrogates, out-of-range scalars, and truncated sequences are rejected strictly.

String is valid UTF-8. Byte length, scalar count, and grapheme segmentation are distinct operations. Indexing a string by arbitrary integer is unavailable. Callers use bytes, scalar iterators, or explicit text-boundary indices.

Unicode normalization is never ambient. Identifier and package policies invoke a specific versioned normalization/confusable profile. Compiler canonical artifacts record the relevant profile identity.

Bytes and builders

Bytes is immutable owned byte data. ByteSlice is borrowed. ByteVec and ByteWriter are bounded mutable buffers. Endian reads and writes are explicit. Checked offset arithmetic fails before partial mutation.

Canonical encoders write to caller-owned or transaction-owned buffers and publish only after success. Decoder cursors carry source offset and remaining bounds and cannot read host memory outside the slice.

Formatting and parsing

Formatting uses deterministic templates and caller-owned writers. Debug formatting has depth and byte limits. Locale, terminal width, pointer address, and map hash order do not enter canonical output.

Integer and floating parsing specify radix, underscore, exponent, overflow, NaN, infinity, and trailing-input behavior. Source literal parsing and standard-library parsing share tested conversion laws but retain source diagnostics.

Paths and source inputs

Path is an opaque host path available only through a filesystem capability. LogicalPath is a portable normalized package path using /, with no root, drive, traversal, NUL, or host case folding.

Compiler and package APIs accept SourceInput and manifests with logical identities and bytes. They do not open arbitrary paths. The host or package manager converts directory enumeration into a sorted bounded manifest before Wheeler code observes it.

Atomic output is a capability operation taking complete bytes and expected destination identity. Partial temporary files are operational host state, not language values or successful artifacts.

Arithmetic and scientific types

Fixed and modular integers

ModInt<N> and BitInt<N> state width and modulus in the type or value schema. Add, subtract, multiply, compare, and controlled forms have exact finite semantics and can satisfy Coherent when resource lowering exists.

Checked signed integers remain separate and trap or return overflow. Saturating arithmetic is separately named.

Fixed point and rationals

Fixed<Scale, Width> supports reproducible bounded numerical applications such as reversible simulation and cost accounting. Rational uses normalized bounded integers and typed overflow or allocation errors.

These types support exact proof and deterministic cross-runtime behavior where floating point is inappropriate.

Complex values and angles

Complex<T> is a product over an explicit scalar model. Angle carries radians or a canonical turn representation and supports exact named fractions where possible. Quantum gate parameters use Angle or typed symbolic Parameter, not unlabelled provider floats.

Exact quantum proof scalars use a profile accepted by WIP-0011. The simulator may use floating approximations but reports tolerance and cannot mint exact certificates from them.

Linear algebra and observables

Bounded vectors, matrices, sparse Pauli strings, and Hamiltonian sums live outside core in focused packages. Dimensions and index order are explicit. Dense exponential algorithms carry limits and are not pulled into every application.

ExpectationEstimate records value, uncertainty, shot count, estimator, observable identity, and target provenance where applicable.

Quantum resource types

Logical qubits

Qubit<'r> is an affine logical resource borrowed from or moved out of a Qreg. It is not an integer, pointer, provider object, copyable handle, serializable host token, or equality-comparable physical identity.

A qubit can participate in gates, controlled operations, measurement, reset when supported, and scoped disjoint borrows. Its source-level debug representation names logical ownership and source span, not provider coordinates.

Quantum registers

Qreg<N> or a dynamically bounded Qreg owns an ordered logical register. Construction is preparation under explicit target/runtime semantics, not ordinary heap allocation.

Operations include:

Register order defines little-endian outcome encoding unless a typed layout says otherwise. Slices preserve origin and logical index mapping through target lowering.

Ordinary remote Qreg values do not survive a job boundary. Persistent quantum memory requires a target-session type with an advertised capability, lifetime, recovery, and failure contract.

Circuits and operations

Circuit<Shape> is immutable semantic region IR or a typed builder that finalizes into it. It contains semantic gates, coherent calls, controls, parameters, measurement only when the circuit kind permits it, and resource requirements.

Builders reject use-after-measure, overlapping mutable qubit views, dirty ancilla release, unsupported control flow, and unbounded construction. Generated adjoint is available only for unitary circuits.

Unitary<In, Out> identifies a checked unitary region. Adjoint<U> and composition preserve exact semantic identity. Target-native circuits remain derived executable records.

Gates

Standard gates include stable semantic operations such as H, X, Y, Z, S, T, phase, rotations, controlled variants, swap, and selected multi-qubit primitives. The language/compiler may treat the minimal set intrinsically. The library supplies typed constructors, composition, identities, adjoints, matrices for bounded proof/simulation, and resource metadata.

Provider-native gates belong to versioned target extension packages and require explicit target constraints. They do not enter the universal prelude.

Parameters

Parameter<T> has stable declaration and position identity. BindingSet maps a complete parameter schema to canonical finite values. Batch tasks identify schema and bindings independently of provider order.

Parameter expressions are bounded symbolic DAGs with canonical ordering and finite evaluation. Unknown functions or nonfinite bindings fail before submission.

Observables and results

Pauli, PauliString, Observable, ExpectationRequest, SampleRequest, and corresponding result types state register layout and endianness.

Counts, per-shot memory, estimates, uncertainty, and diagnostics are separate bounded products. A result always carries task, target, job, request, and schema identity. Convenience access cannot drop provenance silently.

Hybrid runtime types

The standard hybrid API includes immutable values for:

Adapters implement host-owned target capabilities. The library owns provider-neutral records and validation. Credentials and provider SDK objects remain embedding-host values outside portable Wheeler state.

WIP-0032 owns structured I/O requests, operations, scopes, batches, graphs, selection, cancellation, and completion. The standard API doesn't expose backend polling or require callbacks. Local inline completion follows the same lifecycle as delayed remote work.

Effects and capabilities

Host services are unforgeable affine or scoped capability values:

A package declares required capabilities. An entry point receives granted values. Importing a module, constructing a string, or calling a pure helper grants nothing.

Effects appear in function types and contracts. Reversible and proof contexts restrict them. Capability denial occurs before the host effect and returns a stable typed error.

Errors and diagnostics

Recoverable library failure uses Result. Explicit presence uses WIP-0041 Slot. Invariant violations at verified boundaries may trap with stable codes. Native crashes, provider failures, cancellation, timeout, malformed data, and resource exhaustion remain distinct variants.

Diagnostic contains stable code, severity, primary span, bounded labels, notes, and structured causes. Human rendering is derived. Canonical tests compare structured diagnostics instead of terminal color or host paths.

Error values own no unrestricted provider payload. Attachments are bounded, typed, redacted at ownership boundaries, or content-addressed under policy.

Proof support

wheeler.proof supplies proposition constructors, finite decision procedures, certificate values, resource polynomials, quantum region claims, and kernel interfaces used by WIP-0011 syntax elaboration.

Proof types cannot be constructed through ordinary casts or byte decoding. Certificate decoding invokes the trusted kernel. Experiment evidence has separate types and cannot satisfy exact theorem APIs.

Public library contracts include algebraic laws for equality, ordering, hash compatibility, iteration, encoding, reversible operations, quantum adjoints, ownership, and resource bounds. Critical laws ship with canonical certificates once the proof profile supports them.

Testing support

wheeler.test supplies:

Test randomness is explicit input. Failed property cases report a replayable seed and minimized value under bounded deterministic shrinking.

Concurrency

Collection thread safety is not ambient. Immutable values may be shared according to ownership rules. Mutable sharing requires a structured-concurrency and synchronization contract. No type silently maps to Java monitors or volatile fields.

WIP-0032 asynchronous operations and target/build tasks use deterministic result reduction independent of physical completion order unless the program explicitly selects a race. Required concurrency is distinct from independent work that a conforming backend may complete inline. Operational lanes and queues remain separate from semantic event order.

Canonical encoding

Portable library values use versioned canonical schemas. Encoding fixes field order, variant tags, integer width, endian order, collection order, string validity, duplicate handling, unknown fields, and limits.

Generic native memory dumps, Java serialization, provider JSON, pointer identity, randomized hash order, and object-graph reflection are forbidden as canonical encodings.

CanonicalDecode is total over bounded input: it returns a value or structured error without partial publication. Re-encoding an accepted canonical value produces identical bytes.

Package and version policy

Standard modules are ordinary locked Wheeler packages with reserved wheeler.* namespaces. The compiler may provide intrinsics for performance or primitive semantics, but every intrinsic has the same public contract and conformance tests as its library declaration.

The prelude is small and explicit. It contains scalar types, WIP-0041 Done and Slot, Result, core ownership and effect names, and essential annotations. Collections, I/O, quantum algorithms, targets, proof automation, and package APIs require imports.

Package versions and language profiles track API stability. Public type, effect, ownership, inverse, coherent, resource, encoding, and proof contracts participate in compatibility. A method changing from pure to allocating or from intrinsic to logged is a semantic compatibility change.

Bootstrap graph

The recovery graph builds in layers:

  1. primitive VM and native ABI operations.
  2. wheeler.core.
  3. allocator and arenas.
  4. compiler byte/text/collection substrate.
  5. bytecode codec, verifier, proof kernel, and compiler.
  6. package manager and build planner.
  7. runtime, quantum, hybrid, testing, and documentation packages.
  8. the executable application portfolio.

No lower layer imports a higher layer. A generated dependency graph and package lock enforce the layering.

Stage-0 host implementations exist only during conformance migration. The final library source and tests are Wheeler. Native intrinsics are small ABI or backend operations with explicit contracts, not parallel collection or quantum libraries.

Application fixtures

The standard library is accepted through concrete Wheeler programs:

Unified I/O library

WIP-0032 exclusively owns the portable I/O lifecycle and method registry, including Io, IoScope, Request<T>, Operation<T>, batches, graphs, buffer pools, and receipt types. wheeler.io implements that contract. This WIP does not define a parallel API.

Filesystem and network libraries contribute domain types and adapters over that fabric. Positional operations are primary for addressable storage. Sequential readers and writers are ergonomic cursor views under WIP-0032. The standard library doesn't define a second future, stream, callback, cancellation, or universal flush() durability contract. WIP-0032 owns those semantics.

Migration and deletion

  1. Specify ownership protocols, effect signatures, package layering, and canonical schemas.
  2. Implement scalar, WIP-0041 Done and Slot, Result, fixed array and slice, checked arithmetic, and core encoding support.
  3. Implement arenas, vectors, strings, bytes, deterministic maps/sets, queues, and diagnostics.
  4. Port compiler phases to these Wheeler packages and remove matching Java utility ownership phase by phase.
  5. Implement logical paths, source inputs, hashes, archive types, and package graph support.
  6. Implement affine quantum resources, circuits, parameters, observables, tasks, batches, and results.
  7. Implement hybrid event, persistence, target, and transaction records.
  8. Implement proof and test support and certify critical library laws.
  9. Build and test the full library through native wheeler in the recovery graph.
  10. Delete JVM collection adapters, Java serialization, host path leakage, provider-type wrappers, and duplicate stage-0 library implementations at cutover.

Progress

OwnedReturns.w creates every primitive owner in a factory, uses each one in the caller, and transfers all five to a consuming sink. The bytecode verifier and VM also cover typed owner-result relays. Both paths agree under exact rewind, including the Wheeler-written verifier and interpreter.

Entry code can receive strict UTF-8 or immutable binary byteview input. It can publish a bounded byte-output prefix with checked rewind. Below the library, wheeler.core.encoding.binary provides bounded nonnegative little-endian reads and writes, ASCII identity checks, and eight-byte layout alignment.

crypto/Sha256.w computes provider-free SHA-256 for empty, text, binary, and one- or two-block padding fixtures. It uses checked LOCAL_AND and LOCAL_ROTR32, explicit region scratch, and checked subrange hashing.

The entryless wheeler.core package exports a signed FIFO over an exclusive word-buffer borrow with explicit Full and Empty results. It also exports signed-map operations, four-array and two-slice reductions, and immutable UTF-8 metrics and scalar inspection over nonescaping borrows. WorkQueue.w, LongMap.w, FixedArrays.w, and FrozenUtf8.w use that exact locked archive.

Generic option and result types, library String, normalization, generic maps, sets, queues, iteration, canonical collection encoding, decode errors, and broader package layers remain.

Testing and acceptance

Alternatives

Reuse the Java standard library

Rejected. It keeps Java in the semantic and deployment path and imports incompatible ownership, exception, collection, Unicode, thread, and serialization behavior.

Make every useful type a language intrinsic

Rejected. It bloats the compiler and trusted base, prevents package evolution, and makes independent implementations harder. Intrinsics are limited to primitive operations with library-level contracts.

Treat qubits as integer indices

Rejected. Integers are copyable and lack affine ownership, register origin, disjointness, measurement transition, session lifetime, and target semantics.

Make all containers reversible automatically

Rejected. Overwrite, allocation, growth, deletion, aliasing, and external effects discard information. Reversible APIs require explicit ownership, clean storage, witnesses, history, or transactions.

Use randomized hash maps and sort only during serialization

Rejected as the default semantic collection. Iteration affects diagnostics, compilation, proof terms, lockfiles, and build plans before serialization. Determinism belongs in the API contract.

Put provider SDK wrappers in wheeler.quantum

Rejected. Provider SDKs are adapter implementation details. Portable library values identify semantic tasks, capabilities, jobs, and results.

Open questions

Integration with reversible concurrency

Structured-task library

wheeler.concurrent may expose TaskScope, Task, JoinHandle, AtomicCell, AtomicRef, SchedulePlan, and TaskScheduleWitness over WIP-0039 and WIP-0040.

The first slice may use concrete signed and Boolean atomics. Generic atomics wait for WIP-0029 and sealed AtomicValue evidence.

RevCell remains task-local reversible state. AtomicCell is explicitly shared sequentially consistent state. Mutexes, channels, semaphores, and sessions require later focused work.

References