pith. sign in

arxiv: 2606.04352 · v2 · pith:KM2HVG52new · submitted 2026-06-03 · 💻 cs.PL

Negative and Fractional Types in the Fidelity Framework

Houston Haynes This is my paper

Pith reviewed 2026-06-28 03:39 UTC · model grok-4.3

classification 💻 cs.PL
keywords negative typesfractional typesNative Type UniverseFidelity Frameworkdimensional typesBayesian inferencequantum computationadiabatic computation
0
0 comments X

The pith

Negative and fractional types can serve as native first-class constructs in the Native Type Universe while preserving decidability and principal types.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that negative and fractional types, drawing on earlier dualities, can be integrated directly into the Native Type Universe as first-class elements. This substrate then supports compute modalities in the Fidelity Framework that general-purpose systems cannot host natively. The integration relies on an abelian-group pattern to keep type inference decidable and principal types intact. A reader would care because the approach sketches direct type-level expressions for conditioning, adjoints, and reversible constraints across several domains.

Core claim

Negative and fractional types as native first-class constructs in the NTU provide practical benefit for compute modalities in the Fidelity Framework where extant general purpose compute framings lack the substrate to host them as native constructs, while preserving decidability and principal types. The resulting isomorphisms admit new concise forms of resolution within the lowering strategy, and the paper sketches a notional Clef language syntax that admits rational dimensional exponents into the algebra.

What carries the argument

The Native Type Universe (NTU) together with the abelian-group algebraic pattern that admits negative and fractional dimensional exponents.

If this is right

  • Fractional types directly express conditioning obligations in Bayesian inference.
  • Negative types supply the type-level adjoint required for quantum computation and simulation.
  • The combined forms express Hamiltonian deformation as a reversible constraint-propagation process in adiabatic computation.
  • New isomorphisms yield concise resolution steps inside the existing lowering strategy.
  • A sketched Clef syntax incorporates rational dimensional exponents while retaining mature tooling guarantees.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same algebraic pattern might extend to other reversible or constraint-based domains not listed in the paper.
  • Direct type-level adjoints could simplify verification of quantum circuits beyond simulation.
  • If the syntax proves ergonomic, it could reduce the need for external libraries when encoding dimensional analysis.
  • The connection to compact closed categories suggests the framework could support diagrammatic reasoning in addition to textual syntax.

Load-bearing premise

The structure of the NTU is well-suited to the target problem spaces while maintaining decidability and approachable tooling.

What would settle it

A concrete type-checker implementation that either loses decidability or fails to produce principal types when negative and fractional exponents are added to the algebra.

read the original abstract

Our Native Type Universe (NTU) has been detailed through five previous papers establishing the substrate our framework's compilation pipeline targets across multiple hardware platforms. We have found in the course of that work a deeper reach this foundation makes available: negative and fractional types as native first-class constructs. James and Sabry established these dualities in 2012; Chen and Sabry later developed their categorical interpretation in compact closed categories. These dualities have practical benefit for compute modalities in our Fidelity Framework where extant general purpose compute framings lack the substrate to host them as native constructs. We see practicality with these type forms in preserving decidability and principal types through the abelian-group algebraic pattern Kennedy's dimensional types establish. The resulting isomorphisms would admit new, concise forms of resolution within our novel lowering strategy, and we sketch a notional Clef language syntax that would admit rational dimensional exponents into our algebra. We trace the implications across several problem spaces these type forms would open to our compilation and verification disciplines: Bayesian inference where fractional types would express conditioning obligations, quantum computation (and simulations) where negative types would provide the type-level adjoint, and finally adiabatic computation where the combined discipline would express Hamiltonian deformation as a reversible constraint-propagation process. The inherent structure of our NTU together with the supporting framework appears well-suited to problem spaces that current software ecosystems do not directly address, while keeping approachable development ergonomics and mature tooling aligned with operational guarantees the framework aspires to provide.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper proposes extending the authors' Native Type Universe (NTU), established across five prior papers, with negative and fractional types as first-class native constructs. Drawing on James/Sabry dualities and Chen/Sabry compact-closed interpretations, it claims these enable practical benefits in the Fidelity Framework for domains like Bayesian inference (fractional types for conditioning), quantum computation (negative types for adjoints), and adiabatic computation (combined for Hamiltonian deformation). The central technical assertion is that decidability and principal types are preserved via the abelian-group algebraic pattern of Kennedy's dimensional types; the paper sketches a notional Clef syntax admitting rational exponents and discusses implications for compilation, verification, and development ergonomics.

Significance. If the preservation of decidability and principal types were formally established, the extension could supply a native substrate for type-level constructs in specialized compute modalities that lack support in general-purpose type systems, potentially enabling concise isomorphisms and new resolution strategies within the authors' lowering pipeline.

major comments (2)
  1. [Abstract] Abstract: the manuscript asserts that negative and fractional types 'preserve decidability and principal types through the abelian-group algebraic pattern Kennedy's dimensional types establish' and that the resulting isomorphisms admit 'new, concise forms of resolution,' but supplies neither the updated typing rules for the NTU, the precise abelian-group signature, nor any derivation or sketch showing that unification/inference remains decidable once additive inverses and division (rational exponents) are admitted.
  2. [Abstract] Abstract: the suitability claim for the Fidelity Framework and the 'deeper reach' of the NTU rests entirely on the internal structure defined in the authors' five previous papers, without external benchmarks, independent type-system definitions, or comparison to other approaches that might host negative/fractional types.
minor comments (1)
  1. The manuscript would benefit from explicit section headings, a formal definition of the Clef syntax, and at least a high-level signature for the extended abelian group to make the sketch evaluable.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for identifying areas where additional detail would strengthen the presentation. We respond to each major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the manuscript asserts that negative and fractional types 'preserve decidability and principal types through the abelian-group algebraic pattern Kennedy's dimensional types establish' and that the resulting isomorphisms admit 'new, concise forms of resolution,' but supplies neither the updated typing rules for the NTU, the precise abelian-group signature, nor any derivation or sketch showing that unification/inference remains decidable once additive inverses and division (rational exponents) are admitted.

    Authors: We agree that the manuscript does not supply the requested formal elements. The claim rests on the observation that the type constructors form an abelian group under the operations already present in the NTU (as in Kennedy's dimensional types), which is known to preserve decidable unification. To address the gap we will add a dedicated subsection (or short appendix) that (i) states the updated typing rules for negative and fractional types, (ii) gives the precise abelian-group signature, and (iii) sketches why the existing unification algorithm remains terminating and yields principal types when additive inverses and rational exponents are admitted. revision: yes

  2. Referee: [Abstract] Abstract: the suitability claim for the Fidelity Framework and the 'deeper reach' of the NTU rests entirely on the internal structure defined in the authors' five previous papers, without external benchmarks, independent type-system definitions, or comparison to other approaches that might host negative/fractional types.

    Authors: The Fidelity Framework and the core NTU substrate are defined across the cited prior papers; the present manuscript is an incremental extension that shows how negative and fractional types integrate into that substrate. The suitability argument is therefore internal by design. We can partially accommodate the request by expanding the related-work discussion to note how the same dualities appear in other settings (e.g., compact-closed categories for quantum computation and linear-logic interpretations of conditioning), while keeping the focus on the NTU integration rather than new external benchmarks. revision: partial

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proposal depends on the authors' prior definition of the NTU across five papers and on the cited categorical interpretations; no new free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption The abelian-group algebraic pattern Kennedy's dimensional types establish preserves decidability and principal types when extended to fractional exponents.
    Invoked to justify that the new type forms remain usable in the framework.

pith-pipeline@v0.9.1-grok · 5779 in / 1260 out tokens · 45010 ms · 2026-06-28T03:39:29.412803+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Fixed-Point Scaffolding in the Clef Programming Language

    cs.PL 2026-06 unverdicted novelty 5.0

    Clef compiler applies fixed-point scaffolding and a functor from compilation poset to target category to preserve dimensional, grade, escape and numeric structure through MLIR lowering while adding compact-closed nega...

Reference graph

Works this paper leans on

28 extracted references · 15 canonical work pages · cited by 1 Pith paper

  1. [1]

    Bernardi and M

    R. Bernardi and M. Moortgat. Continuation semantics for the Lambek–Grishin calculus. Information and Computation, 208(5):397–416, 2010. DOI: 10.1016/j.ic.2009.11.005

    work page doi:10.1016/j.ic.2009.11.005 2010

  2. [2]

    Chen and A

    C.-H. Chen and A. Sabry. A computational interpretation of compact closed categories: re- versible programming with negative and fractional types.Proceedings of the ACM on Pro- gramming Languages, 5(POPL), Article 9 (January 2021), 29 pages. DOI: 10.1145/3434290

    work page doi:10.1145/3434290 2021

  3. [3]

    M. Coll. Inet dialect: Declarative rewrite rules for interaction nets. MLIR Open Design Meeting, April 2025. University of Buenos Aires

    2025

  4. [4]

    T. Crolard. Subtractive logic.Theoretical Computer Science, 254(1-2):151–185, 2001. DOI: 10.1016/S0304-3975(99)00124-3

    work page doi:10.1016/s0304-3975(99)00124-3 2001

  5. [5]

    T. Crolard. A formulae-as-types interpretation of subtractive logic.Journal of Logic and Computation, 14(4):529–570, 2004. DOI: 10.1093/logcom/14.4.529

    work page doi:10.1093/logcom/14.4.529 2004

  6. [6]

    Curien and H

    P.-L. Curien and H. Herbelin. The duality of computation. InProceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), pages 233–243. ACM, 2000. DOI: 10.1145/351240.351262

    work page doi:10.1145/351240.351262 2000

  7. [7]

    Damas and R

    L. Damas and R. Milner. Principal type-schemes for functional programs. InProceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’82), pages 207–212. ACM, 1982. DOI: 10.1145/582153.582176

    work page doi:10.1145/582153.582176 1982

  8. [8]

    Filinski

    A. Filinski. Declarative continuations: an investigation of duality in programming language semantics. InCategory Theory and Computer Science, LNCS 389, pages 224–249. Springer- Verlag, 1989. DOI: 10.1007/BFb0018355

    work page doi:10.1007/bfb0018355 1989

  9. [9]

    H. Haynes. Dimensional Type Systems and Deterministic Memory Management: Design- Time Semantic Preservation in Native Compilation.arXiv preprint arXiv:2603.16437, 2026

    Pith/arXiv arXiv 2026

  10. [10]

    H. Haynes. The Program Hypergraph: Multi-Way Relational Structure for Geometric Alge- bra, Spatial Compute, and Physics-Aware Compilation.arXiv preprint arXiv:2603.17627, 2026. 23

    Pith/arXiv arXiv 2026

  11. [11]

    H. Haynes. Adaptive Domain Models: Bayesian Evolution, Warm Rotation, and Principled Training for Geometric and Neuromorphic AI.arXiv preprint arXiv:2603.18104, 2026

    Pith/arXiv arXiv 2026

  12. [12]

    H. Haynes. Decidable By Construction: Design-Time Verification for Trustworthy AI.arXiv preprint arXiv:2603.25414, 2026

    Pith/arXiv arXiv 2026

  13. [13]

    H. Haynes. Fixed-Point Scaffolding in the Clef Programming Language: Our Theoret- ical Grounding for Type-Preserving Compilation and Proof Inference.arXiv preprint arXiv:2606.02854, 2026

    Pith/arXiv arXiv 2026

  14. [14]

    H˘ av˘ arneanu

    A. H˘ av˘ arneanu. Classical SNAX: An adjoint classical logic with uniform mode connectives. X post @aramh, May 10, 2026.https://x.com/aramh/status/2053868427375231352

    arXiv 2026

  15. [15]

    R. P. James and A. Sabry. Information Effects. InProceedings of the 39th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL ’12), pages 73–84. ACM, 2012. DOI: 10.1145/2103656.2103667

    work page doi:10.1145/2103656.2103667 2012

  16. [16]

    R. P. James and A. Sabry. The Two Dualities of Computation: Negative and Fractional Types. Technical Report, Indiana University, March 2012

    2012

  17. [17]

    B. Kang, H. Desai, L. Jia, and B. Lucia. WAMI: Compilation to WebAssembly through MLIR without losing abstraction.arXiv preprint arXiv:2506.16048, 2025

    arXiv 2025

  18. [18]

    A. Kennedy. Programming Languages and Dimensions. Technical Report 391, University of Cambridge Computer Laboratory, 1996

    1996

  19. [19]

    A. Kennedy. Types for Units-of-Measure: Theory and Practice. InCentral European Func- tional Programming School (CEFP 2009), LNCS 6299, pages 268–305. Springer, 2009. DOI: 10.1007/978-3-642-17685-2 8

    work page doi:10.1007/978-3-642-17685-2 2009

  20. [20]

    Y. Lafont. Interaction nets. InProceedings of the 17th ACM SIGPLAN-SIGACT Sympo- sium on Principles of Programming Languages (POPL ’90), pages 95–108. ACM, 1990. DOI: 10.1145/96709.96718

    work page doi:10.1145/96709.96718 1990

  21. [21]

    Y. Lafont. Interaction combinators.Information and Computation, 137(1):69–101, 1997. DOI: 10.1006/inco.1997.2643

    work page doi:10.1006/inco.1997.2643 1997

  22. [22]

    Moortgat

    M. Moortgat. Symmetric categorial grammar.Journal of Philosophical Logic, 38(6):681– 710, 2009. DOI: 10.1007/s10992-009-9118-6

    work page doi:10.1007/s10992-009-9118-6 2009

  23. [23]

    Paykin and S

    J. Paykin and S. Zdancewic. The Linearity Monad. InProceedings of the 10th ACM SIG- PLAN International Symposium on Haskell (Haskell 2017), Oxford, UK, September 7–8,

    2017

  24. [24]

    DOI: 10.1145/3156695.3122965

    work page doi:10.1145/3156695.3122965

  25. [25]

    Phillips and I

    I. Phillips and I. Ulidowski. Reversing Event Structures.New Generation Computing, 36(4):281–306, 2018. DOI: 10.1007/s00354-018-0040-8

    work page doi:10.1007/s00354-018-0040-8 2018

  26. [26]

    U. S. Reddy. Acceptors as values: Functional programming in classical linear logic. Preprint, University of Illinois at Urbana-Champaign, December 1991

    1991

  27. [27]

    D. Syme. The Early History of F#.Proceedings of the ACM on Programming Languages, 4(HOPL), Article 75 (June 2020), 58 pages. DOI: 10.1145/3386325

    work page doi:10.1145/3386325 2020

  28. [28]

    P. Tarau. Isomorphic Data Encodings in Haskell and their Generalization to Hylomor- phisms on Hereditarily Finite Data Types.arXiv preprint arXiv:0808.2953, 2008. 24

    Pith/arXiv arXiv 2008