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; value ranges determine representation selection; representation selection determines word width and memory footprint; and memory footprint, combined with escape classification, determines 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, 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, unifies escape analysis and memory placement with the dimensional framework. Escape analysis classifies value lifetimes into four categories (stack-scoped, closure-captured, return-escaping, byref-escaping), each mapping to a verified allocation strategy. We identify implications for auto-differentiation: the dimensional algebra is closed under the chain rule, and forward-mode gradient computation exhibits a coeffect signature that the framework can verify. 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)被形式化为同一图结构中的共效应规则,将逃逸分析与内存布局统一至维度框架中。逃逸分析将值生命周期分类为四种范畴(栈作用域、闭包捕获、返回逃逸、引用逃逸),每类映射至已验证的分配策略。我们阐明了其对自动微分的影响:维度代数在链式法则下封闭,且前向模式梯度计算展现出框架可验证的共效应特征。其实践意义在于构建了一个开发环境,其中逃逸诊断、分配策略、表示保真度与缓存局部性评估均成为编译图上的设计时视图。