pith. sign in

arxiv: 2606.02854 · v2 · pith:YTTD75C7new · submitted 2026-06-01 · 💻 cs.PL · cs.LO· math.CT

Fixed-Point Scaffolding in the Clef Programming Language

Houston Haynes This is my paper

Pith reviewed 2026-06-28 11:27 UTC · model grok-4.3

classification 💻 cs.PL cs.LOmath.CT
keywords fixed-point combinatorprogram semantic graphcategorical loweringMLIR dialectscompiler verificationcompositionality equationClef languagestructural preservation
0
0 comments X

The pith

A fixed-point combinator in the Clef compiler preserves dimensional, grade, escape and numeric structure from the program semantic graph during categorical lowering to MLIR.

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

The paper shows that the Composer compiler for Clef begins lowering with a fixed-point combinator that carries structural properties intact from the program semantic graph into MLIR. This combinator supports a functor from the compilation poset to a target category that obeys a compositionality equation, supplying both code transformation and verification steps. The construction draws on three algebraic foundations to keep the lowering steps material in MLIR's SSA form, attributes and dialects. If the approach holds, proof terms generated at the start remain usable throughout the pipeline, and new compact-closed negative and fractional types can be added while retaining the same preserved structure. Developers obtain the guarantees as an internal scaffold without direct use of the underlying formalism.

Core claim

The compiler middle end performs lowering via a functor from the compilation poset to a target category subject to the compositionality equation; this functor is realized by a fixed-point combinator that preserves the dimensional, grade, escape, and numeric-representation structure of the program semantic graph, allowing the same primitive to supply continuing proof terms inside MLIR.

What carries the argument

The fixed-point combinator that preserves dimensional, grade, escape and numeric-representation structure from the program semantic graph while enabling a functor from the compilation poset to a target category obeying the compositionality equation.

If this is right

  • Compact-closed negative and fractional types can be introduced while carrying the preserved structure through the same machinery.
  • Proof terms generated by the fixed-point combinator continue to be exercised inside MLIR to verify integrity at each pipeline stage.
  • The abstractions remain internal; developers obtain the guarantees without invoking category theory directly.
  • The same foundation supports dimensional types, groupoid structure, and cellular sheaves as additional algebraic objects.

Where Pith is reading between the lines

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

  • Similar fixed-point scaffolding could be tested in other MLIR-based compilers that already use dialects and attributes.
  • The compositionality equation might be checked by constructing small example programs and inspecting whether structure is identical before and after each lowering pass.
  • Extending the types could be validated by adding one new negative or fractional type and confirming that the fixed-point combinator still produces valid MLIR without structural drift.

Load-bearing premise

The fixed-point combinator preserves the dimensional, grade, escape, and numeric-representation structure from the program semantic graph.

What would settle it

A concrete lowering step in which one of the preserved attributes (dimension, grade, escape, or numeric representation) changes between the program semantic graph and the emitted MLIR dialect.

Figures

Figures reproduced from arXiv: 2606.02854 by Houston Haynes.

Figure 1
Figure 1. Figure 1: Three axes meet at a node. The compilation and verification-strength axes are the [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A compact-closed dual carried as type-level pairing from source to target. The pairing [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
read the original abstract

For fans of Gabriel's "Worse is Better" it may be ironic that C++, by way of MLIR, serves as the scaffold for compiling an ML-family language whose correctness properties are structural. A crucial intersection in our Composer compiler initiates its lowering with a fixed-point combinator that preserves the dimensional, grade, escape, and numeric-representation structure from the Program Semantic Graph. And the MLIR that's witnessed from the PSG is no passive host. Its use of static single assignment, attribute system and dialects carry that structure materially. We show that our compiler middle end uses categorical construction for lowering code with companion verification to that strata: a functor from the compilation poset to a target category, subject to the compositionality equation. The grounding of our approach comes from three sources, each on its own algebraic object: Ohori's machine-code proof theory grounds the compilation axis, parametricity grounds the content at the base, and adjoint mode logic grounds the traversal between our verification tiers. To extend the thesis we introduce compact-closed negative and fractional types, and show the type machinery can be carried with preserved structure and realized through tooling MLIR provides. More broadly, the same fixed-point primitive that preserves types through compilation also supplies proof terms that can continue to be exercised in MLIR to verify its integrity as lowering proceeds through the pipeline. We argue that this foundation is a unique additional point anticipated by our framework that includes dimensional types, Tarau's groupoid, and cellular sheaves. Throughout, the formalism is instrumented as an internal scaffold: the abstractions support the compiler's mechanics, where a developer is never required to reach for category theory in order to rely on the guarantees the compiler provides.

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

3 major / 2 minor

Summary. The paper claims that the Clef compiler's middle end begins lowering via a fixed-point combinator that preserves dimensional, grade, escape, and numeric-representation structure from the Program Semantic Graph into MLIR (via SSA, attributes, and dialects), realizes this lowering as a functor from the compilation poset to a target category obeying a compositionality equation, grounds the construction in Ohori's machine-code proof theory, parametricity, and adjoint mode logic, and extends the framework with compact-closed negative and fractional types while supplying proof terms that remain exercisable in MLIR.

Significance. If the claimed functor, compositionality equation, and structure-preserving properties of the fixed-point combinator were supplied with explicit definitions, derivations, and verification, the work would constitute a distinctive integration of categorical methods into a practical compiler pipeline for an ML-family language, offering structural verification that does not require developers to invoke category theory directly. The grounding in three distinct algebraic sources and the extension to negative/fractional types would add further interest.

major comments (3)
  1. [Abstract] The abstract asserts that 'a functor from the compilation poset to a target category, subject to the compositionality equation' is shown, yet neither the functor nor the equation is defined or verified anywhere in the manuscript; without these objects the central claim that lowering is categorically constructed cannot be assessed.
  2. [Abstract] The fixed-point combinator is stated to preserve the four PSG structures (dimensional, grade, escape, numeric-representation) as the 'starting point of lowering,' but no construction, commuting diagram, or check against the SSA/attribute/dialect encoding is supplied; this preservation is load-bearing for the claim that the functor is structure-preserving.
  3. [Abstract] The extension to 'compact-closed negative and fractional types' is introduced with the claim that 'the type machinery can be carried with preserved structure,' yet no type rules, functor action on these types, or realization via MLIR tooling is exhibited.
minor comments (2)
  1. The manuscript repeatedly refers to 'our framework' and 'the thesis' without a preceding section that defines the overall architecture or lists the three grounding sources in one place.
  2. Notation for the Program Semantic Graph, compilation poset, and target category is introduced only in prose; explicit symbols or a small diagram would improve readability.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the detailed and constructive report. The comments correctly identify that the manuscript asserts several categorical constructions without supplying their explicit definitions, derivations, or verifications. We will revise the paper to include these elements.

read point-by-point responses

  1. Referee: [Abstract] The abstract asserts that 'a functor from the compilation poset to a target category, subject to the compositionality equation' is shown, yet neither the functor nor the equation is defined or verified anywhere in the manuscript; without these objects the central claim that lowering is categorically constructed cannot be assessed.

    Authors: We agree that the functor and compositionality equation are asserted in the abstract and manuscript but not formally defined or verified. In the revision we will supply the explicit definition of the functor from the compilation poset to the target category, state the compositionality equation, and provide its verification together with the relevant diagrams. revision: yes

  2. Referee: [Abstract] The fixed-point combinator is stated to preserve the four PSG structures (dimensional, grade, escape, numeric-representation) as the 'starting point of lowering,' but no construction, commuting diagram, or check against the SSA/attribute/dialect encoding is supplied; this preservation is load-bearing for the claim that the functor is structure-preserving.

    Authors: This observation is accurate. The preservation claim is made without an explicit construction or commuting diagrams. The revised manuscript will include the construction of the fixed-point combinator, commuting diagrams demonstrating preservation of the four structures, and explicit checks against the SSA, attribute, and dialect encodings in MLIR. revision: yes

  3. Referee: [Abstract] The extension to 'compact-closed negative and fractional types' is introduced with the claim that 'the type machinery can be carried with preserved structure,' yet no type rules, functor action on these types, or realization via MLIR tooling is exhibited.

    Authors: We accept the point. The extension is claimed without accompanying type rules, functor action, or MLIR realization details. The revision will add the type rules for the compact-closed negative and fractional types, the functor's action on them, and the concrete realization steps using MLIR tooling. revision: yes

Circularity Check

0 steps flagged

No circularity: derivation chain not visible in provided text

full rationale

The abstract asserts that a fixed-point combinator preserves dimensional/grade/escape/numeric structures from the PSG as the initiator of lowering, and that a functor from the compilation poset to a target category obeys a compositionality equation. However, no equations, diagrams, or explicit derivations are supplied in the visible text. Without any quoted reduction (e.g., an equation shown to equal its input by construction or a fitted parameter renamed as prediction), no load-bearing step can be exhibited as circular per the required criteria. The grounding citations (Ohori, parametricity, adjoint mode logic) are external and not self-referential in the given material. The paper therefore presents an independent claim whose internal consistency cannot be assessed from the supplied content.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on the existence of a structure-preserving fixed-point combinator and a functor satisfying compositionality; these are introduced without independent evidence or external benchmarks in the abstract. Background assumptions include standard category theory and three cited algebraic objects (Ohori proof theory, parametricity, adjoint mode logic).

axioms (2)
  • standard math Category theory axioms for posets, functors, and compositionality
    Invoked when defining the functor from compilation poset to target category.
  • domain assumption Ohori's machine-code proof theory, parametricity, and adjoint mode logic ground the approach
    Cited as the three algebraic sources grounding the compilation axis, content, and verification tiers.
invented entities (1)
  • compact-closed negative and fractional types no independent evidence
    purpose: Extend type machinery while preserving structure through compilation
    New types introduced in the paper and claimed to be realizable via MLIR tooling.

pith-pipeline@v0.9.1-grok · 5831 in / 1567 out tokens · 26469 ms · 2026-06-28T11:27:43.722441+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. Negative and Fractional Types in the Fidelity Framework

    cs.PL 2026-06 unverdicted novelty 2.0

    Applies established negative and fractional type dualities to the authors' existing NTU framework to enable new resolution forms in specialized compute modalities.

Reference graph

Works this paper leans on

34 extracted references · 17 canonical work pages · cited by 1 Pith paper

  1. [1]

    A. W. Appel. SSA is functional programming.ACM SIGPLAN Notices, 33(4):17–20, 1998. DOI: 10.1145/278283.278285

    work page doi:10.1145/278283.278285 1998

  2. [2]

    Ayzenberg, T

    A. Ayzenberg, T. Gebhart, G. Magai, and G. Solomadin. Sheaf theory: from deep geometry to deep learning.arXiv preprint arXiv:2502.15476, 2025

    arXiv 2025

  3. [3]

    Beckmann and A

    A. Beckmann and A. Setzer. Access Hoare logic.arXiv preprint arXiv:2511.01754, 2025

    arXiv 2025

  4. [4]

    S. Bhat, A. Peduri, and T. Grosser. Lambda the ultimate SSA: optimizing func- tional programs in SSA. InProceedings of the 2022 IEEE/ACM International Sym- posium on Code Generation and Optimization (CGO), pages 168–178, 2022. DOI: 10.1109/CGO53902.2022.9741279

    work page doi:10.1109/cgo53902.2022.9741279 2022

  5. [5]

    S. Bhat, A. Keizer, C. Hughes, A. Goens, and T. Grosser. Verifying peephole rewriting in SSA compiler IRs. In15th International Conference on Interactive Theorem Proving (ITP 2024), LIPIcs 309, Article 9. Schloss Dagstuhl, 2024. DOI: 10.4230/LIPIcs.ITP.2024.9

    work page doi:10.4230/lipics.itp.2024.9 2024

  6. [6]

    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

  7. [7]

    M. Fehr, Y. Fan, H. Pompougnac, J. Regehr, and T. Grosser. First-class verification dialects for MLIR.Proceedings of the ACM on Programming Languages, 9(PLDI), Article 206, 2025

    2025

  8. [8]

    Worse is Better

    R. P. Gabriel. Lisp: good news, bad news, how to win big, 1991. Contains the section “Worse is Better”

    1991

  9. [9]

    J.-Y. Girard. Linear logic.Theoretical Computer Science, 50(1):1–101, 1987. DOI: 10.1016/0304-3975(87)90045-4. 14

    work page doi:10.1016/0304-3975(87)90045-4 1987

  10. [10]

    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

  11. [11]

    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

  12. [12]

    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

    Pith/arXiv arXiv 2026

  13. [13]

    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

  14. [14]

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

    Pith/arXiv arXiv 2026

  15. [15]

    H. Haynes. Negative and Fractional Types in the Fidelity Framework.arXiv preprint arXiv:2606.04352, 2026

    Pith/arXiv arXiv 2026

  16. [16]

    G. Huet. The zipper.Journal of Functional Programming, 7(5):549–554, 1997. DOI: 10.1017/S0956796897002864

    work page doi:10.1017/s0956796897002864 1997

  17. [17]

    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

  18. [18]

    R. A. Kelsey. A correspondence between continuation passing style and static single as- signment form. InPapers from the 1995 ACM SIGPLAN Workshop on Intermediate Rep- resentations (IR ’95), pages 13–22. ACM, 1995. DOI: 10.1145/202529.202532

    work page doi:10.1145/202529.202532 1995

  19. [19]

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

    1996

  20. [20]

    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

  21. [21]

    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

  22. [22]

    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

  23. [23]

    Lattner, M

    C. Lattner, M. Amini, U. Bondhugula, A. Cohen, A. Davis, J. Pienaar, R. Rid- dle, T. Shpeisman, N. Vasilache, and O. Zinenko. MLIR: scaling compiler infrastruc- ture for domain-specific computation. InProceedings of the 2021 IEEE/ACM Interna- tional Symposium on Code Generation and Optimization (CGO), pages 2–14, 2021. DOI: 10.1109/CGO51591.2021.9370308

    work page doi:10.1109/cgo51591.2021.9370308 2021

  24. [24]

    Mehta and J

    A. Mehta and J. Hsu. Symmetry Hoare logic.arXiv preprint arXiv:2509.00587, 2025

    arXiv 2025

  25. [25]

    A. Ohori. A proof theory for machine code.ACM Transactions on Programming Lan- guages and Systems, 29(6), Article 36, 2007. Preliminary form, FLOPS 1999. DOI: 10.1145/1286821.1286827. 15

    work page doi:10.1145/1286821.1286827 2007

  26. [26]

    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

  27. [27]

    DOI: 10.1145/3156695.3122965

    work page doi:10.1145/3156695.3122965

  28. [28]

    Petricek, D

    T. Petricek, D. Orchard, and A. Mycroft. Coeffects: a calculus of context-dependent compu- tation. InProceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14), pages 123–135. ACM, 2014. DOI: 10.1145/2628136.2628160

    work page doi:10.1145/2628136.2628160 2014

  29. [29]

    Pfenning

    F. Pfenning. A logical foundation for session-based concurrent computation (adjoint logic), 2015

    2015

  30. [30]

    J. C. Reynolds. Types, abstraction and parametric polymorphism. InInformation Process- ing 83, pages 513–523. North-Holland, 1983

    1983

  31. [31]

    Sarkar, O

    D. Sarkar, O. Waddell, and R. K. Dybvig. A nanopass infrastructure for compiler educa- tion. InProceedings of the 9th ACM SIGPLAN International Conference on Functional Programming (ICFP ’04), pages 201–212. ACM, 2004. DOI: 10.1145/1016850.1016878

    work page doi:10.1145/1016850.1016878 2004

  32. [32]

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

    Pith/arXiv arXiv 2008

  33. [33]

    P. Wadler. Theorems for free! InProceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA ’89), pages 347–

  34. [34]

    DOI: 10.1145/99370.99404

    ACM, 1989. DOI: 10.1145/99370.99404. 16

    work page doi:10.1145/99370.99404 1989