We present a compilation framework in which dimensional type annotations persist through multi-stage MLIR lowering, enabling the compiler to jointly resolve numeric representation selection and deterministic memory management as coeffect properties of a single program semantic graph (PSG). Dimensional inference determines value ranges, which in turn determine representation selection, word width, memory footprint, allocation strategy, and cross-target transfer fidelity. The Dimensional Type System (DTS) extends Hindley-Milner unification with constraints drawn from finitely generated abelian groups, yielding inference that is decidable in polynomial time, complete (no annotations required), and principal. Where conventional systems erase dimensional annotations before code generation, DTS carries them as compilation metadata through each lowering stage, making them available where representation and memory placement decisions occur. Deterministic Memory Management (DMM), formalized as a coeffect discipline within the same graph, classifies value lifetimes into four escape categories, each mapping to a verified allocation strategy. The dimensional algebra is closed under the chain rule, and forward-mode gradient computation exhibits a specific coeffect signature that the framework can verify at compile time. The practical consequence is a development environment where escape diagnostics, allocation strategy, representation fidelity, and cache locality estimation are design-time views over the compilation graph.
翻译:我们提出一个编译框架,其中维度类型注解在多层 MLIR 降级过程中持续存在,使得编译器能够将数值表示选择和确定性内存管理作为单一程序语义图(PSG)的共效应属性共同求解。维度推断确定取值范围,进而决定表示选择、字宽、内存占用、分配策略及跨目标传输保真度。维度类型系统(DTS)扩展了 Hindley-Milner 类型推断,增加了由有限生成阿贝尔群导出的约束条件,从而得到多项式时间可判定、完备(无需注解)且具有主类型的推断结果。传统系统在代码生成前会擦除维度注解,而 DTS 将其作为编译元数据携带至每个降级阶段,使其在表示选择和内存放置决策点可用。确定性内存管理(DMM)在同一图中形式化为一种共效应规约,将值生命周期分为四个逃逸类别,每个类别映射至一个经过验证的分配策略。维度代数在链式法则下封闭,前向模式梯度计算表现出框架可在编译时验证的特定共效应签名。实际效果是开发环境中,逃逸诊断、分配策略、表示保真度和缓存局部性估计成为编译图上的设计时视图。