布尔代数子类型的本质：代数并集、交集、否定以及等递归类型的语义正确性

《Proceedings of the ACM on Programming Languages》：The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types

布尔代数子类型（BAS）通过支持递归类型和扩展记录简化了MLstruct语言的设计，但其复杂的子类型规则和证明阻碍了研究。本文通过定义五种布尔同态映射揭示BAS的语义本质，证明其子类型规则正确性，并提出改进的判定算法。研究证实BAS无需额外类型变量即可编码字段移除操作，为类似语言类型系统设计提供新思路。

　　

摘要AI摘要

要查看此由AI生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

布尔代数子类型化（Boolean-algebraic subtyping，简称BAS）是一种强大的子类型化方法，于2022年首次提出。它是MLstruct研究语言中实现无回溯主类型推断的“秘诀”。MLstruct是一种结构化类型的函数式编程语言，支持带标签的记录、标签和记录的子类型化以及基于标签的模式匹配。通过支持分配交集、并集、否定和等递归类型，MLstruct能够表达强大的编程模式（如可扩展的子类型变体），而无需使用行变量。然而，由于使用了非传统的子类型化规则（这些规则违反了某些关于交集和并集类型的解释），以及这些类型之间的相互分配性，再加上等递归类型的共归纳推理的复杂性，使得BAS的研究变得相当困难。原始研究中提供的句法正确性证明极其复杂且冗长，掩盖了BAS正确性背后的直觉。

在本文中，我们提炼了布尔代数子类型化的本质：我们发现，BAS可以通过定义在类型上下文中的五类特征布尔同态来理解。其中两类同态映射到更简单对象的幂集；其余的则映射回类型，但需要在无保护的共归纳假设下进行。这些同态共同使我们能够直接证明BAS是正确的，即它不会关联到不兼容的运行时结构。这些同态具有“特征性”，因为它们足以捕捉子类型化的含义：我们证明了如果在所有这些同态下两个类型之间存在不等式，那么在原始上下文中这两个类型之间也存在子类型关系。这直接提示了一种新的BAS子类型化决策方法，避免了原始算法中的一些效率问题，尽管其最坏情况时间复杂度仍然是指数级的。我们还证明了即使没有递归类型，子类型化问题实际上也是co-NP难的。最后，我们发现BAS已经足够强大，可以用来表示从类型中移除字段的操作。这使我们能够通过一个新的术语形式和一条新的类型规则来支持可扩展的记录，但令人惊讶的是，这几乎不需要对子类型化本身进行任何修改。

我们对BAS语义的新理解为MLstruct类型系统的核心提供了一些新的见解。这种方法可以适应其他具有代数子类型化特性的语言（如Scala 3和Ceylon），使它们的设计和验证变得更加容易。值得注意的是，所有的子类型化正确性证明都包含在本文的正文中，只有少数辅助引理被放在了附录中。

AI摘要

要查看此由AI生成的纯文本摘要，您必须具有高级访问权限。