内置类型视为归纳家族
摘要：依存类型语言的最新优化通路可以帮助消除富有不变性的数据结构和程序中的冗余信息。尽管可能存在更高效的表示方法，但这些自动化过程并不会显着改变数据的结构。使用量化类型理论，我们演示了如何定义一个富有不变性、在类型检查时打包高效运行时表示以及运行时无关不变性的数据结构。编译器可以在编译过程中积极擦除所有这些不变性。与其他方法不同，我们的表示结果的复杂性可以完全预测，我们不要求两种表示具有相同的结构，但我们能够无缝地进行编程，就像使用高级结构一样。
作者：Guillaume Allais
论文ID：2301.02194
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-01-06