Our Native Type Universe (NTU) has been detailed through five previous papers establishing the substrate our framework's compilation pipeline targets across multiple hardware platforms. We have found in the course of that work a deeper reach this foundation makes available: negative and fractional types as native first-class constructs. James and Sabry established these dualities in 2012; Chen and Sabry later developed their categorical interpretation in compact closed categories. These dualities have practical benefit for compute modalities in our Fidelity Framework where extant general purpose compute framings lack the substrate to host them as native constructs. We see practicality with these type forms in preserving decidability and principal types through the abelian-group algebraic pattern Kennedy's dimensional types establish. The resulting isomorphisms would admit new, concise forms of resolution within our novel lowering strategy, and we sketch a notional Clef language syntax that would admit rational dimensional exponents into our algebra. We trace the implications across several problem spaces these type forms would open to our compilation and verification disciplines: Bayesian inference where fractional types would express conditioning obligations, quantum computation (and simulations) where negative types would provide the type-level adjoint, and finally adiabatic computation where the combined discipline would express Hamiltonian deformation as a reversible constraint-propagation process. The inherent structure of our NTU together with the supporting framework appears well-suited to problem spaces that current software ecosystems do not directly address, while keeping approachable development ergonomics and mature tooling aligned with operational guarantees the framework aspires to provide.
翻译:我们的原生类型宇宙(NTU)已通过五篇先前论文得到详细阐述,这些论文奠定了框架编译流水线在多种硬件平台上所针对的基础层。在此过程中,我们发现这一基础层提供了更深层的可达性:将负类型与分类型作为原生一等构造。James与Sabry于2012年确立了这些对偶性;Chen与Sabry随后在紧闭范畴中发展了其范畴论解释。这些对偶性对我们保真度框架中的计算模态具有实际效益,而现有通用计算框架缺乏承载它们作为原生构造的基础层。我们观察到,这些类型形式通过Kennedy量纲类型所建立的阿贝尔群代数模式,在保持可判定性与主类型方面具有实用性。由此产生的同构将允许在我们新颖的下沉策略中实现简洁的新型解析形式,并勾勒出一种设想的Clef语言语法,该语法可将有理量纲指数纳入我们的代数体系。我们追溯了这些类型形式将为我们的编译与验证学科开启的多个问题空间所蕴含的影响:贝叶斯推断中,分类型可表达条件化义务;量子计算(及模拟)中,负类型可提供类型级伴随;最后在绝热计算中,这一联合学科可将哈密顿量形变表达为可逆约束传播过程。我们NTU的固有结构连同支撑框架,似乎非常适合当前软件生态未能直接解决的问题空间,同时保持了可操作的开发人体工程学,并拥有与框架旨在提供的运行保证相一致的成熟工具链。