MLstruct-在结构类型的布尔代数中进行主类型推断

MLstruct-在结构类型的布尔代数中进行主类型推断

MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types*

LIONEL PARREAUX, HKUST, Hong Kong, China, CHUN YIN CHAU, HKUST, Hong Kong, China

Intersection and union types are becoming more popular by the day, entering the mainstream in programming languages like TypeScript and Scala 3. Yet, no language so far has managed to combine these powerful types with principal polymorphic type inference. We present a solution to this problem in MLstruct, a language with subtyped records, equirecursive types, first-class unions and intersections, class-instance matching, and ML-style principal type inference. While MLstruct is mostly structurally typed, it contains a healthy sprinkle of nominality for classes, which gives it desirable semantics, enabling the expression of a powerful form of extensible variants that does not need row variables. Technically, we define the constructs of our language using conjunction, disjunction, and negation connectives, making sure they form a Boolean algebra, and we show that the addition of a few nonstandard subtyping rules gives us enough structure to derive a sound and complete type inference algorithm. With this work, we hope to foster the development of better type inference for present and future programming languages with expressive subtyping systems.

交集类型与并集类型正日益受到人们的重视，它们已经进入了TypeScript和Scala 3等编程语言的主流体系。然而，迄今为止还没有任何一种编程语言能够将这些强大的类型机制与多态类型推断功能完美地结合起来。我们在MLstruct这种支持子类型记录、“等递归类型”、“一等并集与交集类型”、“类实例匹配机制”以及**“基于ML风格的强类型推断系统”的语言中，为这一问题提供了一套解决方案。虽然MLstruct主要采用结构化类型系统，但它也为类类型引入了一些命名性特征，这些特性使得该语言具备理想的语义模型，从而能够实现一种无需使用“行变量”即可表达的、功能强大的可扩展变体机制。从技术角度来看，我们是通过使用连接词“与”、“或”以及“非”来定义这种语言中的各种类型构造，确保它们能够构成一个布尔代数系统；同时我们也证明了，通过添加一些非标准的子类型规则，就可以构建出足够完善的类型推断框架，从而实现可靠且完备的类型推断功能。我们希望通过这项工作，为那些具备强大子类型系统的现有及未来的编程语言的发展带来助力。

Additional Key Words and Phrases: principal type inference, union and intersection types, structural typing

其他相关关键词：主要类型推导、并集类型与交集类型、结构化类型系统

1 INTRODUCTION

1 引言

Programming languages with ML-style type inference have traditionally avoided subtyping because of the complexities it brings over a simple unification-based treatment of type constraints. But Dolan and Mycroft [2017] recently showed with MLsub that an algebraic account of subtyping resolved many of these difficulties and enabled the inference of precise types that more accurately reflect the flow of expressions in programs. Unfortunately, among other limitations, MLsub does not support union and intersection types, which are emerging as important building blocks in the design of structurally-typed programming languages like TypeScript, Flow, Scala 3, and others.

那些具备机器学习风格类型推导功能的编程语言，传统上都会避免使用子类型机制，因为这种机制会使得处理类型约束的工作变得更为复杂，而相比之下，基于统一规则的处理方式要简单得多。但是Dolan和Mycroft在2017年发表的论文中通过MLsub证明了：如果从代数角度来理解子类型机制，许多这类问题就能得到解决，并且这样还能推导出更加精确的类型信息，这些类型信息能更准确地反映程序中各种表达式的执行流程。然而遗憾的是，MLsub目前还存在一些局限性，例如它不支持并集型和交集型这两种类型，而这两种类型恰恰是设计像TypeScript、Flow、Scala 3这类具有结构化类型的编程语言时所必需的重要元素。

We close this gap with MLstruct, showing that MLsub-style type inference can be generalized to include well-behaved forms of union and intersection types as well as pattern matching on single-inheritance class hierarchies. As a first example, consider the following definitions:

我们通过 MLstruct 来弥补这一空白，从而证明了 基于 MLsub 风格的类型推导机制 可以被推广应用，以便涵盖那些表现良好的并集类型、交集类型，以及针对单继承类层次结构进行的模式匹配操作。作为一个最初的例子，让我们来看以下这些定义：

class Some[A]: { value: A }
class None: {}

def flatMap f opt = case opt of
    Some  -> f opt.value,
    None  -> None{}

The type inferred by our system for flatMap is:

我们的系统推断出 flatMap 的类型是：

\[ flatMap : \forall \alpha, \beta. (\alpha \to \beta) \to (\text{Some}[\alpha] \lor \text{None}) \to (\beta \lor \text{None}) \]

Interestingly, this is more general than the traditional type given to flatMap for Option types. Indeed, our flatMap does not require the function passed in argument to return either a None or a Some value, but allows it to return anything it wants (any β), which gets merged with the None value returned by the other branch (yielding type β ∨ None). For example,

有趣的是，这种用法比传统上为 Option 类型提供的 flatMap 方法更为通用。实际上，我们的 flatMap 并不要求作为参数传入的函数必须返回 None 或 Some 值，而是允许它返回任何它想返回的值（即任何 β 类型的值）；这些返回值会与另一分支返回的 None 值合并，最终得到类型为 β ∨ None 的结果。例如……

let res = flatMap (fun x → x) (Some{value = 42})

is given type 42 ∨ None¹ because the function may return either 42 or None. A value of this type can later be inspected with an instance match expression of the form:

其类型被指定为42 ∨ None²，因为该函数可能返回42或None中的任意一个值。后来可以通过如下形式的实例匹配表达式来检查这种类型的值：

case res of Int → res, None → 0

which is inferred to be of type 42 ∨ 0, a subtype of Nat. This is not the most general version of flatMap either. We can also make the function open-ended, accepting either a Some value or anything else, instead of just Some or None, by using a default case (denoted by the underscore ‘_’):

可以推断，该函数的类型为 42 ∨ 0，属于 Nat 的一个子类型。不过，这也不是 flatMap 函数的最通用形式。我们还可以通过使用默认值处理机制（用下划线 “_” 表示），使该函数具有更强的灵活性——它既可以接受 Some 类型的值，也可以接受其他任何类型的值，而不仅仅限于 Some 或 None 这两种情况。

def flatMap2 f opt = case opt of Some → f opt.value, _ → opt

This flatMap2 version has the following type inferred, where ∨ and ∧ have the usual precedence:

这个flatMap2版本具有以下类型推断结果，其中∨和∧遵循它们通常所具有的优先级规则：

\[ flatMap2 : \forall \alpha, \beta. (\alpha \to \beta) \to (\text{Some}[\alpha] \lor \beta \land \neg \#\text{Some}) \to \beta \]

This type demonstrates a central aspect of our approach: the use of negation types (also called complement types), written ¬τ, which allows us to find principal type solutions in tricky typing situations. Here, type #Some is the nominal tag of class Some. A nominal tag represents the identity of a class, disregarding the values of its fields and type parameters: if a value v has type #Some, this means v is an instance of Some, while if v has type ¬#Some, this means it is not. To showcase different usages of this definition, consider the following calls along with their inferred types:³

这种类型体现了我们方法的一个核心特点：即使用否定类型（也被称为补码类型），其表示方式为¬τ。这种机制使我们能够在一些复杂的类型判定情况下找到合适的解决方案。在这里，类型#Some代表类Some的命名标签；命名标签用于表示一个类的“身份”，而忽略该类中各个字段及类型参数的具体值——如果某个值v具有类型#Some，那么说明v是类Some的一个实例；反之，如果v的类型为¬#Some，那就意味着它不是Some类的实例。为了进一步说明这一定义的不同应用方式，让我们来看以下这些调用示例及其被推导出的类型结果：⁴

ex1 = flatMap2 (fun x → x + 1) 42 : Int
ex2 = flatMap2 (fun x → Some{value = x}) (Some{value = 12}) : Some[12]
ex3 = flatMap2 (fun x → Some{value = x}) 42 : Some[⊥] ∨ 42

It is easy to see that instantiating β to Int and Some[12] respectively allows ex1 and ex2 to type check. In ex3, both types Some[γ] and 42 flow into the result, for some type inference variable γ, but γ is never constrained and only occurs positively so it can be simplified, yielding Some[⊥] ∨ 42. We can convert ex3 to 42 through a case expression using the impossible helper function:⁵

显而易见，将 β 分别实例化为 Int 和 Some[12]，就能够使 ex1 和 ex2 通过类型检查。在 ex3 中，对于某个类型推断变量 γ 来说，Some[γ] 和 42 这两种类型都会被赋值给结果，但由于 γ 没有任何约束条件，它的取值只能是肯定的，因此这个表达式可以简化为 Some[⊥] ∨ 42。我们可以利用 impossible 辅助函数，通过 case 表达式将 ex3 转换为 42。⁶

def impossible x = case x of {} : ⊥ → ⊥
case ex3 of Int → ex3, Some → impossible ex3.value : 42

One may naively think that the following type could fit flatMap2 as well:

人们可能会天真地认为，以下这种类型也适用于 flatMap2。

\[ \text{flatMap2\_wrong} : \forall \alpha, \beta, \gamma. (\alpha \to \beta) \to (\text{Some}[\alpha] \lor \gamma) \to (\beta \lor \gamma) \]

but this type does not work. To see why, consider what happens if we instantiate the type variables to α = Int, β = Int, and γ = Some[Bool]. This yields the type:

但是这种类型是行不通的。要理解其中的原因，我们可以设想这样一种情况：如果我们将类型变量分别设置为 α = Int、β = Int 和 γ = Some[Bool]，那么会得到这样的类型：

flatMap2_wrong' : (Int → Int) → (Some[Int] ∨ Some[Bool]) → (Int ∨ Some[Bool])

which would allow the call flatMap2 (fun x → x + 1) (Some{value = false}) because Some[Bool] ≤ Some[Int] ∨ Some[Bool]. This expression, however, would crash with a runtime type mismatch! Indeed, the shape of the Some argument matches the first branch of flatMap2’s case expression, and therefore false is passed to our argument function, which tries to add 1 to it as though it was an integer... So we do need the negation that appears in the correct type of flatMap2, as it prevents passing in arguments that are also of the Some shape, but with the wrong type arguments.

这样就可以调用 flatMap2 (fun x → x + 1) (Some{value = false})，因为 Some[Bool] ≤ Some[Int] ∨ Some[Bool]。然而，这个表达式在运行时会因为类型不匹配而导致程序崩溃！
事实上，Some 类型的参数确实符合 flatMap2 的条件表达式的第一个分支的要求，因此，false会被传递给我们的参数处理函数，而该函数会尝试将1加到这个值上，仿佛它是一个整数一样……所以，我们确实需要flatMap2所提供的那种类型转换功能，因为这种功能能够防止那些具有Some结构但类型不正确的数据被传递进来。

Finally, let us push the generality of our function further yet, to demonstrate the flexibility of the system. Consider this last twist on flatMap for optional values, which we will call mapSome:

最后，让我们进一步拓展我们这个函数的通用性，以此来展现该系统的灵活性。请考虑这种针对可选值的flatMap变体实现方式，我们将它称为mapSome。

def mapSome f opt = case opt of Some → f opt, _ → opt

The difference with the previous function is that this one does not unwrap the Some value received in argument, but simply passes it unchanged to its function argument. Its inferred type is:

与之前的函数不同，这个函数并不会解开作为参数传递进来的 Some 值的结构，而是直接将其原样传递给函数的参数。它的推断类型为：

\[mapSome : \forall \alpha, \beta. (\alpha \to \beta) \to (\alpha \land \#Some \lor \beta \land \neg \#Some) \to \beta\]

This type shows that it does not matter what specific subtype of Some we have in the first branch: as long as the argument has type α when it is a Some instance, then α is the type the argument function should take, without loss of generality. This demonstrates that our type system can tease apart different flows of values based on the nominal identities of individual matched classes.

这种类型说明：无论第一个分支中使用的Some的具体子类型是什么，只要当某个参数是Some实例时它的类型为α，那么函数就应该接受类型为α的参数——这样做并不会丧失任何普遍性。这一现象证明了我们的类型系统能够根据各个匹配类之间的名义身份差异，来区分不同的值流。

As an example of the additional flexibility afforded by this new function, consider the following:

作为这一新功能所带来的额外灵活性的一个例证，请考虑以下情况：

class SomeAnd[A, P]: Some[A] ∧ { payload: P }
let arg = if <arbitrary condition> then SomeAnd{value = 42, payload = 23}
    else None{}
in mapSome (fun x → x.value + x_payload) arg

of inferred type Int ∨ None. Here, we define a new subclass of Some containing an additional payload field, and we use this class instead of Some, allowing the payload field to be used from within the function argument we pass to mapSome. This is not expressible in OCaml polymorphic variants [Garrigue 2001] and related systems [Ohori 1995]. More powerful systems with row variables [Pottier 2003; Rémy 1994] would still fail here because of their use of unification: mapSome merges its opt parameter with the result, so these systems would yield a unification error at the mapSome call site, because the argument function returns an integer instead of a value of the same type as the input: subtyping makes MLstruct more flexible than existing systems based on row variable.

其类型为Int ∨ None。在这里，我们定义了Some的一个新子类，该子类增加了一个payload字段；我们在使用mapSome函数时，会使用这个新子类而非原来的Some类型，这样就可以在传递给mapSome的函数参数中访问payload字段了。在OCaml的多态机制[Garrigue 2001]及相关系统中，这种设计是无法实现的。即便是那些具备行变量功能的更强大的系统[Pottier 2003; Rémy 1994]，也会因为这些系统使用了“统一化”机制而无法实现这一功能：mapSome函数会将其opt参数与函数执行的结果进行合并，因此当传递给mapSome的函数返回的是整数而非与输入类型相同的值时，这些系统就会在调用mapSome的地方出现错误。由此可见，子类型机制使得MLstruct比那些基于行变量的系统更加灵活。

MLscript is a new programming language developed at the Hong Kong University of Science and Technology⁷ featuring first-class unions, intersections, negations, and ML-style type inference, among other features. For simplicity, this paper focuses on a core subset of MLscript referred to as MLstruct, containing only the features relevant to principal type inference in a Boolean algebra of structural types, used in all examples above. An MLstruct implementation is provided as an artifact [Parreaux et al. 2022] and available at github.com/hkust-taco/mlstruct, with a web demonstration at hkust-taco.github.io/mlstruct. The specific contributions we make are the following:

MLscript是一种由香港科技大学开发的新编程语言，它具备了一流的数据类型操作功能（如并集、交集、否定运算等），同时还支持基于ML风格的类型推导机制。为便于说明，本文重点介绍MLscript中的一个核心子集——即被命名为“MLstruct”的部分。该子集仅包含那些与结构类型布尔代数中的类型推导机制直接相关的功能，上述所有示例中均使用了这一子集。关于MLstruct的实现细节，Parreaux等人曾在2022年发表了相关论文，该实现代码可在github.com/hkust-taco/mlstruct网站上获取，同时也有相应的在线演示界面，地址为hkust-taco.github.io/mlstruct。我们在此具体贡献的内容如下：

• We present MLstruct (Section 2), which subsumes both the original ML type system and the newer MLsub [Dolan 2017], extending the latter with simple class hierarchies and class-instance matching based on union, intersection, and negation type connectives.

• We describe our approach to type inference based on the Boolean-algebraic properties of MLstruct's types (Section 3). To the best of our knowledge, MLstruct is the first language to support principal polymorphic type inference with union and intersection types. Moreover, it does not rely on backtracking and yields types that are amenable to simplification.

• We formalize the declarative semantics of MLstruct in the \(\lambda^-\) calculus (Section 4), making sure to establish the Boolean-algebraic properties of its subtyping lattice (Section 4.4.3). We state the standard soundness properties of progress and preservation, whose complete proofs are given in the extended version of this paper [Parreaux and Chau 2022].

• 我们介绍了MLstruct（第2节），该语言既包含了原有的ML类型系统，也融入了较新的MLsub[Dolan 2017]框架；通过引入简单的类层次结构以及基于并集、交集和否定类型运算符的类实例匹配机制，MLstruct进一步拓展了MLsub的功能。*
  

• 第3节中，我们阐述了基于MLstruct类型的布尔代数性质进行类型推导的方法。据我们所知，MLstruct是第一种支持使用并集和交集类型进行多态类型推导的语言；此外，这种推导机制不依赖回溯算法，且能够生成便于进一步简化的类型表达式。*
  

• 第4节我们用\(\lambda^-\)演算形式化了MLstruct的声明性语义，并明确了其子类型结构的布尔代数性质（第4.4.3节）。我们还阐述了进展性与保持性这两种标准性质，其完整证明详见本文的扩展版本[Parreaux and Chau 2022]。

• We formally describe our type inference algorithm (Section 5). We state its soundness and completeness theorems. Again, the proofs can be found in the paper's extended version.

• 我们在第5节中正式描述了我们的类型推导算法，并证明了其“正确性”与“完备性”定理。这些证明的详细内容同样可以在论文的扩展版本中找到。

2 PRESENTATION OF MLSTRUCT

2 MLSTRUCT的介绍

MLstruct subsumes Dolan's MLsub, the previous state of the art in type inference with subtyping, which itself subsumes traditional ML typing: all ML terms are typeable in MLsub and all MLsub terms are typeable in MLstruct. We now present the features and subtyping discipline of MLstruct.

MLstruct实际上包含了Dolan提出的MLsub技术——后者在当时已是类型推导领域的先进技术，而MLsub本身又涵盖了传统的ML类型系统：所有在MLsub中能够被赋予类型的ML术语，在MLstruct中也同样可以被赋予类型；反过来，所有在MLstruct中能够被赋予类型的术语，也都属于MLsub的范畴。现在，我们就来介绍MLstruct的具体特点及其所采用的子类型系统机制。

2.1 Overview of MLscript Features

2.1 MLscript功能概述

An MLstruct program is made of top-level statements followed by an expression, the program's body. A statements can be either a type declaration (class or type alias) or a top-level function definition, written def f = t or rec def f = t when f is recursive. MLstruct infers polymorphic types for def bindings, allowing them to be used at different type instantiations in the program.

一个MLstruct程序由顶层语句以及紧跟其后的表达式组成，这些表达式构成了程序的主体。顶层语句既可以是一条类型声明（用于定义类或类型别名），也可以是一个顶层函数定义；当函数f是递归函数时，其定义形式应为def f = t或rec def f = t。MLstruct会为这样的函数定义自动推导出多态类型，从而使这些函数能够在程序中被用于不同类型的实例化操作中。

2.1.1 Polymorphism. Polymorphic types include a set of type variables with bounds, such as \(\forall (\alpha \le \text{Int})\). \(\text{List}[\alpha] \to \text{List}[\alpha]\). The bounds of polymorphic types are allowed to be cyclic, which can be interpreted as indirectly describing recursive types. For example, \(\forall (\alpha \le \top \to \alpha)\). \(\alpha\) is the principal type scheme of rec def f = fun a \to f which accepts any argument and returns itself.

2.1.1 多态性。多态类型包含一组带有约束条件的类型变量，例如 \(\forall (\alpha \le \text{Int})\)、\(\text{List}[\alpha] \to \text{List}[\alpha]\)。多态类型的这些约束条件可以是循环的，这种结构可以被理解为一种间接描述递归类型的方式。例如，\(\forall (\alpha \le \top \to \alpha)\)；在这里，\(\alpha\) 就是定义 rec def f = fun a \to f 这一递归函数时的主要类型模式——该函数可以接受任何类型的参数，并且会返回自身。

2.1.2 Classes, Inheritance, and Type Aliases. Because object orientation is not the topic of this paper, which focuses on functional-style use cases, the basic OO constructs of MLstruct presented here are intentionally bare-bone. Classes are declared with the following syntax:

2.1.2 类、继承与类型别名。由于本文的重点是函数式编程风格的应用场景，而非面向对象编程本身，因此这里介绍的MLstruct中的基本面向对象构造被刻意简化为最基础的形式。类的声明采用以下语法：

class C[A, B, ...]: D[S, T, ...] ^ { x: X, y: Y, ... }

where A, B, etc. are type parameters, S, T, X, Y, etc. are arbitrary types and D is the parent class of C, which can be left out if the class has no parents. Along with a type constructor \(C[A, B, ...]\), such a declaration also introduces a data constructor C of type:

其中，A、B等代表类型参数；S、T、X、Y等代表任意类型的变量；D则是C的父类——如果某个类没有父类，那么这一字段可以省略不写。除了类型构造函数\(C[A, B, ...]\)之外，这样的声明还会引入一个数据构造函数C，其类型为……

\[C: \forall \beta_1, \beta_2, \dots, (\alpha_1 \le \tau_1), (\alpha_2 \le \tau_2), \dots \{x_1: \alpha_1, x_2: \alpha_2, \dots\} \to C[\beta_1, \beta_2, \dots] \wedge \{x_1: \alpha_1, x_2: \alpha_2, \dots\}\]

where \(x_i\) are all the fields declared by \(C[\beta_1, \beta_2, ...]\) or by any of its ancestors in the inheritance hierarchy, and \(\tau_i\) are the corresponding types – if a field is declared in several classes of the hierarchy, we take the intersection of all the declared types for that field. To retain as precise typing as possible, we let the types of the fields taken in parameters to be arbitrary subtypes \(\alpha_i\) of the declared \(\tau_i\), so we can refine the result type \(C[\beta_1, \beta_2, ...] \wedge \{x_1: \alpha_1, x_2: \alpha_2, ...\}\) to retain these precise types. For instance, assuming class C: { x: Int }, term \(C \{ x = 1 \}\) is given the precise type \(C \wedge \{ x: 1 \}\).

其中，\(x_i\)表示由\(C[\beta_1, \beta_2, ...]\)或其继承层次结构中任何父类所声明的所有字段，而\(\tau_i\)则表示这些字段对应的类型；如果某个字段在层次结构中的多个类中被声明过，那么我们就取所有这些声明中该字段类型的交集作为其最终类型。为了尽可能保持类型的精确性，我们允许那些作为参数被使用的字段类型成为声明的类型\(\tau_i\)的任意子类型 \(\alpha_i\)，这样我们就可以对结果类型\(C[\beta_1, \beta_2, ...] \wedge \{x_1: \alpha_1, x_2: \alpha_2, ...\}\)进行优化，从而保留这些精确的类型。例如，假设class C: { x: Int }，那么表达式\(C \{ x = 1 \}\)的精确类型就是\(C \wedge \{ x: 1 \}\)。

Classes are restricted to single-inheritance hierarchies. Like in the work of Muehlboeck and Tate [2018], this has the nice property that it allows union types to be refined by reducing types like \((C_0 \lor \tau) \land C_1\) to \(C_0 \land C_1 \lor \tau \land C_1\) by distributivity and to just \(\tau \land C_1\) when \(C_0\) and \(C_1\) are unrelated \((C_0 \land C_1 \equiv \perp)\). But MLstruct can easily be extended to support traits, which are not subject to this restriction, by slightly adapting the definition of type normal forms (our artifact [Parreaux et al. 2022] implements this). Thanks to their use of negation types (described in Section 4.3), the typing rules for pattern matching do not even have to change, and traits can also be pattern-matched.

这些规则仅适用于单继承层次结构。正如Muehlboeck和Tate在[2018]年的研究中指出的，这种限制具有一个显著的优势：它使得可以通过运用分配律将诸如\((C_0 \lor \tau) \land C_1\)这样的类型简化为\(C_0 \land C_1 \lor \tau \land C_1\)；而当\(C_0\)与\(C_1\)互不相关（即\(C_0 \land C_1 \equiv \perp\)）时，这类类型甚至可以进一步简化为\(\tau \land C_1\)。不过，通过略微调整类型规范形式的定义，MLstruct也可以轻松地支持那些不受这种限制的特征结构——我们的研究[Parreaux等人，2022年]实际上就已经实现了这一功能。由于这些系统使用了否定类型（其具体概念在第4.3节中有详细说明），因此模式匹配的类型规则甚至无需进行任何调整，特征结构也同样可以被用来进行模式匹配操作。

2.1.3 Shadowing. Non-recursive defs use shadowing semantics,⁸ so they can simulate the more traditional field initialization and overriding semantics of traditional class constructors. For instance:

2.1.3 阴影覆盖机制。非递归形式的def语句会使用阴影覆盖机制，⁹因此它们能够模拟传统类构造函数中那种更为传统的字段初始化机制以及方法重写机制。例如：

class Person: {name: Str, age: Nat, isMajor: Bool}
def Person n a = Person{name = capitalize n, age = a, isMajor = a >= 18}

in which the def, of inferred type Person₁: \(\forall (\alpha \le \text{Nat})\). Str \(\to \alpha \to\) Person \(\wedge \{\text{age} : \alpha\}\), shadows the bare constructor of the Person class (of type Person₀: \(\forall (\alpha \le \text{Str})\), \((\beta \le \text{Nat})\), \((\gamma \le\)

在这个例子中，def语句的推导类型为Person₁：\(\forall (\alpha \le \text{Nat})\)。表达式Str → α → Person ∧ {age : α}实际上“覆盖”了Person类的原始构造函数（其类型为Person₀：\(\forall (\alpha \le \text{Str}), (\beta \le \text{Nat}), (\gamma \le …\)）。

Bool). `{ name : α, age : β, isMajor : γ } → Person ∧ { name : α, age : β, isMajor : γ }), forcing users of the class to go through it as the official Person constructor. Function capitalize returns a Str, so no ‘name’ refinement is needed (Person ∧ { age : α, name : Str } ≡ Person ∧ { age : α }).

布尔值类型。{ name: α, age: β, isMajor: γ } → Person ∧ { name: α, age: β, isMajor: γ }，这一规定强制要求该类的使用者必须通过这种方式来创建Person对象，因为这才是官方规定的构造方式。函数capitalize会返回一个Str类型的值，因此无需对name字段进行进一步的处理（即Person ∧ { age: α, name: Str } ≡ Person ∧ { age: α }）。

2.1.4 Nominality. Classes are not equivalent to their bodies. Indeed, they include a notion of “nominal identity”, which means that while a class type is a subtype of its body, it is not a supertype of it. So unlike TypeScript, it is not possible to use a record { x = 1 } as an instance of a class declared as class C: { x: Int}. To obtain a C, one must use its constructor, as in C{x = 1}. This nominality property is a central part of our type system and is much demanded by users in practice.¹⁰ It comes at no loss of generality, as type synonyms can be used if nominality is not wanted.

2.1.4 名义性。类别与其所代表的具体实例并不等同。事实上，类型系统中存在着“名义身份”的概念：也就是说，虽然某种类型是其对应实例的子类型，但它本身却不是该实例的超类型。因此，与TypeScript不同，在TypeScript中可以使用{ x = 1 }这种记录形式来作为声明为class C: { x: Int }的类的实例；而在TypeScript的基础上，却无法这样做。要想创建C类型的对象，就必须使用其构造函数，例如通过C{x = 1}这种方式来创建对象。这种名义性特征是我们类型系统的核心组成部分，在实际使用中也被用户们广泛需求。¹¹此外，如果不需要强调这种名义性区别，也可以使用类型别名来保持类型的通用性。

2.1.5 Type Aliases. Arbitrary types can be given names using the syntax type X[A, B, ...] = T. Type aliases and classes can refer to each other freely and can be mutually recursive.

2.1.5 类型别名。可以使用以下语法为任意类型指定名称：type X[A, B, ...] = T。
类型别名与类之间可以相互引用，而且这种引用关系可以是递归的。

2.1.6 Guardedness Check. Classes and type aliases are checked to ensure they do not inherit or refer to themselves immediately without going through a “concrete” type constructor first (i.e., a function or record type). For instance, the recursive occurrence of A in type A[X] = Id[A[X]] ∨ Int where type Id[Y] = Y is unguarded and thus illegal, but type A[X] = { x: A[X] } ∨ Int is fine.

2.1.6 安全性检查：会对类以及类型别名进行检测，以确保它们在未被通过“具体”的类型构造函数进行处理之前，不会直接继承自身或引用自身。例如，在类型表达式“A[X] = Id[A[X]] ∨ Int”中，如果“A”以递归方式出现，且此时Id[Y]的定义仅为“Y”，那么这种写法是不安全的、因此是非法的；而类型表达式“A[X] = { x: A[X] } ∨ Int”则是合法的。

2.1.7 Class-Instance Matching. As presented in the introduction, one can match values against class patterns in a form of primitive pattern matching. Consider the following definitions:

2.1.7 类与实例的匹配。正如引言中所提到的，人们可以通过原始模式匹配的方式，将具体的值与类模板进行对比匹配。请考虑以下定义：

class Cons[A]: Some[A] ∧ { tail: List[A] } type List[A] = Cons[A] ∨ None
rec def mapList f ls = case ls of
  Cons → Cons{value = f ls.value, tail = mapList f ls.tail},
  None → None{}

of inferred type:¹² mapList : ∀α, β. (α → β) → γ → δ where γ ≤ (Cons[α] ∧ { tail : γ } ∨ None) δ ≥ (Cons[β] ∧ { tail : δ } ∨ None)

其推导出的类型为：¹³ mapList : ∀α, β. (α → β) → γ → δ 其中，γ ≤ (Cons[α] ∧ { tail: γ } ∨ None) 且 δ ≥ (Cons[β] ∧ { tail: δ } ∨ None)。

We define a List type using None as the “nil” list and whose Cons constructor extends Some (from the introduction). A list in this encoding can be passed to any function that expects an option in input — if the list is a Cons instance, it is also a Some instance, and the value field representing the head of the list will be used as the value wrapped by the option. This example demonstrates that structural typing lets us mix and match as well as refine different constructors in a flexible way.

我们使用 None 作为“空列表”，并定义了一种名为 List 的数据类型；该类型的构造函数 Cons 实际上是继承自 Some 类型的。在这种编码方式下，任何期望接收一个选项类型作为输入的函数都可以接受这种形式的列表：如果这个列表是一个 Cons 实例，那么它同时也属于 Some 类型，而代表列表首元素的 value 字段将会被当作该选项所包装的值来使用。这个例子清楚地说明了：结构化类型系统使我们能够以灵活的方式组合不同的构造函数，并对它们进行进一步的优化或调整。

2.2 Constructing the Lattice of Types

2.2 构建类型格架

The algebraic subtyping philosophy of type system design is to begin with the subtyping of data types (records, functions, etc.) and to define the order connectives to fit this subtyping order, rather than to follow set-theoretic intuitions. We follow this philosophy and aim to design our subtyping order to tackle the following design constraints:

在类型系统设计中，采用代数子类型化的理念意味着应首先确定数据类型（如记录、函数等）之间的子类型关系，并据此定义相应的连接规则，而非遵循集合论的思维方式。我们正是秉承这一理念来设计子类型化规则，以便应对以下设计挑战：

1. The order connectives ∧, ∨, and ¬ should induce a Boolean algebra, so that we can manipulate types using well-known and intuitive Boolean-algebraic reasoning techniques.

2. 连接词 ∧、∨ 和 ¬ 应该能够构成一个布尔代数，这样我们就可以利用那些众所周知且直观易懂的布尔代数推理方法来处理各种类型的数据。

3. Nominal tags and their negations specifically should admit an intuitive set-theoretic understanding, in the sense that for any class C, type #C should denote all instances of C while type ¬#C should correspondingly denote all instances that are not derived from class C.¹⁴

4. 名义标签及其否定形式应当能够被人们以直观的方式用集合论的概念来理解。也就是说，对于任何类别C来说，类型#C应该表示该类别C的所有实例；而类型¬#C则应对应地表示那些并非源自类别C的所有实例。¹⁵

5. The resulting system should admit principal types as well as an effective polymorphic type inference strategy, where “effective” means that it should not rely on backtracking.

6. 所构建的系统应当既能识别各种基本类型，同时也应具备一种“有效的”多态类型推导机制；所谓“有效”，是指这种推导机制不应依赖回溯算法。

2.2.1 Lattice Types. Top, written \(\top\), is the type of all values, a supertype of every other type. Its dual bottom, written \(\bot\), is the type of no values, a subtype of every other type. For every \(\tau\), we have \(\bot \le \tau \le \top\). Intersection \(\wedge\) and union \(\vee\) types are the respective meet and join operators in the subtyping lattice. It is worth discussing possible treatments one can give these connectives:

2.2.1 格结构类型。位于顶部的类型，用符号\(\top\)表示，是所有值的统称，也是其他所有类型的超类型；而位于底部的对偶类型，用符号\(\bot\)表示，则是不包含任何值的类型，属于其他所有类型的子类型。对于任意类型\(\tau\)，我们都あり \(\bot \le \tau \le \top\)。交集运算符\(\wedge\)与并集运算符\(\vee\)，在这种子类型关系构成的格结构中，分别对应于“交集”与“并集”的操作。对于这些逻辑连接词，人们可以考虑采用多种不同的处理方式来进行分析。

1. We can axiomatize them as denoting the intersection \(\cup\) and union \(\cap\) of the sets of values that their operands denote, which is the approach taken by semantic subtyping.

2. We can axiomatize them as greatest lower bound (GLB) and least upper bound (LUB) operators, usually written \(\sqcap\) and \(\sqcup\), whose meaning is given by following the structure of a preexisting lattice of simple types (types without order connectives). In this interpretation, we can calculate the results of these operators when their operands are concretely known.

3. Finally, we can view \(\wedge\) and \(\vee\) as type constructors in their own right, with dedicated subtyping derivation rules. Then unions and intersections are not “computed away” but instead represent proper constructed types, which may or may not be equivalent to existing simple types.

4. 我们可以将它们公理化为表示其操作数所代表的值集合的交集 \(\cup\) 与并集 \(\sqcup\)，这种做法正是语义子类型化所采用的方法。
   

5. 我们也可以将它们公理化为最大下界运算符 \(\sqcap\) 与最小上界运算符 \(\sqcup\)，其含义是通过遵循现有的简单类型格的结构来确定的（简单类型是指不包含顺序连接词的类型）。在这种解释模式下，当这些运算数的操作数具体已知时，我们就可以计算出它们的结果。
   

6. 最后，我们可以将 \(\wedge\) 与 \(\vee\) 视为独立的类型构造器，并为其制定专门的子类型化推导规则。在这种情况下，并集与交集并不会被“自动计算出来”，而是代表着经过专门构造的类型，这些构造出的类型可能与现有的简单类型相等，也可能不相等。

2.2.2 Subtyping. We base our approach primarily on (3) but we do include a number of subtyping rules whose goal is to make the order connectives behave like (2) in some specific cases:

2.2.2 子类型划分。我们的方法主要基于第（3）点，但同时也包含了一些子类型划分规则，这些规则的目的是让某些特定情况下的顺序连接词能够表现出与第（2）点描述的一致的行为。

• We posit \(\#C_1 \wedge \#C_2 \le \bot\) whenever classes \(C_1\) and \(C_2\) are unrelated.¹⁶ This makes sense because there are no values that can be instances of both classes at the same time, due to single inheritance. We obviously also have \(\#C_1 \wedge \#C_2 \ge \bot\), meaning the two sides are equivalent (they subtype each other), which we write \(\#C_1 \wedge \#C_2 \equiv \bot\). On the other hand, \(\#C \le \#D\) for all \(C, D\) where \(C\) inherits from \(D\); so when \(\#C_1\) and \(\#C_2\) are related then either \(\#C_1 \wedge \#C_2 \equiv \#C_1\) or \(\#C_1 \wedge \#C_2 \equiv \#C_2\). Overall, we can always “reduce” intersections of nominal class tags to a single non-intersection type, making \(\wedge\) behave like a GLB operator in the class inheritance sublattice, made of nominal tags, \(\top\), \(\bot\), and \(\vee\), evocative of (2).

• We also posit the nonstandard rule \((\tau_1 \to \tau_2) \wedge (\tau_3 \to \tau_4) \le (\tau_1 \vee \tau_3) \to (\tau_2 \wedge \tau_4)\). The other direction holds by function parameter contravariance and result covariance, so again the two sides are made equivalent. \(\wedge\) behaves like a GLB operator on function types in a lattice which does not contain subtyping-based overloaded functions types, such as those of Dolan [2017]; Pottier [1998b]. This rule is illogical from the set-theoretic point of view: a function that can be viewed as returning a \(\tau_2\) when given a \(\tau_1\) and returning a \(\tau_4\) when given a \(\tau_3\) cannot be viewed as always returning a \(\tau_2 \wedge \tau_4\). For instance, consider \(\lambda x. x\), typeable both as \(\text{Int} \to \text{Int}\) and as \(\text{Bool} \to \text{Bool}\). According to both classical intersection type systems and the semantic subtyping interpretation, this term could be assigned type \((\text{Int} \to \text{Int}) \wedge (\text{Bool} \to \text{Bool})\). But we posited that this type is equivalent to \((\text{Int} \vee \text{Bool}) \to (\text{Int} \wedge \text{Bool})\). Thankfully, in MLstruct \(\lambda x. x\) cannot be assigned such an intersection type; instead, its most general type is \(\forall \alpha. \alpha \to \alpha\), which does subsume both \(\text{Int} \to \text{Int}\) and \(\text{Bool} \to \text{Bool}\), but not \((\text{Int} \to \text{Int}) \wedge (\text{Bool} \to \text{Bool})\). This explains why intersection types cannot be used to encode overloading in MLstruct.¹⁷

• For record intersections, we have the standard rule that \(\{x : \tau\} \wedge \{x : \pi\} \le \{x : \tau \wedge \pi\}\), making the two sides equivalent since the other direction holds by depth subtyping. Intersections of distinct record fields, on the other hand, do not reduce and stay as they are — in fact, multi-field record types are encoded, in MLstruct, as intersections of individual single-field record types, following Reynolds [1997]. For instance, assuming \(x \ne y\), then \(\{x : \tau_1, y : \tau_2\}\) is not a core form but merely syntax sugar for \(\{x : \tau_1\} \wedge \{y : \tau_2\}\).

• We apply similar treatments to various forms of unions: First, \((\tau_1 \to \tau_2) \vee (\tau_3 \to \tau_4) \equiv (\tau_1 \wedge \tau_3) \to (\tau_2 \vee \tau_4)\), the dual of the function intersection treatment mentioned above.

• 我们认为，当类\(C_1\)与类\(C_2\)之间不存在关联关系时，必有\(\#C_1 \wedge \#C_2 \le \bot\)。这一结论是合理的，因为由于单继承机制的存在，没有任何值能够同时属于这两个类。显然，我们也会有\(\#C_1 \wedge \#C_2 \ge \bot\)，这意味着这两者是等价的（即一个类是另一个类的子类型），我们将其表示为\(\#C_1 \wedge \#C_2 \equiv \bot\)。另一方面，对于所有满足\(C\)从\(D\)继承的类别对\(C, D\)来说，都有\(\#C \le \#D\)；因此，当\(\#C_1\)与\(\#C_2\)之间存在关联关系时，必然有\(\#C_1 \wedge \#C_2 \equiv \#C_1\)或\(\#C_1 \wedge \#C_2 \equiv \#C_2\)。总而言之，我们总是可以将名义类标签的交集“简化”为一种单一的非交集类型，这使得\(\wedge\)在这个由名义标签\(\top\)、\(\bot\)和\(\vee\)构成的类继承子格中表现得类似于最大下界运算符，这一点与(2)中的描述是一致的。

• 我们还提出了这样一个非标准规则：\((\tau_1 \to \tau_2) \wedge (\tau_3 \to \tau_4) \le (\tau_1 \vee \tau_3) \to (\tau_2 \wedge \tau_4)\)。由于函数参数的逆向变性与结果的同向变性，这个规则的双向都成立，因此这两者是等价的。在这样一个不包含基于子类型机制的重载函数类型的格结构中，\(\wedge\)对于函数类型来说就类似于最大下界运算符——这种格结构类似于Dolan [2017]和Pottier [1998b]所研究的模型。然而，从集合论的角度来看，这个规则是不合逻辑的：一个函数如果在接收到\(\tau_1\)时返回\(\tau_2\)，而在接收到\(\tau_3\)时返回\(\tau_4\)，那么它就不能被视为总是返回\(\tau_2 \wedge \tau_4\)。例如，考虑表达式\(\lambda x. x\)，它可以被定义为\(\text{Int} \to \text{Int}\)类型，也可以被定义为\(\text{Bool} \to \text{Bool}\)类型。根据传统的交集类型系统以及语义子类型解释，这个表达式的类型应该被确定为\((\text{Int} \to \text{Int}) \wedge (\text{ Bool} \to \text{Bool})\)；但我们认为这种类型实际上等价于\((\text{Int} \vee \text{Bool}) \to (\text{Int} \wedge \text{Bool})\)。值得庆幸的是，在MLstruct中，\(\lambda x. x\)无法被赋予这样的交集类型；相反，它的最通用类型是\(\forall \alpha. \alpha \to \alpha\)，这种类型确实包含了\(\text{Int} \to \text{Int}\)和\(\text{Bool} \to \text{Bool}\)这两种类型，但并不包含\((\text{Int} \to \text{Int}) \wedge (\text{Bool} \to \text{Bool})\)。这也解释了为什么在MLstruct中无法使用交集类型来表示函数的重载机制。

• 对于记录类型的交集，我们遵循标准的规则：\(\{x : \tau\} \wedge \{x : \pi\} \le \{x : \tau \wedge \pi\}\)，因为根据深度子类型机制，这个规则的双向都是成立的。然而，不同记录字段的交集并不会被简化，它们会保持原有的形式——事实上，在MLstruct中，多字段记录类型是按照Reynolds [1997]的方法，被表示为单个单字段记录类型的交集。例如，假设\(x \ne y\)，那么\(\{x : \tau_1, y : \tau_2\}\)并不是一种核心形式，而只是\(\{x : \tau_1\} \wedge \{y : \tau_2\}\)的一种语法简化表示。

• 对于各种形式的并集，我们也采用了类似的处理方式：首先有\((\tau_1 \to \tau_2) \vee (\tau_3 \to \tau_4) \equiv (\tau_1 \wedge \tau_3) \to (\tau_2 \vee \tau_4)\)，这是上面提到的函数交集处理规则的对偶形式。

Second, we recognize that {\(x : \tau\)} ∨ {\(y : \pi\)} and {\(x : \tau\)} ∨ (\(\pi_1\) → \(\pi_2\)), where \(x \neq y\), cannot be meaningfully used in a program, as the language has no feature allowing to tease these two components apart, so we identify these types with \(\top\), the top type. This is done by adding \(\top \le \{x : \tau\} \lor \{y : \pi\}\) and \(\top \le \{x : \tau\} \lor (\pi_1 \rightarrow \pi_2)\) as subtyping derivation rules.

其次，我们认识到表达式{\(x : \tau\)} ∨ {\(y : \pi\)}以及{\(x : \tau\)} ∨ (\(\pi_1\) → \(\pi_2\))，在\(x \neq y\)的情况下，无法在程序中被有效地使用——因为该语言不存在任何能够区分这两个组成部分的结构或机制。因此，我们将这类表达式归为“顶层类型\(\top\)”。为此，我们追加了以下两条子类型推导规则：\(\top \le \{x : \tau\} \lor \{y : \pi\}\)以及\(\top \le \{x : \tau\} \lor (\pi_1 \rightarrow \pi_2)\)。

The full specification of our subtyping theory is presented later, in Section 4 (Figure 4).

我们这种子类型化理论的完整规范将在后面的第4节（图4）中予以介绍。

2.2.3 Soundness.

The soundness of subtyping disciplines was traditionally studied by finding semantic models corresponding to types and subtyping, where types are typically understood as predicates on the denotations of \(\lambda\) terms (obtained from some \(\lambda\) model) and where subtyping is understood as inclusion between the corresponding sets of denotations. In this paper, we take a much more straightforward approach: all we require from the subtyping relation is that it be consistent, in the sense that it correctly relate types constructed from the same constructors and that it not relate unrelated type constructors. For instance, \(\tau_1 \rightarrow \tau_2 \le \pi_1 \rightarrow \pi_2\) should hold if and only if \(\pi_1 \le \tau_1\) and \(\tau_2 \le \pi_2\), and {\(x : \text{Int}\)} \(\le \#C\) should not be derivable. This turns out to be a sufficient condition for the usual soundness properties of progress and preservation to hold in our language. Consistency is more subtle than it may first appear. We cannot identify, e.g., \(\#C \lor \{x : \tau\}\) with \(\top\) even though the components of this type cannot be teased apart through instance matching, as doing so is incompatible with distributivity. Notice the conjunctive normal form of \(\pi = \#C \land \{x : \tau\} \lor \#D \land \{y : \tau'\}\) is \(\pi \equiv (\#C \lor \#D) \land (\#C \lor \{y : \tau'\}) \land (\{x : \tau\} \lor \#D) \land (\{x : \tau'\} \lor \{y : \tau'\})\). We can make {\(x : \tau\)} \(\lor\) {\(y : \tau'\)} equivalent to \(\top\) when \(x \neq y\) because that still leaves \(\pi \equiv (\#C \lor \#D) \land (\#C \lor \{y : \tau'\}) \land (\{x : \tau\} \lor \#D)\), which is equivalent to the original \(\pi\) by distributivity and simplification. But making \(\#C \lor \{y : \tau'\}\) and {\(x : \tau\)} \(\lor \#D\) equivalent to \(\top\) would make \(\pi \equiv \#C \lor \#D\), losing all information related to the fields, and breaking pattern matching!

2.2.3 正确性

传统上，人们通过寻找与类型及子类型关系相对应的语义模型来研究这类学科的正确性。在这里，类型通常被视为对某些\(\lambda\)模型所对应的对象的谓词，而子类型关系则被理解为这些对象集合之间的包含关系。在本文中，我们采用了更为直接的方法：我们对子类型关系所要求的一点就是它必须具备一致性，也就是说，它必须能够正确地反映那些由相同构造函数构建出来的类型之间的关系，并且不能将无关的类型构造函数关联在一起。例如，只有当\(\pi_1 \le \tau_1\)且\(\tau_2 \le \pi_2\)时，才能认为\(\tau_1 \rightarrow \tau_2 \le \pi_1 \rightarrow \pi_2\)成立；同时，不可能推出{\(x : \text{Int}\)} \(\le \#C\)这一结论。事实证明，这种一致性是我们的语言能够满足“进度”与“保持性”这些常规正确性性质的充分条件。其实，一致性的要求比表面上看起来要复杂得多。例如，我们不能将\(\#C \lor \{x : \tau\}\)等同于\(\top\)，因为即使这两个类型的组成部分无法通过实例匹配来区分，这样的等同也是不符合分配律的。注意到，表达式\(\pi = \#C \land \{x : \tau\} \lor \#D \land \{y : \tau'\}\)的连词标准形式其实是\(\pi \equiv (\#C \lor \#D) \land (\#C \lor \{y : \tau'\}) \land (\{x : \tau\} \lor \#D) \land (\{x : \tau'\} \lor \{y : \tau'\})\)。当\(x \neq y\)时，我们可以将{\(x : \tau\)} \(\lor\) {\(y : \tau'\)}等同于\(\top\)，因为这样仍然可以得到\(\pi \equiv (\#C \lor \#D) \land (\#C \lor \{y : \tau'\}) \land (\{x : \tau\} \lor \#D)\)这一结果，而根据分配律与简化规则，这个表达式本质上与原始的\(\pi\)是等价的。但是，如果将\(\#C \lor \{y : \tau'\}\)与{\(x : \tau\)} \(\lor \#D\)等同于\(\top\)，那么就会使得\(\pi \equiv \#C \lor \#D\)，从而丢失掉所有与字段相关的信息，进而导致模式匹配无法正常进行！

2.2.4 Negation Types.

Finally, we can add Boolean-algebraic negation to our subtyping lattice. However, its interpretation is considerably constrained by the Boolean structure and by the rules already presented in Section 2.2.2. In some languages, the values of a negation type \(\neg \tau\) are intuitively understood as all values that are not of the negated type \(\tau\), but in MLstruct, this intuition only holds for nominal tags.¹⁸ Negations can express interesting patterns, such as safe division, as seen below, where ‘e : T’ is used to ascribe a type T to an expression e:

2.2.4 否定类型

最后，我们可以将布尔代数中的否定操作添加到我们的子类型结构中。然而，其含义在很大程度上受到布尔结构的限制，同时也受到第2.2.2节中已经介绍过的规则的限制。在某些编程语言中，否定类型\(\neg \tau\)所表示的含义直观上可以被理解为“所有不属于类型\(\tau\)的值”；但在MLstruct中，这种直觉只有针对那些用于标识类型的标记时才成立。¹⁹ 否定操作能够用来表达一些有趣的模式，例如安全除法操作。如下例所示，在这里‘e : T’这一表示被用来为表达式e指定类型T。

def div n m = n / (m : Int ^ \neg 0)
div: Int -> (Int ^ \neg 0) -> Int

```  
def div n m = n / (m : Int ^ \neg 0)  
div: Int -> (Int ^ \neg 0) -> Int

def g (x: Int) = div 100 x  <> error: found Int, expected Int ^ \neg 0

def g(x: Int) = div 100 x; 错误：实际接收到的参数类型为Int，而预期应该接收的是类型为Int且值不等于0的参数。

def div_opt n m = case m of 0 -> None{}, _ -> Some{value = div n m}
div_opt: Int -> Int -> None ^ Some[Int]

def div_opt n m = case m of 0 -> None {}, _ -> Some{value = div n m}
div_opt: Int -> Int -> None ^ Some[Int]

Here, case m of ... is actually a shorthand for the core form case m = m of ... which shadows the outer m with a local variable m that is assigned a more refined type in each case branch.

在这里，case m of ...实际上是一种简写形式，它对应于核心表达式case m = m of ...。这种写法会用一个局部变量m来“替代”外层的作用域中的m，而在每个case分支中，这个局部变量m会被赋予更具体的类型。

As we saw in the introduction, \(\neg\) also allows for the sound typing of class-instance matching with default cases. Moreover, together with \(\top\), \(\bot\), \(\land\), and \(\lor\), our type structure forms a Boolean lattice, whose algebraic properties are essential to enabling principal type inference (see Section 3.2.1).

正如我们在引言中所看到的，符号“\(\neg\)”也使得类与实例之间的匹配关系能够被严谨地表示出来，尤其是那些包含默认情况的情况。此外，再加上符号“\(\top\)”、“\(\bot\)”、“\(\land\)”以及“\(\lor\)”，我们所构建的类型结构实际上构成了一个布尔格子，而这个布尔格子的代数性质对于实现主要的类型推导机制而言是至关重要的（详见第3.2.1节）。

2.2.5 Structural Decomposition.

We reduce complex object types to simpler elementary parts, which can be handled in a uniform way. Similarly to type aliases, which can always be replaced by their bodies, we can replace class types by their fields intersected with the corresponding nominal tags. For example, Cons[\tau] as defined in Section 2.1.7 reduces to #Cons ^ {value : \tau, tail : List[\tau]}. Recall that class tags like #Cons represent the nominal identities of classes. They are related with other class tags by a subtyping relationship that follows the inheritance hierarchy. For instance,

2.2.5 结构分解

我们将复杂的对象类型拆分为更为简单的基本组成部分，这样就可以用统一的方式来处理这些组件。与类型别名类似——别名总是可以被其对应的实际内容所替代——我们也可以将类类型替换为那些与该类相关的字段与相应的命名标签的交集。例如，如2.1.7节中所定义的Cons[\tau]，其实可以表示为#Cons ^ {value : \tau, tail : List[\tau]}。需要注意的是，像#Cons这样的类标签实际上代表着这些类的名义身份；它们与其他类标签之间的关系遵循继承层次结构中的子类型关系。例如……

given class C[α] : D[α ∨ 2] ∧ {x : 0 ∨ α} and class D[β] : {x : β, y : Int}, then we have #C ≤ #D. Moreover, the refined class type C[1] ∧ {y : Nat} reduces to the equivalent #C ∧ {x : 0 ∨ 1} ∧ {x : 1 ∨ 2, y : Int} ∧ {y : Nat}, which reduces further to #C ∧ {x : 1, y : Nat}.

假设存在类 C[α] : D[α ∨ 2] ∧ {x : 0 ∨ α} 以及 类 D[β] : {x : β, y : Int}，那么我们有 #C ≤ #D。
此外，精炼后的类类型 C[1] ∧ {y : Nat} 可以被简化为等价的表达式 #C ∧ {x : 0 ∨ 1} ∧ {x : 1 ∨ 2, y : Int} ∧ {y : Nat}，而这个表达式进一步简化后就是 #C ∧ {x : 1, y : Nat}。

Decomposing class types into more elementary types makes MLstruct’s approach fundamentally structural, while retaining the right amount of nominality to precisely reflect the semantics of runtime class-instance matching (i.e., pattern matching based on the runtime class of object values). It also means that there is no primitive notion of nominal type constructor variance in MLstruct: the covariance and contravariance of type parameters simply arise from the way class and alias types desugar into basic structural components.

将类类型分解为更基本的类型，使得MLstruct的方法在本质上是结构化的；同时，这种方法也保留了足够的“名义性”，从而能够准确反映运行时类与实例之间的匹配机制——即基于对象值在运行时的实际类类型所进行的模式匹配。此外，这也意味着在MLstruct中并不存在关于“名义类型构造函数的协变性与逆变性”这样的概念：类型参数的协变性与逆变性实际上只是由类类型及别名类型如何被分解为基本的结构成分所决定的。

2.3 Limitations

2.3 局限性

MLstruct comes with some limitations. We already mentioned in Section 2.2.2 that intersections cannot be used to type overloading. Here we explain several other significant limitations.

MLstruct存在一些局限性。我们在2.2.2节中已经提到过，交叉操作不能被用来实现类型重载。在这里，我们将进一步说明其他几项重要的限制之处。

2.3.1 Regular Structural Types. We restrict the shapes of MLstruct data types to be regular trees to make the problem of deciding whether one subsumes another decidable: concretely, occurrences of a class or alias type transitively reachable through the body of that type must have the same shape as the type’s head declaration. For instance, the following are disallowed:

2.3.1 规则结构类型。我们将MLstruct数据类型的形态限制为“规则树”，这样就能使得判断某个类型是否包含另一个类型的问题变得可判定：具体来说，如果某种类或别名类型可以通过该类型的定义体进行传递性访问，那么这种类型的形态就必须与该类型的首次声明所指定的形态相同。例如，以下情况是不被允许的：

class C[A]: {x: C(Int]} class C[A]: C[{x: List[A]}] class C[A]: {x: C[C[A]]}

class C[A]: {x: C(Int)}
class C[A]: C[{x: List[A]}]
class C[A]: {x: C[C[A]]}

We conjecture that allowing such definitions would give our types the expressive power of context-free grammars, for which language inclusion is undecidable, making subtyping undecidable.²⁰ To replace illegal non-regular class fields, one can use either top-level functions or methods. The latter solve this problem by having their types known in advance and not participating in structural subtype checking. Methods are implemented in MLstruct but not presented in this paper.

我们推测，如果允许使用这样的定义，那么我们的类型系统就会具备上下文无关文法所具有的表达能力；对于这类文法而言，语言之间的包含关系是无法判定的，因此子类型关系的判定也必然无法完成。²¹ 为了替换那些非法的非正则类字段，人们可以使用顶层函数或方法。后者之所以能够解决这个问题，是因为它们的类型在事先就已经被确定了，因此不会参与结构性的子类型检查过程。虽然MLstruct中实现了方法这一机制，但本文并未对此进行详细介绍。

2.3.2 Simplified Treatment of Unions. MLstruct keeps the expressiveness of unions in check by identifying {x : τ₁} ∨ {y : τ₂} (x ≠ y) and {x : τ₁} ∨ (τ₂ → τ₃) with ⊤, as described in Section 2.2.2. To make unions of different fields useful, one needs to “tag” the different cases with class types, as in C₁ ∧ {x : τ₁} ∨ C₂ ∧ {y : τ₂}, allowing us to separately handle these cases through instance matching ‘case v of C₁ → ... v.x ..., C₂ → ... v.y ...’, whereas this is not necessary in, e.g., TypeScript.

2.3.2 对联合类型的简化处理
MLstruct通过将 {x : τ₁} ∨ {y : τ₂}（其中x ≠ y）以及 {x : τ₁} ∨ (τ₂ → τ₃) 视为⊤来限制联合类型的表现力，这一机制已在2.2.2节中详细说明。为了使不同字段之间的联合操作能够发挥实际作用，人们需要使用类类型来“标记”这些不同的情况。例如，在C₁ ∧ {x : τ₁} ∨ C₂ ∧ {y : τ₂}这样的表达式中，这种标记机制使我们能够通过实例匹配来分别处理各种情况，即“case v of C1 → ... v.x ..., C2 → ... v.y ...”；而在TypeScript中，则无需采取这种做法。

A direct consequence of this restriction is that in MLstruct, there is no difference between {x : Int, y : Int} ∨ {x : Str, y : Str} and {x : Int ∨ Str, y : Int ∨ Str} (still assuming x ≠ y). Indeed, remember that {x : τ₁, y : τ₂} is syntax sugar for {x : τ₁} ∧ {y : τ₂} and by distributivity of unions over intersections, we can take {x : Int, y : Int} ∨ {x : Str, y : Str} to:

这一限制所带来的直接后果是：在MLstruct中，{x : Int, y : Int} ∨ {x : Str, y : Str}与{x : Int ∨ Str, y : Int ∨ Str}之间没有任何区别（仍然假设x ≠ y）。事实上，请记住，{x : τ₁, y : τ₂}其实只是{x : τ₁} ∧ {y : τ₂}的一种语法简化形式；而根据并集对交集的分配律，我们可以将{x : Int, y : Int} ∨ {x : Str, y : Str}理解为……

\((\{x : \text{Int}\} \lor \{x : \text{Str}\}) \land (\{x : \text{Int}\} \lor \{y : \text{Str}\}) \land (\{y : \text{Int}\} \lor \{x : \text{Str}\}) \land (\{y : \text{Int}\} \lor \{y : \text{Str}\})\)

\((\{x : \text{整数}\} \lor \{x : \text{字符串}\}) \land (\{x : \text{整数}\} \lor \{y : \text{字符串}\}) \land (\{y : \text{整数}\} \lor \{x : \text{字符串}\}) \land (\{y : \text{整数}\} \lor \{y : \text{字符串}\})\)

and since {x : τ₁} ∨ {y : τ₂} is identified with ⊤, as explained in Section 2.2.2, this reduces to:

由于如2.2.2节所解释的那样，{x : τ₁} ∨ {y : τ₂}与⊤是等同的，因此上述表达式可以简化为：

\((\{x : \text{Int}\} \lor \{x : \text{Str}\}) \land (\{y : \text{Int}\} \lor \{y : \text{Str}\})\)

\((\{x : \text{整数}\} \lor \{x : \text{字符串}\}) \land (\{y : \text{整数}\} \lor \{y : \text{字符串}\})\)

which reduces by field merging to {x : Int ∨ Str} ∧ {y : Int ∨ Str}, i.e., {x : Int ∨ Str, y : Int ∨ Str}.

通过字段合并，这种表达式可以简化为 {x : Int ∨ Str} ∧ {y : Int ∨ Str}，也就是 {x : Int ∨ Str, y : Int ∨ Str}。

Another consequence is that, e.g., List[Int] ∨ List[Str] is identified with List[Int ∨ Str]. Again, to distinguish between these two, one should prefer the use of class-tagged unions or, equivalently, proper sum types such as Either List[Int], List[Str], defined in terms of Left and Right classes.

另一个由此产生的后果是，例如，List[Int] ∨ List[Str]会被视为与List[Int ∨ Str]同义。为区分这两种情况，人们应该优先使用带有类标签的联合类型，或者等效地使用诸如Either List[Int], List[Str]这样的适当求和类型——这些类型是通过Left和Right这两个类来定义的。

2.3.3 Fewer Relationships. Unlike in semantic subtyping approaches, but like in most practical programming languages, we do not have {x : ⊥} ≤ ⊥. This would in fact lead to unsoundness in MLstruct: consider π = ({x : Some[Int], y : τ₁} ∨ {x : None, y : τ₂}) ∧ {x : None}; we would have π ≡ {x : ⊥, y : τ₁} ∨ {x : None, y : τ₂} ≡ {x : None, y : τ₂} by distributivity and also π ≡ {x : ⊥ ∨ None, y : τ₁ ∨ τ₂} by using (2.3.2) before distributing, but τ₁ ≠ τ₁ ∨ τ₂ in general.

2.3.3 关系数量较少。与语义子类型化方法不同，但与大多数实际使用的编程语言类似，在MLstruct中我们并不满足 {x : ⊥} ≤ ⊥这一条件。事实上，如果允许这种关系存在，就会导致MLstruct出现逻辑上的矛盾：以π = ({x : Some[Int], y : τ₁} ∨ {x : None, y : τ₂}) ∧ {x : None} 为例，根据分配律，我们可以得出 π ≡ {x : ⊥, y : τ₁} ∨ {x : None, y : τ₂}，进一步推导还可以得到 π ≡ {x : None, y : τ₂}；然而，根据公式(2.3.2)在进行分配运算之前，我们应该先计算{x : Some[Int], y : τ₁} ∨ {x : None, y : τ₂}的值，而实际上τ₁ ≠ τ₁ ∨ τ₂，因此这种推导是错误的。

3 INFERRING PRINCIPAL TYPES FOR MLSTRUCT

用于MLSTRUCT的主要推理原理类型

We now informally describe our general approach to principal type inference in MLstruct.

我们现在非正式地介绍一下我们在MLstruct中用于进行主类型推导的一般方法。

3.1 Basic Type Inference Idea

3.1 基本类型推导机制

We base the core of our type inference algorithm on a simple formulation of MLstruct type inference we formulated in previous work [Parreaux 2020]. The constraint solver attaches a set of lower and upper bounds to each type variable, and maintain the transitive closure of these constraints, i.e., it makes sure that at all times the union of all lower bounds of a variable remains a subtype of the intersection of all its upper bounds. This means that when registering a new constraint of the form \(\alpha \le \tau\), we not only have to add \(\tau\) to the upper bounds of \(\alpha\), but also to constrain \(\text{lowerBounds}(\alpha) \le \tau\) in turn. One has to be particularly careful to maintain a “cache” of subtyping relationships currently being constrained, as the graphs formed by type variable bounds may contain cycles. Because types are regular, there is always a point, in a cyclic constraint, where we end up checking a constraint we are already in the process of checking (it is in the cache), in which case we can assume that the constraint holds and terminate. Constraints of the general form \(\tau_1 \le \tau_2\) are handled by losslessly decomposing them into smaller constraints, until we arrive at constraints on type variables, which is made possible by the algebraic subtyping rules. The losslessness of this approach is needed to ensure that we only infer principal types. In other words, when decomposing a constraint, we must produce a set of smaller constraints that is equivalent to the original constraint. For example, we can decompose the constraint \(\tau_1 \lor (\tau_2 \rightarrow \tau_3) \le \tau_4 \rightarrow \tau_5\) into the equivalent set of constraints: \(\tau_1 \le \tau_4 \rightarrow \tau_5\); \(\tau_4 \le \tau_2\); and \(\tau_3 \le \tau_5\). If we arrive at a constraint between two incompatible type constructors, such as \(\tau_1 \rightarrow \tau_2 \le \{x : \tau_3\}\), an error is reported.

我们构建类型推导算法的核心原理，是基于我们在之前的研究工作中提出的MLstruct类型推导模型[Parreaux 2020]。该约束求解机制会为每一个类型变量设定一组“下界”和“上界”，并维护这些约束关系之间的传递封闭性——也就是说，它会确保任何时候，一个变量的所有下界的并集始终是其所有上界交集的子类型。这意味着，在新增形如\(\alpha \le \tau\)的约束时，我们不仅要将\(\tau\)添加到\(\alpha\)的上界集合中，还必须同时确保\(\text{lowerBounds}(\alpha) \le \tau\)这一约束成立。特别需要注意的是，我们需要维护一个“缓存”，用来记录当前正在被处理的子类型关系，因为由类型变量界限构成的图结构中可能会出现循环。由于类型系统具有规律性，在这种循环约束中，总会存在某个时刻我们需要检查那些已经被缓存的约束；在这种情况下，我们可以认为这些约束是成立的，从而终止当前的推导过程。对于形如\(\tau_1 \le \tau_2\)的一般约束，我们会通过将其“无损地”分解为更小的约束来处理它们，直到最终得到针对类型变量的直接约束——这一过程正是借助代数意义上的子类型规则来实现的。这种无损性处理方式的意义在于，它能确保我们仅推导出“本质上的”正确类型。换句话说，在对约束进行分解时，我们必须生成一组与原约束等价的、规模更小的约束集合。例如，我们可以将约束\(\tau_1 \lor (\tau_2 \rightarrow \tau_3) \le \tau_4 \rightarrow \tau_5\)分解为以下三组等价约束：\(\tau_1 \le \tau_4 \rightarrow \tau_5\)、\(\tau_4 \le \tau_2\)以及\(\tau_3 \le \tau_5\)。如果我们在分解过程中遇到了两个不兼容的类型构造器之间的约束，比如\(\tau_1 \rightarrow \tau_2 \le \{x : \tau_3\}\)，系统会立即报告错误。

3.2 Solving Constraints with Unions and Intersections

3.2 使用并集与交集来解除约束条件

By contrast with MLstruct, MLstruct supports union and intersections types in a first-class capacity, meaning that one can use these types in both positive and negative positions. This is particularly important to type check instance matching, which requires unions in negative positions, and class types, which require intersections in positive positions (both illegal in MLstruct).

与MLstruct不同，MLstruct能够以“第一类类型”的身份支持并集和交集类型，这意味着人们可以在这些类型的“正位置”以及“负位置”上使用它们。这一点对于进行类型检查尤其重要——因为在实例匹配过程中，需要在负位置使用并集类型；而在处理类类型时，则需要在正位置使用交集类型。而在MLstruct中，这两种用法都是不被允许的。

The main problem that arises in this setting is: How to resolve constraints with the shapes \(\tau_1 \le \tau_2 \lor \tau_3\) and \(\tau_1 \land \tau_2 \le \tau_3\)? Such constraints cannot be easily decomposed into simpler constraints without losing information — which would prevent us from achieving complete type inference — and without having to perform backtracking — which would quickly become intractable, even in non-pathological cases, and would yield a set of possible types instead of a single principal type. When faced with such constraints, we distinguish two cases: (1) there is a type variable among \(\tau_1\), \(\tau_2\), and \(\tau_3\); and (2) conversely, none of these types are type variables.

在这种情况下出现的主要问题是：如何处理这样的约束条件——即\(\tau_1 \le \tau_2 \lor \tau_3\)以及\(\tau_1 \land \tau_2 \le \tau_3\)？这类约束条件无法被轻易地分解为更简单的形式，同时也不会丢失任何信息；否则我们就无法完成类型的推导工作。此外，我们也不需要采用回溯算法来解决问题，因为即使是在不影响推理过程的情况下，使用回溯算法也会导致计算变得极其复杂，最终得到的只会是一组可能的类型而不是一个唯一的、确定的类型。面对这类约束条件时，我们可以将其分为两种情况：(1) 在\(\tau_1\)、\(\tau_2\)和\(\tau_3\)中至少有一个是类型变量；(2) 相反地，这三个值都不是类型变量。

3.2.1 Negation Types.

We use negation types to reformulate constraints involving type variables into forms that allow us to make progress, relying on the Boolean-algebraic properties of negation. A constraint such as \(\tau_1 \le \tau_2 \lor \alpha\) can be rewritten to \(\tau_1 \land \neg \tau_2 \le \alpha\) by turning the “positive” \(\tau_2\) on the right into a “negative” on the left, as these are equivalent in a Boolean algebra.²² Therefore, it is sufficient and necessary to constrain \(\alpha\) to be a supertype of \(\tau_1 \land \neg \tau_2\) to solve the constraint at hand. Similarly, we can solve \(\alpha \land \tau_1 \le \tau_2\) by constraining \(\alpha\) to be a subtype of \(\tau_2 \lor \neg \tau_1\).²³ When both

3.2.1 否定类型

我们利用否定类型将那些涉及类型变量的约束重写为便于进一步处理的形式，这一过程依托的是否定运算所具有的布尔代数性质。例如，像 \(\tau_1 \le \tau_2 \lor \alpha\) 这样的约束可以通过将其右边的“正向”表达式转换为左边的“负向”表达式来重新写成 \(\tau_1 \land \neg \tau_2 \le \alpha\)，因为在布尔代数中这两种表达式是等价的。²⁴ 因此，要想解决这个约束，就必须规定 \(\alpha\) 必须是 \(\tau_1 \land \neg \tau_2\) 的上级类型；同样地，要解决 \(\alpha \land \tau_1 \le \tau_2\) 这个约束，也可以规定 \(\alpha\) 必须是 \(\tau_2 \lor \neg \tau_1\) 的下级类型。²⁵ 当这两种规定同时满足时……

transformations are possible, one may pick one or the other equivalently. The correctness of these transformations is formally demonstrated in the Swapping theorem of the extended version of this paper [Parreaux and Chau 2022]. This approach provides a solution to case (1), but in a way it only pushes the problem around, delaying the inevitable apparition of case (2).

这些变换都是可行的，人们可以任意选择其中一种方式进行操作。这些变换的正确性在本文扩展版本中的“交换定理”中得到了形式上的证明[Parreaux和Chau 2022]。这种方法确实为情况（1）提供了解决方案，但从某种程度上来说，它只是将问题暂时搁置起来，从而推迟了情况（2）不可避免地出现的时间。

3.2.2 Normalization of Constraints.

To solve problem (2), we normalize constraints until they are in the shape “\(\tau_{con} \le \tau_{dis}\)”, where (using a horizontal overline to denote 0 to n repetitions):

3.2.2 约束条件的标准化

为了解决问题（2），我们需要对这些约束条件进行标准化处理，使其呈现“\(\tau_{con} \le \tau_{dis}\)”这样的形式。其中，上线号表示该操作需要重复0到n次。

• \(\tau_{con}\) represents \(\top\), \(\bot\), or the intersection of any non-empty subset of \(\{\#C, \tau_1 \to \tau_2, \{x : \tau\}\}\).

• \(\tau_{dis}\) represents types of the form \(\top\), \(\bot\), \((\tau_1 \to \tau_2) \lor \#C\), \(\{x : \tau\} \lor \#C\), or \(\#C \lor \#C'\).

• \(\tau_{con}\) 表示 \(\top\)、\(\bot\)，或者集合 \(\{\#C, \tau_1 \to \tau_2, \{x : \tau\}\}\) 中的任何非空子集的交集。
  

• \(\tau_{dis}\) 表示形式为 \(\top\)、\(\bot\)、\((\tau_1 \to \tau_2) \lor \#C\)、\(\{x : \tau\} \lor \#C\)，或者 \(\#C \lor \#C'\) 的类型。

Let us consider a few examples. First, given a constraint like \((\tau_1 \lor \tau_2) \land \tau_3 \le \tau_4\), we can distribute the intersection over the union thanks to the rules of Boolean algebras (see Section 4.4.3), which results in \((\tau_1 \land \tau_3) \lor (\tau_2 \land \tau_3) \le \tau_4\), allowing us to solve \(\tau_1 \land \tau_3 \le \tau_4\) and \(\tau_2 \land \tau_3 \le \tau_4\) independently. Second, given a constraint like \(\tau_1 \le \{x : \tau_2\} \lor \tau_3 \to \tau_4\), we simply use the fact that \(\{x : \tau_2\} \lor \tau_3 \to \tau_4 \equiv \top\) (as explained in Section 2.2.2) to reduce the constraint to \(\tau_1 \le \top\), a tautology. Third, with constraints containing intersected nominal class tags on the left, we can compute their greatest lower bound based on our knowledge of the single-inheritance class hierarchy. We eventually end up with constraints of the shape “\(\tau_{con} \le \tau_{dis}\)” and there always exists a \(\tau_i \in \tau_{con}\) and \(\tau'_j \in \tau_{dis}\) such that we can reduce the constraint to an equivalent constraint \(\tau_i \le \tau'_j\). Notice that if two related nominal tags appears on each side, it is always safe to pick that comparison, as doing so does not entail any additional constraints. If there are no such related nominal tags, the only other choice is to find a type in the right-hand side to match a corresponding type in the left-hand side, and the syntax of these normal forms prevents there being more than one possible choice. All in all, our Boolean algebra of types equipped with various algebraic simplification laws ensures that we have a lossless way of resolving the complex constraints that arise from union and intersection types, enabling principal type inference.

让我们来看几个例子。首先，对于像\((\tau_1 \lor \tau_2) \land \tau_3 \le \tau_4\)这样的约束条件，根据布尔代数的规则（详见第4.4.3节），我们可以将交集运算分配到并集上，从而得到\((\tau_1 \land \tau_3) \lor (\tau_2 \land \tau_3) \le \tau_4\)，这样我们就可以分别求解\(\tau_1 \land \tau_3 \le \tau_4\)和\(\tau_2 \land \tau_3 \le \tau_4\)了。其次，对于像\(\tau_1 \le \{x : \tau_2\} \lor \tau_3 \to \tau_4\)这样的约束条件，由于\(\{x : \tau_2\} \lor \tau_3 \to \tau_4 \equiv \top\)（如第2.2.2节所解释的），我们可以将这个约束条件简化为\(\tau_1 \le \top\)，而\(\tau_1 \le \top\)显然是一个恒真命题。第三，对于那些左侧包含交叉命名类标签的约束条件，我们可以利用对单继承类层次结构的理解来计算它们的大下界。最终，这些约束条件会转化为形如“\(\tau_{con} \le \tau_{dis}\)”的形式，而且总能找到满足\(\tau_i \in \tau_{con}\)且\(\tau'_j \in \tau_{dis}\)的元素，从而使该约束条件简化为等价的\(\tau_i \le \tau'_j\)。需要注意的是，如果两侧都存在相关的命名标签，选择进行这种比较总是安全的，因为这样做不会引入任何额外的约束条件；如果不存在这样的相关标签，那么就只能寻找右侧中的某个类型与左侧中的对应类型相匹配，而这类表达式的语法结构确保了只存在一个唯一的选择。总之，我们这套配备了各种代数简化规则的布尔型代数体系，为解决由并集和交集类型所引发的复杂约束条件提供了可靠的方法，从而使得主类型推导成为可能。

The constraint solving algorithm described in Section 5.3 and implemented in the artifact uses the ideas explored above but puts the entire constraint into a normal form, instead of normalizing constraints on the fly. This helps to efficiently guarantee termination by maintaining a cache of currently-processed subtyping relationships in normal forms, which is straightforward to query.

第5.3节中描述的那种约束求解算法，在该实现方案中被加以运用。这种算法借鉴了前面讨论过的思想，但会将所有的约束都转化为标准形式，而不是在运行过程中动态地对这些约束进行标准化处理。通过维护一个用于存储目前已处理的、处于标准形式的子类型关系信息的缓存，这种方法能够有效地确保算法能够及时终止执行；此外，这个缓存也便于被查询和使用。

3.3 Subsumption Checking

3.3 吸收关系检验

Subsumption checking, denoted by \(\leq \nabla\), is important to check that definitions conform to given signatures. Contrary to MLsub, which syntactically separates positive from negative types (the polarity restriction), and therefore requires different algorithms for constraint solving and subsumption checking, in MLstruct we can immediately reuse the constraint solving algorithm for subsumption checking, without requiring much changes to the type system. To implement \(\forall \Xi_1. \tau_1 \leq \nabla \forall \Xi_2. \tau_2\), we instantiate all the type variables in \(\Xi_1\), with their bounds, to fresh type variables, and we turn all the variables in \(\Xi_2\) into rigid variables (so-called “skolems”). The latter can be done by turning these type variables into fresh flexible nominal tags and by inlining their bounds, expressing them in terms of unions, intersections, and recursive types. Since there is no polarity restrictions in our system, the resulting types can be compared directly using the normal constraint solving algorithm.

“包含关系检查”，用符号 \(\leq \nabla\) 表示，这一过程对于验证各种定义是否符合预先设定的类型规范而言至关重要。与 MLsub 不同，MLsub 在语法层面会将正类型与负类型区分开来（即所谓的“极性限制”），因此需要采用不同的算法来分别处理约束条件的求解与包含关系检查；而在 MLstruct 中，我们可以直接将用于约束条件求解的算法拿来用于包含关系检查，而且几乎不需要对类型系统进行任何修改。为了实现 \(\forall \Xi_1. \tau_1 \leq \nabla \forall \Xi_2. \tau_2\) 这一要求，我们首先会将 \(\Xi_1\) 中的所有类型变量及其对应的范围限定转换成新的类型变量，同时将 \(\Xi_2\) 中的所有变量转换为“刚性变量”（也就是所谓的“斯科勒姆变量”）。实现这一转换的方法是将这些类型变量转化为新的、具有灵活性质的命名标签，并将其范围限定直接内联到相关表达式中，使其能够用并集、交集以及递归类型的形式来表示。由于我们的系统中不存在极性限制，因此最终得到的类型可以直接使用常规的约束条件求解算法来进行比较。

Flexible nominal tags #F are just like nominal class tags #C, except that they can coexist with unrelated tags without reducing to ⊥. For example, while #C_1 ∧ #C_2 is equivalent to ⊥ in MLstruct when C_1 and C_2 are unrelated, #F ∧ #C_2 is not.²⁶ Flexible nominal tags are also the feature used to encode the nominal tags of traits, necessary to implement mixin traits as described in Section 2.1.2.

灵活的命名标签#F与命名类标签#C类似，不同之处在于：它们可以与不相关的标签共存，而不会导致结果变为⊥。例如，在MLstruct中，当C_1和C_2不相关时，#C_1 ∧ #C_2的结果会等于⊥；然而#F ∧ #C_2的结果则不会如此。²⁷这种灵活的命名标签特性也被用于编码属性中的命名标签，而这一点对于实现第2.1.2节中提到的混合属性机制来说是必不可少的。

For lack of space, we do not formally describe subsumption checking in this paper.

由于篇幅限制，我们在本文中并未对“包含关系检验”的具体方法进行详细描述。

3.4 Simplification and Presentation of Inferred Types

3.4 推断出的类型的简化表示方法

Type simplification and pretty-printing are important components of any practical implementation of MLstruct and MLstruct. They indeed perform a lot of the heavy-lifting of type inference, massaging inferred types, which are often big and unwieldy, into neat and concise equivalent type expressions. In this section, we briefly explain how simplification is performed in MLstruct.

类型简化与美观化输出是任何实际使用MLstruct进行类型系统实现时不可或缺的重要组成部分。这些功能确实承担了大部分类型推导的工作——将那些往往庞大而复杂的推导结果转化为简洁明了的等效类型表达式。在本节中，我们将简要说明MLstruct是如何实现类型简化的。

3.4.1 Basic Simplifications. For basic simplifications, we essentially follow Parreaux [2020] — we remove polar occurrences of type variables, remove type variables “sandwiched” between identical bounds, and we perform some hash consing to simplify inferred recursive types. The simplification of unions, intersections, and negations is not fully addressed by Parreaux, since MLsub does not fully supports these features. In MLstruct, we apply standard Boolean algebra simplification techniques to simplify these types, such as putting them into disjunctive normal forms, simplifying complements, and factorizing common conjuncts. We also reduce types as they arise, based on Section 2.2.2.

3.4.1 基本简化方法。在进行基本简化时，我们主要遵循Parreaux [2020]的研究方法：移除类型变量出现的极性情况，剔除那些被相同上下界“夹在中间的”类型变量，并通过一些哈希处理技术来简化推导出的递归类型。对于并集、交集及取反运算的简化方法，Parreaux并未进行全面探讨，因为MLsub并不完全支持这些功能。在MLstruct中，我们采用了标准的布尔代数简化技巧来处理这类类型，例如将其转化为析取范式、简化补码形式，或是分解其中的共同连接项。此外，我们也根据第2.2.2节的内容，在类型生成的过程中及时对其进行进一步简化处理。

3.4.2 Bound Inlining. Many types can be represented equivalently using either bounded quantification or inlined intersection and union types, so we often have to choose between them. For instance, \(\forall (\alpha \le \text{Int}) \cdot (\beta \ge \text{Int})\). \(\alpha \to \alpha \to \beta\) is much better expressed as the equivalent \(\text{Int} \to \text{Int} \to \text{Int}\). But whether \((\alpha \land \text{Int}) \to (\alpha \land \text{Int}) \to \alpha\) is better than the equivalent \(\forall (\alpha \le \text{Int})\). \(\alpha \to \alpha \to \alpha\) may depend on personal preferences. As a general rule of thumb, we only inline bounds when doing so would not duplicate them and when they are not cyclic (i.e., we do not inline recursive bounds).

3.4.2 有界量词的内联使用。许多类型都可以通过有界量词或者内联的交集/并集类型来等效地表示，因此我们常常需要在这两种表达方式之间进行选择。例如，对于表达式 \(\forall (\alpha \le \text{Int}) \cdot (\beta \ge \text{Int})\)，将其表示为 \(\alpha \to \alpha \to \beta\) 会更为清晰；而表达式 \((\alpha \land \text{Int}) \to (\alpha \land \text{Int}) \to \alpha\) 与等价的 \(\forall (\alpha \le \text{Int}) \cdot (\alpha \to \alpha \to \alpha)\) 相比，哪种表达方式更好，可能取决于个人偏好。一般来说，只有当内联使用有界量词不会导致重复计算，并且这些量词不是循环结构时，我们才会选择对其进行内联处理——也就是说，我们不会对递归类型的量词进行内联编码。

3.5 Implementation

3.5 实施过程

MLstruct is implemented in ~5000 lines of Scala code, including advanced type simplification algorithms and error reporting infrastructure.²⁸ We have an extensive tests suite consisting of more than 4000 lines of well-typed and ill-typed MLstruct expressions, for which we automatically check the output of the type simplifier and error reporting for regressions. Running this test suite in parallel takes ~2s on a 2020 iMac with a 3.8 GHz 8-Core Intel Core i7 and 32 GB 2667 MHz DDR4.

MLstruct是用大约5000行Scala代码实现的，其中包含了先进的类型简化算法以及错误报告机制。²⁹我们构建了一套规模庞大的测试套件，其中包含了超过4000行各种类型的MLstruct表达式（包括那些类型定义正确的表达式以及类型定义错误的表达式）。对于这些测试用例，我们会自动检查类型简化工具的输出结果以及错误报告系统的功能，以便及时发现任何潜在的异常变化。在拥有一颗3.8 GHz、8核心的Intel Core i7处理器以及32 GB、2667 MHz DDR4内存的2020款iMac上，同时运行这套测试套件大约需要2秒钟的时间。

4 FORMAL SEMANTICS OF MLSTRUCT

4 MLSTRUCT的形式语义学

In this section, we introduce \(\lambda^-\), a formal calculus which reflects the core features of MLstruct.

在本节中，我们介绍了\(\lambda^-\)这一形式化计算系统，它充分体现了MLstruct的核心特性。

4.1 Syntax

4.1 语法

The syntax of \(\lambda^-\) is presented in Figure 1. We use the notation \(\overline{E_i}^i\) to denote a repetition of \(i = 0\) to \(n\) occurrences of a syntax form \(E\), and we use the shorthand \(\overline{E}\) when \(i\) is not needed for disambiguation.

图1展示了\(\lambda^-\)的语法结构。我们使用符号\(\overline{E_i}^i\)来表示语法形式\(E\)从第0次到第\(n\)次的出现；当不需要通过\(i\)来消除歧义时，我们也使用简写\(\overline{E}\)来表示这一语法形式。

4.1.1 Core Syntax. The core syntax of \(\lambda^-\) follows the MLstruct source language presented previously quite closely, though it introduces a syntactic novelty: the mode \(\diamond\) or \(\circ\) of a syntactic form is used to deduplicate sentences that refer to unions and intersections as well as top and bottom, which are respective duals and can therefore often be treated symmetrically. For instance, \(\vdash^\diamond\) is to be understood as either \(\vdash\) when \(\diamond = \cdot\), i.e., \(\vdash\), or as \(\vdash^\nabla\) when \(\diamond = \nabla\), i.e., \(\perp\). A similar idea was developed independently by d. S. Oliveira et al. [2020] to cut down on boilerplate and repetition in formalizing subtyping systems.

4.1.1 核心语法。\(\lambda^-\)的核心语法与之前提到的MLstruct源语言在很大程度上是一致的，但其中引入了一种新的语法机制：某种语法形式的“模式”\(\diamond\)或\(\circ\)被用来消除那些针对并集、交集以及“顶部”与“底部”这类互为对偶的概念而编写出来的重复性语句。因为这些概念往往具有对称性，所以可以使用这种机制来简化代码结构。例如，当\(\diamond = \cdot\)时，\(\vdash^\diamond\)应被理解为\(\vdash\)；而当\(\diamond = \nabla\)时，则应被理解为\(\vdash^\nabla\)，即\(\perp\)。d. S. Oliveira等人[2020]也独立提出了类似的思路，目的是为了在形式化子类型系统时减少冗余代码和重复性表述。

Parametric polymorphism in \(\lambda^-\) is attached solely to top-level ‘def’ bindings, whose semantics, as in languages like Scala, is to re-evaluate their right-hand side every time they are referred to in the program. In contrast, local let bindings are desugared to immediately-applied lambdas, and are treated monomorphically. Let polymorphism is orthogonal to the features presented in this paper,

在 \(\lambda^-\) 中，参数多态性仅与顶层的 “def” 字符串相关；与 Scala 等语言类似，这类语法规则要求：每当程序中再次引用这些 “def” 字符串时，其右侧表达式都会被重新求值。相比之下，局部的 “let” 语句所引用的匿名函数会被优化为可立即执行的 lambda 表达式，并且这些匿名函数会被视为单态对象来处理。“Let 多态性”与本文所介绍的特性是相互独立的。

Fig. 1. Syntax of types, terms, and contexts.

图1. 类型、术语及上下文的语法结构。

and can be handled by using a level-based algorithm [Parreaux 2020] on top of the core algorithm we describe here, as well as a value restriction if the language is meant to incorporate mutation.

可以通过在我们在这里描述的核心算法基础上使用基于级别的算法[Parreaux 2020]来处理这类问题；此外，如果该语言旨在支持变异操作，还可以引入值限制机制。

In \(\lambda^{-}\), def bindings are never recursive. This simplification is made without loss of generality, as recursion can be recovered using a Z fixed point combinator, typeable in MLsub [Dolan 2017] and thus also in \(\lambda^{-}\). This combinator is defined as \(t_Z = \lambda f. t'_Z t'_Z\) where \(t'_Z = \lambda x. f (\lambda v. x x v)\). One can easily verify that \(t_Z\) can be typed as \(((\alpha \rightarrow \beta) \rightarrow ((\alpha \rightarrow \beta) \wedge \gamma)) \rightarrow \gamma\).

在 \(\lambda^{-}\) 中，定义性绑定永远不会呈现递归形式。这种简化并不会损失一般的适用性，因为可以通过使用 Z 固定点组合器来恢复递归特性——这种组合器可以在 MLsub [Dolan 2017] 中被赋予类型，因此也能在 \(\lambda^{-}\) 中使用。该组合器的定义如下：\(t_Z = \lambda f. t'_Z t'_Z\)，其中 \(t'_Z = \lambda x. f (\lambda v. x x v)\)。可以很容易地验证，\(t_Z\) 确实可以被赋予类型 \(((\alpha \rightarrow \beta) \rightarrow ((\alpha \rightarrow \beta) \wedge \gamma)) \rightarrow \gamma\)。

To keep the formalism on point, we only present class object types, and ignore uninteresting primitive and built-in types like Int and Bool, which can be encoded as classes. Note that singleton types like 1, 2, and true, as we use them in the introduction, are easily encoded as subclasses \(1_C\), \(2_C\), and true\(_C\) of the corresponding built-in types.

为了保持形式上的严谨性，我们仅讨论类对象类型，而忽略那些不具备研究价值的原始类型及内置类型——比如 Int 和 Bool，因为这些类型完全可以被编码为对应的类。需要指出的是，像 1、2 这样的单例类型，以及我们在引言中提到的 true，都可以很容易地被编码为相应内置类型的子类，即 \(1_C\)、\(2_C\) 和 true\(_C\)。

Finally, the syntax of pattern matching ‘case x = t of ...’ includes a variable binding because the rules for typing it will refine the type of that variable in the different branches. We do not use ‘case x of ...’ as the core form in order to allow for simple substitution of variables with terms.

最后，模式匹配语法“case x = t of …”实际上包含了一种变量赋值机制，因为使用这种语法的规则会在不同的分支中“确定”该变量的具体类型。我们并未将“case x of …”作为核心表达方式，这样做是为了允许变量与术语之间进行简单的替换操作。

4.1.2 Contexts.

We use four kinds of contexts. Declarations contexts \(\mathcal{D}\) hold the type declarations of the program. Throughout this paper, we assume an ambient declarations context (i.e., our formal developments are implicitly parameterized by \(\mathcal{D}\)). Typing contexts \(\Gamma\) bind both monomorphic and polymorphic types, the latter corresponding to ‘def’ bindings. Subtyping contexts \(\Sigma\) record assumptions about subtyping relationships, with some of these assumptions potentially hidden behind a \(\triangleright\) (explained in Section 4.4.1). Finally, polymorphic or constraining contexts \(\Xi\) contain bounds/constraints on type variables and possibly errors (\(err \in \Xi\)) encountered during type inference. The typing rules will ensure that in a polymorphic type \(\forall \Xi. \tau\), context \(\Xi\) is consistent, which implies \(err \notin \Xi\). Note that \(\Sigma\) contexts are rooted in \(\Xi\) contexts because subtyping judgments require the former but are invoked from typing judgments, which use the latter for polymorphism.

4.1.2 上下文

我们使用了四种类型的上下文。声明上下文\(\mathcal{D}\)用于存储程序中的类型声明；在本文中，我们假设存在一个环境声明上下文（也就是说，我们的形式化推导过程实际上是隐式地以\(\mathcal{D}\)为参数进行的）。类型赋值上下文\(\Gamma\)用于绑定单态类型以及多态类型，其中后者对应于“def”语句所进行的类型声明。子类型关系上下文\(\Sigma\)用来记录有关子类型关系的各种假设，其中某些假设可能会被“\(\triangleright\)”符号所隐藏起来（具体解释见第4.4.1节）。最后，多态或约束性上下文\(\Xi\)则包含对类型变量的各种限制条件，以及在类型推导过程中可能遇到的错误信息（即\(err \in \Xi\)）。类型规则会确保，在一个多态类型\(\forall \Xi. \tau\)中，上下文\(\Xi\)必须是一致的，这意味着\(err \notin \Xi\)。需要注意的是，\(\Sigma\)上下文其实是“根植于”\(\Xi\)上下文之中的——因为进行子类型关系判断时需要使用\(\Sigma\)上下文，而这些判断又是通过使用\(\Xi\)上下文来实现多态性处理的。

4.1.3 Shorthands.

Throughout this paper, we make use of the following notations and shorthands:

4.1.3 缩写符号

在本文中，我们使用了以下缩写符号和简写形式：

\[ \begin{align*} R &::= \{\overline{x = v}\} & N &::= A \mid C & H &::= \tau \le \tau & N &::= N[\epsilon] & C \to t &::= C \to t, \epsilon \\ \{\overline{x : \tau_x}^{x \in S}, y : \tau_y \} &::= \{\overline{x : \tau_x}^{x \in S}\} \wedge \{y : \tau_y\} & (y \notin S) & \text{let } x = t_1 \text{ in } t_2 &::= (\lambda x. t_2) t_1 & \text{case } y \text{ of } M &::= \text{case } x = y \text{ of } [y \mapsto x]M & (x \notin FV(M)) \end{align*} \]

Fig. 2. Small-step evaluation rules.

图2. 小步评估规则。

4.2 Evaluation Rules

4.2 评估规则

The small-step reduction semantics of \(\lambda^-\) is shown in Figure 2. The relation \(P \rightsquigarrow P'\) reads “program P evaluates to program \(P'\) in one step.” Note that P here may refer to a simple term t.

\(\lambda^-\)这种“小步递归简化”机制的运作方式如图2所示。关系式\(P \rightsquigarrow P'\)的含义是：“程序P可以在一步之内被转化为程序\(P'\)。”需要注意的是，这里的P实际上也可以指代一个简单的术语t。

We write \(\{x = v_2\} \in v_1\) to say that \(v_1\) is a value of the form '\(C \{\overline{z = w}, x = v_2\}\)' or of the form '\(C \{\overline{z = w}, y = v_2'\}\)' where \(y \neq x\) and \(\{x = v_2\} \in C \{\overline{z = w}\}\). Class instances are constructed via the C R introduction form, where R is a record of the fields of the instance. Instance matching works by inspecting the runtime instance of a scrutinee value, in order to determine which corresponding branch to evaluate. This is done through the superclasses function \(S(\tau)\). We define the superclasses \(S(\tau)\) of a type \(\tau\) as the set of classes transitively inherited by type \(\tau\), assuming \(\tau\) is a class type or the expansion of a class type. Note that a term of the shape '\(case x = v of \epsilon\)' is stuck.

我们用“\(\{x = v_2\} \in v_1\)”这样的表达式来表示：\(v_1\)实际上是形式为“\(C \{\overline{z = w}, x = v_2\}\)”或“\(C \{\overline{z = w}, y = v_2'\}\)”的数值，其中\(y \neq x\)，且\(\{x = v_2\} \in C \{\overline{z = w}\}\)。类实例是通过所谓的“C R引入形式”来创建的，其中R表示该实例所包含的各种字段信息。实例匹配的过程实际上是通过对被检测数值在运行时的实际表现来进行分析，从而确定应该执行哪一个对应的处理分支；这一过程是通过函数\(S(\tau)\)来实现的。我们定义类型\(\tau\)的超类集合 \(S(\tau)\)为：当\(\tau\)本身是一个类类型或某个类类型的扩展时，\(\tau\)所继承的所有类的集合。需要注意的是，形如“\(case x = v of \epsilon\)”这样的表达式属于固定不变的结构，因此无法在实例匹配过程中被修改。

4.3 Declarative Typing Rules

4.3 声明性类型规则

Program-typing judgments \(\Xi, \Gamma \vdash_* P : \tau\) are used to type programs while term-typing judgments \(\Xi, \Gamma \vdash t : \tau\) are used to type def right-hand sides and program bodies. The latter judgement is read “under type variable bounds \(\Xi\) and in context \(\Gamma\), term \(t\) has type \(\tau\).” We present only the rules for the latter judgment in Figure 3, as they are the more interesting ones, and relegate the auxiliary program-typing (\(\Xi, \Gamma \vdash_* P : \tau\)), consistency (\(\Sigma \text{ cons.}\)) and subtyping entailment (\(\Sigma \vdash \sigma \leq^\forall \sigma\) and \(\Sigma \vdash \Sigma\)) rules to the extended version of this paper. The consistency judgment is used to make sure we type def s and program bodies under valid (i.e., consistent) bounds only.³⁰

程序类型判定规则 \(\Xi, \Gamma \vdash_* P : \tau\) 用于给程序指定类型，而项类型判定规则 \(\Xi, \Gamma \vdash t : \tau\) 则用于为 def 语句的右侧部分及程序主体指定类型。后一种判定规则的含义是：“在类型变量范围 \(\Xi\) 的限制下，并在上下文 \(\Gamma\) 中，项 \(t\) 具有类型 \(\tau\)。”我们在图 3中仅展示了后一种判定规则的规则内容，因为这些规则更为重要；而辅助性的程序类型判定规则 (\(\Xi, \Gamma \vdash_* P : \tau\))、一致性判定规则 (\(\Sigma \text{ cons.}\)) 以及子类型关系判定规则 (\(\Sigma \vdash \sigma \leq^\forall \sigma\) 与 \(\Sigma \vdash \Sigma\)) 则被纳入本文的扩展版本中。一致性判定规则的用途在于确保我们仅为那些处于有效（即一致性良好）的范围之内的 def 语句及程序体指定类型。³¹

Rule T-OBJ features a few technicalities deserving of careful explanations. First, notice that its result type is an intersection of the nominal class tag #C with a record type of all the fields passed in the instantiation. Importantly, these fields may have any types, including ones not compatible with the field declarations in C or its parents. This simplifies the meta theory (especially type inference) and is done without loss of generality: indeed, we can desugar '\(C \{x = t, \dots\}\)' instantiations in MLstruct into a type-ascribed instantiation '\(C\{x = t, \dots\} : C[\bar{\alpha}]\)' in \(\lambda^-, 18\) where all \(\bar{\alpha}\) are fresh, which will ensure that the provided fields satisfy their declared types in C.

规则T-OBJ中存在一些需要仔细解释的技术细节。首先，请注意，该规则的结果类型实际上是命名类标记#C与在实例化过程中传递的所有字段的记录类型之间的交集。重要的是，这些字段可以具有任何类型，包括那些与C语言或其父语言中的字段声明不兼容的类型。这种设计简化了元理论的结构（尤其是类型推导机制），而且这种设计并不会导致通用性的丧失：实际上，在MLstruct中，我们将形如$C \{x = t, \dots\}$的实例化表达式转化为在\(\lambda^-, 18\)范式中表示为$C\{x = t, \dots\} : C[\bar{\alpha}]$的形式，其中所有的\(\bar{\alpha}\)都是“新鲜的”变量；这种转换能够确保所提供的字段确实符合C语言中规定的类型要求。

T-OBJ also requires C to be “final” using the C final judgment (formally defined in the extended version of the paper). This means that C is not extended by any other classes in \(\mathcal{D}\). It ensures that, at runtime, for every class pattern D, pattern-matching scrutinees are always instances of a class \(D'\) that is either a subclass of D (meaning $\#D' \le \#D$) or an unrelated class (meaning $\#D' \le \neg \#D$). Without this property, type preservation would technically not hold. Indeed, consider the program:

T-OBJ还要求C类满足“最终性”这一性质，这一性质需要通过“C是最终类”这一判定标准来加以确认（这一判定标准在论文的扩展版本中得到了正式定义）。这意味着C类不会被\(\mathcal{D}\)集合中的任何其他类所继承或扩展。这一条件能够确保：在程序运行时，对于任意类别模式D来说，所有用于进行模式匹配检验的对象，要么属于D类的子类（即满足“\(\#D' \le \#D\)”这一关系），要么属于与D类无关的类（即满足“\(\#D' \le \neg \#D\)”这一关系）。如果没有这一性质，类型守恒这一原则在技术上就无法得到保证。事实上，以以下程序为例……

Fig. 3. Term typing rules. The full set of typing rules is available in the paper’s extended version.

图3. 术语输入规则。完整的规则集可见于论文的扩展版本中。

class C₁ class C₂: C₁ class C₃ case x = C₁{} of C₂ → C₃{}, _ → x

类C1、类C2：当x属于类C1时，执行C2中的代码并返回结果C3；否则，返回x本身。

This program can be given type \(\neg C_2\) since \(C_1 \le C_2 \lor \neg C_2 \equiv \top\) (in T-CASE3, we pick \(\tau_2 = \neg C_2\)), but it reduces to \(C_1\{}\), which does not have type \(\neg C_2\) because \(C_1\) and \(C_2\) are not unrelated classes.

这个程序可以被赋予类型\(\neg C_2\)，因为\(C_1 \le C_2 \lor \neg C_2 \equiv \top\)（在T-CASE3中，我们选择\(\tau_2 = \neg C_2\)）；然而，该程序实际上会简化为\(C_1\{}\)，而\(C_1\{}\)并不属于类型\(\neg C_2\)，因为\(C_1\)与\(C_2\)并非互不相关的类别。

This finality requirement is merely a technicality of \(\lambda^-\) and it does not exist in MLstruct, where non-final classes can be instantiated. This can be understood as each MLstruct class C implicitly defining a final version \(C^F\) of itself, which is used upon instantiation. So the MLstruct program above would actually denote the following desugared \(\lambda^-\) program:

这种“最终性”的要求只不过是\(\lambda^-\)语言中的一个技术性细节罢了；在MLstruct中并不存在这样的限制，因为在该语言中可以实例化非最终的类。实际上，每一个MLstruct类C都隐含地定义了自己的“最终版本”\(C^F\)，而在进行实例化操作时就会使用这个最终版本。因此，上面的MLstruct程序实际上代表的就是以下这种去掉了语法冗余的\(\lambda^-\)语言程序：

class C₁ class C₁^F: C₁ class C₂: C₁ class C₃ class C₃^F: C₃ case x = C₁{} : C₁ of C₂ → C₃{} : C₃, _ → x

C1类、C1^{F类：属于C1类；C2类：也属于C1类；C3类、C3}F类：属于C3类。
当x等于C1{}时：C1类中的元素；对于C2类中的任意元素，其对应的结果都属于C3{}类；而对于其他所有元素，它们的结果都是x。

The refined program above now evaluates to \(C_1^F\{}\), of type \(C_1^F\), which is a subtype of \(\neg C_2\).

上述经过优化后的程序最终生成的结果是 \(C_1^F\{}\)，其类型为 \(C_1^F\)，而 \(C_1^F\) 实际上是 \(\neg C_2\) 的子类型。

In T-SUBS, we use the current constraining context \(\Xi\) as a subtyping context \(\Sigma\) when invoking the subtyping judgement \(\Xi \vdash \tau_1 \le \tau_2\) (presented in the next subsection), which is possible since the syntax of constraining contexts is a special case of the syntax of subtyping contexts.

在T-SUBS中，我们在调用次类型判定\(\Xi \vdash \tau_1 \le \tau_2\)时，会将当前的约束上下文\(\Xi\)视为一个次类型上下文\(\Sigma\)来使用——这种做法是可行的，因为约束上下文的语法结构其实是次类型上下文语法结构的一种特例。这种判定方法将在下一小节中详细介绍。

Rule T-VAR2 uses the entailment judgment \(\Xi \vdash \sigma \le \neg \forall \epsilon. \tau\) defined in appendix to instantiate the polymorphic type found in the context.

规则T-VAR2使用了附录中定义的“蕴含”判断\(\Xi \vdash \sigma \le \neg \forall \epsilon. \tau\)，来“实例化”上下文中所出现的多态类型。

The typing of instance matching is split over three rules. Rule T-CASE1 specifies that no scrutinee can be matched by a case expression with no branches, which is expressed by assigning type \(\bot\) (the type inhabited by no value) to the scrutinee.

实例匹配的相关规则被分为三条。规则T-CASE1规定：任何被检测的对象都无法通过一个没有任何分支的case表达式来进行匹配；为此，该规则会将类型\(\bot\)（即不存在任何值的类型）分配给被检测的对象。

Rule T-CASE2 handles case expressions with a single, default case, which is equivalent to a let binding, where the body \(t_2\) of the default case is typed within a typing context extended with the case-bound variable \(x\) and the type of the scrutinee. This rule requires the scrutinee to have a class type #C; this is to prevent functions from being matched, because that would technically break preservation in a similar way as described above (since we do not have \(\pi_1 \rightarrow \pi_2 \le \neg \#D\)).

规则T-CASE2用于处理那些仅包含一个默认情况的case表达式；这种表达式等同于一种“let”绑定语句，其中默认情况下的代码块\(t_2\)所在的类型上下文会扩展为包含变量\(x\)以及被检测对象的类型。该规则要求被检测对象必须属于类类型#C，这样就能防止函数与这些case表达式进行匹配——因为从技术层面来讲，这种匹配行为会破坏上述所述的类型保持性原则（毕竟我们并不存在\(\pi_1 \rightarrow \pi_2 \le \neg \#D\)这样的关系）。

T-CASE3 is the more interesting instance matching rule. We first assume that the scrutinee \(t_1\) has some type \(\tau_1\) in order to type the first case branch, and then assume \(t_1\) has type \(\tau_2\) to type the rest

T-CASE3是一种更为有趣的实例匹配规则。首先，我们假设被检查的对象\(t_1\)具有某种类型\(\tau_1\)，这样才能为第一个案例分支确定其类型；随后，我们再假设\(t_1\)具有类型\(\tau_2\)，从而为其余的案例确定它们的类型。

of the instance matching (by reconstructing a smaller case expression binding a new variable x which shadows the old variable occurring in M). Then, we make sure that the scrutinee t₁ can be typed at #C ∧ τ₁ ∨ ¬#C ∧ τ₂, which ensures that if t₁ is an instance of C, then it is also of type τ₁, and if not, then it is of type τ₂. In this rule, τ₁ can be picked to be anything, so assuming Γ·(x : τ₁) to type t₂ is sufficient, and there is no need to assume Γ·(x : τ₁ ∧ #C). If the t₂ branch needs τ₁ to be a subtype of #C, we can always pick τ₁ = τ'₁ ∧ #C. Notice that the required type for t₁ still has the same shape #C ∧ τ₁ ∨ ¬#C ∧ τ₂ ≡ #C ∧ (#C ∧ τ*'₁) ∨ ¬#C ∧ τ₂ ≡ #C ∧ τ*'₁ ∨ ¬#C ∧ τ₂.

在这种情况下，我们通过重构一个较小的case表达式来匹配相应的实例——该表达式会绑定一个新的变量x，这个新变量会“屏蔽”在M中出现的旧变量。随后，我们确保被检查的对象t₁具有类型#C ∧ τ₁ ∨ ¬#C ∧ τ₂；这样一来，如果t₁是类型C的实例，那么它必然也是类型τ₁的；如果不是，那么它就是类型τ₂的。在这个规则中，τ₁可以被指定为任何类型，因此假设Γ·(x : τ₁)使得t₂具有所需类型就已经足够了，没有必要再假设Γ·(x : τ₁ ∧ #C)。如果t₂这个分支要求τ₁必须是类型#C的子类型，那么我们总是可以选择τ₁ = τ'₁ ∧ #C作为解决方案。需要注意的是，t₁所必须具有的类型仍然满足相同的结构：#C ∧ τ₁ ∨ ¬#C ∧ τ₂ ≡ #C ∧ (#C ∧ τ*'₁) ∨ ¬#C ∧ τ₂ ≡ #C ∧ τ*'₁ ∨ ¬#C ∧ τ₂。

4.4 Declarative Subtyping Rules

4.4 声明式子类型规则

The declarative subtyping rules are presented in Figure 4. Remember that the mode syntax ♦ is used to factor in dual formulations. For instance, \(τ \llcorner \top^\diamond\) is to be understood as either \(τ \le \top\) when \(\diamond = \cdot\), i.e., \(τ \le \top\), or as \(τ \llcorner \top^\rightarrow\) when \(\diamond = \searrow\), i.e., \(τ \ge \bot\), also written \(\bot \le \tau\). The purpose of rule S-WEAKEN is solely to make rules which need no context slightly more concise to state. In this paper, we usually treat applications of S-WEAKEN implicitly.

图4展示了这些声明性子类型化规则。需要注意的是，模式语法♦被用来表达这两种不同的表述方式。例如，当\(\diamond = \cdot\)时，\(τ \llcorner \top^\diamond\)应该被理解为\(τ \le \top\)；而当\(\diamond = \searrow\)时，则应将其理解为\(τ \llcorner \top^\rightarrow\)，即\(τ \ge \bot\)，也可写作\(\bot \le \tau\)。规则S-WEAKEN的意义就在于让那些不需要依赖上下文的信息表达得更加简洁明了。在本文中，我们通常会隐含地运用这一规则来进行相关分析。

4.4.1 Subtyping Recursive Types.

A consequence of our syntactic account of subtyping is that we do not define types as some fixed point over a generative relation, as done in, e.g., [Dolan 2017; Pierce 2002]. Instead, we have to account for the fact that we manipulate finite syntactic type trees, in which recursive types have to be manually unfolded to derive things about them. This is the purpose of the S-EXP rules, which substitute a possibly-recursive type with its body to expose one layer of its underlying definition. As remarked by Amadio and Cardelli [1993, §3.2], to

4.4.1 递归类型的子类型化

根据我们对子类型化的句法分析，我们并没有像[Dolan 2017; Pierce 2002]等人那样，将类型定义为某种生成关系下的不动点。相反，我们必须考虑到这样一个事实：我们所操作的实际上是有限的句法类型树，在这类结构中，递归类型需要被手动展开才能从中提取有用的信息。这就是S-EXP规则的作用——这些规则通过用类型的内部结构来替换该类型本身，从而揭示其定义结构中的某一层内容。正如Amadio和Cardelli在[1993, §3.2]中所指出的，这样做……

Fig. 4. Declarative subtyping rules.

图4. 声明式子类型规则。

subtype recursive types, it is not enough to simply allow unfolding them a certain number of times. Moreover, in our system, recursive types may arise from cyclic type variable constraints (which is important for type inference), and thus not be attached to any explicit recursive binders. Thus, we cannot simply follow Castagna [2012, §1.3.4] in admitting a \(\mu\) rule, which would still be insufficient.

对于子类型的递归类型来说，仅仅允许对其进行有限次次的展开是不够的。此外，在我们的系统中，递归类型可能源于循环类型的变量约束（这一点对于类型推导而言非常重要），因此这类递归类型并不会与任何明确的递归绑定器相关联。因此，我们不能简单地模仿Castagna在[2012, §1.3.4]中的做法来允许使用某种\(\mu\)规则，因为这样的做法仍然是不够的。

4.4.2 Subtyping Hypotheses.

We make use of the \(\Sigma\) environment to store subtyping hypotheses via S-ASSUM, to be leveraged later using the S-HYP rule. We should be careful not to allow the use of a hypothesis right after assuming it, which would obviously make the system unsound (as it could derive any subtyping). In the specification of their constraint solving algorithm, Hosoya et al. [2005] use two distinct judgments \(\vdash\) and \(\vdash'\) to distinguish from places where the hypotheses can or cannot be used. We take a different, but related approach. Our S-ASSUM subtyping rule resembles the Löb rule described by Appel et al. [2007], which uses the “later” modality \(▷\) in order to delay the applicability of hypotheses — by placing this symbol in front of the hypothesis being assumed, we prevent its immediate usage by S-HYP. We eliminate \(▷\) when passing through a function or record constructor: the dual \(▷\) symbol is used to remove all \(▷\) from the set of hypotheses, making them available for use by S-HYP. These precautions reflect the “guardedness” restrictions used by Dolan [2017] on recursive types, which prevents usages of \(\alpha\) that are not guarded by \(\rightarrow\) or \(\{ \dots \}\) in a recursive type \(\mu\alpha\). \(\tau\). Such productivity restriction is also implemented by our guardedness check, preventing the definition of types such as type A = A and type A = A (Section 2.1.6).³²

4.4.2 子类型化假设

我们利用\(\Sigma\)环境，通过S-ASSUM来存储子类型化假设，以便后续使用S-HYP规则来处理这些假设。需要注意的是，我们不能在刚提出某个假设就立即允许使用它，因为这样做显然会使得系统变得不稳定（因为系统可能会根据这个假设推导出任何类型的子类型）。在Hosoya等人[2005]对他们的约束求解算法所做的规定中，他们使用了两种不同的判断符号\(\vdash\)和\(\vdash'\)，来区分那些可以或不可以使用假设的情形。我们采取了另一种类似的方法。我们的S-ASSUM子类型化规则与Appel等人[2007]描述的Löb规则颇为相似——后者也使用了“后续”模态符号\(▷\)来延迟假设的可适用性；通过将这个符号放在被假设的命题前面，我们可以防止S-HYP规则立即使用该假设。当代码穿过函数或记录构造函数时，我们会删除这些\(▷\)符号；而对应的\(▷^*\)符号则会用来移除假设集合中所有的\(▷\)符号，从而使这些假设可以被S-HYP规则使用。这些预防措施实际上体现了Dolan[2017]在处理递归类型时所提出的“谨慎性”要求——这种要求能够防止在递归类型\(\mu\alpha \tau\)中，出现那些没有被\(\rightarrow\)或\(\{ \dots \}\)之类的结构所约束的\(\alpha\)的使用情况。我们的谨慎性检查机制也实现了类似的限制，从而避免了诸如type A = A或type A = A这样的类型定义（详见第2.1.6节）。³³

4.4.3 A Boolean Algebra.

The subtyping preorder in \(\lambda^-\) gives rise to a Boolean lattice or algebra when taking the equivalence relation \(\tau_1 \equiv \tau_2\) to be the relation induced by \(\tau_1 \le \tau_2\) and \(\tau_2 \le \tau_1\). To see why, let us inspect the standard way of defining Boolean algebras, which is as the set of complemented distributive lattices. We can define a lattice equivalently as either:

4.4.3 布尔代数

在 \(\lambda^-\) 中，子类型排序关系会形成一种布尔格或布尔代数；当我们将等价关系 \(\tau_1 \equiv \tau_2\) 视为由 \(\tau_1 \le \tau_2\) 与 \(\tau_2 \le \tau_1\) 引导出来的关系时，这一结论尤为明显。为了理解其中的原因，让我们来看看定义布尔代数的传统方法：即将其定义为具有补运算且符合分配律的格结构。实际上，我们也可以用另一种方式来等价地定义这种格结构……

• An algebra \(\langle L, \wedge, \vee \rangle\) such that \(\wedge\) and \(\vee\) are idempotent, commutative, associative, and satisfy the absorption law, i.e., \(\tau \wedge (\tau \vee \pi) = \tau \vee (\tau \wedge \pi) = \tau\). Then \(\tau_1 \le \tau_2\) is taken to mean \(\tau_1 = \tau_1 \wedge \tau_2\) or (equivalently) \(\tau_1 \vee \tau_2 = \tau_2\).

• A partially-ordered set \(\langle L, \le \rangle\) (i.e., \(\le\) is reflexive, transitive, and antisymmetric) where every two elements \(\tau_1\) and \(\tau_2\) have a least upper bound \(\tau_1 \vee \tau_2\) (supremum) and a greatest lower bound \(\tau_1 \wedge \tau_2\) (infimum). That is, \(\forall \pi \le \tau_1, \tau_2\). \(\pi \le \tau_1 \wedge \tau_2\) and \(\forall \pi \ge \tau_1, \tau_2\). \(\pi \ge \tau_1 \vee \tau_2\).

• 一种代数结构\(\langle L, \wedge, \vee \rangle\)，其中运算符\(\wedge\)和\(\vee\)满足幂等性、交换律、结合律，并且符合吸收律，即\(\tau \wedge (\tau \vee \pi) = \tau \vee (\tau \wedge \pi) = \tau\)。在这种情况下，当表示“\(\tau_1 \le \tau_2\)”时，意味着\(\tau_1 = \tau_1 \wedge \tau_2\)，或者等价地，\(\tau_1 \vee \tau_2 = \tau_2\)。

• 一个偏序集\(\langle L, \le \rangle\)（即关系\(\le\)满足自反性、传递性和反对称性），在这个集合中，任意两个元素\(\tau_1\)和\(\tau_2\)都存在最小上界\(\tau_1 \vee \tau_2\)以及最大下界\(\tau_1 \wedge \tau_2\)。也就是说，对于所有的\(\pi\)，都有\(\pi \le \tau_1 \wedge \tau_2\)，并且\(\pi \ge \tau_1 \vee \tau_2\)。

The latter is most straightforward to show: we have reflexivity by S-REFL, transitivity by S-TRANS, antisymmetry by definition of \(\equiv\), and the supremum and infimum properties are given directly by S-ANDOR2. and S-ANDOR2\(\vdash\) respectively.

后一点最为直观易懂：根据S-REFL性质，我们可以证明反射性；根据S-TRANS性质，可以证明传递性；而根据\(\equiv\)的定义，显然可以得出反称性。至于最大值和最小值的性质，则分别由S-ANDOR2直接得出的，同时也可以通过S-ANDOR2\(\vdash\)这一推理规则来验证其正确性。

Moreover, to be a Boolean algebra, our lattice needs to be:

此外，要想构成一个布尔代数，我们的格结构必须满足以下条件：

• a complemented lattice, which is

  • bounded: \(\top\) and \(\bot\) are respective least and greatest elements (S-TOB\(\diamond\));
  • such that every \(\tau\) has a complement \(\neg\tau\) where \(\tau \vee \neg\tau = \top\) and \(\tau \wedge \neg\tau = \bot\) (S-COMPL\(\diamond\));³⁴

• a distributive lattice, meaning that \(\tau \wedge^\diamond (\tau_1 \vee^\diamond \tau_2) = (\tau \wedge^\diamond \tau_1) \vee^\diamond (\tau \wedge^\diamond \tau_2)\) for \(\diamond \in \{\nvDash, \cdot\}\).

• 一个“补集完备的格”：
  – 它是有界的，即\(\top\)和\(\bot\)分别是最小元素和最大元素（满足S-TOB\(\diamond\)条件）；
  – 对于其中的任意元素\(\tau\)，都存在其补集\(\neg\tau\)，使得\(\tau \vee \neg\tau = \top\)且\(\tau \wedge \neg\tau = \bot\)（满足S-COMPL\(\diamond\)条件）。³⁵
  

• 一个“分配律完备的格”：这意味着对于任意属于集合\(\{\nvDash, \cdot\}\)的运算符号\(\diamond\)，都有\(\tau \wedge^\diamond (\tau_1 \vee^\diamond \tau_2) = (\tau \wedge^\diamond \tau_1) \vee^\diamond (\tau \wedge^\diamond \tau_2)\)。

The first direction \(\leq^\diamond\) of distributivity is given directly by S-DISTRIB. The other direction \(\geq^\diamond\) is admissible: since \(\tau_1 \vee^\diamond \tau_2 \geq^\diamond \tau_1\) (S-ANDOR11\(\diamond\)) and \(\tau_1 \vee^\diamond \tau_2 \geq^\diamond \tau_2\) (S-ANDOR12\(\diamond\)), we can easily derive \(\tau \wedge^\diamond (\tau_1 \vee^\diamond \tau_2) \geq^\diamond \tau \wedge^\diamond \tau_1\) and \(\tau \wedge^\diamond (\tau_1 \vee^\diamond \tau_2) \geq^\diamond \tau \wedge^\diamond \tau_2\), and by (S-ANDOR2\(\diamond\)) we conclude that \(\tau \wedge^\diamond (\tau_1 \vee^\diamond \tau_2) \geq^\diamond (\tau \wedge^\diamond \tau_1) \vee^\diamond (\tau \wedge^\diamond \tau_2)\).

分配律的第一个方向“\(\leq^\diamond\)”可以直接通过规则S-DISTRIB得出。另一个方向“\(\geq^\diamond\)”也是成立的：由于\(\tau_1 \vee^\diamond \tau_2 \geq^\diamond \tau_1\)（规则S-ANDOR11\(\diamond\)）以及\(\tau_1 \vee^\diamond \tau_2 \geq^\diamond \tau_2\)（规则S-ANDOR12\(\diamond\)），我们可以很容易地推导出\(\tau \wedge^\diamond (\tau_1 \vee^\diamond \tau_2) \geq^\diamond \tau \wedge^\diamond \tau_1\)和\(\tau \wedge^\diamond (\tau_1 \vee^\diamond \tau_2) \geq^\diamond \tau \wedge^\diamond \tau_2\)；而根据规则S-ANDOR2\(\diamond\)，我们还可以得出结论：\(\tau \wedge^\diamond (\tau_1 \vee^\diamond \tau_2) \geq^\diamond (\tau \wedge^\diamond \tau_1) \vee^\diamond (\tau \wedge^\diamond \tau_2)\)。

A useful property of Boolean algebras is that the usual De Morgan's laws hold, which will allow us to massage constraints into normal forms during type inference.

布尔代数的一个重要性质是，通常的德摩根定律在布尔代数中同样成立。这一性质使得我们能够在类型推导的过程中将各种约束条件转化为标准形式。

4.4.4 Algebraic Rules. We call S-FUNMRG and S-RCDTOP algebraic subtyping rules because they do not follow from a set-theoretic interpretation of order connectives (\(\wedge\), \(\vee\), \(\neg\)). S-FUNMRG and S-RCDMRG respectively make function and record types lattice homomorphisms,³⁶ which is required to make type inference complete — this allows the existence of well-behaved normal forms. Though one can still think of types as sets of values, as in the semantic subtyping approach, in \(\lambda^{-}\) the sets of values of \(\tau_1 \wedge \tau_2\) is not the intersection of the sets of values of \(\tau_1\) and \(\tau_2\) (unless \(\tau_1\) and \(\tau_2\) are nominal tags or records), and similarly for unions and complements. These algebraic rules are sound in \(\lambda^{-}\) because of the careful use we make of unions and intersections, e.g., not using intersections to encode overloading. Notably, S-RCDTOP implies surprising relationships like \(\neg(\tau_1 \to \tau_2) \le \{x : \pi\}\) and \(\neg\{x : \pi\} \le \{y : \pi\}\) (\(x \ne y\)), exemplifying that negation in \(\lambda^{-}\) is essentially algebraic.

4.4.4 代数规则。我们将S-FUNMRG和S-RCDTOP称为“代数”子类型规则，因为这些规则并不能通过基于集合论的解释来理解顺序连接词（\(\wedge\)、\(\vee\)、\(\neg\)）的含义而得出。S-FUNMRG使得函数类型和记录类型成为格同态³⁷，而这一点对于实现完整的类型推导机制是必不可少的——只有这样，才能确保存在行为规范的规范形式。尽管人们仍然可以将类型视作值集合，就像在“语义子类型”方法中所做的那样，但在\(\lambda^{-}\)中，\(\tau_1 \wedge \tau_2\)的值集合并非 \(\tau_1\)与\(\tau_2\)的值集合的交集（除非\(\tau_1\)和\(\tau_2\)是符号标签或记录类型），对于并集和补集也是如此。由于我们在使用并集和交集时十分谨慎——例如，不会用交集来表示重载现象——因此这些代数规则在\(\lambda^{-}\)中是成立的。值得注意的是，S-RCDTOP还揭示了一些令人惊讶的关系，比如\(\neg(\tau_1 \to \tau_2) \le \{x : \pi\}\)以及\(\neg\{x : \pi\} \le \{y : \pi\}\)（其中\(x \ne y\)），这些例子充分说明了在\(\lambda^{-}\)中，否定操作本质上属于代数性质。

4.5 Soundness of the Declarative Type System

4.5 声明型语法系统的正确性

We now state the main soundness theorems for \(\lambda^{-}\)'s type system, proven in the extended version of this paper. In the following, \(\vdash^* P\) is used as the syntax for program-typing judgments.

我们现在陈述本文扩展版本中证明的、关于\(\lambda^{-}\)类型系统的主要正确性定理。在后续内容中，符号\(\vdash^* P\)被用来表示“程序”类型判定的语法形式。

THEOREM 4.1 (PROGRESS). If \(\vdash^* P : \tau\) and \(P\) is not a value, then \(\vdash P \rightsquigarrow P'\) for some \(P'\).

定理 4.1（进展性）。 如果 \(\vdash^* P : \tau\)，且 \(P\) 并不表示某个具体的值，那么存在某个 \(P'\) 使得 \(\vdash P \rightsquigarrow P'\)。

THEOREM 4.2 (PRESERVATION). If \(\vdash^* P : \tau\) and \(\vdash P \rightsquigarrow P'\), then \(\vdash^* P' : \tau\).

定理4.2（保持性）。 如果 \(\vdash^* P : \tau\) 且 \(\vdash P \rightsquigarrow P'\)，那么 \(\vdash^* P' : \tau\)。

5 PRINCIPAL TYPE INFERENCE FOR \(\lambda^{-}\)

关于 \(\lambda^{-}\) 的五种主要类型推理方法

We now formally describe the type inference algorithm which was presented in Section 3.

我们现在正式描述一下第3节中介绍的那种类型推导算法。

5.1 Type Inference Rules

5.1 类型推断规则

Our type inference rules are presented in Figure 5. The judgments \(\Gamma \vdash^* P : \tau \Rightarrow \Xi\) and \(\Xi, \Gamma \vdash t : \tau \Rightarrow \Xi\) are similar to their declarative typing counterparts, except that they are algorithmic and produce constraining contexts \(\Xi\) containing inferred type variables bounds.

我们的类型推断规则在图5中进行了说明。判断式\(\Gamma \vdash^* P : \tau \Rightarrow \Xi\)以及\(\Xi, \Gamma \vdash t : \tau \Rightarrow \Xi\)与它们对应的声明性类型推导规则相似，只不过这些判断式属于算法性质的，并且会生成包含推断出的类型变量取值范围的限制性上下文\(\Xi\)。

We give the following formal meaning to premises of the form '\(\alpha\) fresh', and in the rest of this paper, we implicitly only consider well-formed derivations:

我们为形如“\(\alpha\) 新鲜”这样的前提赋予了如下形式化的含义；在本文的其余部分，我们所讨论的内容仅限于那些格式正确、结构合理的推导过程。

Definition 5.1 (Well-formed derivations). A type inference or constraining derivation is said to be well-formed if, for every \(\alpha\), the '\(\alpha\) fresh' premise appears at most once in the entire derivation and, if it does, \(\alpha\) does not occur in any user-specified type (i.e., on the right of ascription trees '\(t : \tau\)').

定义5.1（形式正确的推导）。 如果对于任意符号\(\alpha\)来说，在整个推导过程中，“\(\alpha\)是‘新鲜的’”这一前提至多出现一次，并且当它确实出现时，\(\alpha\)也不会出现在任何用户指定的类型中（即不会出现在赋值表达式“\(t : \tau\)”的右侧），那么这样的类型推断或推导过程就被认为是形式正确的。

The program-typing inference rules I-BODY and I-DEF mirror their declarative counterparts. In I-DEF, notice how the output context corresponding to the definition's body is the one used to quantify the corresponding type in the typing context.

我-BODY和I-DEF这两种与程序类型推断相关的规则，其形式与它们对应的声明性规则完全一致。在I-DEF中，请注意：定义的主体部分所对应的环境，正是用于在类型推理环境中确定相应类型的那个环境。

The main difference between type inference rules and declarative typing rules is that in the former, we immediately produce a type for each subexpression irrelevant of its context, using type variables for local unknowns, and we then use a constraining judgement \(\Sigma \vdash \tau \ll \pi \Rightarrow \Xi\) (explained in the next subsection) to make sure that the inferred type \(\tau\) conforms to the expected type \(\pi\) in this context. So whenever we need to guess a type (such as the type of a lambda's parameter in I-ABS), we simply introduce a fresh type variable. As an example, in I-PROJ, we infer an unconstrained type \(\tau\) for the field projection's prefix \(t\), and then make sure that this is a subtype of a record type by constraining \(\Xi_0 \vdash \tau \ll \{x : \alpha\} \Rightarrow \Xi_1\) — where \(\Xi_1\) is the output context containing the type variable bounds necessary to make this relationship hold. Rules I-APP, I-ASC, I-CASE1, I-CASE2, and I-CASE3 all work according to the same principles, threading the set of constraining contexts currently inferred through the next type inference steps, which is necessary to make sure that all inferred type variable bounds are consistent with each other. Rule I-VAR2 refreshes all the variables

类型推断规则与声明性类型规则之间的主要区别在于：在前者中，我们会为每个子表达式立即确定其类型，而无需考虑该子表达式的上下文环境；我们会使用类型变量来表示那些在当前上下文中尚未确定的未知类型，然后通过某种“约束性判断”（具体内容将在下一个小节中说明）来确保推断出的类型确实符合预期的类型要求。因此，每当我们需要猜测某个类型的值时（例如在I-ABS模型中判断lambda表达式参数的类型时），我们只需引入一个新的类型变量即可。举个例子，在I-PROJ模型中，我们会先为字段投影操作前的前缀部分推断出一个未受约束的类型\(\tau\)，然后通过约束性判断\(\Xi_0 \vdash \tau \ll \{x : \alpha\} \Rightarrow \Xi_1\)来确保这个类型是某个记录类型的子类型——其中\(\Xi_1\)表示包含使这种类型关系成立所必需的所有类型变量限制条件的上下文环境。I-APP、I-ASC、I-CASE1、I-CASE2和I-CASE3这些规则都是按照相同的原理工作的：它们会将目前已经推断出的所有约束性上下文信息串联起来，引导后续的类型推断过程继续进行，从而确保所有推断出的类型变量限制条件之间能够保持一致性。而I-VAR2规则则会“刷新”所有已经被引入的类型变量及其相关的限制条件。

Fig. 5. Algorithmic type inference rules.

图5. 算法类型推断规则。

of a type \(\forall \Xi. \tau\) obtained from the typing context, which includes both variables that occur in the constraining context \(\Xi\) as well as those that occur in the underlying type \(\tau\), even when some of the latter may not be mentioned in \(\Xi\); indeed, in \(\lambda^-\) all type variables are implicitly quantified.

这种类型\(\forall \Xi. \tau\)是从类型指定上下文中得出的，该上下文既包括了那些出现在限制性上下文\(\Xi\)中的变量，也包括了那些出现在基础类型\(\tau\)中的变量——即便其中有些变量在\(\Xi\)中并未被明确提及；事实上，在\(\lambda^-\)类型系统中，所有类型变量都经过了隐式的量化处理。

5.2 Reduced Disjunctive Normal Forms

5.2 简化析取范式

To facilitate constraint solving, it is useful to massage types into a normal form which we call RDNF, for reduced disjunctive normal form. This normal form is similar to a classical disjunctive normal form (DNF) except that we reduce all “incompatible” intersections and unions to \(\perp\) and \(\top\) respectively. Here, incompatible means that the type holds no useful information, either because it is inhabited by no value or because it cannot be used meaningfully, as explained in Section 2.2.2.

为了便于进行约束满足问题的求解，将类型转化为一种我们称之为“简化析取范式”的标准形式是非常有用的。这种标准形式与传统意义上的析取范式类似，不同之处在于：我们会将所有“不兼容”的交集和并集分别转化为\(\perp\)和\(\top\)。所谓“不兼容”，是指这类类型包含没有实用价值的信息——要么是因为它们不包含任何有效的值，要么就是因为它们无法被合理地运用，这一点在2.2.2节中有详细解释。

The syntax of RDNF is given below. It is indexed by a level \(n\) and there are two possible levels: level-0 RDNF, written \(D^0\) does not contain any occurrence of class or alias types at the top level (they will have been expanded); whereas level-1 RDNF, written \(D^1\), allows them. Notation: we will often write \(D\) as a shorthand for \(D^1\) (and similarly for the other indexed syntax forms).

RDNF的语法结构如下所述。该语法结构会根据层级\(n\)进行分类，其中存在两种不同的层级：层级0的RDNF，记为\(D^0\)，在顶层不允许出现类或别名类型的元素（这些元素会在后续被展开处理）；而层级1的RDNF，记为\(D^1\)，则允许出现这类元素。注记：我们通常会将\(D\)作为\(D^1\)的简写形式来使用（其他带有层次编号的语法结构也是如此）。

\[ \begin{align*} D^n &::= \bot | C^n | D^n \lor C^n & C^n &::= I^n \land \neg U^n | C^n \land \alpha | C^n \land \neg \alpha \\ I^1 &::= I^0 | I^1 \land N[\overline{D^1}] & I^0 &::= \mathcal{I}^N[\mathcal{N}] | \mathcal{I} \rightarrow [\mathcal{F}] | \mathcal{I}^{}[\mathcal{R}] \\ U^1 &::= U^0 | U^1 \lor N[\overline{D^1}] & U^0 &::= \bot | D^1 \rightarrow D^1 | \{x : D^1\} | U^0 \lor \#C \end{align*} \]

where the I· contexts stand for combinations of nominal tags N, functions F, and records R:

其中，I·上下文代表名词标签N、函数F以及记录R的组合。

\[ \begin{align*} \mathcal{I}^N[\Box] &::= \Box \wedge \mathcal{F} \wedge \mathcal{R} & \mathcal{N} &::= \top | \#C & \mathcal{I}[\Box] &::= \mathcal{I}^N[\Box] | \mathcal{I} \rightarrow [\Box] | \mathcal{I}^{}[\Box] \\ \mathcal{I} \rightarrow [\Box] &::= \mathcal{N} \wedge \Box \wedge \mathcal{R} & \mathcal{F} &::= \top | D^1 \rightarrow D^1 & \top^3 &::= \top \wedge \top \wedge \top \\ \mathcal{I}^{}[\Box] &::= \mathcal{N} \wedge \mathcal{F} \wedge \Box & \mathcal{R} &::= \top | \{\overline{x : D^1}\} \end{align*} \]

As an example, '\(D_1 = \#C \wedge \top \wedge \{x : \top\} \wedge C[\text{Int, Bool}] \wedge A[\text{Str}] \wedge \neg \bot \wedge \neg \alpha\)' is a valid level-1 RDNF, but not a valid level-0 one because \(C[\text{Int, Bool}]\) and \(A[\text{Str}]\) occur at the top level and are not expanded, while '\(D_2^n = \top \wedge \top \wedge \{x : C[\text{Int, Bool}]\} \wedge \neg \bot\)' is well-defined for both \(n \in \{0, 1\}\).

例如，‘\(D_1 = \#C \wedge \top \wedge \{x : \top\} \wedge C[\text{Int, Bool}] \wedge A[\text{Str}] \wedge \neg \bot \wedge \neg \alpha\)’是一个有效的1级RDNF表达式，但不是一个有效的0级RDNF表达式，因为\(C[\text{Int, Bool}]\)和\(A[\text{Str}]\)出现在顶层且没有被展开；而‘\(D_2^n = \top \wedge \top \wedge \{x : C[\text{Int, Bool}]\} \wedge \neg \bot\)’对于所有\(n \in \{0, 1\}\)来说都是一个明确定义的表达式。

5.2.1 Algorithm. Figures 6 and 7 give an algorithm to convert types \(\tau\) to level-\(n\) RDNFs, written \(dnf^n(\tau)\). The task is essentially straightforward, if relatively tedious. Essentially, \(dnf^n\) pushes negations in using DeMorgan laws, distributes intersections over unions, and at the same time ensures that all constructed conjunctions are de-duplicated and as reduced as possible, so that for instance intersections of unrelated classes are reduced to \(\bot\) and function and record types are merged with themselves. We write \((\neg)\tau\) as a shorthand for either \(\tau\) or \(\neg\tau\) (used uniformly in a rule) and make use of auxiliary functions \(\text{union}^n(D^n, D^n)\) and \(\text{inter}^n(D^n, D^n)\), which rely on the following context definitions \(S^+[\cdot]\) and \(S^-[\cdot]\), used to “dig into” the various shapes of \(C^n\) syntaxes:

5.2.1 算法。图6和图7展示了一种将类型\(\tau\)转换为第\(n\)层RDNF的算法，该转换结果记为\(dnf^n(\tau)\)。这一过程本质上是直接可行的，尽管具体实现起来可能较为繁琐。本质上，\(dnf^n\)会运用德摩根定律来处理否定运算，将交集运算分配到并集运算上，并同时确保所有构建出的合取式都是去重过的且尽可能简化；例如，不相关的类之间的交集会被简化为\(\bot\)，函数类型与记录类型也会被合并为同一类型。我们用\((\neg)\tau\)这一简写形式来表示\(\tau\)或\(\neg\tau\)（在规则中始终使用这种写法），同时还会借助辅助函数\(\text{union}^n(D^n, D^n)\)和\(\text{inter}^n(D^n, D^n)\)来进行运算；这些辅助函数依赖于以下上下文定义\(S^+[\cdot]\)和\(S^-[\cdot]\)，它们用于帮助我们分析\(C^n\)语法结构的各种表现形式。

\[ \begin{align*} S^+[\Box] &::= \mathcal{I}[\Box] | S^+[\Box] \wedge \alpha | S^+[\Box] \wedge \neg \alpha | S^+[\Box] \wedge \neg U | S^+[\Box] \wedge N[\overline{D^1}] \\ S^-[\Box] &::= S^-[\Box] \wedge \alpha | S^-[\Box] \wedge \neg \alpha | I \wedge \neg S^-[\Box] \\ S^-[\Box] &::= \Box | S^-[\Box] \lor N[\overline{D^1}] | S^-[\Box] \lor \#C | U \lor \Box \end{align*} \]

For example, we can decompose \(C^n = I^n \wedge \neg((D_1^n \rightarrow D_2^n) \vee \#C) \wedge \alpha\) as \(C^n = S^-[D_1^n \rightarrow D_2^n]\) where \(S^-[\Box] = I^n \wedge \neg(\Box \vee \#C) \wedge \alpha\).

例如，我们可以将表达式 \(C^n = I^n \wedge \neg((D_1^n \rightarrow D_2^n) \vee \#C) \wedge \alpha\) 分解为 \(C^n = S^-[D_1^n \rightarrow D_2^n]\)，其中 \(S^-[\Box] = I^n \wedge \neg(\Box \vee \#C) \wedge \alpha\)。

The algorithm is well-defined on well-formed types \(\tau\) wf$, assuming a well-formed declarations context \(\mathcal{D}\) wf. These notions of well-formedness are defined formally in the extended paper version.

在假设声明上下文 \(\mathcal{D}\) 是格式正确的条件下，该算法对于那些格式正确的类型 \(\tau\) 是完全可定义的。关于“格式正确”这一概念，其正式定义详见扩展版的论文内容。

LEMMA 5.2 (WELL-DEFINED dnf). If \(\mathcal{D}\) wf, \(\tau\) wf, and \(n \in \{0, 1\}\), then \(dnf^n(\tau) = D^n\) for some \(D^n\).

引理5.2（定义良好的dnf）。如果\(\mathcal{D}\)是良定的，\(\tau\)也是良定的，并且\(n \in \{0, 1\}\)，那么对于某个\(D^n\)来说，有\(dnf^n(\tau) = D^n\)。

LEMMA 5.3 (CORRECTNESS OF dnf). For all \(\tau\), \(n \in \{0, 1\}\), and \(D^n = dnf^n(\tau)\), we have \(\tau \equiv D^n\).

引理5.3（dnf的正确性）。对于任意\(\tau\)、\(n \in \{0, 1\}\)，以及\(D^n = dnf^n(\tau)\)，我们有\(\tau \equiv D^n\)。

5.3 Type Constraining Rules

5.3 类型约束规则

The type constraining rules are defined in Figure 8. They are defined for any pairs of types and input subtyping contexts, returning an output context containing err in case the constraining fails. We need err cases to distinguish an infinite loop in the algorithm from a subtype constraining error, i.e., we want to justify that we have a proper algorithm and not just a semi-algorithm.

类型约束规则在图8中有所规定。这些规则适用于任意类型的组合以及输入的子类型限定上下文；当约束操作失败时，这些规则会返回一个包含err元素的输出结果。我们需要这种err情况，以便区分算法中的无限循环与子类型限定错误——这样我们才能证明自己所设计的确实是一个完整的算法，而不仅仅是一个半成品算法。

In top-level constraining judgments, of the form \(\Sigma \vdash \tau \llcorner \tau \Rightarrow \Xi\), we check whether a subtyping relationship is currently in the assumptions; if not, we extend the set of assumptions with the current constraint (protected by a \(\triangleright\)) and call the nested constraining rules with the two sides \(\tau_1\) and \(\tau_2\) merged into a single \(dnf^0(\tau_1 \wedge \neg \tau_2)\) normal form.³⁸ Nested constraining judgments have syntax \(\Sigma \vdash D^0 \Rightarrow \Xi\); they implicitly solve the constraint \(D^0 \le \bot\). We can do this because for all \(\tau_1\) and \(\tau_2\), the subtyping relationship \(\Sigma \vdash \tau_1 \le \tau_2\) is formally equivalent to \(\Sigma \vdash \tau_1 \wedge \neg \tau_2 \le \bot\). This technique was inspired by Pearce [2013], who also puts constraints into this form to solve subtyping problems involving unions, intersections, and negations. Our constraining rules are deterministic except for C-VAR1 and C-VAR2. By convention, we always pick C-VAR1 in case both can be applied.

在形式为 \(\Sigma \vdash \tau \llcorner \tau \Rightarrow \Xi\) 的高级约束判断中，我们会检查当前的假设集合中是否已经包含了某种子类型关系；如果没有，就会将这个新的约束条件添加到假设集合中（该约束条件会被用 \(\triangleright\) 符号标出），然后调用那些涉及 \(\tau_1\) 和 \(\tau_2\) 这两项内容的嵌套约束规则，将这些规则所描述的逻辑形式合并为一种 \(dnf^0(\tau_1 \wedge \neg \tau_2)\) 的标准形式。³⁹ 嵌套约束判断的语法结构为 \(\Sigma \vdash D^0 \Rightarrow \Xi\)；这类判断实际上是在隐式地满足条件 \(D^0 \le \bot\)。我们之所以能够这样做，是因为对于任意的 \(\tau_1\) 和 \(\tau_2\) 来说，子类型关系 \(\Sigma \vdash \tau_1 \le \tau_2\) 在形式上等同于 \(\Sigma \vdash \tau_1 \wedge \neg \tau_2 \le \bot\)。这种处理方法的灵感来源于 Pearce [2013] 的研究——他也将约束条件转化为这种形式，以便解决那些涉及并集、交集以及否定操作的语法问题。除了 C-VAR1 和 C-VAR2 之外，我们制定的所有约束规则都是确定性的；按照惯例，当这两种规则都可以被应用时，我们总会选择 C-VAR1 来进行后续处理。

Fig. 6. Normal form construction algorithm.

图6. 标准形式的构建算法。

Definition 5.4 (Upper and lower bounds). We use the following definitions of lower and upper bounds \(lb_Ξ(α)\) and \(ub_Ξ(α)\) of a type variable \(α\) inside a constraining context \(Ξ\):

定义5.4（上界与下界）。 在受限上下文Ξ中，我们对类型变量α的定义如下：下界表示为lb_Ξ(α)，上界表示为ub_Ξ(α)。

Notice how the C-VAR1/2 rules solve tricky constraints involving type variables by moving the rest of a type expression to the other side of the inequality, relying on negation types and on the properties of Boolean algebras. Moreover, C-VAR1/2 look up the existing bounds of the type variable being constrained and perform a recursive call to ensure that the new bound is consistent with these existing ones. This is required to ensure we only produce consistent output contexts, and it explains why we have to thread constraining contexts throughout all type inference derivations. As part of this recursive call, we extend the subtyping assumptions context with the bound being recorded. For example, C-VAR2 recurses with context \(Σ·(C ≤ α)\) instead of just \(Σ\). This is crucial

请注意，C-VAR1/2规则是如何通过将类型表达式的其余部分移到不等式的另一侧，并利用否定类型的特性以及布尔代数的性质来处理那些涉及类型变量的复杂约束条件的。此外，C-VAR1/2会查找被约束的类型变量已有的取值范围，并进行递归调用，以确保新的取值范围与这些现有范围保持一致。这样做是为了保证我们得到的结果始终是合理的、一致的；这也解释了为什么在所有的类型推导过程中，我们都必须将那些涉及类型变量的约束条件贯穿于整个推导过程之中。在这种递归调用过程中，我们会将新的取值范围记录下来，并更新原有的子类型推理假设环境。例如，C-VAR2在进行递归处理时，会使用包含“C ≤ α”这一约束条件的环境来进行推导，而不仅仅是原来的\(Σ\)环境——这一点至关重要。

Fig. 7. Normal form construction algorithm (continued).

图7. 正规形式构建算法（续）。

Fig. 8. Normal form constraining rules.

图8. 正规形式约束规则。

for two reasons: First, it is possible that new upper bounds \(\tau_i\) be recorded for \(\alpha\) as part of the recursive call. By adding C to the current lower bounds of \(\alpha\) within the recursive call, we make sure that any such new upper bounds \(\tau_i\) will be checked against C as part of the resulting \(lb_\Sigma(\alpha) \ll \tau_i\) constraining call performed when adding bound \(\tau_i\). Second, it is quite common for type inference to result in direct type variable bound cycles, such as \(\alpha \le \beta\), \(\beta \le \alpha\), which can for instance arise from constraining \(\beta \to \beta \le \alpha \to \alpha\). These cycles do not lead to divergence of type inference thanks to the use of \(\Sigma \cdot (C \le \alpha)\) instead of \(\Sigma\) in the recursive call, ensuring that any constraint resulting from a type variable bound cycle will end up being caught by C-HYP.

原因有两条：首先，在递归调用过程中，很可能为变量\(\alpha\)记录新的上界值\(\tau_i\)。通过在递归调用中将这些新上界值加到现有的下界值中，我们可以确保在后续生成约束表达式lb_\Sigma(\alpha) \ll \tau_i时，这些新上界值会与常量C进行比较。其次，在类型推导过程中，经常会出现直接的类型变量约束循环，例如\(\alpha \le \beta\)、\(\beta \le \alpha\)这样的关系——这类循环可能源于对类型变量\(\beta\)的约束被表达为β \to β \le α \to α的形式。由于在递归调用中使用了Σ \cdot (C \le α)而不是单纯的Σ，这些循环并不会导致类型推导过程出现错误；因为这种结构能够确保所有由类型变量约束循环产生的约束条件最终都会被常量C捕获并进行检查。

The other constraining rules are fairly straightforward. The “beauty” of the RDNF is that it essentially makes constraint solving with \(\lambda^-\) types obvious. In each case, there is always an obvious choice to make: either (1) the constraint is unsatisfiable (for example with \(\top \le \bot\) in C-NOTBOT, which yields an err); or (2) the constraint needs to unwrap an irrelevant part of the type to continue (for example with \(D_1 \to D_2 \le U \lor \#C\) in C-CLS3, which can be solved iff \(D_1 \to D_2 \le U\) itself can be solved, because function types are unrelated to nominal class tags); or (3) we can solve the constraint in an obvious, unambiguous way (for example with \(\{x : D_x^{x \in S}\} \le \{y : D\}\) where \(y \in S\) in C-RCD1).

其他一些约束规则其实也相当直观易懂。RDNF的真正优点在于：它使得利用\(\lambda^-\)类型来进行约束求解变得显而易见。在每种情况下，总存在一种显而易见的处理方式：要么（1）该约束本身就不满足条件（例如，在C-NOTBOT中，当\(\top \le \bot\)时就会产生错误结果）；要么（2）该约束需要剔除类型结构中那些无关的部分才能继续被处理（例如，在C-CLS3中，对于表达式\(D_1 \to D_2 \le U \lor \#C\)来说，只有当\(D_1 \to D_2 \le U\)这一部分能够被解决时，整个问题才有可能得到解答——因为函数类型与命名类标签其实是没有关联的）；要么（3）我们可以用一种显而易见且不会产生歧义的方法来解决该约束（例如，在C-RCD1中，对于表达式\(\{x : D_x^{x \in S}\} \le \{y : D\}\)来说，只要\(y \in S\)，这个约束就能被直接解决）。

Normalizing types deeply (i.e., not solely on the outermost level) makes the termination of constraining straightforward. If we did not normalize nested types and for example merged \(\{x : \tau_1\} \land \{x : \tau_2\}\) syntactically as \(\{x : \tau_1 \land \tau_2\}\), constraining recursive types in a way that repetitively merges the same type constructors together could lead to unbounded numbers of equivalent types being constrained, such as \(\{x : \tau_1 \land \tau_1 \land \tau_1 \land \dots\}\), failing to terminate by C-HYP.

对嵌套类型进行深度规范化处理（而不仅仅是在最外层层面进行规范化）可以让类型的约束过程变得更加简洁明了。如果我们不对嵌套类型进行规范化处理，例如不把 \(\{x : \tau_1\} \land \{x : \tau_2\}\) 在语法上合并为 \(\{x : \tau_1 \land \tau_2\}\)，那么在对递归类型进行约束时，如果反复将相同的类型构造器合并在一起，就可能会导致出现数量无限多的等价类型被同时纳入约束范围，例如 \(\{x : \tau_1 \land \tau_1 \land \tau_1 \land \dots\}\) 这样的类型。在这种情况下，C-HYP规则就无法保证约束过程能够正常终止。

Example. Consider the constraint \(\tau = \{x : \text{Nat}, y : \text{Nat}\} \ll \pi = \{x : \text{Int}, y : \top\}\). After adding the pair to the set of hypotheses, C-Assum computes the RDNF \(dnf^0(\tau \land \neg \pi) = \{x : \text{Nat}, y : \text{Nat}\} \land \neg \{x : \text{Int}\} \lor \{x : \text{Nat}, y : \text{Nat}\} \land \neg \{y : \top\}\). Then this constrained type is decomposed into

示例。考虑以下约束：\(\tau = \{x : \text{Nat}, y : \text{Nat}\} \ll \pi = \{x : \text{Int}, y : \top\}\)。在将这一对元素加入假设集合后，C-Assum会计算出相应的RDNF表达式：\(dnf^0(\tau \land \neg \pi) = \{x : \text{Nat}, y : \text{Nat}\} \land \neg \{x : \text{Int}\} \lor \{x : \text{Nat}, y : \text{Nat}\} \land \neg \{y : \top\}\)。随后，这种被施加了约束的类型会被进一步分解为……

two smaller constrained types {\(x\): Nat, \(y\): Nat} ∧ ¬{\(x\): Int} and {\(x\): Nat, \(y\): Nat} ∧ ¬{\(y\): ⊤} by C-OR, and each one is solved individually by C-RCD1, which requires constraining respectively Nat ≪ Int and Nat ≪ ⊤. The former yields RDNF #Nat ∧ ¬#Int, which is solved by C-CLsCLs1, and the latter yields RDNF ⊥, which is solved by C-BOT.

通过C-OR规则，可以将这两个较小的约束类型分别表示为{\(x\): Nat, \(y\): Nat} ∧ ¬{\(x\): Int}以及{\(x\): Nat, \(y\): Nat} ∧ ¬{\(y\): ⊤}；接着分别使用C-RCD1规则来求解这两个类型。在求解过程中，需要分别满足Nat ≪ Int和Nat ≪ ⊤这两个约束条件。前者所得的结果是RDNF #Nat ∧ ¬#Int，该问题可以通过C-CLsCLs1规则来解决；后者所得的结果则是RDNF ⊥，这个问题可以通过C-BOT规则来解决。

5.4 Correctness of Type Inference

5.4 类型推断的正确性

We conclude this section by presenting the main correctness lemmas and theorems of type inference.

我们在本节的最后部分，总结了类型推断中的一些主要正确性命题及定理。

THEOREM 5.5 (SOUNDNESS OF TYPE INFERENCE). If the type inference algorithm successfully yields a type for program P, then P has this type. Formally: if \(\vdash^* P : \tau \Rightarrow \Xi\) and \(err \notin \Xi\), then \(\Xi \vdash^* P : \tau\).

定理5.5（类型推导的正确性）。 如果类型推导算法能够成功地为程序P确定一个类型，那么程序P确实具有该类型。用形式化的语言表达就是：如果\(\vdash^* P : \tau \Rightarrow \Xi\)且\(err \notin \Xi\)，那么\(\Xi \vdash^* P : \tau\)。

LEMMA 5.6 (SUFFICIENCY OF CONSTRAINING). Successful type constraining ensures subtyping: if \(\Sigma \text{ cons.}\) and \(\Sigma \vdash \tau \ll \pi \Rightarrow \Xi\) and \(err \notin \Xi\), then \(\Xi \cdot \Sigma \text{ cons.}\) and \(\Xi \cdot \Sigma \vdash \tau \le \pi\).

引理5.6（约束条件的充分性）。成功的类型约束必然能够确保子类型的存在：如果\(\Sigma\)满足约束条件，并且\(\Sigma \vdash \tau \ll \pi \Rightarrow \Xi\)，同时\(err \notin \Xi\)，那么\(\Xi \cdot \Sigma\)也满足约束条件，并且\(\Xi \cdot \Sigma \vdash \tau \le \pi\)。

THEOREM 5.7 (CONSTRAINING TERMINATION). For all \(\tau\), \(\pi\), \(D\), \(\Sigma\) wf, \(\Sigma \vdash \tau \ll \pi \Rightarrow \Xi\) for some \(\Xi\).

定理5.7（限制性终止条件）。 对于任意\(\tau\)、\(\pi\)、\(D\)、\(\Sigma\)及其满足“wf”条件的性质，如果\(\Sigma \vdash \tau \ll \pi\)，那么必然存在某个\(\Xi\)使得\(\Sigma \vdash \Xi\)。

THEOREM 5.8 (COMPLETENESS OF TYPE INFERENCE). If a program P can be typed at type \(\sigma\), then the type inference algorithm derives a type \(\sigma'\) such that \(\sigma' \leq^{\forall} \sigma\). Formally: if \(\Xi \vdash^* P : \tau\), then \(\vdash^* P : \tau' \Rightarrow \Xi'\) for some \(\Xi'\) and \(\tau'\) where \(\Xi'\) cons. and \(\forall \Xi' . \tau' \leq^{\forall} \forall \Xi . \tau\).

定理5.8（类型推断的完备性）。 如果某个程序P可以被赋予类型σ，那么类型推理算法会推导出另一个类型σ’，使得σ’满足对于所有的Ξ，都有σ’ ≤ σ。具体来说：如果Σ能够推出P具有类型τ，那么必然存在某个Σ’和τ’，使得Σ’能够推出P具有类型τ’，并且Σ’是良构的；同时，对于所有的Σ’和τ’，都ありσ’ ≤ σ。

In the following lemma, which is crucial for proving the above theorem, \(\rho\) refers to type variable substitutions and \(\Xi \models \Xi'\) denotes that \(\Xi\) entails \(\Xi'\) (both defined formally in the extended version).

在以下引理中，该引理对于证明上述定理而言至关重要，\(\rho\)表示类型变量的替换操作，而\(\Xi \models \Xi'\)则表示\(\Xi\)蕴含\(\Xi'\)（这两个概念都在扩展版本中得到了正式的定义）。

LEMMA 5.9 (COMPLETENESS OF CONSTRAINING). If there is a substitution \(\rho\) that makes \(\rho(\tau_1)\) a subtype of \(\rho(\tau_2)\) in some consistent \(\Xi\), then constraining \(\tau_1 \ll \tau_2\) succeeds and only introduces type variable bounds that are entailed by \(\Xi\) (modulo \(\rho\)). Formally: if \(\Xi \text{ cons.}\) and \(\Xi \vdash \rho(\tau_1) \le \rho(\tau_2)\) and \(\Xi \models \rho(\Xi_0)\), then \(\Xi_0 \vdash \tau_1 \ll \tau_2 \Rightarrow \Xi_1\) for some \(\Xi_1\) so that \(err \notin \Xi_1\) and \(\Xi \models \rho(\Xi_1)\).

引理5.9（约束条件的完备性）：如果存在某个替换规则\(\rho\)，使得在某种一致性体系\(\Xi\)中\(\rho(\tau_1)\)成为\(\rho(\tau_2)\)的子类型，那么使用约束条件\(\tau_1 \ll \tau_2\)一定能够成功，并且由此引入的类型变量范围必然满足\(\Xi\)中的约束规则（在考虑替换规则\(\rho\)的影响之后）。具体来说：如果体系\(\Xi\)是一致的，且\(\Xi \vdash \rho(\tau_1) \le \rho(\tau_2)\)，同时\(\Xi \models \rho(\Xi_0)\)，那么对于某个满足条件\(err \notin \Xi_1\)且\(\Xi \models \rho(\Xi_1)\)的体系\(\Xi_1\)来说，必有\(\Xi_0 \vdash \tau_1 \ll \tau_2 \Rightarrow \Xi_1\)。

6 RELATED WORK

6 相关研究工作

We now relate the different aspects of MLstruct and \(\lambda^-\) with previous work.

我们现在将MLstruct及\(\lambda^-\)的各个方面与以往的研究成果联系起来进行探讨。

Intersection type systems. Intersection types for lambda calculus were pioneered by Coppo and Dezani-Ciancaglini [1980]; Barendregt et al. [1983], after whom the “BCD” type system is named. BCD has the very powerful “T-∧-I” rule, stating: if \(\Gamma \vdash t : \tau_1\) and \(\Gamma \vdash t : \tau_2\), then \(\Gamma \vdash t : \tau_1 \wedge \tau_2\). Such systems have the interesting property that typeability coincides with strong normalization [Ghilezan 1996], making type inference undecidable. Thankfully, we do not need something as powerful as T-∧-I – instead, we introduce intersections in less general ways (i.e., through T-OBJ), and we retain decidability of type inference. Most intersection type systems, including MLstruct and \(\lambda^-\), do admit the following standard BCD subtyping rules given by Barendregt et al.: (1) \(\tau_1 \wedge \tau_2 \le \tau_1\); (2) \(\tau_1 \wedge \tau_2 \le \tau_2\); and (3) if \(\tau_1 \le \tau_2\) and \(\tau_1 \le \tau_3\), then \(\tau_1 \le \tau_2 \wedge \tau_3\). Some systems use intersection types to encode a form of overloading [Pierce 1991]. However, Smith [1991] showed that ML-style type inference with such a general form of overloading and subtyping is undecidable (more specifically, finding whether inferred sets of constraints are satisfiable is) and proposed constructor overloading, a restricted form of overloading with more tractable properties, sufficient to encode many common functions, such as addition on different primitive types as well as vectors of those types. Constructor overloading is eminently compatible with MLstruct and MLscript. Another design decision for intersection systems is whether and how this connective should distribute over function types. BCD subtyping states⁴⁰ \((\tau \rightarrow \pi_1) \wedge (\tau \rightarrow \pi_2) \le \tau \rightarrow (\pi_1 \wedge \pi_2)\) and Barbanera et al. [1995] also propose \((\tau_1 \rightarrow \pi) \wedge (\tau_2 \rightarrow \pi) \le (\tau_1 \vee \tau_2) \rightarrow \pi\). Together, these correspond to the minimal relevant logic B+ [Dezani-Ciancaglini et al. 1998]. Approaches like that of Pottier [1998b] use a greatest

交集类型系统。 在λ演算中引入交集类型的概念最早是由Coppo和Dezani-Ciancaglini在1980年提出的；Barendregt等人也在1983年进一步发展了这一理论，之后这种类型系统便被命名为“BCD类型系统”。BCD类型系统具备一个非常强大的规则“T-∧-I”，该规则规定：如果\(\Gamma \vdash t : \tau_1\)且\(\Gamma \vdash t : \tau_2\)，那么\(\Gamma \vdash t : \tau_1 \wedge \tau_2\)。这类类型系统具有一个有趣的特性：类型合法性与强规范化是完全一致的[Ghilezan 1996]，因此这种类型推导机制其实是不可判定的。幸运的是，我们并不需要像T-∧-I这样强大的规则——相反，我们可以通过较为简单的方式引入交集类型的概念（例如通过T-OBJ机制），这样就依然能够保持类型推导的可判定性。包括MLstruct和\(\lambda^-\)在内的大多数交集类型系统都遵循Barendregt等人提出的以下标准BCD子类型化规则：(1) \(\tau_1 \wedge \tau_2 \le \tau_1\)；(2) \(\tau_1 \wedge \tau_2 \le \tau_2\)；以及(3) 如果\(\tau_1 \le \tau_2\)且\(\tau_1 \le \tau_3\)，那么\(\tau_1 \le \tau_2 \wedge \tau_3\)。某些系统还利用交集类型来实现某种形式的重载功能[Pierce 1991]；然而Smith在1991年指出，使用这种通用重载和子类型化机制的ML风格类型推导其实是不可判定的（更具体地说，确定推导出的约束条件是否可满足本身就是不可判定的），因此他提出了一种受限形式的重载机制——构造函数重载。这种机制具有更易处理的特性，足以用来表示许多常见的功能，例如不同基本类型之间的加法运算，或者这些类型所构成的向量上的操作。构造函数重载与MLstruct和MLscript等编程语言是高度兼容的。对于交集类型系统而言，另一个需要考虑的设计问题是：这种连接运算应该如何应用于函数类型上。BCD子类型化规则规定\((\tau \rightarrow \pi_1) \wedge (\tau \rightarrow \pi_2) \le \tau \rightarrow (\pi_1 \wedge \pi_2)\)，而Barbanera等人也在1995年提出了\((\tau_1 \rightarrow \pi) \wedge (\tau_2 \rightarrow \pi) \le (\tau_1 \vee \tau_2) \rightarrow \pi\)这一规则。这些规定实际上对应于最小相关逻辑B+ [Dezani-Ciancaglini et al. 1998]。像Pottier在1998b年提出的那种方法，则采用了“最大值”操作来处理这类问题。

lower bound connective ∧ that resembles type intersection ∧ but admits a more liberal rule that generalizes the previous two: \((\tau_1 \to \pi_1) \land (\tau_2 \to \pi_2) \le (\tau_1 \lor \tau_2) \to (\pi_1 \land \pi_2)\), which we will refer to as (full) function distributivity. However, notice that in a system with primitives, full function distributivity is incompatible with T-∧-I and thus precludes intersection-based overloading.⁴¹

下界联结运算 ∧，它类似于类型交集运算 ∧，但采用了更为宽松的规则，这种规则能够推广前两种规则的含义：\((\tau_1 \to \pi_1) \land (\tau_2 \to \pi_2) \le (\tau_1 \lor \tau_2) \to (\pi_1 \land \pi_2)\)，我们将其称为“完全函数 Distributivity”。然而需要注意的是，在包含原语的系统中，完全函数 Distributivity 与 T-∧-I 是不兼容的，因此这种规则会导致基于类型交集的重载操作无法实现。⁴²

Union and intersection types in programming. Union types are almost as old as intersection types, first introduced by MacQueen et al. [1986],⁴³ and both have a vast (and largely overlapping) research literature, with popular applications such as refinement types [Freeman and Pfenning 1991]. These types have seen a recent resurgence, gaining a lot of traction both in academia [Alpuim et al. 2017; Binder et al. 2022; Castagna et al. 2022; Dunfield 2012; Huang and Oliveira 2021; Muehlboeck and Tate 2018; Rehman et al. 2022] and in industry,⁴⁴ with several industry-grade programming languages like TypeScript, Flow, and Scala 3 supporting them, in addition to a myriad of lesser-known research languages.

编程中的并集类型与交集类型。 并集类型的出现时间几乎与交集类型一样早，最早由MacQueen等人于1986年提出⁴⁵；这两种类型都拥有大量相关的研究文献，而且这些研究在很大程度上是相互交叉、重叠的。它们在诸多实际应用中发挥了重要作用，例如类型细化技术[Freeman和Pfenning，1991]。近来，这两种类型又重新受到了人们的关注，在学术界[Alpuim等人，2017；Binder等人，2022；Castagna等人，2022；Dunfield，2012；Huang和Oliveira，2021；Muehlboeck和Tate，2018；Rehman等人，2022]以及工业领域[⁴⁶]都获得了广泛应用。包括TypeScript、Flow和Scala 3在内的多种商用编程语言都已支持这两种类型，此外还有许多不太知名的研究型编程语言也在使用它们。

Type inference for unions and intersections. None of the previous approaches we know have proposed a satisfactory ML-style type inference algorithm for full union and intersection types. By satisfactory, we mean that the algorithm should infer principal polymorphic types without backtracking. Earlier approaches used heavily-restricted forms of unions and intersections. For instance, Aiken and Wimmers [1993]; Aiken et al. [1994] impose very strict restrictions on negative unions (they must be disjoint) and on positive intersections (they must not have free variables and must be “upward closed”). Trifonov and Smith [1996] go further and restrict intersections to negative or input positions (those appearing on the right of \(\le\) constraints) and unions types to positive or output positions (those appearing on the left). Binder et al. [2022]; Dolan [2017]; Parreaux [2020]; Pottier [1998b] all follow the same idea. In these systems, unions and intersections are not first-class citizens: they cannot be used freely in type annotations. Frisch et al. [2008] infer set-theoretic types (see semantic subtyping below) for a higher-order language with overloading but do not infer polymorphic types. Castagna et al. [2016] propose a complete polymorphic set-theoretic type inference system, but their types are not principal so their algorithm returns several solutions, which leads to the need for backtracking. It seems this should have severe scalability issues, as the number of possible types for an expression would commonly grow exponentially.⁴⁷ Petrucciani [2019] describes ways to reduce backtracking, but recognizes it as fundamentally “unavoidable.”

并集与交集类型的类型推断。 我们所了解的以往所有方法，都没有提出一种令人满意的、基于机器学习思路的类型推断算法，用于处理完整的并集与交集类型。所谓“令人满意”，是指这种算法应该能够在不使用回溯机制的情况下推导出主要的多元类型。早期的研究采用了对并集和交集类型进行严格限制的方法。例如，Aiken与Wimmers在1993年、Aiken等人在1994年的研究中，对负并集（必须是不相交的）和正交集（不能包含自由变量且必须是“向上封闭”的）施加了极为严格的限定；Trifonov与Smith在1996年则进一步将交集类型限制为仅出现在\(\le\)约束右侧的位置，而将并集类型限制为仅出现在左侧的位置。Binder等人在2022年、Dolan在2017年、Parreaux在2020年以及Pottier在1998年的研究中也都采用了类似的方法。在这些系统中，并集与交集类型并不属于“一线公民”：它们不能被自由地用于类型注释中。Frisch等人在2008年为一种支持重载的高阶语言提出了基于集合论的类型推断方法，但并未能够推导出多元类型；Castagna等人在2016年提出了一种完善的多元类型推断系统，但由于他们推导出的类型并非主要类型，因此他们的算法会返回多个解，这就需要使用回溯机制。显然，这种方法会带来严重的可扩展性问题——因为一个表达式可能存在的类型数量通常会呈指数级增长。⁴⁸ Petrucciani在2019年提出了减少回溯所需的方法，但他也承认这种现象从根本上来说是“不可避免的”。

Negation or complement types. Negation types have not been nearly as ubiquitous as unions and intersection in mainstream programming language practice and theory, except in the field of semantic subtyping (see below). Nevertheless, our use of negation types to make progress while solving constraints is not new — Aiken and Wimmers [1993] were the first to propose using complement types in such a way. However, their complement types are less precise than our negation types,⁴⁹ and in their system \(\alpha \land \tau_1 \le \tau_2\) and \(\alpha \le \tau_2 \lor \neg \tau_1\) are not always equivalent.

否定类型或补码类型。 在主流编程语言的实践与理论中，否定类型的应用范围远不及并集和交集那么广泛，除非是在语义子类型化的领域中（详见下文）。不过，我们在解决约束条件时使用否定类型来帮助推进问题求解这一做法并不新鲜——Aiken和Wimmers在1993年首次提出了以这种方式利用补码类型的想法。然而，他们所提出的补码类型相比我们提出的否定类型来说精度较低，而且在他们的系统中，“\(\alpha \land \tau_1 \le \tau_2\)”与“\(\alpha \le \tau_2 \lor \neg \tau_1\)”这两个表达式并不总是等价的。

Recursive types. Recursive types in the style of MLstruct, where a recursive type is equivalent to its unfolding (a.k.a. equi-recursive types, not to be confused with iso-recursive types), have a

递归类型。 类似于MLstruct中的递归类型，这种类型的递归性其实等同于其“展开形式”；这类递归类型也被称为“等价递归类型”，需要注意的是，它们与“同构递归类型”是不同的。

long history in programming languages research [Abadi and Fiore 1996; Amadio and Cardelli 1993; Appel et al. 2007; Hosoya et al. 2005; MacQueen et al. 1986; Pierce 2002], dating as far back as Morris' thesis, where he conjectured their use under the name of cyclic types [Morris 1969, pp.122–124]. Recursive types with subtyping were developed in the foundational work of Amadio and Cardelli [1993] and Brandt and Henglein [1998] gave a coinductive axiomatization of such recursive types. Jim and Palsberg [1999] described a co-inductive formalization of recursive types as arbitrary infinite trees which is more general than approaches like ours, which only allows reasoning about regular types. Nevertheless, the algorithms they gave were unsurprisingly restricted to regular types. Gapeyev et al. [2002]; Pierce [2002] reconciled the representation as infinite regular trees with the representation as \(\mu\) types, and described the standard algorithms to decide the corresponding subtyping relationship. An important aspect of practical recursive type algorithms is that one needs to maintain the cache of discovered subtyping relationships across recursive calls to avoid exponential blowup [Gapeyev et al. 2002]. Our implementation of MLstruct follows the same principle, as a naive implementation of \(\lambda^-\) would lead to exactly the same blowup. Also refer to Section 4.4.2 for more parallels between the handling of recursive types in \(\lambda^-\) and previous work.

在编程语言研究领域，人们拥有悠久的探索历史[Abadi和Fiore 1996；Amadio和Cardelli 1993；Appel等人2007；Hosoya等人2005；MacQueen等人1986；Pierce 2002]。这一研究传统可追溯到Morris的博士论文——他在其中推测人们早就可以使用这类类型，并将其称为“循环类型”[Morris 1969，第122–124页]。Amadio和Cardelli[1993]以及Brandt和Henglein[1998]在他们的基础性研究中发展出了带有子类型的递归类型系统，而Brandeis和Pierce[2000]则为这类递归类型提供了共归纳形式的公理化描述。Jim和Palsberg[1999]进一步将递归类型形式化为任意的无限树结构，这种表述方式比我们目前使用的方法更为通用——因为我们的方法仅允许对“规则类型”进行推理。不过，他们提出的算法同样也只能用于处理规则类型。Gapeyev等人[2002]以及Pierce[2002]将递归类型表示为无限规则树的结构与将其表示为\(\mu\)类型的结构进行了统一，并描述了用于判断这两种表示方式之间子类型关系标准算法。在实际应用中，递归类型算法的一个重要要点在于：必须要“在多次递归调用过程中”保持已经发现的子类型关系缓存信息，这样才能避免计算规模呈指数级膨胀[Gapeyev等人2002]。我们对MLstruct的实现就是遵循这一原理的——因为如果采用简单的\(\lambda^-\)实现方式，同样会导致计算效率急剧下降。关于\(\lambda^-\)中递归类型的处理方法与以往研究之间的相似之处，更多内容可参见第4.4.2节。

Early approaches to subtype inference. The problem of type inference in the presence of subtyping was kick-started in the 1980s [Fuh and Mishra 1989; Mitchell 1984; Stansifer 1988] and studied extensively in the 1990s [Aiken and Wimmers 1993; Curtis 1990; Fuh and Mishra 1990; Jim and Palsberg 1999; Kozen et al. 1994; Palsberg et al. 1997; Pottier 1998a,b; Smith 1991], mostly through the lens of constraint solving on top of Hindley-Milner-style type inference [Damas and Milner 1982; Hindley 1969; Milner 1978]. These approaches often involved combinations of record, intersection, union, and recursive types, but as far as we know none proposed an effective (i.e., without backtracking) principal type inference technique for a system with all of these combined. Odersky et al. [1999] gave them a unified account by proposing a general framework called HM(X), where the ‘X’ stands for a constraint solver to plug into their generic system. While these approaches often claimed a form of principal type inference (also called minimality⁵⁰), the constrained types they inferred were often large and unwieldy. Beyond inferring constraint sets and ensuring their satisfiability, the related problem of simplification to produce more readable and efficiently-processable types was also studied, often by leveraging the connection between regular type trees and finite-state automata [Aiken 1996; Eifrig et al. 1995; Pottier 1996, 1998b, 2001; Simonet 2003]. A major stumbling block with all of these approaches was the problem of non-structural subtyping entailment⁵¹ (NSSE), which is to decide whether a given type scheme, which consists in a polymorphic type along with its constraints on type variables, subsumes another. Solving this issue is of central importance because it is needed to check implementations against user-provided interfaces and type signatures, and because it provides a foundation from which to derive sound type simplification techniques. However, to this day NSSE remains an open problem, and it is not known whether it is even decidable [Dolan 2017]. Due to these difficulties, interest in this very powerful form of subtyping all but faded in the subsequent decade, in what we interpret as a minor “subtype inference winter.” Indeed, many subsequent approaches were developed in reaction to this complexity with the aim of being simpler to reason about (e.g., polymorphic variants — see below).

早期关于子类型推断的研究。在存在子类型机制的情况下进行类型推断这一问题最早可追溯到20世纪80年代[Fuh和Mishra 1989; Mitchell 1984; Stansifer 1988]，并在90年代得到了广泛研究[Aiken和Wimmers 1993; Curtis 1990; Fuh和Mishra 1990; Jim和Palsberg 1999; Kozen等人1994; Palsberg等人1997; Pottier 1998a,b; Smith 1991]。这些研究大多是在Hindley-Milner式的类型推断机制基础上，通过约束求解的方法来展开的[Damas和Milner 1982; Hindley 1969; Milner 1978]。这些方法通常会结合使用记录型、交集型、并集型以及递归型等类型，但据我们所知，没有任何一种方法能够为同时包含这些类型的系统提出一种高效且无需回溯的主类型推断机制。Odersky等人[1999]通过提出了一个名为HM(X)的通用框架，为这些问题提供了一个统一的解决方案，其中“X”代表可以插入到他们这个通用系统中的约束求解器。虽然这些方法都声称实现了某种形式的主类型推断（也称为“最小性”⁵²），但它们所推导出的“受限类型”往往结构复杂且难于处理。除了推断出约束集合并确保其满足性之外，人们还研究了如何通过“简化”这些类型来使其更易于阅读和处理，这方面的研究常常借助正则类型树与有限状态自动机之间的关联来进行[Aiken 1996; Eifrig等人1995; Pottier 1996, 1998b, 2001; Simonet 2003]。然而，所有这些方法都面临着一个严重的问题，即“非结构化子类型蕴含关系”⁵³（NSSE）的判定问题——也就是需要判断某个由多态类型及其对类型变量的约束所构成的类型体系是否包含另一个类型体系。解决这个问题具有至关重要的意义，因为只有在此基础上才能验证程序实现是否符合用户所提供的接口和类型规范，同时也才能开发出合理的类型简化技术。不过直到今天，NSSE仍然是一个未解决的问题，目前甚至还不确定它是否属于可判定问题[Dolan 2017]。由于这些困难，在随后的十年里，人们对这种强大的子类型机制的兴趣几乎消失了，我们可以将这一时期视为一次“子类型推断研究的低谷期”。事实上，后来出现的许多研究方法都是为了应对这种复杂性而提出的，其目的就是使类型推理过程变得更简单易懂（例如，多态变体的概念——详见下文）。

Algebraic subtyping. Approaches like that of Pottier [1998b] used a lattice-theoretic construction of types inspired by the connection between types and term automata. Meet \(\sqcap\) and join \(\sqcup\) operators resembling intersection and union types are used to compactly representing conjunctions

代数子类型概念。诸如Pottier在[1998b]中采用的方法，这类技术借鉴了类型与术语自动机之间的关联，运用格论理论来构造类型结构。其中，表示交集的“ meet ”运算符与表示并集的“ join ”运算符，被用来简洁地表达类型间的结合关系。

of constraints, but these are not first-class types, in that they are restricted to appearing respectively in negative and positive positions only. Full function distributivity (defined above, in intersection type systems) holds in these approaches due to the lattice structure. Pottier's system still suffered from a lack of complete entailment algorithm due to NSSE. Dolan [2017]; Dolan and Mycroft [2017] later built upon that foundation and proposed an algebraic construction of types which allowed breaking free of NSSE and finally enjoying a sound and complete entailment algorithm. Two magical ingredients allowed this to be possible: 1. the definition of “extensible” type semantics based on constructing types as a distributive lattice of coproducts; and 2. a different treatment of type variables than in previous work, representing them as part of the lattice of types and not as unknowns ranging over a set of ground types. In this paper, we in turn build on these foundations, although we only retain the latter innovation, somehow forgoing the “extensible” construction of types.⁵⁴ Together with our generalization of the subtyping lattice to a Boolean one by adding negations and with the additional structure we impose on types (such as reducing unions of unrelated records to \(\top\)), this turns out to be sufficient for allowing principal type inference and decidable entailment (though we only sketched the latter in this paper for lack of space). Ingredient 1 allowed Dolan to show the soundness of his system in a very straightforward way, relying on the property (called Proposition 12 by Dolan [2017]) that any constraint of the form \(\bigwedge_i \tau_i \le \bigvee_j \pi_j\) holds iff there is a \(k\) such that \(\tau_k \le \pi_k\) when all \(\tau_i\) have distinct constructors and all \(\pi_j\) similarly. By contrast, we allow some intersections of unrelated type constructors to reduce to \(\bot\) and some unions of them to \(\top\), and we are thus not “extensible” in Dolan's terminology. This is actually desirable in the context of pattern matching, where we want to eliminate impossible cases by making the intersections of unrelated class types empty. It is also needed in order to remove the ambiguity from constraints like \((\tau_1 \rightarrow \tau_2) \wedge \{x : \pi\} \le (\tau'_1 \rightarrow \tau'_2) \vee \{x : \pi'\}\) which in our system reduces to \((\tau_1 \rightarrow \tau_2) \wedge \{x : \pi\} \le \top\). The present paper also takes heavy inspiration from our earlier operationally-focused take on Dolan's type inference algorithm [Parreaux 2020]. While Dolan shirks from explicitly representing constraints, which he prefers to inline inside types on the fly as \(\sqcap\) and \(\sqcup\) types, we use an approach closer to the original constrained-types formulation followed by Pottier. Besides being much easier to implement, our approach has other concrete advantages, such as the ability to deal with invariance seamlessly (class C[A]: {f : A A}*), which is invariant in A, is valid in MLstruct) and a simpler treatment of cyclic type variable constraints.

虽然存在这些约束条件，但它们并非“一级”类型，因为这些类型仅能分别出现在否定位置和肯定位置上。由于 lattice 结构的存在，在这些方法中仍然满足完整的函数分配律（如上文在交集类型系统中所定义的）。然而，由于 NSSE 的限制，Pottier 的系统依然缺乏完备的蕴含算法。后来，Dolan [2017] 以及 Dolan 和 Mycroft [2017] 在这一基础上进一步研究，提出了一种“代数化”的类型构造方法，这种方法使得系统能够摆脱 NSSE 的束缚，最终实现了完备且正确的蕴含算法。实现这一目标得益于两大关键因素：首先是以余积构成的分配 lattice 为基础来定义“可扩展”类型语义；其次是对类型变量的处理方式与以往不同——我们将类型变量视为类型 lattice 的组成部分，而不是视为取值于一组基础类型的未知量。在本文中，我们也在这些基础上进行了进一步探索，不过仅保留了第二种创新方法，而放弃了“可扩展”类型构造的方式。⁵⁵ 结合我们将子类型化 lattice 扩展为包含否定操作的结构，以及我们对类型所施加的其他约束条件（比如将无关记录的并集简化为 \(\top\)），这些措施已经足以支持主类型推断和可判定的蕴含关系推导（不过由于篇幅限制，本文仅简要介绍了后者）。第一种关键因素使得 Dolan 能够以非常直接的方式证明其系统的正确性；他依据这样一个性质（Dolan [2017] 将其称为命题 12）来论证这一点：任何形如 \(\bigwedge_i \tau_i \le \bigvee_j \pi_j\) 的约束条件成立当且仅当存在一个 \(k\)，使得当所有 \(\tau_i\) 的构造函数都不相同时有 \(\tau_k \le \pi_k\)，而所有的 \(\pi_j\) 也满足同样的条件。相比之下，我们的系统允许某些无关类型构造函数的交集简化为 \(\bot\)，某些并集简化为 \(\top\)，因此从 Dolan 的角度来看，我们的方法并不具备“可扩展性”。但实际上，在模式匹配的背景下，这种设定是很有必要的——我们希望通过将无关类别类型的交集设为空来排除那些不可能的情况。此外，这样的设计也有助于消除诸如 \((\tau_1 \rightarrow \tau_2) \wedge \{x : \pi\} \le (\tau'_1 \rightarrow \tau'_2) \vee \{x : \pi'\}\) 这类约束条件所带来的歧义；在我们的系统中，这样的表达式会简化为 \((\tau_1 \rightarrow \tau_2) \wedge \{x : \pi\} \le \top\)。本文在很大程度上也受到了我们之前针对 Dolan 的类型推断算法所提出的操作性视角的研究[Parreaux 2020]的启发。虽然 Dolan 不愿意显式地表示约束条件，而是倾向于将它们动态地内嵌到类型中，表现为 \(\sqcap\) 或 \(\sqcup\) 类型，但我们的方法更接近于 Pottier 那种原始的受限类型构造方式。除了实现起来更为容易之外，我们的方法还具有其他实际优势，比如能够顺利处理各种不变性要求（例如在 MLstruct 中，表达式 class C[A]: {f : A A}* 是有效的，因为它的定义与 A 的值无关），同时也更易于处理循环类型变量约束条件。

Semantic subtyping and set-theoretic types. The semantic subtyping approaches [Castagna et al. 2022, 2016; Frisch et al. 2002, 2008; Petrucciani 2019] view types as sets of values which inhabit them and define the subtyping relationship as set inclusion, giving set-based meaning to union, intersection, and negation (or complement) connectives. This is by contrast to algebraic subtyping, which may admit subtyping rules that violate the set-theoretic interpretation, such as function distributivity, to ensure that the subtyping lattice has desirable algebraic properties. For more detailed discussions contrasting semantic subtyping with other approaches, we refer the reader to Parreaux [2020] and Muehlboeck and Tate [2018].

语义子类型化与集合论类型的概念。在[Castagna等人2022年、2016年；Frisch等人2002年、2008年；Petrucciani 2019年]提出的语义子类型化方法中，类型被视作包含其中各种值的集合，而子类型化关系则被定义为集合间的包含关系。这种定义使得“并集”、“交集”以及“否定”（或“补集”）等运算具备基于集合论的意义。这与代数子类型化的处理方式截然不同——后者往往会允许一些违反集合论解释的子类型化规则的存在，例如函数分配律，仅仅是为了确保子类型化结构具备理想的代数性质。关于语义子类型化与其他方法之间的区别，读者可参考Parreaux [2020年]以及Muehlboeck和Tate [2018年]的相关研究。

Occurrence and flow typing. Occurrence typing was originally introduced by Tobin-Hochstadt and Felleisen [2008] for Typed Scheme, and was later incorporated into TypeScript and Flow, where it is known as flow typing. It allows the types of variables to be locally refined based on path conditions encountered in the program. Instance-matching in MLstruct can be understood as a primitive form of occurrence typing in that it refines the types of scrutinee variables in case expressions, similarly to the approach of Rehman et al. [2022]. Occurrence typing was also recently extended to the semantic subtyping context [Castagna et al. 2021, 2022], where negation types

出现类型判定与流程类型判定。出现类型判定这一概念最初由Tobin-Hochstadt和Felleisen在2008年为Typed Scheme提出，后来被引入TypeScript和Flow中，而在这些语言中它被称为“流程类型判定”。这种机制允许根据程序中遇到的特定条件来局部细化变量的类型。在MLstruct中进行的实例匹配其实可以被视为出现类型判定的一种原始形式——因为它会类似Rehman等人2022年提出的方法那样，在case表达式中细化被检测变量的类型。最近，出现类型判定这一概念还被扩展到了语义子类型判定的领域[Castagna等人，2021、2022]；在这一点上，否定类型……

are first-class types. The latter work proposes a powerful type inference approach that can infer overloaded function signatures as intersections types; however, this approach does not support polymorphism and likely does not admit principal types.

前者属于一类高级类型；而后者的研究提出了一种强大的类型推导方法，该方法能够将重载函数的签名推断为“交叉类型”；然而，这种方法并不支持多态性，而且很可能也不认可“主类型”这一概念。

Polymorphic records/variants and row polymorphism. Polymorphic records are structurally-typed products whose types admit the usual width and depth subtyping relationships. Their dual, polymorphic variants, are another useful language feature [Garrigue 1998, 2001], used to encode structural sum types. In their simplest expression, polymorphic records (resp. variants) do not support ad-hoc field extension (resp. default match cases). Previous approaches have thus extended polymorphic records and variants with row polymorphism, which uses a new kind of variables, named “row” variables, to record the presence and absence of fields (resp. cases) in a given type. Some approaches, like OCaml’s polymorphic variants and object types, use row polymorphism exclusively to simulate subtype polymorphism, in order to avoid subtyping in the wider languages. However, row polymorphism and subtyping actually complement each other well, and neither is as flexible without the other [Pottier 1998b, Chapter 14.7]. There are also techniques for supporting variant and record extensibility through union, intersection, and negation types, as shown by Castagna et al. [2016], who also explain that their system resolves long-standing limitations with OCaml-style row polymorphism. In our system, we solve many (though not all) of these limitations, but we also support principal type inference. It is worth pointing out that OCaml’s polymorphic variants [Garrigue 2001] and related systems based on kinds [Ohori 1995] lack support for polymorphic extension [Gaster and Jones 1996; White 2015], whereas MLstruct does (see mapSome in the introduction). As a simpler example, def foo x dflt els = case x of { Apple -> dflt | _ -> els x } would be assigned a too restrictive type in OCaml and as a consequence foo (Banana{}) 0 (fun z -> case z of { Banana -> 1 }) would not type check (OCaml would complains that the function argument does not handle Apple). A more expressive row-polymorphic system exposing row variables to users would support this use case [Gaster and Jones 1996; Rémy 1994], but as explained in the introduction, even these have limitations compared to our subtyped unions.

多态记录/变体与行多态性。 多态记录是一种结构化类型的代码单元，其类型具备常见的“宽度”与“深度”子类型关系。它们的对应概念——多态变体——也是该语言中另一项非常有用的特性[Garrigue 1998, 2001]，这类变体用于表示结构化的“和型”——即由多种类型组合而成的类型。在最简单的形式下，多态记录（或变体）并不支持自定义字段的添加功能，也不支持默认值处理机制。因此，以往的研究者们通过引入“行多态性”来扩展这些功能：这种机制借助一种名为“行变量”的新型变量，用于记录特定类型中是否存在某些字段或缺少哪些字段。有些编程语言，比如OCaml的多态变体系统及对象类型机制，专门利用行多态性来模拟子类型关联关系，从而避免在更复杂的语言结构中使用传统的子类型机制。然而实际上，行多态性与传统子类型机制是相辅相成的，缺少其中任何一方都会导致代码灵活性的大幅下降[Pottier 1998b, 第14.7章]。此外，Castagna等人[2016]还提出了通过“并集类型”、“交集类型”及“否定类型”来支持对记录/变体进行扩展的技术，他们的系统有效解决了OCaml-style行多态性机制所存在的诸多局限性。在我们的系统中，我们也解决了其中的大部分问题，同时还实现了主类型推导功能。值得指出的是，OCaml的多态变体机制[Garrigue 2001]以及基于“种类”概念的相关系统[Ohori 1995]并不支持多态扩展功能[Gaster and Jones 1996; White 2015]，而MLstruct却具备这一功能（详见引言中的mapSome示例）。举一个更简单的例子：在OCaml中，代码def foo x dflt els = case x of { Apple -> dflt | _ -> els x }会被赋予一个过于严格的类型限制，因此foo (Banana{}) 0 (fun z -> case z of { Banana -> 1 })这种用法是无法通过类型检验的（OCaml会提示函数参数无法处理Apple类型）。如果有一种行多态性机制能允许用户直接操作“行变量”，那么这种用法自然是可行的[Gaster and Jones 1996; Rémy 1994]，但正如引言中所提到的，即使这样的机制相比我们的子类型并集模型也存在一定局限性。

7 CONCLUSION AND FUTURE WORK

7 结论与未来研究方向

In this paper, we saw that polymorphic type inference for first-class union, intersection, and negation types is possible, enabling class-instance matching patterns yielding very precise types, comparable in expressiveness to row-polymorphic variants. We saw that this type inference approach relies on two crucial aspects of MLstruct’s type system: 1. using the full power of Boolean algebras to normalize types and massage constraints into shapes amenable to constraint solving without backtracking; and 2. approximating some unions and intersections, most notably unions of records and intersections of functions, in order to remove potential ambiguities during constraint solving without threatening the soundness of the system.

在本文中，我们发现对于一等联合型、交集型和否定型来说，实现多态类型推断是完全可能的。这种类型的推断机制使得类与实例之间的匹配过程能够生成非常精确的类型结果，其表达能力可与行多态版本相媲美。我们还了解到，这种类型推断方法实际上依赖于MLstruct类型系统中的两个关键要素：第一，充分利用布尔代数的强大功能来对类型进行规范化处理，并将各种约束条件转化成便于进行无回溯求解的形式；第二，通过近似表示某些类型的联合或交集操作（尤其是记录的联合以及函数的交集），从而在解决约束条件的过程中消除潜在的歧义，同时也不会威胁到整个类型系统的可靠性。

Future Work. In the future, we intend to explore more advanced forms of polymorphism present in MLscript, such as first-class polymorphism, as well as how to remove some of the limitations of regular types, which currently prevent fully supporting object-oriented programming idioms.

后续工作。未来，我们计划研究MLscript中存在的更高级的多态性形式，比如一类多态性，并探索如何消除那些目前限制语言完全支持面向对象编程风格的因素。

Acknowledgements. We would like to sincerely thank the anonymous reviewers as well as François Pottier, Didier Rémy, Alan Mycroft, Bruno C. d. S. Oliveira, Andong Fan, and Anto Chen for their constructive and helpful comments on earlier versions of this paper. We are particularly grateful to Stephen Dolan, who gave us some invaluable feedback and mathematical intuitions on the development of this new algebraic subtyping system.

致谢。我们衷心感谢那些匿名的审稿人，以及François Pottier、Didier Rémy、Alan Mycroft、Bruno C. d. S. Oliveira、Andong Fan和Anto Chen对本文早期版本所提出的宝贵意见与帮助。我们尤其要感谢Stephen Dolan，他为我们提供了关于这一新的代数子类型系统开发过程中一些极为宝贵的建议与数学上的直觉性见解。

---

1. MLstruct supports singleton types for constant literals, e.g., 42 is both a value and a type, with 42 : 42 ≤ Nat ≤ Int.↩︎

2. MLstruct支持将常量字面量定义为单例类型。例如，42既是一个数值，也是一个类型，且满足关系 42 : 42 ≤ Nat ≤ Int。↩︎

3. Notice that only ex3 features a union of two distinct type constructors ‘Some[⊥] ∨ 42’ because in ex1 and ex2 only one concrete type constructor statically flows into the result of the expression (42 and Some, respectively).↩︎

4. 需要注意的是，只有例3中出现了两种不同类型构造函数的结合形式“Some[⊥] ∨ 42”；因为在例1和例2中，表达式(42)以及(Some)的结果分别只由一种具体的类型构造函数生成。↩︎

5. One may expect Some[⊥] ≡ ⊥, but this does not hold in MLstruct, as it would prevent effective principal type inference.↩︎

6. 人们可能会认为 Some[⊥] ≡ ⊥，但在 MLstruct 中这一恒等关系并不成立，因为如果承认这一点的话，就会妨碍有效的主类型推导机制的正常运作。↩︎

7. The GitHub repository of the full MLscript language is available at https://github.com/hkust-taco/mlscript.↩︎

8. Type names, on the other hand, live in a different namespace and are not subject to shadowing.↩︎

9. 另一方面，类型名称属于不同的命名空间，因此不会受到“阴影效应”的影响。↩︎

10. The lack of nominal typing for classes has been a major pain point in TypeScript. The issue requesting it, created in 2014 and still not resolved, has accumulated more than 500 “thumbs up”. See: https://github.com/Microsoft/Typescript/issues/202.↩︎

11. TypeScript中类缺乏命名类型指定这一问题一直备受诟病。这个早在2014年就提出的建议至今仍未得到解决，而已获得的“支持投票”数量已经超过了500条。详情请参见：https://github.com/Microsoft/Typescript/issues/202。↩︎

12. The where keyword is used to visually separate the specification of type variable bounds, making them more readable.↩︎

13. 使用 “where” 关键字可以直观地区分类型变量取值范围的定义内容，从而使这些描述更加易于阅读。↩︎

14. By contrast, we have no specific requirements on the meaning of negated function and record types, which are uninhabited.↩︎

15. 相比之下，我们对被否定的函数以及那些空闲的、未被使用的记录类型的含义并没有具体的要求。↩︎

16. This class intersection annihilation rule is not novel; for example, Ceylon has a similar one [Muehlboeck and Tate 2018].↩︎

17. Other forms of overloading, such as type classes and constructor overloading (see Section 6), are still possible.↩︎

18. For other constructs, such as functions and records, negations assume a purely algebraic role. For instance, we have relationships like \(\neg \{x : \tau\} \le \pi_1 \rightarrow \pi_2\) due to \(\{x : \tau\} \lor \pi_1 \rightarrow \pi_2\) being identified with \(\top\) (see also Section 4.4.4).↩︎

19. 对于函数和记录等其他数据结构而言，否定运算仅具有代数意义。例如，根据\(\{x : \tau\} \lor \pi_1 \rightarrow \pi_2\)这一表达式与\(\top\)相等这一事实，我们可以得出\(\neg \{x : \tau\} \le \pi_1 \rightarrow \pi_2\)这一结论（详见第4.4.4节）。↩︎

20. TypeScript does allow such definitions, meaning its type checker would necessarily be either unsound or incomplete.↩︎

21. TypeScript确实允许这样的定义方式，不过这意味着它的类型检查机制要么存在缺陷，要么不够完备。↩︎

22. Aiken and Wimmers [1993] used a similar trick, albeit in a more specific set-theoretic interpretation of unions/intersections.↩︎

23. If it were not for pattern matching, we could avoid negation types by adopting a more complicated representation of type variable bounds that internalizes the same information. That is, instead of \(\alpha \le \tau\) and \(\alpha \ge \tau\) for a given type variable \(\alpha\), we would have bounds of the form \(\alpha \land \pi \le \tau\) and \(\alpha \lor \pi \ge \tau\), representing \(\alpha \le \tau \lor \neg \pi\) and \(\alpha \ge \tau \land \neg \pi\) respectively. But reducing several upper/lower bounds into a single bound, which previously worked by simply intersecting/taking the union of them, would now be impossible without generalizing bounds further. Type simplification would also become difficult.↩︎

24. Aiken与Wimmers在1993年使用了类似的技巧，只不过他们是从更为具体的集合论角度来理解并集与交集的概念的。↩︎

25. 如果不存在模式匹配机制，我们可以通过采用一种更为复杂的类型变量界限表示方法来避免使用否定形式。也就是说，对于某个给定的类型变量\(\alpha\)，我们可以不用使用\(\alpha \le \tau\)和\(\alpha \ge \tau\)这样的表达式，而是使用\(\alpha \land \pi \le \tau\)和\(\alpha \lor \pi \ge \tau\)这类表达式来表示相应的含义，即\(\alpha \le \tau \lor \neg \pi\)以及\(\alpha \ge \tau \land \neg \pi\)。但是，如果不能进一步对这些界限进行抽象化处理，那么将多个上下界合并为一个单一的界限就变得不可能了——因为以前我们只需要简单地取这些界限的交集或并集就能完成这一操作。此外，类型的简化也会因此变得十分困难。↩︎

26. This requires extending the syntax of normal forms in a straightforward way to \(\tau'_{con} ::= \tau_{con} \land \overline{\#F}\) and \(\tau'_{dis} ::= \tau_{dis} \lor \overline{\#F}\).↩︎

27. 这意味着需要以一种直接的方式扩展正常形式的语法结构，使其变为 \(\tau'_{con} ::= \tau_{con} \land \overline{\#F}\) 以及 \(\tau'_{dis} ::= \tau_{dis} \lor \overline{\#F}\)。↩︎

28. This does not include about 1200 additional lines of code to generate JavaScript (the tests are run through NodeJS).↩︎

29. 这里并未包括另外大约1200行用于生成JavaScript代码的代码——这些测试是通过NodeJS来运行的。↩︎

30. Indeed, under inconsistent bounds, ill-typed terms become typeable. For example, we have \((\text{Int} \le \text{Int} \to \text{Int}) \vdash 1 1 : \text{Int}\).↩︎

31. 的确，在不统一的类型限制条件下，那些原本被认定为不符合类型规范的表达式也会变得可以被合法使用。例如，我们可以写出 \((\text{Int} \le \text{Int} \to \text{Int}) \vdash 1 1 : \text{Int}\) 这样的表达式。↩︎

32. Perhaps counter-intuitively, it is not a problem to infer types like ‘\(\forall (\alpha \le \alpha)\). \(\tau\)’ and ‘\(\forall (\alpha \le \neg\alpha)\). \(\tau\)’ because such “funny” cyclic bounds, unlike unproductive recursive types, do not actually allow concluding incorrect subtyping relationships.↩︎

33. 或许这与人们的直觉相反，但推断诸如“\(\forall (\alpha \le \alpha)\). \(\tau\)”以及“\(\forall (\alpha \le \neg\alpha)\). \(\tau\)”这样的类型其实并不会引发任何问题。因为这种“奇怪”的循环限制与那些会导致无结果的分析过程不同，并不会真正导致人们得出错误的子类型关系结论。↩︎

34. We can also show that our lattice is uniquely complemented, i.e., \(\neg\tau_1 \equiv \neg\tau_2\) implies \(\tau_1 \equiv \tau_2\).↩︎

35. 我们还可以证明，我们的这种格结构是唯一具有互补性质的，也就是说，如果 \(\neg\tau_1 \equiv \neg\tau_2\)，那么必然有 \(\tau_1 \equiv \tau_2\)。↩︎

36. A lattice homomorphism \(f\) is such that \(f(\tau \vee \pi) \equiv f(\tau) \vee f(\pi)\) and \(f(\tau \wedge \pi) \equiv f(\tau) \wedge f(\pi)\). Function types are lattice homomorphisms in their parameters in the sense that \(f(\tau) = (\neg\tau) \to \pi\) is a lattice homomorphism.↩︎

37. 一个格同态\(f\)应满足以下条件：\(f(\tau \vee \pi) \equiv f(\tau) \vee f(\pi)\)，且\(f(\tau \wedge \pi) \equiv f(\tau) \wedge f(\pi)\)。从某种意义上说，函数类型也可以被视为其参数所构成的格同态；例如，映射\(f(\tau) = (\neg\tau) \to \pi\)显然是一个格同态。↩︎

38. The real implementation is a little smarter and does not always put the entire constraint into DNF to avoid needless work in common cases. It also uses a mutable cache to reuse previous computations and avoid exponential blowups [Pierce 2002].↩︎

39. 实际上，实际的实现方式更为聪明一些，在常见情况下，并不会总是将整个约束条件都放入DNF表达式中，从而避免不必要的计算开销。此外，该实现还会使用可变的缓存机制来重用之前已经计算过的结果，以避免计算量呈指数级增长的情况[Pierce 2002]。↩︎

40. This rule together with T-∧-I was shown unsound in the presence of imperative features by Davies and Pfenning [2000].↩︎

41. For instance, term \(id = \lambda x. x\) has both types \(Int \to Int\) and \(Bool \to Bool\) so by T-∧-I it would also have type \((Int \to Int) \land (Bool \to Bool)\). But by function distributivity and subsumption, this would allow typing \(id\) as \((Int \lor Bool) \to (Int \land Bool)\) and thus typing \(id \ 0\) (which reduces to \(0\)) as \(Int \land Bool\), breaking type preservation.↩︎

42. 例如，项 \(id = \lambda x. x\) 具有两种类型：\(Int \to Int\) 和 \(Bool \to Bool\)；因此根据 T-∧-I 规则，它也应该被赋予类型 \((Int \to Int) \land (Bool \to Bool)\)。然而，由于函数的分配律以及类型包含关系，我们实际上可以将 \(id\) 的类型定义为 \((Int \lor Bool) \to (Int \land Bool)\)；这样一来，当我们对 \(id \ 0\) 进行运算时（这个运算的结果实际上是 \(0\)），它的类型就会变成 \(Int \land Bool\)，从而违反了类型保持规则。↩︎

43. Funnily, MacQueen et al. reported at the time that “type-checking difficulties seem to make intersection and union awkward in practice; moreover it is not clear if there are any potential benefits from their use,”↩︎

44. The first author of this paper has received emails from various people reimplementing Simple-sub [Parreaux 2020] and wanting to know how to add support for first-class union and intersection types, showing the enduring interest in these.↩︎

45. 有趣的是，MacQueen等人当时报告称：“类型检查所带来的种种困难使得在实践中使用‘交集’和‘并集’这些数据结构变得很不方便；此外，目前也不清楚使用这些数据结构是否有任何潜在的优势。”↩︎

46. 本文的第一作者收到了许多人的电子邮件，这些人都正在尝试重新实现Simple-sub算法[Parreaux 2020]，并希望了解如何为这种数据结构添加对一等并集和交集类型的支持。由此可见，人们对此仍保持着浓厚的兴趣。↩︎

47. Hindley-Milner type inference and derived systems like MLsub and MLstruct can also infer types that grow exponentially in some situations, but these mostly occur in pathological cases, and not in common human-written programs.↩︎

48. Hindley-Milner类型的推断系统以及MLsub、MLstruct等衍生系统在某些情况下确实能够推断出那些呈指数级增长的类型，但这类情况大多只出现在一些异常或病态的程序中，并不会出现在常规的人类编写程序中。↩︎

49. For example, in their system \(\neg (\tau \to \pi)\) is the type of all values that are not functions, regardless of \(\tau\) and \(\pi\).↩︎

50. Some authors like Aiken et al. [1994] make a distinction between a concept of principality which is purely syntactic (relating types by a substitution instance relationship) and minimality which involve a semantic interpretation of types.↩︎

51. “Non-structural” here is by opposition to so-called structural subtyping, which is a more tractable but heavily restricted form of subtyping that only relates type constructors of identical arities [Palsberg et al. 1997] (precluding, e.g., {\(x : \tau\)} \(\leq \top\)).↩︎

52. 一些学者，如Aiken等人[1994]，将“原则性”这一概念与“最低限度性”区分开来；前者纯粹是一种句法层面的概念（通过替换关系来关联各种类型），而后者则涉及对类型的语义解读。↩︎

53. 此处所提到的“非结构性”类型系统，是与所谓的结构化子类型系统相对而言的。后者其实是一种更为易于处理、但同时也受到诸多限制的子类型系统形式——这种系统仅允许那些具有相同参数个数的类型构造函数之间进行比较[Palsberg等人，1997年]；因此，诸如{\(x : \tau\)} \(\leq \top\)这样的表达式在结构化子类型系统中是无效的。↩︎

54. As discussed in prior work [Parreaux 2020], we believe the argument for Dolan’s notion of extensibility to be rather weak.↩︎

55. 正如在之前的研究[Parreaux 2020]中所探讨的，我们认为，支持多兰关于“可扩展性”这一概念的观点其实相当薄弱。↩︎