依赖类型代数层次结构中的多重继承危险
摘要：摘要：抽象代数提供了一组对象可以满足的大量属性，例如形成阿贝尔群或半环。这些分类可以排列成一个广泛且通常呈无环的有向图。这个图的视角在类似Lean的定理证明器的类型类系统中自然地编码，其中节点可以表示为包含所需公理的结构（或记录）。这种设计不可避免地需要某种形式的多重继承；一个环既是半环又是阿贝尔群。 在具有依赖类型的类型类存在的情况下，这些类型类本身作为类型参数消耗，例如假设存在现有可加结构的向量空间类型类，结构多重继承的实现细节就很重要。外部类型类的类型受到解决它所消耗的类型类所经过的路径的影响。除非所有可能的路径在判断上相等，否则这是一个灾难的配方。 本文详细解释了这些情况是如何发生的（从mathlib中的真实例子简化而来），比较了多重继承的实现方法，判断是否保留判断平等，并概述了发现的问题的解决方案（特别是：内核对结构的$eta$-规约的支持）。
作者：Eric Wieser
论文ID：2306.00617
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-24