摘要
布尔代数子类型化（Boolean-algebraic subtyping，简称BAS）是一种强大的子类型化方法，于2022年首次提出，它是MLstruct研究语言中实现无回溯主要类型推断的“秘诀”。MLstruct是一种结构化类型的函数式编程语言，支持带标签的记录、标签和记录的子类型化以及基于标签的模式匹配。通过支持分布式的交集、并集、否定和等递归类型，MLstruct能够表达强大的编程模式（如可扩展的变体），而无需使用行变量。然而，由于使用了非传统的子类型化规则（这些规则违反了某些对交集和并集类型的解释），以及这些类型之间的相互分配性，再加上等递归类型的归纳推理复杂性，使得BAS的研究变得相当困难。原始研究中提供的句法正确性证明极其复杂且冗长，掩盖了BAS正确性背后的直觉。
在本文中，我们提炼了布尔代数子类型化的本质：我们发现，BAS可以通过定义在类型上下文中的五类特征布尔同态来理解。其中两类同态映射到更简单对象的幂集；其余的则映射回类型，但需要无保护的归纳假设。这些同态共同使我们能够直接证明BAS是正确的，即它不会关联不兼容的运行时结构的构造函数。这些同态具有“特征性”，因为它们足以捕捉子类型化的含义：我们证明了如果在所有这些同态下两个类型之间存在不等式，那么在原始上下文中这两个类型之间也存在子类型关系。这直接提出了一种新的BAS子类型化决策方法，避免了原始算法中的一些效率问题，尽管其最坏情况时间复杂度仍然是指数级的。我们还证明了即使没有递归类型，子类型化问题实际上也是co-NP难问题。最后，我们发现BAS已经足够强大，可以用来实现从类型中移除字段的功能。这使我们能够通过一个新的术语形式和一条新的类型规则来支持可扩展的记录，但令人惊讶的是，这几乎不需要对子类型化进行任何修改。
我们对BAS语义的新理解为MLstruct类型系统的核心提供了一些新的见解。这种方法也可以适应其他具有代数子类型特性的语言，如Scala 3和Ceylon，使它们的设计和验证变得更加容易。值得注意的是，所有的子类型化正确性证明都包含在本文的正文中，只有少数辅助引理被放在了附录中。
