轻松处理的累积全域：理论与实践
Fuss-free cumulative universes: theory and practice
浏览论文内容
中文总结 AI 辅助
研究依赖类型理论中全域处理难题，提出新的轻松处理广义代数表示，通过归一化定理证明其等价性，给出双向细化算法规范与Haskell实现，还实现了全域层次结构扩展及相关概念导出。
中文摘要 AI 辅助
全域在依赖类型理论中至关重要，但以正确且可用的方式处理却极为困难。我们为多态累积全域提出一种新的‘轻松处理’广义代数表示，摒弃复杂的一致全域强制理论，采用更简单的表述，并通过归一化定理证明其等价性。以双向细化算法的抽象规范和Haskell中的具体实现形式提供了该轻松处理表述实用性的证据。我们还描述并实现了轻松处理全域层次结构的扩展，带有数据类型描述的判断概念，可从中导出先前的累积归纳类型概念。
英文摘要
Universes are central to dependent type theory, and they are notoriously difficult to handle in a way that is both correct and usable. We propose a new "fuss-free" generalised algebraic presentation for polymorphic cumulative universes that dispenses with the intricate theory of coherent universe coercions in favour of a simpler formulation, which we prove equivalent by means of a normalisation theorem for the former. Evidence for the utility of the fuss-free formulation is provided in the form of (1) an abstract specification of its bidirectional elaboration algorithm, and (2) a concrete implementation in Haskell. We also describe and implement an extension of the fuss-free universe hierarchy with a judgemental notion of datatype description from which prior notions of cumulative inductive type may be derived.
