Negative and Fractional Types

The Native Type Universe is built on an abelian-group algebraic substrate. Kennedy’s units of measure established the pattern: dimensional consistency reduces to unification over a finitely-generated free abelian group, decidable in polynomial time, and it composes with Hindley-Milner inference without sacrificing principal types. NTU generalizes that one pattern across several disciplines, the dimensional algebra, the memory-placement coeffects, the capability coeffects, the BAREWire schema, and the grade discipline of the Program Hypergraph, each a finitely-generated abelian-group structure that rides the same unification machinery.

An abelian group has inverses. That is the property this page is about. Once the substrate carries inverses, two further constructors fall out of the same algebra: the additive inverse, a negative type, and the multiplicative inverse, a fractional type. James and Sabry established these as the two dualities of computation in 2012; Chen and Sabry gave them a categorical interpretation in compact closed categories. The argument here is that NTU is the substrate on which they can be native first-class constructs rather than research artifacts, because the structural commitments their soundness requires are commitments the framework already makes. The full treatment is in the Negative and Fractional Types pre-print; this page is the design orientation.

The two dualities

The duality of computation has been treated under many banners, call-by-value versus call-by-name, value versus continuation, classical versus constructive, often as a single phenomenon. Liskov’s CLU staked out a careful position inside the first of these decades ago, which we acknowledge in retrospect: call-by-sharing, where an argument is a reference passed by value, so mutation is visible to the caller but rebinding is not. James and Sabry’s result is that the duality is, more precisely, two orthogonal phenomena.

The additive duality gives every type 'T a negative type Neg<'T>, with the isomorphism 'T + Neg<'T> ↔ 0. A value of Neg<'T> is an ordinary 'T value flowing in the reverse direction of evaluation. When it enters a computation, the operational reading is that execution reverses to satisfy the demand it represents. This is the type-level account of backtracking.

The multiplicative duality gives every type 'T a fractional type Recip<'T>, with the isomorphism 'T × Recip<'T> ↔ 1. A value of Recip<'T> is a constraint on the surrounding context, a logic variable whose value is fixed by unification at a corresponding site. When it flows through a computation, it carries the demand that some 'T will eventually be supplied. This is the type-level account of constraint propagation.

The orthogonality is the technical claim. Prior work treated continuations as one thing; the two dualities separate at the type level into backtracking (negative) and constraint propagation (fractional), with the type system encoding which discipline governs which value. These are categorical entities, distinct from the operational delimited continuations the framework uses at runtime through the DCont dialect; the decomposition is at the type level and leaves the operational primitives intact.

Why the substrate matters

The literature on negative and fractional types shows a consistent pattern: each construction requires the surrounding language to prevent values from being silently duplicated or erased. Filinski’s declarative continuations impose linearity to prevent duplication; Reddy’s acceptors track acceptance points to prevent erasure; Crolard’s subtractive logic isolates local environments; James and Sabry’s own calculus is built atop a reversible language that enforces information preservation at the level of primitive operations. In every case the negative or fractional value is a first-class entity flowing through computation, and its soundness depends on the language not duplicating or erasing it.

Most general-purpose languages do the opposite. Garbage collection erases values whose references go out of scope; aliased pointers duplicate them; implicit conversions erase precision and dimensional information; unsafe escape hatches bypass the tracking entirely. Implementations of these types in conventional languages have therefore been research artifacts carrying substantial runtime machinery to enforce what the language does not.

The framework’s primary development has gone into exactly those structural commitments. The memory-placement coeffect tracks every allocation and its lifetime, with escape classification preventing values from being silently captured across boundaries, and the flat closure representation makes captured environments structurally explicit. BAREWire extends the same guarantees across process boundaries as zero-copy typed transport. The capability coeffect surfaces an unsupported operation as a design-time error. What these share is information preservation: every value in a Clef program is structurally accounted for at the type level, so duplication would violate the escape classification, erasure would violate the lifetime discipline, and silent transformation would violate the dimensional algebra. That is the property negative and fractional types have always required, supplied here by infrastructure built for other reasons.

What it would look like in Clef

The additive dual would be written Neg<'T> or, in infix notation, -'T. The multiplicative dual would be written Recip<'T> or 1/'T. The duals inherit the appropriate dimensional transformation through Kennedy’s algebra:

// Negative types inherit the dimension of their positive counterpart;
// the reversal is in the direction of evaluation, not the dimension.
type ReverseForce   = Neg<float<N>>      // dimension N, reverse direction
type ReverseCurrent = -float<A>          // dimension A, reverse direction

// Fractional types invert the dimension through the abelian-group inverse.
type Compliance  = Recip<float<N>>       // dimension N⁻¹, a constraint
type Conductance = 1/float<ohm>          // dimension ohm⁻¹, a constraint

The η and ε morphisms that establish the compact closed structure appear as primitive operations, eta_plus introducing a ('T + Neg<'T>) pair and epsilon_plus annihilating it, with multiplicative variants eta_times and epsilon_times for the fractional case. These are not function calls. They are type-level structural transitions that Baker recognizes during elaboration and settles on the Program Semantic Graph as codata, which the middle end later witnesses and elides into the corresponding MLIR constructs, the same mechanism the dimensional and lifetime annotations already use.

Inference would extend the existing HM unification with a direction annotation on each judgment, a forward judgment (e produces a 'T) and a backward judgment (e demands a 'T), dispatching to different operational semantics. A complete program typechecks by producing only forward judgments at its boundary; an unresolved backward judgment or an unsatisfied fractional constraint at program scope is a design-time error. This matches the observability constraint of the source calculus, where complete programs must have positive, non-fractional types at their boundaries.

The cost of the extension is the cost of the additional unification step. The negative constructor introduces the additive inverse element, the fractional constructor the multiplicative inverse, and both preserve the abelian-group structure, with the dimensional algebra extending from integer to rational exponents. Unification at η and ε sites reduces to algebraic identity checking, which the existing engine already performs for dimensional consistency, so the cost remains polynomial.

A worked case: reversible decision support

Consider a clinical decision-support component that maps a patient identifier to a recommended dosage, with the requirement that every lookup be reversible so the audit log can reconstruct the prior state of any decision. The ordinary forward function has type PatientId -> Dosage. A reversible version carries the audit commitment as a type-level structure, with the negative type of the result providing the reversal:

let dosageLookup_reversible
    (patient : PatientId)
    : (Dosage * Neg<PatientId>) =
    let (weight, weight_rev)       = getWeight_reversible patient
    let (condition, condition_rev) = getCondition_reversible patient
    let dosage      = computeDosage weight condition
    let patient_rev = negate(reconstitute(weight_rev, condition_rev))
    (dosage, patient_rev)

The function produces both the forward result and a negative-typed proof object that, annihilated against the result, reproduces the original input. The compiler would verify the reversal information is structurally complete: every piece of state the forward computation depends on has a corresponding piece of reversal information in the negative-typed output, and the verification stays decidable because the dependencies are structurally explicit in the flat closure representation. An audit trail on this discipline replays in reverse as a structural operation, re-running each adjoint and annihilating it against the forward result, recovering the prior state without a stored record of values.

The fractional dual carries a conditioning demand instead. Where the dosage depends on a population prior refined as evidence arrives, Recip<Evidence> records the unsatisfied obligation, and an epsilon_times at the application site satisfies it by unifying the supplied evidence with the demand:

let dosageLookup_bayesian
    (patient : PatientId)
    (prior   : Distribution<Dosage>)
    : (Dosage * Recip<Evidence>) =
    let (proposed, demand_evidence) = eta_times<Evidence>()
    let dosage = sampleFromPosterior prior proposed
    (dosage, demand_evidence)

The two duals compose: a function that must be reversible for audit and conditioning-dependent for refinement carries both annotations, with the η/ε operations for each duality dispatched separately.

Where this sits in the framework

Pair annihilation, the η/ε cancellation, is not new to the framework with these types; it recurs across the architecture. The Program Hypergraph’s grade-annihilation operations (a ∧ a = 0 for a grade-1 element) capture the elimination of paired elements at the hyperedge level, landing on the zero of the geometric algebra. The mode-shift discipline’s round-trip tier coercions collapse back to the source constraint. The negative and fractional constructors would add the same pattern at the type level. Categorically, they promote the framework’s existing symmetric-monoidal PSG semantics to compact closed: every object gains a dual, with η and ε connecting them, along a fourth structural dimension, the duality dimension, parallel to the compilation, joint-constraint, and verification-strength dimensions the hypergraph already carries.

These problem spaces motivate the work. Negative types provide a type-level adjoint for reversible computation and for the unitarity of quantum circuit expression. Fractional types express the conditioning obligations of Bayesian inference as constraint propagation. The combined discipline expresses adiabatic computation, Hamiltonian deformation as a reversible constraint-propagation process. The reversible ThreeBody demonstrator is the watchable instance of the reversibility half.

These are proposed extensions. The framework’s published type universe, the dimensional system, the memory discipline, and the schema verification, is complete and sound within its current scope and does not depend on them. What the extension would add is the structural capacity to express reversible and constraint-propagating computations as type-level disciplines, resolved through the same compilation infrastructure that carries the rest. The depth here is not a requirement the everyday surface imposes; the framework is conceived as a gradient, broadest at ordinary concurrent programming and narrowing to the depth a given domain requires.