Dimensional Type Systems and Deterministic Memory Management: Design-Time Semantic Preservation in Native Compilation
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908995777724416 |
|---|---|
| author | Haynes, Houston |
| author_facet | Haynes, Houston |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_16437 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Dimensional Type Systems and Deterministic Memory Management: Design-Time Semantic Preservation in Native Compilation Haynes, Houston Programming Languages Category Theory Logic 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. |
| title | Dimensional Type Systems and Deterministic Memory Management: Design-Time Semantic Preservation in Native Compilation |
| topic | Programming Languages Category Theory Logic |
| url | https://arxiv.org/abs/2603.16437 |