WIP-0031: Effect-, reversible-, coherent-, and unitary-polymorphic callables

Summary

Wheeler supports generic code over callable behavior while keeping ordinary functions, reversible functions, coherent permutations, unitary operations, measurements, and host effects distinct.

A callable signature records parameter and result types, ownership modes, an effect row, trap contract, callable kind, inverse or adjoint availability, controlled support, capture ownership, and static resource limits. The first callable kinds are:

Function
ReversibleFunction
CoherentFunction
UnitaryOperation

Hybrid and asynchronous work remains normal effectful code built on WIP-0004 lifecycle values. A completed queue item does not make an operation unitary.

Effect variables support bounded row-like propagation. A higher-order wrapper may expose the effects of its argument. It cannot erase those effects or create the capabilities they need.

Before inverse generation or quantum lowering, generic reversible, coherent, and unitary code resolves every WIP-0029 argument, WIP-0030 evidence value, associated constant, callable specialization, and quantum shape. The first coherent and unitary profile has no runtime class or callable dispatch.

Accepted generic transformations obey these laws:

instantiate(inverse(g), arguments)
    == inverse(instantiate(g, arguments))

instantiate(adjoint(u), arguments)
    == adjoint(instantiate(u, arguments))

A name or annotation cannot make code reversible, coherent, or unitary. The body, effects, ownership, finite encoding, and required WIP-0011 evidence must all agree.

Motivation

Wheeler already separates forward calls, generated inverses, VM rewind, coherent lifting, unitary application, generated adjoints, measurement, replay, retry, and host or target effects. Generic code must keep those meanings.

A Java-style Function<A, B> omits moves and borrows, allocation, history, measurement, host effects, inverse or adjoint identity, controlled support, and quantum resource limits. Dynamic trait objects postpone choices that the compiler must settle before verified .wbc, inverse generation, and quantum-region emission.

Duplicating every algorithm for ordinary, reversible, coherent, and unitary calls would also be wasteful. The library needs safe composition, repetition, apply-to-each, effect propagation, caller-owned clean workspace, generic circuits, and adjoint or controlled transformations.

Q# usefully records adjoint and controlled characteristics in operation types. Wheeler needs a wider contract because classical inverse, coherent lifting, VM history, affine ownership, proof evidence, and hybrid effects remain separate.

Representative source

Effect-polymorphic map

public Vec<B> map<A, B, effect E>(
  Vec<A> values,
  Function<A, B, E> transform,
  borrow mut Allocator allocator
) effects E + allocate {
  ...
}

The caller sees both transform effects and allocation. The callable type does not grant an allocator capability.

Reversible values and composition

public ReversibleFunction<A, C> compose<A, B, C>(
  ReversibleFunction<A, B> first,
  ReversibleFunction<B, C> second
) {
  ...
}

public rev void swap<T>(borrow mut T left, borrow mut T right) {
  ...
}

The composed inverse invokes second.inverse and then first.inverse. Generic swap needs disjoint exclusive loans, not Copy.

Coherent and unitary operations

public coherent rev void repeatPermutation<T, F, const long N>(
  borrow mut T value,
  F operation
) where F: CoherentAction<T>
 where N >= 0 {
  ...
}

public unitary void applyEach<Target, Op, const long N>(
  borrow mut Qreg<N> register,
  Op operation
) where Op: UnitaryElementOperation<Target> {
  ...
}

UnitaryOperation<Shape> inverse = adjoint(operation);

All evidence, shape, adjoint, and controlled behavior closes before lowering.

Capturing closure

A closure capturing a move-only owner is move-only. One capturing an exclusive loan cannot outlive the origin. One capturing a must-consume value becomes must-consume. A unitary closure may capture finite immutable classical parameters but not a mutable host capability.

Goals

• Define callable kinds separately from nominal value classes.
• Record ownership, borrows, origins, effects, traps, captures, characteristics, and bounds in signatures.
• Support ordinary higher-order functions and WIP-0028-safe closures.
• Support bounded effect variables, union, subset constraints, and accurate propagation.
• Define reversible callable values with exact inverse evidence and composition.
• Define coherent callable values with finite permutation evidence.
• Define unitary callable values with adjoint and optional controlled evidence.
• Resolve every generic/evidence choice statically before coherent or unitary lowering.
• Preserve inverse/adjoint behavior through WIP-0029 specialization.
• Keep allocation, release, history, measurement, host, target, workflow, and failure explicit.
• Prevent class wrappers or effect variables from masking effects or granting capabilities.
• Bind callable/effect/resource/proof metadata into .wbc and package compatibility.
• Keep runtime dispatch out of first-profile coherent/unitary code.
• Emit bounded diagnostics explaining exactly which characteristic or effect failed.

Non-goals

This WIP does not:

• define one universal callable.
• infer semantic authority from provider behavior.
• permit dynamic dispatch in quantum regions.
• trust named class instances without evidence.
• hide measurement, allocation, target, history, or host effects.
• equate rewind or compensation with an inverse.
• treat cleanup callbacks as inverse evidence.
• admit arbitrary host callbacks in semantic code.
• add unrestricted effect handlers.
• let a Monad erase effects.
• violate capture ownership.
• adjoint measurement.
• reflect on callable characteristics at runtime.
• leave quantum bounds unresolved.
• require heap allocation for every higher-order call.

Callable model

Kinds

A Function performs ordinary forward execution under an effect row.

A ReversibleFunction has a checked language-level inverse relation. It is not WIP-0001 rewind.

A CoherentFunction is a reversible callable whose closed finite behavior is an exact WIP-0002 permutation suitable for coherent lifting.

A UnitaryOperation lowers to a verified backend-neutral quantum region and has an adjoint.

These are semantic callable kinds, not ordinary classes. WIP-0030 classes may constrain values that provide operations, but privileged conversion to a callable kind requires admitted evidence.

Canonical signature

CallableSignature {
    kind
    generic_parameters
    parameter_types_and_modes
    result_types_and_modes
    reversible_result_slot_descriptor
    effect_row
    trap_contract
    capture_mode
    inverse_descriptor
    coherent_descriptor
    adjoint_descriptor
    controlled_descriptor
    resource_bound_descriptor
}

Unused descriptors are absent. WIP-0041 makes reversible_result_slot_descriptor mandatory for a non-void reversible callable and keeps it absent from an ordinary direct-result ABI. The descriptor names the Slot<R> precondition, postcondition, ownership transition, and inverse relation. Callable equality, if exposed, uses declaration and instance identity instead of a code pointer.

Illustrative source may use:

Function<A, B, E>
ReversibleFunction<A, B>
CoherentFunction<A, B>
UnitaryOperation<Shape>

or a future arrow notation. Declarations retain rev, coherent rev, and unitary. WIP-0005/WIP-0006 choose punctuation once semantics and parser ambiguity are settled.

A declaration becomes a callable value only after overload, generic, ownership, effect, and characteristic resolution. Partial application creates a closure. In coherent/unitary code it must be statically eliminated and may capture only permitted finite immutable parameters.

Effects

Sets and rows

An effect set is a canonical finite set of labels. An effect variable ranges over sets under explicit bounds. An effect row is a set expression containing zero or more variables.

The initial namespace includes at least:

allocate    release     history     state       trap
prepare     measure     reset       target      event
file        network     process     clock       random
ffi         blocking    async

target includes submission/materialization, not ownership of credentials or target capability. Exact parameter payloads and effect ownership are frozen with the first executable descriptor profile.

rev, coherent, and unitary are callable characteristics, not effect labels. pure means an empty ordinary effect row. The final trap model is explicit in the separate trap contract. WIP-0002 preparation, measurement, reset, and target boundaries map to these labels.

Propagation

Calling operations forms canonical set union in source evaluation order. For example:

public B apply<A, B, effect E>(
  A value,
  Function<A, B, E> operation
) effects E {
  return operation(value);
}

The body performs no effects outside E. Bounds may require E subset deterministic, exclude measure, or exclude named host effects. Named sets are preferred to arbitrary Boolean effect formulas.

A public callable exposes its complete row. Broadening it may be a compatibility break. A wrapper cannot declare fewer effects than its body. Transforming or handling an effect requires a separately specified checked boundary, not a smaller annotation.

An effect label grants no capability. A file row without a file capability remains unable to open anything, as required.

Ordinary higher-order calls and closures

An ordinary higher-order function may borrow or move a closure. When the closure is structurally Copy, the function may copy it instead. The function may also receive an explicit WIP-0030 strategy or refer to a static declaration. Ordinary classical execution may use a verified closure environment plus callable-table identity. Indirect call targets are exact descriptors, never native addresses.

Capture ownership follows WIP-0028:

• all-copy captures may make a closure Copy.
• an owned move-only capture makes it move-only.
• a borrow capture binds closure lifetime to origin.
• an exclusive capture suspends competing access.
• a must-consume capture makes the closure must-consume.
• closure drop requires every capture to be droppable.
• external resource obligations cannot hide in a droppable environment.

Reversible callables

A ReversibleFunction<A, B> carries forward/inverse identities and a checked relation. Simple value functions have forward: A -> B and inverse: B -> A. Stateful descriptors also record owner/frame pre- and postconditions.

A generic rev body checks under abstract constraints. Every called class method requires certified reversible evidence. Inverse generation before and after monomorphization must agree:

Monomorph(inverse(G), args, evidence)
==
inverse(Monomorph(G, args, evidence))

Composition reverses order:

inverse(second ∘ first) = inverse(first) ∘ inverse(second)

A reversible signature names preconditions and trap exclusions. Arbitrary trapping calls aren't presumed reversible. Legal implementation tools include moves, swaps, loans, clean caller-owned workspace, and certified reversible collections/allocators. It may not discard information, close external resources, or allocate and abandon storage.

Coherent callables

A CoherentFunction<A, B> is a closed exact finite permutation accepted by WIP-0002. Every type has certified cardinality, basis mapping, width, ownership, and validity evidence.

The first profile follows WIP-0017 and accepts exact power-of-two bases with no invalid bit patterns. A later subspace profile may admit non-power-of-two domains only with a complete valid-subspace permutation, leakage behavior, and target or lowering contract. Padding states have no backend-defined fallback semantics.

Allowed operations are coherent primitives, certified static calls, finite control, and clean workspace. Disallowed behavior includes unmodeled allocation/release, history, measurement, host/target effects, clock/random, FFI, admissible-input traps, runtime dispatch, and shared mutable state.

Generic coherent code closes finite encoding, operation evidence, ownership, total basis behavior, and bounds before lowering. Every called class method is exact certified evidence.

Unitary operations

A UnitaryOperation<Shape> ordinarily takes disjoint exclusive quantum loans and returns no classical observation. Immutable classical parameters may configure gates.

Every unitary operation has an adjoint, generated structurally, supplied as a declared specialization, or checked from evidence:

adjoint(adjoint(U)) == U

Generic adjoint generation commutes with monomorphization:

Monomorph(adjoint(G), args, evidence)
==
adjoint(Monomorph(G, args, evidence))

A declared controlled specialization has exact identity and resource contract. When both characteristics exist, accepted evidence establishes:

controlled(adjoint(U))
==
adjoint(controlled(U))

Descriptors bind shape, qubit/ancilla count, clean-ancilla obligations, gate count, depth bound, zero measurement count, and target capability requirements. Generic associated constants and proofs may contribute bounds.

Runtime selection among unitary bodies is excluded inside semantic region IR. Ordinary classical planning may select one concrete operation before circuit construction. The selected identity enters plan and circuit identity.

Generic algorithms include apply-to-each, repeat, compose, conjugation, controlled application, register permutation, QFT, and finite arithmetic oracles. Provider qubit objects and native gate handles remain unavailable to source.

Measurement, workflows, and replay

Measurement is not unitary and cannot hide behind UnitaryOperation. Ordinary/hybrid callables may measure under explicit effects and return provenance-bearing classical results.

WIP-0004 target submission, event recording, polling, acceptance, replay, and retry remain lifecycle operations. Effect variables preserve their labels. Replay-only code rejects a callable row that may perform fresh target, ffi, or other prohibited host effects.

Class evidence and conversion

WIP-0030 may define classes such as:

Callable<F, A, B, E>
ReversibleAction<F, A>
CoherentAction<F, A>
UnitaryAction<F, Shape>
Adjointable<F>
Controllable<F>

Operational instances help typecheck ordinary source. Certified instances reference exact inverse, finite-permutation, adjoint, controlled, effect, and ownership evidence. Names alone grant nothing.

Explicit strategy values enter coherent/unitary code only when statically known, immutable, certified, and erased or monomorphized before region lowering. Runtime-selected evidence cannot change a verified circuit.

The initial profile avoids broad callable subtyping. Safe explicit views may widen an effect allowance, view reversible/coherent as ordinary, or view coherent as reversible. Reverse conversions require evidence. Viewing a unitary as a classical circuit builder is an explicit conversion with builder effects.

Proof and package identity

WIP-0011 propositions may establish inverse round trips, finite permutations, adjoint/controlled laws, effect subsets, frame conditions, clean workspace, bounds, and specialization commutation. Certificates bind generic declaration, closed instantiation, selected evidence, effect row, semantic region, and compiler profile. One monomorph proof does not prove all instantiations without a valid parametric proof.

Public higher-order APIs record callable kind, ownership, effects, traps, generic/class constraints, characteristics, bounds, and evidence. Changes may be package compatibility breaks. Runtime closures are not canonically serializable unless a separate schema admits the exact callable and capture types. Function pointers and addresses never enter package identity.

Reversible IR, bytecode, and native lowering

Callables are typed edges in Wheeler's reversible IR. An ordinary edge declares its forward effects and its inverse, log, or barrier class. A reversible edge binds an exact inverse relation. A coherent edge binds a complete finite permutation, while a unitary edge binds a semantic quantum region and adjoint. Measurement, reset, target work, replay, and compensation remain explicit nonunitary edges. No lowering pass may flatten these into an untyped call and reconstruct semantics from a method name later.

Canonical .wbc callable metadata records kind, ownership, effect row, direct/indirect target descriptor, closure layout, inverse/adjoint/controlled IDs, evidence, bounds, and generic relation. Indirect calls use bounded verified callable tables.

The verifier checks effect compatibility and characteristics at every call. First-profile coherent/unitary bodies contain only direct statically resolved semantic operations. Forged effect rows or characteristic IDs fail before execution.

Native lowering preserves the same descriptors. WIP-0025 foreign callables are ordinary effectful calls unless a separately certified deterministic build-tool profile says otherwise. A native function pointer cannot cast itself into reversibility or unitarity. Embedding APIs export concrete closed callables only.

Determinism, limits, and failures

Callable, row, characteristic, evidence, closure-layout, and specialization identities use canonical encodings. Rows are ordered canonically but semantically set-like. Parallel lowering/proof checking reduces by callable and instantiation identity. Runtime address and hash order are excluded.

Limits cover parameters/results, labels/variables, captures, indirect targets, inverse/adjoint/controlled variants, generic callable instances, proof obligations, resource expressions, diagnostics, memory, and total inference work.

Ambiguous conversion, unresolved variable, masking, invalid capture, missing inverse, incoherent evidence, nonfinite coherent type, invalid adjoint/control, measurement in unitary code, dynamic quantum dispatch, resource overflow, malformed metadata, and limit exhaustion fail before publication. No partial callable table or circuit is emitted.

I/O effects and indexed actions

WIP-0032 operations carry explicit host or target effects and suspension behavior. Higher-order I/O may propagate effect variables, but it cannot erase capability use, cancellation, uncertainty, persistence stages, measurement, or target submission.

An optional IoAction<Effects, Result> or QuantumAction<Input, Output, Effects, Result> is a library and semantic view. Direct request/scope style remains authoritative. Quantum state is not a conventional duplicable state monad, no matter how charming the notation looks on a whiteboard.

Migration and deletion

1. Define canonical effect rows and callable descriptors.
2. Add ordinary function values and WIP-0028-owned closures.
3. Add effect variables and higher-order propagation.
4. Add reversible callable values and composition.
5. Add WIP-0030 certified callable evidence.
6. Add generic inverse/instantiation commutation fixtures.
7. Add coherent callable types and exact finite evidence.
8. Add unitary operation values, adjoint, and controlled characteristics.
9. Add generic shape/operation quantum algorithms.
10. Add proof and resource certificates.
11. Add native lowering and package metadata.
12. Delete duplicate ordinary/reversible/unitary helper families, runtime characteristic strings, dynamic quantum prototypes, and compatibility readers for replaced schemas.

Progress

• [ ] Callable signature and effect-row model is accepted.
• [ ] Ordinary function values and closures execute.
• [ ] Closure ownership follows captures.
• [ ] Effect variables propagate through higher-order functions.
• [ ] Reversible callable values and composition execute.
• [ ] Generic inverse commutation passes.
• [ ] Coherent callable evidence and lowering execute.
• [ ] Unitary operation values and adjoints execute.
• [ ] Controlled specializations execute where supported.
• [ ] Generic adjoint commutation passes.
• [ ] Bounds and proof evidence integrate.
• [ ] Semantic quantum IR contains no dynamic dispatch.
• [ ] Duplicate helper APIs are deleted.

Testing and acceptance

• [ ] Higher-order functions preserve ownership, origins, traps, and effects.
• [ ] Move-only, borrowed, exclusive, and must-consume captures derive the exact closure mode.
• [ ] Effect-polymorphic wrappers cannot hide effects or forge capabilities.
• [ ] An ordinary callable cannot become ReversibleFunction without evidence.
• [ ] Reversible composition uses inverse order and generic inverse commutes with specialization.
• [ ] Intrinsic reversible bodies reject arbitrary allocation/release/foreign/measurement effects.
• [ ] Coherent types require admitted exact finite encoding and complete bijection.
• [ ] Coherent output contains no runtime class/callable dispatch.
• [ ] Unitary bodies contain no measurement or host effect.
• [ ] Double adjoint restores exact semantic region identity.
• [ ] Generic adjoint commutes with specialization.
• [ ] Controlled/adjoint specializations commute where declared.
• [ ] Resource bounds close and pass before target submission.
• [ ] Classical operation selection is recorded in circuit identity.
• [ ] Replay-only generic code rejects fresh target/FFI effects.
• [ ] Forged class evidence cannot grant semantic characteristics.
• [ ] Forged callable/effect metadata fails verification.
• [ ] VM, simulator, native runtime, and proof kernel agree on accepted semantics.
• [ ] Generic quantum examples compile without provider-specific dispatch.

Alternatives

One universal function type or runtime characteristic tests

Rejected. Both erase facts required before verification, inverse generation, resource accounting, and quantum lowering.

Duplicate every algorithm

Rejected. Some APIs remain distinct, but static characteristics permit safe common composition.

Naming conventions for reversibility

Rejected. Inverse availability is a checked relation, not a suffix.

Treat every circuit builder as unitary

Rejected. Builders may allocate, branch, measure, submit, or perform host effects. UnitaryOperation is stricter and carries adjoint evidence.

Copy Q# characteristics unchanged

Rejected as a direct transplant. Adjoint/control are useful. Wheeler also distinguishes classical inverse, coherent lifting, rewind, ownership, proofs, and hybrid effects.

Use Monad as the effect system

Rejected. A library class may compose values, but cannot erase capabilities, measurement, target submission, or replay boundaries.

Dynamic trait objects in quantum regions or tests as proof

Rejected. Static semantic IR and checked universal evidence are required. Tests do not replace either requirement.

Open questions

• Does the trap contract remain wholly separate from rows, or do selected recoverable traps also carry a row label (owner: language and runtime maintainers. Decision point: effect syntax freeze)?
• Which callable type syntax avoids dense punctuation while retaining Java-shaped readability (owner: language and formatter maintainers. Decision point: parser implementation)?
• Is controlled specialization first-profile acceptance or its immediate successor (owner: quantum and compiler maintainers. Decision point: WIP acceptance)?
• Which acceptance fixtures are mandatory: QFT, arithmetic oracle, apply-to-each, phase estimation, or all four (owner: quantum and library maintainers. Decision point: implementation)?
• May ordinary classical code share verified runtime closure/dictionary representations, or are all first-profile calls monomorphized (owner: compiler and native maintainers. Decision point: optimization)?
• Which effect labels are compiler-owned and which may be package-qualified (owner: type-system and capability maintainers. Decision point: public effect APIs)?

Integration with reversible concurrency

Structured-task effects

The initial effect vocabulary adds task and shared. task covers spawn, join, yield, and lifecycle. shared covers WIP-0039 atomics and later synchronization. blocking covers possible suspension. WIP-0032 async remains logical external work and promises no VM task or physical overlap.

A task scope adds no callable kind. An eligible relation remains ReversibleFunction under WIP-0040. Task, shared, blocking, and async effects reject from CoherentFunction and UnitaryOperation. A finite WIP-0015 model may remain coherent only as closed reversible data with no live scheduler.

References

• WIP-0039
• WIP-0040

• WIP-0001
• WIP-0002
• WIP-0004
• WIP-0011
• WIP-0017
• WIP-0021
• WIP-0025
• WIP-0028
• WIP-0029
• WIP-0030
• WIP-0032
• Koka: Programming with Row Polymorphic Effect Types
• Q# functor application
• Q# ApplyToEachCA