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

《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安全性且优化决策算法，揭示其支持类型字段删除的能力，为代数子类型语言设计提供更简洁的验证方法。

　　

摘要总结

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

了解更多登录

摘要

摘要

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

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

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

总结

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