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.

翻译：对于推崇Gabriel"更糟即更好"理念的开发者而言，颇具讽刺意味的是，C++通过MLIR平台成为编译一个结构正确性属性显著的ML家族语言的脚手架。在Composer编译器中，关键交汇点始于一个定点组合子：该组合子在程序语义图（PSG）降级过程中保持维度、阶次、逃逸及数值表示结构。而作为见证者的MLIR绝非被动宿主——其静态单赋值机制、属性系统及方言体系将上述结构实质化。我们证明编译器中间端通过范畴论构造实现代码降级，并附带对应层级的验证：即从编译偏序集到目标范畴的函子，满足组合性方程。该方法的基础源于三个代数对象：Ohori的机器码证明理论奠基编译轴线，参数化范式奠基基层内容，伴随模态逻辑则贯通验证层级间的遍历。为扩展该理论，我们引入紧闭负类型与分数类型，并展示类型机制可通过MLIR工具链保持结构且可实例化。更广泛而言，贯穿编译过程保持类型的定点原语，同样能提供证明项，这些证明项可在MLIR中持续运作，以验证降级流水线各阶段的完整性。我们认为该基础框架预见了包含维度类型、Tarau群胚及细胞层状结构的独特扩展点。整个形式系统作为内部脚手架实现：抽象层支撑编译器运作机制，开发者无需理解范畴论即可依赖编译器提供的保障。