WIP-0029: Parametric polymorphism, kinds, const generics, and bounded specialization

Summary

Wheeler supports typed generics for functions, records, variants, classes, type aliases, and selected callable, theorem, reversible, and quantum declarations. Generic code is ordinary typed Wheeler code. It is not textual substitution.

Parameters may stand for types, finite compile-time values, regions, shapes, WIP-0031 effects, and type constructors. Declarations state their kinds, ownership limits, finite relations, and WIP-0030 class constraints.

Executable code uses deterministic bounded monomorphization. The compiler starts from selected package roots and finds each reachable closed instantiation. It checks the constraints and gives the instantiation a canonical identity. Then it specializes the body checked at the definition, merges equal identities, and emits concrete verified .wbc types and functions.

Expansion depth, count, type size, proof work, generated bytes, memory, and total work have hard limits. Cyclic expansion fails before publication.

Wheeler does not support C++-style textual templates, SFINAE, overlapping partial specialization, import-order lookup, arbitrary compile-time user programs, or unbounded metaprogramming. The kind model grows in stages:

1. normal type parameters.
2. finite const and shape parameters.
3. first-order constructor parameters.
4. higher-kinded classes under WIP-0030.

Runnable .wbc contains no unresolved generic variable. When canonical non-executable generic IR is added, it will live in a versioned library section of .wbc, not in a separate semantic artifact.

Motivation

The standard library and self-hosted toolchain need types such as:

Slot<T>            Result<T, E>       Array<T, N>
Slice<T>           Vec<T, R>          Map<K, V, R>
Circuit<Shape>     Qreg<N>            Complex<T>
Fixed<Scale, Width>

Without generics, Wheeler would repeat types, algorithms, diagnostics, and proof duties, or rely on host-generated source. Both choices weaken self-hosting.

Generic declarations also make ownership composition visible. For a closed type, the compiler must derive whether it can be copied, dropped, consumed exactly once, borrowed, represented as a finite value, encoded, reversed, or lifted coherently. That result comes from fields, parameters, and accepted evidence.

C++ templates use the wrong model for Wheeler. Bodies may change meaning at each use, substitution failure affects overload selection, partial specializations overlap, lookup depends on distant declarations, and expansion can consume unbounded work. Wheeler needs one definition-site meaning, explicit constraints, finite type-level values, canonical identities, and errors tied to exact instantiation chains.

The first executable strategy is monomorphization. Concrete ownership modes, widths, shapes, effects, and evidence make the VM, verifier, inverse generator, quantum lowering, and native backend easier to check. Runtime type objects and universal boxing would spread the same hard problem into every backend.

Representative source

Algebraic values and identity

public variant Slot<T> {
  case Vacant();
  case Holding(T value);
}

public variant Result<T, E> {
  case Value(T value);
  case Error(E error);
}

public T identity<T>(T value) {
  return value;
}

Ownership derives from payloads. identity moves a move-only value through. Callers may copy a Copy value under WIP-0028.

Const-generic array

public record Matrix<T, const long ROWS, const long COLS>(
  Array<T, ROWS * COLS> elements
)
where ROWS > 0
where COLS > 0
where ROWS * COLS <= MAX_MATRIX_ELEMENTS
{}

Dimensions use WIP-0017's checked constant model and are known before layout or code emission.

Constraints and borrowed values

public boolean contains<T>(
  borrow Slice<T> values,
  borrow T needle
) where T: Eq {
  ...
}

public Vec<T, R> collect<T, region R>(
  borrow Iterator<T> source,
  borrow mut Allocator<R> allocator
) {
  ...
}

WIP-0030 resolves Eq<T>. WIP-0028 owns move/loan/origin behavior. The result region is canonical public metadata even if final surface punctuation changes.

Shapes and constructor kinds

public unitary void reverseBits<const long N>(
  borrow mut Qreg<N> q
) {
  ...
}

public typeclass Functor<F<Type -> Type>> {
  F<B> map<A, B>(F<A> values, Function<A, B> transform);
}

The compiler specializes N before quantum-region emission. WIP-0030 owns Functor instances. This WIP owns the kind and application of F.

Goals

• Add explicit generic declarations for values, functions, methods, aliases, callables, theorems, and accepted quantum forms.
• Support type, finite value, region, shape, effect, and constructor parameters under explicit canonical kinds.
• Reuse WIP-0017 for finite dimensions, widths, capacities, moduli, and resource expressions.
• Infer call-site arguments only when one unique bounded substitution exists. Exported declarations remain explicit.
• Check every generic body once at its definition under abstract constraints.
• Enumerate and monomorphize reachable closed instances in canonical identity order.
• Deduplicate exact equal identities while preserving nominal package-instance distinctions.
• Bound expansion, normalization, proof work, code bytes, diagnostics, memory, and total compiler work.
• Preserve source spans and stable declaration/instantiation backtraces.
• Store public generic bodies as canonical typed library .wbc sections for separate compilation.
• Integrate ownership with WIP-0028, classes with WIP-0030, and callable/effect/reversible/quantum behavior with WIP-0031.
• Keep .wbc, native output, package API identity, documentation, and clean rebuilds canonical.
• Delete generated-source substitutes and duplicated type-specific APIs after replacements pass acceptance.

Non-goals

The first profile excludes:

• textual or AST templates.
• arbitrary compile-time Wheeler execution.
• Turing-complete metaprogramming.
• SFINAE and argument-dependent lookup.
• overlapping partial specialization.
• implicit generalization of arbitrary locals.
• runtime reflection or type objects.
• native-layout inspection and dynamic generic dispatch.
• unbounded recursion.
• identity based on source or import order.
• hidden assumptions that T is copyable or droppable.
• unknown quantum shape during lowering.
• higher-rank or impredicative polymorphism.
• general dependent types.
• the full range of higher-kinded features.

Representation sharing may later optimize verified equal-layout monomorphs. It cannot alter nominal identity, traps, ownership, effects, source maps, native ABI, or semantic artifacts.

Kinds and parameters

A kind classifies a type-level entity. Canonical metadata initially defines:

Type
Nat
Bool
Region
Shape
Effect
Type -> Type
(Type, Type) -> Type
(Nat, Type) -> Type

Constructor kinds may be inferred when public parameter lists determine them. The canonical descriptor remains fully explicit. Kinds are not runtime values. Kind aliases cannot hide infinite recursive constructors.

Examples:

Slot          : Type -> Type
Result        : (Type, Type) -> Type
Array         : (Type, Nat) -> Type
Qreg          : Nat -> Type

Slot<long>         // valid
Slot<4>            // kind error
Array<long, 4>     // valid
Array<4, long>     // kind error
Functor<Slot>      // valid once higher-kinded classes execute

A generic parameter is a type, finite value, region, shape, effect under WIP-0031, or constructor. Higher-rank impredicative values and type-level lambdas remain outside the initial profile.

Constraints and inference

Constraints include:

• WIP-0028 ownership capability and outlives relations.
• WIP-0030 class membership and associated normalization.
• kind equality.
• finite value equality/order.
• shape compatibility.
• WIP-0031 effect subsets.
• explicit WIP-0011 proof propositions where required.

Every exported parameter and constraint appears in the declaration. Wheeler does not silently generalize value = identity into a polymorphic local with hidden allocator, ownership, or effect variables.

Call sites may omit arguments only when parameter types, expected result, finite expressions, and coherent evidence determine one unique substitution. Failure reports the declaration, unresolved parameter, equations, constraints, candidate substitutions, and their source locations.

Generic and nongeneric overload resolution never uses substitution failure to make a candidate vanish. Name, receiver, explicit call form, and arity select a bounded candidate set. Unsatisfied constraints are diagnostics. The first profile may reject overload sets requiring speculative class search.

Const generics

Initial finite values are nonnegative long within declared bounds, Boolean, finite enum members, and later canonical finite shapes.

The type-level expression language is WIP-0017 plus a closed set of total bounded intrinsics required by collections and quantum shapes:

N + 1
ROWS * COLS
powerOfTwoCeil(N)

Overflow, division failure, invalid range, and intrinsic domain failure are compile-time diagnostics. User-defined arbitrary const functions are excluded.

Declarations may state decidable conditions such as:

where N > 0
where ROWS * COLS <= MAX_MATRIX_ELEMENTS
where isPowerOfTwo(cardinality<T>)

Simple normalized relations are compiler-decided. Stronger accepted propositions require WIP-0011 evidence. No runtime value selects a const-generic type or a generated monomorph. Dynamic size remains an ordinary bounded value.

Generic ownership

An unconstrained type parameter passes by value and therefore moves unless its closed type is Copy or the signature borrows it. Generic code cannot assume Drop, equality, encoding, finite representation, or ordinary destruction.

A generic aggregate is Copy only when representation and all fields are Copy. It is droppable only when every live owner is droppable and no must-consume obligation remains. Variants join the properties of every possible payload. User class instances cannot forge those sealed facts.

Borrowed projections preserve canonical owner origin. A collection may return an element loan only when its signature binds the result to the collection input. Quantum types are admitted only when every operation preserves must-consume affinity. Constraints requiring ordinary copy/drop/equality/encoding reject them.

Definition-site checking

The compiler checks a generic body under abstract kinds and declared evidence before examining current calls. It proves:

• each operation follows from structural rules, a declared class constraint, or sealed evidence.
• ownership is valid for every admissible argument.
• no physical layout or address assumption exists.
• effects and traps fit the signature.
• finite expressions are kind-correct and bounded.
• all paths return with valid owner states.
• recursion obeys finite structural rules.
• WIP-0031 reversible/coherent/unitary requirements hold abstractly.

Instantiation then resolves constraints, normalizes associated members, checks concrete bounds/layouts/resource counts, and verifies that specialization introduces no effect or ownership change. A body invalid for abstract affine T stays invalid when the current callers happen to choose long. Call-site frequency does not change the type rule.

Instantiation identity

A closed instantiation substitutes canonical arguments for every parameter. Its identity is:

InstantiationId = hash(
    generic declaration identity,
    ordered canonical type arguments,
    ordered canonical finite arguments,
    region/effect/shape arguments affecting semantics or ABI,
    selected WIP-0030 evidence identities,
    associated reductions,
    compiler profile
)

A generic declaration identity includes exact package instance, module/name, kind schema, public signature, constraints, semantic modifiers, and canonical typed body identity. Non-runtime loan names may normalize only under a fixed verifier-checked rule. Physical addresses and discovery order never participate.

A monomorph is one concrete emitted type or function. Distinct nominal package types never deduplicate because their native layout happens to match.

Deterministic monomorphization

Reachability and worklist

Starting from selected package targets and roots, the compiler discovers concrete uses through fields, calls, callable values, class evidence, proof references, quantum operations, and native export descriptors. Unreachable combinations are not emitted.

Requests enter a worklist sorted by InstantiationId. Source traversal, hash maps, worker scheduling, and repository response order cannot alter output or diagnostics. Equal identities share one body.

Recursion and limits

Self-recursion at the same closed arguments is permitted. Expansion such as:

F<T> -> F<Array<T, 2>> -> F<Array<Array<T, 2>, 2>> -> ...

must prove a finite decreasing measure or fails as an expanding cycle. Polymorphic recursion requires an explicit signature and a statically finite closed instance set.

Limits cover parameters, kind depth, constructor depth, type nodes, const nodes/arithmetic, constraints, class-resolution steps, instance count/depth, generated function/type bytes, proof obligations, memory, diagnostics, and total generic work. Exhaustion reports the chain and emits no partial artifact.

Each monomorph contributes to package/target code-size reports. Parallel specialization reduces in identity order.

Packages and canonical generic IR

The initial source-linked implementation compiles exact reachable modules from the locked package graph. An exported generic API records parameter kinds, constraints, ownership/effects, source-visible signature, required class identities, proof obligations, compiler profile, and canonical body identity. Body changes may affect compatibility even when the header does not.

Binary-library support adds canonical generic typed IR as a required feature section of the library's .wbc 1.0 container. It is typechecked, bounded, verifier-readable, host-class-independent, and non-executable. Its operations already carry Wheeler ownership, effect, trap, reversibility, coherent-eligibility, unitary, and resource semantics. Specialization does not recover those meanings from a host AST. Consumers instantiate it into ordinary closed reversible typed .wbc bodies and quantum regions, then verify those concrete bodies independently. No .wgi, cache blob, source template, or other parallel semantic artifact is introduced.

The section's numeric ID, limits, and exact encoding are frozen before implementation through WIP-0001's extension rules. Package locks bind its body identity. Final consumers own emitted monomorphs unless a library carries an exact prebuilt body matching full package/compiler/profile/evidence identity. Caches are untrusted and reverified.

Transparent aliases normalize before identity. Opaque nominal types retain exact package/declaration identity and expose only declared operations/evidence. All user generic parameters are invariant initially. Compiler-owned borrowed views may support lifetime shortening.

Generic I/O values

WIP-0032 owns generic I/O declarations such as requests, operations, results, and receipt families. This WIP supplies only the kind checking, ownership propagation, definition-site validation, instance identities, specialization bounds, and canonical generic IR needed to compile them.

Specialization cannot duplicate a must-consume operation, shorten a held buffer loan, erase effects, remove cancellation/uncertainty variants, or strengthen receipt evidence. Physical backend type, queue, pointer, and completion order never enter a portable instantiation identity.

Reversible, coherent, quantum, and proof code

WIP-0031 owns detailed callable rules. This WIP requires deterministic specialization and the commutation law:

instantiate(inverse(G), arguments)
==
inverse(instantiate(G, arguments))

for every accepted reversible instance.

Before coherent or unitary lowering, every generic argument, class instance, associated value, and finite shape is concrete. No runtime generic dispatch enters semantic quantum IR. Each circuit instance contributes concrete qubit, ancilla, gate, depth, and step bounds.

Generic theorems quantify over explicit type/finite parameters and constraints. The kernel may check one parametric term, instantiate a certificate, or check concrete certificates. Proof search remains bounded, and absence of a proof is not compile-time branching.

Bytecode, native lowering, and determinism

Executable .wbc contains concrete type/function descriptors. Metadata retains generic declaration identity, arguments, source relation, evidence, and monomorph identity. The verifier checks every concrete body independently and does not trust specialization metadata.

Native lowering consumes verified closed monomorphs. FFI exports are concrete. Source code cannot branch on native layout or pointer identity.

Canonical output fixes parameter/constraint ordering, kind normalization, argument encoding, evidence identity, worklist order, symbol identity, source-map relation, diagnostics, and code-size accounting.

Safety and failures

Unknown kinds, malformed generic metadata, ambiguous arguments, failed constraints, expanding recursion, type-size overflow, const arithmetic failure, ownership/effect mismatch, incoherent evidence, quantum overflow, corrupt prebuilt monomorphs, and work exhaustion all fail before output publication. The compiler never leaves a half-set of monomorphs on disk for the next invocation to misinterpret creatively.

Migration and deletion

1. Add generic parameter/kind syntax, formatter ownership, and Tree-sitter nodes.
2. Add canonical argument/constraint models and definition-site checking.
3. Add generic records, variants, and ordinary functions over ownership-safe types.
4. Add finite const parameters and Array<T, N>.
5. Replace handwritten WIP-0041 Slot, Result, and scalar collection families.
6. Add canonical identities, worklist, limits, and monomorph metadata.
7. Add exact package source-link support.
8. Add WIP-0030 class constraints and WIP-0031 callable semantics.
9. Add generic typed .wbc library sections.
10. Add shape-generic quantum declarations.
11. Add constructor parameters and higher-kinded classes.
12. Delete generated-source substitutes, duplicate scalar APIs, permissive template parsers, and compatibility readers for unreleased schemas.

Progress

• [x] WIP-0041 closed Slot<T> uses one compiler-owned specialization path over canonical variant metadata. General generic declarations remain outside this slice.
• [ ] Kind and generic parameter model is accepted.
• [ ] Generic records and variants execute.
• [ ] Generic ordinary functions execute.
• [ ] Ownership propagation passes WIP-0028.
• [ ] Const generics and Array<T, N> execute.
• [ ] Instantiation identities and limits are canonical.
• [ ] Monomorphization is deterministic and deduplicated.
• [ ] Package source linking supports public generics.
• [ ] Canonical generic typed IR is specified inside .wbc.
• [ ] Class bounds resolve under WIP-0030.
• [ ] Reversible and quantum laws pass WIP-0031.
• [ ] Higher-kinded constructor parameters compile.
• [ ] Duplicated bootstrap/library APIs are deleted.

Testing and acceptance

• [ ] Generic type/function syntax parses, Tree-sitter parses, and formats canonically.
• [ ] Bodies typecheck once under abstract constraints.
• [ ] WIP-0041 Slot<T> and Result<T, E> derive copy, move, drop, and must-consume behavior.
• [ ] Move-only and must-consume values pass through generic identity without copying.
• [ ] Array<T, N> enforces finite dimensions. Overflow and false bounds fail at compile time.
• [ ] Inference finds one result or emits stable ambiguity equations.
• [ ] Substitution failure never silently removes a declaration.
• [ ] Instantiation order ignores source, package, map, and task ordering.
• [ ] Equal identities deduplicate. Distinct nominal package types do not deduplicate by layout.
• [ ] Expanding recursion and all count/depth/type/code/work limits fail before partial output.
• [ ] Public body identity participates in package and build identity.
• [ ] Corrupt prebuilt/cache monomorphs fail verification.
• [ ] Concrete monomorphs pass the ordinary verifier independently.
• [ ] Generic inverse and instantiation commute.
• [ ] Quantum shapes close before coherent/unitary lowering.
• [ ] Native layout and pointers cannot influence generic behavior.
• [ ] Higher-kinded examples produce canonical kind and evidence diagnostics.
• [ ] Self-hosted compiler and standard library use generics without host source generation.

Alternatives

Full C++ templates

Rejected. Textual/AST substitution, SFINAE, ADL, overlap, and arbitrary compile-time execution conflict with typed bounded canonical builds.

Java-style erasure

Rejected as the first executable model. Universal representation, boxing, casts, runtime descriptors, and backend-wide ownership/quantum complexity buy less than they cost. Verified representation sharing remains a later optimization.

Runtime generics or generated source

Rejected. Runtime type objects complicate portable bytecode and quantum lowering. Generated source creates another package identity, diagnostics, and proof pipeline.

Arbitrary compile-time functions

Rejected initially. Checked finite constants and proof terms cover dimensions and laws without opening a second unrestricted runtime in the compiler.

Overlapping specialization or implicit public polymorphism

Rejected. Both obscure API meaning and make resolution dependent on context. Compiler optimizations may specialize without changing selected semantics.

Open questions

• Which final parameter punctuation best preserves Java-shaped source without expression ambiguity (owner: language and tooling maintainers. Decision point: parser implementation)?
• Which closed type-level intrinsics beyond WIP-0017 do the first collections and quantum shapes require (owner: language, library, and quantum maintainers. Decision point: const-generic acceptance)?
• May representation-identical bodies share machine code while retaining distinct symbols and source identity (owner: compiler and native maintainers. Decision point: optimization)?
• Do first-order constructor parameters precede WIP-0030 acceptance or its second milestone (owner: type-system maintainers. Decision point: class-library stabilization)?

Integration with reversible concurrency

Generic task and atomic values

Generic façades may expose Task, JoinHandle, AtomicCell, AtomicRef, and TaskScheduleWitness only after ownership and effects specialize to closed facts.

Atomic element types require sealed evidence for width, representation, equality, arithmetic where present, and canonical encoding. The first extension may expose concrete signed and Boolean forms only.

Task entry, captures, atomic types, effects, transfer facts, and witness bounds close before bytecode emission. Coherent and unitary lowering has no dynamic task dispatch.

References

• WIP-0039
• WIP-0040

• WIP-0001
• WIP-0005
• WIP-0007
• WIP-0011
• WIP-0012
• WIP-0013
• WIP-0017
• WIP-0022
• WIP-0028
• WIP-0030
• WIP-0031
• WIP-0032