渐进归纳族的近似正规化与Eager相等性检验
Approximate Normalization and Eager Equality Checking for Gradual Inductive Families
摘要：
利用依赖类型语言的能力可能很困难。程序员必须手动构造证明以生成良好类型的程序，这不是一件容易的事情。特别是，将代码迁移到这些语言是具有挑战性的。渐进式类型化通过以一种原则性的方式混合静态和动态检查，可以使依赖类型化语言更容易使用。使用渐变类型，程序员可以逐步将代码迁移到依赖类型的语言。然而，将渐进类型添加到依赖类型会带来新的挑战：在全功能语言中混合可判定类型检查和增量迁移是一种不稳定的平衡。程序员期望类型检查终止，但依赖类型检查器在编译时评估术语，这是有问题的，因为渐进类型可能会将非终止性引入到否则终止的语言中。为缓解这种不终止现象而采取的步骤不得危及动态和静态之间的平稳过渡。我们提出了一种渐进依赖类型语言，它支持归纳类型族，具有可判定的类型检查，并可证明支持静态和动态之间的平滑迁移，正如Siek等人（2015）提出的渐进类型化的细化标准所编码的那样。与Eremondi等人（2019）一样，我们使用近似归一化来终止编译时求值。与Eremondi等人不同，我们的规范化不需要变量的比较，允许我们用容纳归纳类型的语法模型来显示终止。此外，我们设计了一种新的技术跟踪类型索引的约束，使动态约束违反信号运行时的错误急切。为了方便这些检查，我们定义了一个代数概念的渐进精度，公理化的渐进条款的某些语义属性。
英文摘要：
Harnessing the power of dependently typed languages can be difficult. Programmers must manually construct proofs to produce well-typed programs, which is not an easy task. In particular, migrating code to these languages is challenging. Gradual typing can make dependently-typed languages easier to use by mixing static and dynamic checking in a principled way. With gradual types, programmers can incrementally migrate code to a dependently typed language. However, adding gradual types to dependent types creates a new challenge: mixing decidable type-checking and incremental migration in a full-featured language is a precarious balance. Programmers expect type-checking to terminate, but dependent type-checkers evaluate terms at compile time, which is problematic because gradual types can introduce non-termination into an otherwise terminating language. Steps taken to mitigate this non-termination must not jeopardize the smooth transitions between dynamic and static. We present a gradual dependently-typed language that supports inductive type families, has decidable type-checking, and provably supports smooth migration between static and dynamic, as codified by the refined criteria for gradual typing proposed by Siek et al. (2015). Like Eremondi et al. (2019), we use approximate normalization for terminating compile-time evaluation. Unlike Eremondi et al., our normalization does not require comparison of variables, allowing us to show termination with a syntactic model that accommodates inductive types. Moreover, we design a novel a technique for tracking constraints on type indices, so that dynamic constraint violations signal run-time errors eagerly. To facilitate these checks, we define an algebraic notion of gradual precision, axiomatizing certain semantic properties of gradual terms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
