一篇论文的中英文翻译版本：
《The Simple Essence of Algebraic Subtyping. Principal Type Inference with Subtyping Made Easy (Functional Pearl)》 --- LIONEL PARREAUX, EPFL, Switzerland
本文使用了 https://tool.latexdiff.cn/ 进行OCR与LLM翻译，然后放在这里不断校对和改进翻译。下面是正文。
MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand.
MLsub在保留紧凑主类型的同时，扩展了传统的Hindley-Milner类型推断并引入了子类型，这是一个令人兴奋的新发展。然而，它在biunification方面的具体操作难以理解，依赖于bisubstitution和polar types的新概念，并使用了抽象代数中的高级概念。我们在本文中展示，这些实际上并非理解MLsub中运作机制的必要条件。我们提出了一种替代算法，称为Simple-sub，它可以在不到500行代码（包括解析、简化和美化打印）的情况下高效实现，显得更加熟悉，且易于理解。
译者注：这里的Hindley-Milner类型推理算法是一种针对ML语言的类型推理算法。ML语言是一个用于编程语言和类型系统学习和教学的语言。即，《Types and Programming Languages》TAPL这本书里就有相关的讲解。了解相关内容对理解本文有帮助，但不是必须的。
译者注：不太了解类型系统的，可能不太看得懂这个对MLsub的评价。类比一下的话，ML语言就像是课本里的C语言。子类型是一个非常常用的概念，比如说接口或者继承。MLsub还是很不错的，它在类型推理领域做到的事情，类比一下的话，类似于在编程语言里面引入了接口或者继承。
We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system.
我们对Simple-sub和MLsub在百万个随机生成的良好作用域表达式上的实验评估，展示了这两个系统的一致性。基于自动机的MLsub实现与其代数规范相距甚远，留下了许多出错的空间；实际上，我们的评估发现了其中的几个bug。我们基于类型系统的句法规范，简要概述了Simple-sub更直接的正确性和完备性论证。
This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.
本文旨在保持形式上的简洁，提供丰富的见解，并易于新类型系统和编程语言潜在设计者消化。特别是，未对读者施加任何抽象符号的负担。
The ML family of languages, which encompasses Standard ML, OCaml, and Haskell, have been designed around a powerful “global” approach to type inference, rooted in the work of Hindley [1969] and Milner [1978], later closely formalized by Damas and Milner [1982]. In this approach, the type system is designed to be simple enough that types can be unambiguously inferred from terms without the help of any type annotations. That is, for any well-typed unannotated term, it is always possible to infer a principal type which subsumes all other types that can be assigned to this term. For instance, the term \(\lambda x. x\) can be assigned types \(bool \rightarrow bool\) and \(int \rightarrow int\), but both of these are subsumed by the polymorphic type \(\forall \alpha. \alpha \rightarrow \alpha\), also written '\(a \rightarrow 'a\), which is the principal type of this term.
ML语言家族，包括Standard ML、OCaml和Haskell，围绕一种强大的“全局”类型推断方法进行设计，这种方法源于Hindley [1969]和Milner [1978]的工作，后来由Damas和Milner [1982]进行了紧密的形式化。在这种方法中，类型系统的设计足够简单，以至于可以从术语中不借助任何类型注释不明确地推断出类型。也就是说，对于任何良构的未注释术语，总是可以推断出一个主类型，该主类型包含所有可以分配给该术语的其他类型。例如，术语\(\lambda x. x\)可以被分配类型\(bool \rightarrow bool\)和\(int \rightarrow int\)，但是这两者都被多态类型\(\forall \alpha. \alpha \rightarrow \alpha\)所包含，也可以写作'\(a \rightarrow 'a\)，这是该术语的主类型。
This “Hindley-Milner” (HM) type inference approach contrasts with more restricted “local” approaches to type inference, found in languages like Scala, C#, and Idris, which often require the types of variables to be annotated explicitly by programmers. On the flip side, abandoning the principal type property allows these type systems to be more expressive, and to support features like object orientation and dependent types. Even ML languages like OCaml and Haskell have adopted type system features which, when used, break the principal type property1 and sometimes require explicit type annotations. Supporting principal types is a delicate tradeoff.
这种“Hindley-Milner”（HM）类型推断方法与更受限制的“局部”类型推断方法形成对比，后者在像Scala、C#和Idris这样的语言中常常需要程序员显式地注释变量的类型。另一方面，放弃主要类型属性使这些类型系统能够更加表达性，并支持像面向对象和依赖类型一样的特性，即使是像 OCaml 和 Haskell 这样的 ML 语言也采纳了类型系统的特性，当这些特性被使用时，会打破主类型属性2，有时需要显式的类型注释。支持主类型是一种微妙的权衡。
Subtyping is an expressive approach allowing types to be structured into hierarchies — usually a subtyping lattice — with the property that types can be refined or widened implicitly following this hierarchy. This lets one express the fact that some types are more precise (contain more information) than others, but still have a compatible runtime representation, so that no coercions between them are needed. For instance, in a system where the type ‘nat’ is a subtype of ‘int’, one can transparently use a ‘nat list’ in place where an ‘int list’ is expected, without having to apply a coercion function on all the elements of the list. Subtyping can be emulated using somewhat heavy type system machinery (which both OCaml and Haskell do, to some extent3), but first-class support for subtyping gives the benefit of simpler type signatures and better type inference.
子类型化是一种表达能力强的方法，允许将类型结构化为层次——通常是一个子类型 格——其特性是类型可以在这个层次下被细化或扩展，而不需要显式转换。这让人们能表达某些类型比其他类型更精确（包含更多信息），但仍然具有兼容的运行时表示，这样就不需要在它们之间进行任何强制转换。例如，在一个类型‘nat’是‘int’的子类型的系统中，可以透明地在预期为‘int list’的地方使用‘nat list’，而无需对列表的所有元素应用强制转换函数。子类型化可以通过一些较复杂的类型系统机制进行模拟（OCaml 和 Haskell 在某种程度上都这样做4），但是对子类型化的第一类支持则带来了更简单的类型签名和更好的类型推断的好处。
While subtyping is a staple of object-oriented programming (being used to mirror class inheritance hierarchies), it is by no means limited to that paradigm, and has found vast domains of applications in functional programming too, including refinement types for ML data types [Freeman and Pfenning 1991], lightweight verification [Rondon et al. 2008; Rushby et al. 1998; Vazou et al. 2014], full dependent types [Hutchins 2010], first-class modules [Amin et al. 2016; Rossberg 2015], polymorphic variants [Castagna et al. 2016], XML transformations [Hosoya et al. 2005], and higher-rank polymorphism [Dunfield and Krishnaswami 2013; Odersky and Läufer 1996].
虽然子类型是面向对象编程的基本概念（用于反映类继承层次），但这绝不是该范式的唯一应用，它在函数式编程中也找到了广泛的应用领域，包括 ML 数据类型的细化类型 [Freeman and Pfenning 1991]、轻量级验证 [Rondon et al. 2008；Rushby et al. 1998；Vazou et al. 2014]、全依赖类型 [Hutchins 2010]、一类模块 [Amin et al. 2016；Rossberg 2015]、多态变体 [Castagna et al. 2016]、XML 转换 [Hosoya et al. 2005] 和高阶多态 [Dunfield and Krishnaswami 2013；Odersky and Läufer 1996]。
For a long time, it was widely believed that implicit subtyping got in the way of satisfactory global type inference. Indeed, previous approaches to inferring subtypes failed to support principal types, or resulted in the inference of large types containing sets of unwieldy constraints, making them difficult to understand by programmers.
长期以来，人们普遍认为隐式子类型妨碍了令人满意的全局类型推断。事实上，以前的推断子类型的方法未能支持主要类型，或者导致推断出包含一组难以处理的约束的大类型，使得程序员难以理解。
MLsub was introduced by Dolan and Mycroft [2017] as an ML-style type system supporting subtyping, polymorphism, and global type inference, while still producing compact principal types. Here, compact refers to the fact that the inferred types are relatively simple type expressions without any visible constraints, making them easy to read and understand. This was achieved by carefully designing the semantics of the subtyping lattice using an algebra-first approach, also referred to as algebraic subtyping [Dolan 2017].
MLsub 是由 Dolan 和 Mycroft [2017] 提出的 ML 风格类型系统，支持子类型、多态和全局类型推断，同时仍然生成紧凑的主类型。这里的 compact 指的是推断出的类型是相对简单的类型表达式，且没有任何明显的约束，使得它们易于阅读和理解。这是通过精心设计子类型格的语义，采用 algebra-first 方法实现的，这也被称为 algebraic subtyping [Dolan 2017]。
However, the specification of MLsub’s type inference algorithm as biunification is difficult to understand for experts and non-experts alike. On the surface, it looks more complicated than the algorithm W traditionally used for HM type systems, requiring additional concepts such as bisubstitution, polar types, and advanced notions from abstract algebra. Although its elegant presentation will appeal to mathematically-minded researchers, experience has shown that grasping an understanding of the approach complete enough to reimplement the algorithm required reading Dolan’s thesis in full, and sometimes more [Courant 2018].
然而，MLsub 的类型推断算法的规范被称为 biunification 对于专家和非专家来说都很难理解。从表面上看，它看起来比传统上用于 HM 类型系统的 algorithm W 更复杂，要求引入诸如 bisubstitution、polar types 和抽象代数中的高级概念等额外概念。尽管其优雅的呈现方式将吸引有数学思维的研究人员，但经验表明，要完全掌握该方法以重新实现算法，通常需要通读 Dolan 的论文，有时还需要更多的阅读 [Courant 2018]。
Thankfully, it turns out that the essence of algebraic subtyping can be captured by a much simpler algorithm, Simple-sub, which is also more efficient than biunification (or at least, than the basic syntax-driven form of biunification used as a specification for MLsub5). In this paper, we show that inferring MLsub types is surprisingly easy, and can be done in under 300 lines of Scala code, with an additional 200 lines of code for simplification and pretty-printing. Simple-sub is available online at https://github.com/LPTK/simple-sub. While the implementation we present is written in Scala, it is straightforward to translate into any other functional programming languages.
值得庆幸的是，代数子类型的本质可以通过一个更简单的算法Simple-sub来捕获，该算法在效率上也优于双一化（至少优于作为MLsub6规范使用的基本语法驱动形式）。在本文中，我们展示了推导MLsub类型是出乎意料的简单，并且可以在不到300行的Scala代码中完成，另外再增加200行代码用于简化和美化输出。Simple-sub可以在https://github.com/LPTK/simple-sub 在线获取。尽管我们提出的实现是用Scala编写的，但将其转换为其他功能性编程语言是非常简单的。
Our main contribution is to recast MLsub into a simpler mold and to disentangle its algebraic construction of types from the properties actually needed by the type inference and type simplification processes. We believe this will allow future designers of type systems and programming languages to benefit from some of the great insights of the approach, without having to delve too deeply into the theory of algebraic subtyping. In the rest of this paper, we:
我们的主要贡献 是将MLsub重新塑造为一个更简单的模型，并将其类型的代数构造与类型推理和类型简化过程实际需要的属性解开。我们相信将使未来的类型系统和编程语言设计者能够从这种方法的一些重要见解中受益，而无需深入研究代数子类型理论。在本文的其余部分，我们：
- present MLsub and the algebraic subtyping discipline on which it is based (Section 2);
- describe our new Simple-sub type inference algorithm (Section 3);
- explain how to perform basic simplification on the types inferred by Simple-sub (Section 4);
- sketch the correctness proofs of Simple-sub through soundness and completeness theorems, formalizing the minimal subtyping relation needed to carry out these proofs. (Section 5);
- describe our experimental evaluation: we verified that Simple-sub and MLsub agreed on the results of type inference for over a million automatically-generated programs (Section 6).
- 介绍 MLsub 及其所基于的 algebraic subtyping 学科（第 2 节）；
- 描述我们新的 Simple-sub 类型推断算法（第 3 节）；
- 解释如何对由 Simple-sub 推断出的类型进行基本简化（第 4 节）；
- 通过 soundness 和 completeness 定理勾勒 Simple-sub 的正确性证明，形式化进行这些证明所需的最小子类型关系。（第 5 节）；
- 描述我们的实验评估：我们验证了 Simple-sub 和 MLsub 在超过一百万个自动生成的程序的类型推断结果上是一致的（第 6 节）。
Algebraic Subtyping and MLsub
2 代数子类型和MLsub
Let us first describe MLsub and the algebraic subtyping philosophy that underlies its design.
让我们首先描述 MLsub 及其设计所依据的代数子类型哲学。
2.1 Background on Algebraic Subtyping
2.1 代数子类型的背景
There are at least three major schools of thought on formalizing subtyping. Syntactic approaches, as in this paper, use direct specifications (usually given as inference rules) for the subtyping relationship, closely following the syntax of types. Semantic approaches [Frisch et al. 2008] view types as sets of values which inhabit them, and define the subtyping relationship as set inclusion between these sets. Algebraic approaches [Dolan 2017] define types as abstract elements of a distributive lattice, whose algebraic properties are carefully chosen to yield good properties, such as “extensibility” and principal types.
Syntactic approaches somehow pay for their simplicity by forcing type system designers to consider the consequences and interactions of all their inference rules, having to manually verify that they result in a subtyping relationship with the desired algebraic properties.
The semantic approach is probably the most intuitive, and is also very powerful; however, it suffers from difficulties related to polymorphism – an understanding of type variables as ranging over ground types can lead to paradoxes and a lack of extensibility [Dolan 2017].
关于形式化子类型，至少有三种主要的思想流派。语法方法，如本文所述，使用直接的规范（通常以推理规则的形式给出）来描述子类型关系，紧密跟随类型的语法。语义方法 [Frisch et al. 2008] 将类型视为其所占用的值的集合，并将子类型关系定义为这些集合之间的集合包含关系。代数方法 [Dolan 2017] 将类型定义为分布格的抽象元素，其代数性质经过精心选择，以产生良好的性质，如“可扩展性”和主类型。
句法方法在某种程度上因其简单性而付出了代价，使类型系统设计者必须考虑所有推理规则的后果和相互作用，手动验证它们是否产生具有所需代数性质的子类型关系。
语义方法可能是最直观的，且也非常强大；然而，它受到与多态性相关的困难的困扰——将类型变量理解为范围在基础类型上可能导致悖论和缺乏可扩展性 [Dolan 2017]。
As a response to these perceived shortcomings, Dolan argues that algebra (not syntax) should come first, in order to guarantee from the start that type systems are well-behaved, as opposed to ensuring it as a sort of afterthought. In particular, he emphasizes the concept of extensibility of type systems, the idea being that existing programs should remain well-typed when new type forms are added. While the practical usefulness of this notion of extensibility is unclear,7 the general approach of making the subtyping lattice distributive does help simplify types aggressively and construct algorithms for checking subsumption effectively (i.e., checking whether one type signature is as general as another).
In the rest of this section, we explain the basics of MLsub and its static semantics, to set the stage for the presentation of Simple-sub in Section 3.
作为对这些被认为的不足之处的回应，Dolan 认为 algebra（而不是 syntax）应该优先考虑，以确保从一开始就保证类型系统的良好行为，而不是将其视为一种事后考虑。尤其是，他强调了类型系统的 extensibility 概念，核心思想是当添加新的类型形式时，现有程序应该保持良好的类型。虽然这种可拓展性的实际有用性尚不明确，8 但使子类型格 distributive 的一般方法确实有助于有效地简化类型并构建检查包含关系的算法（即检查一个类型签名是否与另一个一样通用）。
在本节的其余部分，我们将解释 MLsub 的基础及其静态语义，为第 3 节中 Simple-sub 的介绍奠定基础。
2.2 Basics of MLsub
2.2.1 Term Language. The term syntax of MLsub is given in Figure 1. We make some simplifications compared to the original MLsub presentation: first, we omit boolean literals and if-then-else, as they can easily be typed as primitive combiners; second, we use only one form of variables x (MLsub distinguished between lambda-bound and let-bound variables, for technical reasons).
\[t ::= x | \lambda x. t | t t | \{ l_0 = t; \dots; l_n = t \} | t.l | \text{let rec } x = t \text{ in } t\]
Fig. 1. Syntax of MLsub terms, for which we want to infer types.
2.2 MLsub基础
2.2.1 项语言。MLsub的项语法如图1所示。与原始的MLsub介绍相比，我们进行了一些简化：首先，我们省略布尔字面量和if-then-else，因为它们可以很容易地被归类为原始组合子；第二，我们仅使用一种形式的变量x（MLsub在技术原因上区分了lambda绑定和let绑定的变量）。
\[ t ::= x | \lambda x. t | t t | \{ l_0 = t; \dots; l_n = t \} | t.l | \text{let rec } x = t \text{ in } t \]
图1. MLsub项的语法，我们希望推导其类型。
2.2.2 Type Language. The type syntax of MLsub, summarized in Figure 2, consists in primitive types (such as int and bool) function types, record types, type variables, top \(\top\) (the type of all values — supertype of all types), bottom \(\bot\) (the type of no values — subtype of all types), type union \(\sqcup\), type intersection \(\sqcap\), and recursive types \(\mu\alpha.\tau\).
\[\tau ::= \text{primitive} | \tau \to \tau | \{ l_0 : \tau; \dots; l_n : \tau \} | \alpha | \top | \bot | \tau \sqcup \tau | \tau \sqcap \tau | \mu\alpha.\tau\]
Fig. 2. Syntax of MLsub types.
2.2.2 类型语言。MLsub 的类型语法如图 2 所示，包含基本类型（如 int 和 bool）、函数类型、结构体类型、类型变量、上界 \(\top\)（所有值的类型——所有类型的超类型）、下界 \(\bot\)（没有值的类型——所有类型的子类型）、类型并 $ $、类型交 $ $ 和递归类型 $ .$。
\[ \tau ::= \text{primitive} | \tau \to \tau | \{ l_0 : \tau; \dots; l_n : \tau \} | \alpha | \top | \bot | \tau \sqcup \tau | \tau \sqcap \tau | \mu\alpha.\tau \]
图 2. MLsub 类型的语法。
2.2.3 Type System. The declarative type system of MLsub is given in Figure 3. It is mostly as presented by Dolan and Mycroft [2017]. We support recursive let bindings explicitly for clarity, though recursion could also be factored out into a combinator [Damas and Milner 1982]. We write \(\overline{E}^i\) for a repetition of elements E indexed by i. Of particular interest are the rules T-SUB, which takes a term from a subtype to a supertype implicitly (without a term-level coercion), T-LET, which types x in its recursive right-hand side in a monomorphic way, but types x in its body polymorphically, and T-VAR, which instantiates polymorphic types using the substitution syntax \([\tau_0/\alpha_0]\tau\).
We appeal to the reader's intuition and leave the precise definition of subtyping unspecified for now, as it requires some technicalities around recursive types. In contrast to MLsub, which gives an algebraic account of subtyping, we will present a syntactic subtyping system in Section 5.1.
\[ \text{T-LIT:} \quad \frac{}{\Gamma \vdash n : \text{int}} \]
\[ \text{T-VAR:} \quad \frac{\Gamma(x) = \overline{\forall \alpha_i.\, \tau}^i}{\Gamma \vdash x : [\tau_i / \alpha_i]^i \tau} \]
2.2.3 类型系统。MLsub 的声明性类型系统如图 3 所示。它大部分与 Dolan 和 Mycroft [2017] 的介绍相同。为了清晰起见，我们显式支持递归 let 绑定，尽管递归也可以被抽象为一个组合子 [Damas 和 Milner 1982]。我们用 \(\overline{E}^i\) 表示索引为 i 的元素 E 的重复。特别值得关注的是规则 T-SUB，它隐式地将一个子类型的项转换为超类型（没有项级的强制转换），规则 T-LET，它以单一类型的方式类型化其递归右侧的 x，但在其主体中以多态的方式类型化 x，以及规则 T-VAR，它使用替换语法 \([\tau_0/\alpha_0]\tau\) 实例化多态类型。
我们借用读者的直觉，目前暂时不对子类型的精确定义进行说明，因为这涉及到递归类型的一些技术细节。与 MLsub 提供的代数子类型描述相比，我们将在第 5.1 节中展示一个语法子类型系统。
\[ \text{T-LIT:} \quad \frac{}{\Gamma \vdash n : \text{int}} \]
\[ \text{T-VAR:} \quad \frac{\Gamma(x) = \overline{\forall \alpha_i.\, \tau}^i}{\Gamma \vdash x : [\tau_i / \alpha_i]^i \tau} \]
\[ \text{T-ABS:} \quad \frac{\Gamma, x : \tau_1 \vdash t : \tau_2}{\Gamma \vdash \lambda x.\, t : \tau_1 \to \tau_2} \]
\[ \text{T-APP:} \quad \frac{\Gamma \vdash t_0 : \tau_1 \to \tau_2 \quad \Gamma \vdash t_1 : \tau_1}{\Gamma \vdash t_0\, t_1 : \tau_2} \]
\[ \text{T-RCD:} \quad \frac{\Gamma \vdash t_i : \tau_i^i}{\Gamma \vdash \{ l_i = t_i \}^i : \{ l_i : \tau_i \}^i} \]
\[ \text{T-PROJ:} \quad \frac{\Gamma \vdash t : \{ l : \tau \}}{\Gamma \vdash t.l : \tau} \]
\[ \text{T-SUB:} \quad \frac{\Gamma \vdash t : \tau_1 \quad \tau_1 \leq \tau_2}{\Gamma \vdash t : \tau_2} \]
\[ \text{T-LET:} \quad \frac{\Gamma, x : \tau_1 \vdash t_1 : \tau_1 \quad \Gamma, x : \overline{\forall \alpha_i.\, \tau_1}^i \vdash t_2 : \tau_2}{\Gamma \vdash \mathbf{let}\ \mathbf{rec}\ x = t_1\ \mathbf{in}\ t_2 : \tau_2} \]
\[ \begin{align*} \text{succ} &: \text{int} \to \text{int} \\ \text{iszero} &: \text{int} \to \text{bool} \\ \text{true} &: \text{bool} \\ \text{false} &: \text{bool} \\ \text{if} &: \forall \alpha.\, \text{bool} \to \alpha \to \alpha \to \alpha \end{align*} \]
Fig. 3. Declarative typing rules of MLsub (and Simple-sub).
2.3 Informal Semantics of Types
\[ \text{T-ABS:} \quad \frac{\Gamma, x : \tau_1 \vdash t : \tau_2}{\Gamma \vdash \lambda x.\, t : \tau_1 \to \tau_2} \]
\[ \text{T-APP:} \quad \frac{\Gamma \vdash t_0 : \tau_1 \to \tau_2 \quad \Gamma \vdash t_1 : \tau_1}{\Gamma \vdash t_0\, t_1 : \tau_2} \]
\[ \text{T-RCD:} \quad \frac{\Gamma \vdash t_i : \tau_i^i}{\Gamma \vdash \{ l_i = t_i \}^i : \{ l_i : \tau_i \}^i} \]
\[ \text{T-PROJ:} \quad \frac{\Gamma \vdash t : \{ l : \tau \}}{\Gamma \vdash t.l : \tau} \]
\[ \text{T-SUB:} \quad \frac{\Gamma \vdash t : \tau_1 \quad \tau_1 \leq \tau_2}{\Gamma \vdash t : \tau_2} \]
\[ \text{T-LET:} \quad \frac{\Gamma, x : \tau_1 \vdash t_1 : \tau_1 \quad \Gamma, x : \overline{\forall \alpha_i.\, \tau_1}^i \vdash t_2 : \tau_2}{\Gamma \vdash \mathbf{let}\ \mathbf{rec}\ x = t_1\ \mathbf{in}\ t_2 : \tau_2} \]
\[ \begin{align*} \text{succ} &: \text{int} \to \text{int} \\ \text{iszero} &: \text{int} \to \text{bool} \\ \text{true} &: \text{bool} \\ \text{false} &: \text{bool} \\ \text{if} &: \forall \alpha.\, \text{bool} \to \alpha \to \alpha \to \alpha \end{align*} \]
图 3. MLsub（和 Simple-sub）的声明性类型规则。
2.3 类型的非正式语义
While most MLsub type forms are usual and unsurprising, two kinds of types require our special attention: set-theoretic types (especially unions and intersections), and recursive types.
2.3.1 Set-Theoretic Types.
To a first approximation, union and intersection types can be understood in set-theoretic terms: \(τ_0 ⊔ τ_1\) (resp. \(τ_0 ⊕ τ_1\)) represents the type of values that are either (resp. both) of type \(τ_0\) or (resp. and) of type \(τ_1\).
MLsub uses these types to indirectly constrain type variables: When a type variable \(α\) is supposed to be a subtype of some type \(τ\) (i.e., values of type \(α\) may be used at type \(τ\)), MLsub substitutes all occurrences of \(α\) in input position with \(α ⊔ τ\), making sure that any arguments passed in as \(α\) values are also \(τ\) values. Similarly, when \(α\) is supposed to be a supertype of some \(τ\) (i.e., values of type \(τ\) may be used at type \(α\)), MLsub substitutes all occurrences of \(α\) in output position with \(α ⊔ τ\), making sure that results returned as \(α\) values are also \(τ\) values.
虽然大多数 MLsub 类型形式是常见且不令人惊讶的，但有两种类型需要我们特别关注：集合论类型（尤其是并集和交集）和递归类型。
2.3.1 集合论类型
初步来看，联结类型和交集类型可以用集合论术语来理解：\(τ_0 ⊔ τ_1\)（分别为 \(τ_0 ⊕ τ_1\)）表示的值的类型要么是（分别是）\(τ_0\) 类型，要么是（分别是）\(τ_1\) 类型。
MLsub 使用这些类型来间接约束类型变量：当一个类型变量 \(α\) 应该是某类型 \(τ\) 的 子类型 时（即，类型为 \(α\) 的值可以在类型 \(τ\) 中使用），MLsub 会用 \(α ⊔ τ\) 替换输入位置中所有 \(α\) 的出现，确保作为 \(α\) 值传入的任何参数也是 \(τ\) 值。类似地，当 \(α\) 应该是某个 \(τ\) 的 超类型 时（即，类型为 \(τ\) 的值可以在类型 \(α\) 中使用），MLsub 会用 \(α ⊔ τ\) 替换输出位置中所有 \(α\) 的出现，确保作为 \(α\) 值返回的结果也是 \(τ\) 值。
As an example, one type inferred for the term \(λx. \{ L = x - 1; R = x \}\) could be \(α ⊕ int → \{ L : int; R : α \}\), assuming operator \((-)\) has type \(int → int → int\). This type reflects the fact that the original argument, of some type \(α\), is returned in the R field of the result record (as the input of the function ends up in that position), but also that this argument should be able to be treated as an int, expressed via the type intersection \(α ⊕ int\) on the left-hand side of the function type. Keeping track of the precise argument type \(α\) is important: it could be later substituted with a more specific type than int, such as \(α = nat\), which would give us \(nat → \{ L : int; R : nat \}\). On the other hand, there may be type signatures where \(α\) becomes undistinguishable from int. For instance, consider the term '\(λx. if true then x - 1 else x\)', whose simplified inferred type would be just int → int, as the seemingly-more precise type \(α ⊕ int → α ⊔ int\) does not actually contain more information (we expand on this in Section 4.3.1).
作为一个例子，术语 \(λx. \{ L = x - 1; R = x \}\) 推断出的一个类型可以是 \(α ⊕ int → \{ L : int; R : α \}\)，假设运算符 \((-)\) 的类型为 \(int → int → int\)。这个类型反映了一个事实，即原始参数，某个类型为 \(α\) 的值，被返回在结果结构体的 R 字段中（因为函数的输入最终位于这个位置），同时也表明这个参数应该能够被视为一个 int，通过函数类型左侧的类型交集 \(α ⊕ int\) 表达。跟踪精确的参数类型 \(α\) 是重要的：它可以在后面用比 int 更具体的类型替代，例如 \(α = nat\)，这将给我们 \(nat → \{ L : int; R : nat \}\)。另一方面，可能存在某些类型签名，其中 \(α\) 变得与 int 无法区分。例如，考虑术语 '\(λx. if true then x - 1 else x\)，其简化后的推断类型将只是 int → int，因为看似更精确的类型 \(α ⊕ int → α ⊔ int\) 实际上并未包含更多信息（我们将在第 4.3.1 节中对此进行扩展）。
The beauty of MLsub is that this sort of reasoning scales to arbitrary flows of variables and higher-order functions; for instance, the previous example can be generalized by passing in a function \(f\) to stand for the \(· - 1\) operation, as in \(λf. λx. \{ L = f x; R = x \}\) whose type could be inferred as \((β → γ) → α ⊕ β → \{ L : γ; R : α \}\) and further simplified to \((α → γ) → α → \{ L : γ; R : α \}\). Applying this function to argument \((λx. x - 1)\) yields the same type (after simplification) as in the example of the previous paragraph.
2.3.2 Recursive Types.
A recursive type \(μα. τ\) represents a type we can unroll as many times as we want; for instance, \(μα. (T → α)\), which we write just \(μα. T → α\), is equivalent to \(T → μα. T → α\), which is equivalent to \(T → T → μα. T → α\), etc., and is the type of a function that can be applied to any arguments (any subtypes of \(T\)) indefinitely. A recursive type is conceptually infinite — if we unrolled the above fully, it would unfold as an infinitely-deep tree \(T → T → T → ...\)
MLsub 的美在于这种推理可以扩展到任意的变量流和高阶函数；例如，之前的例子可以通过传递一个函数 \(f\) 来代表 \(· - 1\) 操作进行广义化，如 \(λf. λx. \{ L = f x; R = x \}\)，其类型可以推断为 \((β → γ) → α ⊕ β → \{ L : γ; R : α \}\)，进一步简化为 \((α → γ) → α → \{ L : γ; R : α \}\)。将此函数应用于参数 \((λx. x - 1)\) 产生与前一段示例相同的类型（经过简化后）。
2.3.2 递归类型。
递归类型 \(μα. τ\) 代表一个我们可以展开任意次的类型；例如，\(μα. (T → α)\)，我们简写为 \(μα. T → α\)，它等同于 \(T → μα. T → α\)，进一步等同于 \(T → T → μα. T → α\)，等等，这就是一个可以无限期应用于任何参数（T 的任何子类型）的函数的类型。递归类型在概念上是无限的——如果我们完全展开上述内容，它将展现为一个无限深的树 \(T → T → T → ...\)
If this sounds confusing, that's perfectly fine. We will get some deeper intuition on recursive types and why we need them in Section 3.4.1, and we will give them a formal treatment in Section 5.1. The high-level idea is that recursive types are sometimes necessary to give principal types to MLsub terms. The example given by Dolan [2017] is that of the term \(Y(λf. λx. f)\) where \(Y\) is the call-by-value \(Y\) combinator. This term represents a function which ignores its parameter and returns itself. It can be given type \(T → T\) as well as \(T → T → T\), and \(T → T → T → T\), etc. Its principal type is the recursive type shown in the previous paragraph.
2.3.3 Typing Surprises.
It is worth noting that inferring recursive types can lead to typing terms which appear ill-typed, and would in fact not be well-typed in ML.9 This kind of surprises can also arise simply due to subtyping. For instance, in MLsub, the strange-looking term \(\lambda x. x x\), which takes a function in parameter and applies it to itself, can be typed as \(\forall \alpha, \beta. (\alpha \to \beta) \sqcap \alpha \to \beta\). Indeed, if the input \(x\) passed to the function has type \((\alpha \to \beta) \sqcap \alpha\), that means it has type \(\alpha \to \beta\) (a function taking an \(\alpha\) argument) and type \(\alpha\), meaning that it can be passed as an argument to itself.
如果这听起来让人困惑，那是完全可以理解的。我们将在第3.4.1节中深入理解递归类型以及我们为什么需要它们，并将在第5.1节中对它们进行正式处理。总体思路是，递归类型有时是必要的，以便为MLsub术语提供主类型。Dolan [2017]给出的例子是术语\(Y(λf. λx. f)\)，其中\(Y\)是按值调用的\(Y\)组合子。这个术语表示一个忽略其参数并返回自身的函数。它可以被赋予类型\(T → T\)以及\(T → T → T\)，还有\(T → T → T → T\)，等等。它的主类型是前一段中所示的递归类型。
2.3.3 类型意外
值得注意的是，推断递归类型可能导致出现看起来类型不正确的术语，实际上在ML中并不会是良好类型的。10 这类意外也可能简单地源于子类型。例如，在 MLsub 中，奇怪的术语 \(\lambda x. x x\)，它以一个函数作为参数并将其应用于自身，可以被类型化为 \(\forall \alpha, \beta. (\alpha \to \beta) \sqcap \alpha \to \beta\)。事实上，如果传递给函数的输入 \(x\) 的类型是 \((\alpha \to \beta) \sqcap \alpha\)，这意味着它具有类型 \(\alpha \to \beta\)（一个接受 \(\alpha\) 参数的函数）和类型 \(\alpha\)，意味着它可以作为自身的参数传递。
2.4 Expressiveness
2.4 表达能力
There is an important caveat to add to the definition of types we gave above: these types cannot actually be used freely within type expressions. The true syntax of MLsub is segregated between positive and negative types. In particular, unions are positive types (and may not appear in negative position) and intersections are negative types (and may not appear in positive position).
2.4.1 Polarity of Type Positions.
Positive positions correspond to the types that a term outputs, while negative positions correspond to the types that a term takes in as input. For instance, in \((\tau_0 \to \tau_1) \to \tau_2\), type \(\tau_2\) is in positive position since it is the output of the main function, and the function type \((\tau_0 \to \tau_1)\) is in negative position, as it is taken as an input to the main function. On the other hand, \(\tau_1\), which is returned by the function taken as input is in negative position (since it is provided by callers via the argument function), and \(\tau_0\) is in positive position (since it is provided by the main function when calling the argument function).
需要在上述类型定义中添加一个重要的警告：这些类型实际上不能在类型表达式中被自由使用。MLsub 的真实语法在 正 类型和 负 类型之间是分隔的。特别地，联合是正类型（不能出现在负位置），而交集是负类型（不能出现在正位置）。
2.4.1 类型位置的极性。
正位置对应于一个术语 输出 的类型，而负位置对应于一个术语 作为输入接收 的类型。例如，在 \((\tau_0 \to \tau_1) \to \tau_2\) 中，类型 \(\tau_2\) 位于正位置，因为它是主函数的输出，而函数类型 \((\tau_0 \to \tau_1)\) 位于负位置，因为它作为主函数的输入。另一方面，\(\tau_1\) 是由 作为输入的函数返回 的，所以它位于负位置（因为它是通过调用者提供的参数函数提供的），而 \(\tau_0\) 位于正位置（因为它是由主函数在调用参数函数时提供的）。
2.4.2 Consequence of the Polarity Restriction.
These polarity restrictions mean that the full syntax of
types we saw above cannot actually be used as is; programmers cannot
write, in their own type annotations, types that violate the polarity
distinction. In fact, in MLsub, one cannot express the type of
a function which takes “either an integer or a string”: type
int \(\sqcup\)
string \(\to\) \(\tau\) is illegal because it has the
int \(\sqcup\)
string union in negative position. On the other hand, MLsub
may assign the legal type \(\tau \to\)
int \(\sqcup\)
string to functions which may return either an integer or a
string... but this is not a very useful type, since one cannot do
anything useful with an int \(\sqcup\) string value in
MLsub.11
What this all comes down to, perhaps surprisingly, is that the MLsub language is fundamentally no more expressive12 than a “structurally-typed Java”, by which we mean a hypothetical Java dialect with structural records and lower as well as upper bounds for type variables. To understand this, consider the following function:
\[ \lambda x. \{ L = x - 1; R = \text{if } x < 0 \text{ then } 0 \text{ else } x \} \]
2.4.2 极性限制的后果。
这些 极性
限制意味着我们上面看到的类型的完整语法实际上无法按原样使用；程序员不能在自己的类型注释中编写违反极性区分的类型。事实上，在
MLsub 中，人们 无法
表达一个接受“整数或字符串”的函数的类型：类型 int \(\sqcup\) string \(\to\) \(\tau\) 是非法的，因为它在负位置上有
int \(\sqcup\)
string 的并集。另一方面，MLsub 可以将合法类型 \(\tau \to\) int \(\sqcup\) string
分配给可能返回整数或字符串的函数……但这并不是一个非常有用的类型，因为在
MLsub 中，人们无法对 int \(\sqcup\) string
值进行任何有用的操作。13
这一切归结起来，也许令人惊讶的是，MLsub 语言在表达能力上根本不比“结构类型（structurally-typed）的 Java”更强14，我们指的是一种假设的 Java 方言，具有结构化的结构体（structural records）以及类型变量的下限和上限。要理解这一点，请考虑以下函数：
\[ \lambda x. \{ L = x - 1; R = \text{if } x < 0 \text{ then } 0 \text{ else } x \} \]
which could be given the following unsimplified type by MLsub or Simple-sub:
\[ \alpha \sqcap \text{int} \to \{ L : \text{int}; R : \beta \sqcup \text{nat} \sqcup \alpha \} \]
or equivalently, after simplification:
\[ \alpha \sqcap \text{int} \to \{ L : \text{int}; R : \text{nat} \sqcup \alpha \} \]
The \(\beta\) type variable is introduced to represent the result type of the if expression. During type inference, both constraints \(\text{nat} \le \beta\) and \(\alpha \le \beta\) are registered, which is handled by replacing all occurrences of \(\beta\) in positive positions (there is only one here) by \(\beta \sqcup \text{nat} \sqcup \alpha\). In this simple example, the \(\beta\) type variable turns out to be redundant, and is later removed during simplification.
Now, recall that Java allows users to quantify types using type variables, and also allows bounding these type variables with subtypes and supertypes.15 The insight is that unions and intersections,
可以通过 MLsub 或 Simple-sub 给出以下 未简化 类型：
\[ \alpha \sqcap \text{int} \to \{ L : \text{int}; R : \beta \sqcup \text{nat} \sqcup \alpha \} \]
或者等价地，在简化后：
\[ \alpha \sqcap \text{int} \to \{ L : \text{int}; R : \text{nat} \sqcup \alpha \} \]
\(\beta\) 类型变量被引入以表示 if 表达式的结果类型。在类型推断期间，两个约束 \(\text{nat} \le \beta\) 和 \(\alpha \le \beta\) 被记录，这通过将所有正位置上（这里只有一个）的 \(\beta\) 替换为 \(\beta \sqcup \text{nat} \sqcup \alpha\) 来处理。在这个简单的例子中，\(\beta\) 类型变量被证明是多余的，并在简化过程中被移除。
现在，回想一下 Java 允许用户使用类型变量来量化类型，同时也允许用子类型和超类型来限制这些类型变量。16 这个见解是，联合和交叉，
when used at the appropriate polarity, are only a way of indirectly
bounding type variables. For instance, the unsimplified MLsub type seen
above is equivalent to the following Java-esque type, where type
parameters are written between ⟨ and ⟩:
\[ \langle \alpha \ extends \ int, \ \beta \ super \ nat \mid \alpha \rangle(\alpha) \to \{ L : int; R : \beta \} \]
meaning that \(\alpha\) should be a subtype of int and that \(\beta\) should be a supertype of both nat and \(\alpha\). Moreover, the simplified type is equivalent to:
\[ \langle \alpha \ super \ nat \ extends \ int \rangle(\alpha) \to \{ L : int; R : \alpha \} \]
当在适当的极性下使用时，仅仅是在间接限制类型变量的一种方式。例如，上面未简化的MLsub类型等同于以下Java风格的类型，其中类型参数写在⟨和⟩之间：
\[ \langle \alpha \ extends \ int, \ \beta \ super \ nat \mid \alpha \rangle(\alpha) \to \{ L : int; R : \beta \} \]
这意味着\(\alpha\)应该是int的子类型，而\(\beta\)应该是nat和\(\alpha\)的超类型。此外，简化后的类型等同于：
\[ \langle \alpha \ super \ nat \ extends \ int \rangle(\alpha) \to \{ L : int; R : \alpha \} \]
meaning that \(\alpha\) should be a supertype of nat and also a subtype of int.
As for MLsub's recursive types, they are expressible via F-bounded polymorphism, which Java also supports. F-bounded polymorphism allows a type variable \(\alpha\) to be bounded by a type expression that contains occurrences of \(\alpha\) itself.
The fact that type intersections can be used to encode upper bounds on type variables was originally remarked by Castagna and Xu [2011, footnote 4]. Naturally, the same goes for type unions and lower bounds respectively. What we proposed above is, in a sense, the reverse direction of this translation: stating that polar usages of unions and intersections can be encoded as lower and upper bounds on type variables.
2.5 Essence of MLsub Type Inference
Reading Dolan [2017]; Dolan and Mycroft [2017], one could be led to think that MLsub is all about:
- supporting unions and intersections in the type language, forming a distributive lattice;
- a new algorithm called biunification as an alternative to traditional unification;
- separating the syntax of types between positive and negative types.
意味着 \(\alpha\) 应该是 nat 的超类型，同时也是 int 的子类型。
至于 MLsub 的递归类型，它们可以通过 F-bounded polymorphism 来表达，Java 也支持这一点。F-bounded polymorphism 允许一个类型变量 \(\alpha\) 受到一个包含 \(\alpha\) 本身的类型表达式的限制。
类型交集可用于编码类型变量的上界这一事实最初是由 Castagna 和 Xu [2011, footnote 4] 提出的。自然，类型并集和下界同样适用。我们上面所提的在某种意义上是这种翻译的反向方向：即表明极性使用的并集和交集可以作为类型变量的下界和上界进行编码。
2.5 MLsub 类型推断的本质
阅读 Dolan [2017]; Dolan 和 Mycroft [2017]，人们可能会认为 MLsub 全部是关于：
- 在类型语言中支持并集和交集，形成一个分布格；
- 一种名为 biunification 的新算法，作为传统统一的替代方案；
- 将类型的语法分为正类型和负类型。
However, we argue that this is not the most helpful way of understanding the processes at work in this type inference algorithm; instead, we argue that the essence of the approach is:
- making the semantics of types simple enough that all inferred subtyping constraints can be reduced to constraints on type variables, which can be recorded efficiently (for instance using mutation, as done in this paper and in MLsub's actual implementation);
- using intersection, union, and recursive types to express compact type signatures where type variables are indirectly constrained, avoiding the need for separate constraint specifications.
3 THE SIMPLE-SUB TYPE INFERENCE ALGORITHM
然而，我们认为这并不是理解这种类型推导算法中运行过程的最有帮助的方法；相反，我们认为该方法的本质是：
- 使类型的语义足够简单，以便所有推导出的子类型约束都可以简化为对类型变量的约束，这些约束可以高效记录（例如使用变异，如本文和MLsub的实际实现所做的那样）；
- 使用交集、并集和递归类型来表达紧凑的类型签名，其中类型变量受到间接约束，避免了单独约束规范的需要。
3 SIMPLE-SUB 类型推导算法
We now present Simple-sub. We start with the internal Scala syntax used in the algorithms (Section 3.1); we then describe the basic mechanisms of type inference, at first omitting let bindings for simplicity (Section 3.2); we show how to produce user-facing type representations from the results of type inference (Section 3.3); we discuss some insights on recursive types and unroll an example of type inference (Section 3.4); and we explain how to support let polymorphism and recursive let bindings (Section 3.5). Finally, we summarize the full Simple-sub algorithm (Section 3.6).
3.1 Simple-sub Syntax
3.1.1 Term Syntax. The Scala implementation of the term syntax is shown in Figure 4. We derive it directly from Figure 1, except that we add a construct for integer literals.
As mentioned before, there is no need for an if-then-else feature, since we can just add one as a combinator: our parser actually parses code of the form "if \(e_0\) then \(e_1\) else \(e_2\)" as if it were written
我们现在介绍 Simple-sub。我们首先介绍算法中使用的内部 Scala 语法（第 3.1 节）；然后描述类型推断的基本机制，最初省略 let 绑定以简化问题（第 3.2 节）；接着展示如何从类型推断的结果生成用户可见的类型表示（第 3.3 节）；我们讨论一些关于递归类型的见解，并演示一个类型推断的例子（第 3.4 节）；最后，我们解释如何支持 let 多态性和递归 let 绑定（第 3.5 节）。最后，我们总结完整的 Simple-sub 算法（第 3.6 节）。
3.1 Simple-sub 语法
3.1.1 项语法。 Scala 对项语法的实现如图 4 所示。我们直接从图 1 中推导出来，除了我们添加了一个整数字面量的构造。
如前所述，实际上不需要 if-then-else 特性，因为我们可以将其作为一个组合子添加：我们的解析器实际上将形式为 "if \(e_0\) then \(e_1\) else \(e_2\)" 的代码解析为它被写成的样子。
1 | enum Term { |
Fig. 4. Scala syntax for MLsub terms (using the enum¹⁰
keyword for defining algebraic data types).
“\(\text{if } e_0 e_1 e_2\),” and we perform type checking starting from a context which assigns to the ‘if’ identifier the type \(\forall \alpha\). \(bool \to \alpha \to \alpha \to \alpha\).17
1 | enum SimpleType { |
1 | enum Term { |
图 4. Scala 语法用于 MLsub 术语（使用 enum¹⁰
关键字定义代数数据类型）。
“\(\text{if } e_0 e_1 e_2\)，”并且我们从一个上下文开始进行类型检查，该上下文将 'if' 标识符分配类型为 \(\forall \alpha\). \(bool \to \alpha \to \alpha \to \alpha\).18
1 | enum SimpleType { |
3.1.2 Type Syntax.
We start from the realization that union, intersection, top, bottom, and recursive types are all not really core to the type inference approach. Therefore, we focus on type variables, basic type constructors (primitive types), function types, and record types as the cornerstone of the algorithm. Their Scala syntax is shown above.
The state of a type variable is simply given by all the bounds that are recorded for it:
1 | class VariableState(var lowerBounds: List<SimpleType], |
Notice that we use mutable variables (var instead of
val) in order to hold the current state of the algorithm —
these lists will be mutated as the algorithm proceeds.
All we need to do in order to perform type inference now is to find all subtyping constraints entailed by a given program, and to propagate these constraints until they reach type variables, which we can constrain by mutating their recorded bounds.
3.2 Basic Type Inference
3.1.2 类型语法。
我们从意识到联合、交集、上界、下界和递归类型实际上并不是类型推断方法的核心开始。因此，我们将焦点放在类型变量、基本类型构造（原始类型）、函数类型和结构体类型上，作为算法的基石。它们的 Scala 语法如上所示。
类型变量的状态仅由为其记录的所有约束给出：
1 | class VariableState(var lowerBounds: List<SimpleType], |
请注意，我们使用可变变量（var 而非
val）来保持算法的当前状态——这些列表将在算法进行过程中被修改。
为了执行类型推断，我们现在需要做的就是找到给定程序所涉及的所有子类型约束，并传播这些约束，直到它们达到类型变量，然后我们可以通过修改其记录的约束来限制它们。
3.2 基本类型推断
3.2.1 Typing.
The core function for type inference is typeTerm, which
assigns a type to a given term in some context of type Ctx;
it is complemented by a constrain function to imperatively
constrain one type to be a subtype of another, raising an error if that
is not possible:
1 | type Ctx = Map String, SimpleType] |
Above, we made the ctx parameter in
typeTerm implicit so it does not have to be passed
explicitly into each recursive call if it does not change.
We make use of two small helper functions, freshVar and
err, to generate new type variables and raise errors,
respectively:
1 | def freshVar: Variable = |
3.2.1 类型推断。
类型推断的核心功能是 typeTerm，它在某个类型为
Ctx 的上下文中为给定的术语分配类型；它由一个
constrain
函数补充，该函数用于强制一个类型是另一个类型的子类型，如果不可能，则抛出错误：
1 | type Ctx = Map[String, SimpleType] |
在上面，我们将 typeTerm 中的 ctx
参数设为隐式的，这样如果它不变，就不必在每个递归调用中显式传入。
我们使用两个小辅助函数 freshVar 和
err，分别用于生成新的类型变量和引发错误：
1 | def freshVar: Variable = |
Remember that VariableState is a class and not a case
class (also called data class). This means that each
VariableState instance, created with new, is
unique and distinct from other instances.
Now that we have established the necessary premises, we can start writing the core of the basic type inference algorithm:
1 | def typeTerm(term: Term)(implicit ctx: Ctx): SimpleType = term match { |
Below, the ctx.getOrElse(k, t) function is used to
access the ctx map at a given key k,
specifying a chunk t to execute in case that key is not
found:
1 | // variable references: |
In order to type a lambda abstraction, we create a fresh variable to
represent the parameter type, and we type the body of the lambda in the
current context extended with a binding for this parameter, where
name -> param is another syntax for the pair
(name, param):
请记住，VariableState 是一个类，不是一个案例类（也称为
data class）。这意味着每个通过 new 创建的
VariableState 实例都是唯一的，与其他实例不同。
现在我们已经建立了必要的前提，我们可以开始编写基本类型推断算法的核心部分：
1 | def typeTerm(term: Term)(implicit ctx: Ctx): SimpleType = term match { |
下面，ctx.getOrElse(k, t) 函数用于在给定键
k 的 ctx
映射中访问，指定在未找到该键的情况下执行的代码块 t：
1 | // 变量引用： |
为了为一个 lambda
抽象指定类型，我们创建一个新的变量来表示参数类型，并在当前上下文中使用该参数的绑定类型化
lambda 的主体，其中 name -> param 是对配对
(name, param) 的另一种语法：
1 | // lambda abstractions: |
To type applications, we similarly introduce a fresh variable standing for the result type of the function that we are applying:
1 | // applications: |
Finally, record accesses result in a constraint that the receiver on the left-hand side of the selection is a record type with the appropriate field name:
1 | // record field selections: |
As one can observe, the basic MLsub type inference algorithm so far is quite similar to the traditional algorithm W for HM-style type inference.
3.2.2 Constraining
The first thing to diverge from algorithm W is the handling of constraints.
1 | // λ 抽象: |
为了分析函数调用的类型，我们同样引入一个新变量，表示我们正在调用的函数的结果类型：
1 | // 函数调用: |
最后，结构体访问导致了一个约束，要求选择左侧的接收是具有适当字段名称的结构体类型：
1 | // 结构体字段选择: |
如可以观察到的，基本的 MLsub 类型推断算法到目前为止与传统的算法 W 在 HM 风格的类型推断中非常相似。
3.2.2 约束
第一个与算法 W 不同的地方是约束的处理。
First, note that type variable bounds, which are updated using mutation, may very well begin to form cycles as type inference progresses. We have to account for this by using a cache parameter (initially empty) which remembers all the type comparisons that have been or are being made. This not only prevents us from falling into infinite recursion, but also avoids repeating identical work (i.e., solving some of the sub-constraints more than once), which is important to avoid making the algorithm exponential in complexity [Pierce 2002, Chapter 21.10].
1 | def constrain(lhs: SimpleType, rhs: SimpleType) |
The next step is to match each possible pair of basic types which can be constrained successfully, and propagate the constraints accordingly:
首先，请注意，随着类型推断的进行，使用变异更新的类型变量边界很可能开始形成循环。我们必须通过使用一个缓存参数（初始为空）来考虑这一点，该参数记住所有已进行或正在进行的类型比较。这不仅可以防止我们陷入无限递归，还可以避免重复相同的工作（即，对某些子约束的求解进行多次），这对于避免使算法的复杂性变为指数级是很重要的 [Pierce 2002, Chapter 21.10]。
1 | def constrain(lhs: SimpleType, rhs: SimpleType) |
下一步是匹配每对可以成功约束的基本类型，并相应地传播约束：
1 | (lhs, rhs) match { |
Function types are constrained according to the usual rules of contra- and co-variance of parameter and result types (respectively), and record types according to the usual width and depth subtyping.
The case for type variables appearing on the left- or right-hand side is interesting, as this is when we finally mutate the bounds of variables. Crucially, after adding the corresponding upper or lower bound to the variable state, we need to iterate19 over the existing opposite bounds of the variable being constrained, in order to make sure that they become consistent with the new bound:
1 | case (Variable(lhs), rhs) => |
1 | (lhs, rhs) match { |
Function 类型根据参数和结果类型（分别）的协变和反变的常规规则进行约束，而结构体类型则根据常规的宽度和深度子类型进行约束。
在左侧或右侧出现的类型变量的情况是有趣的，因为这时我们最终改变变量的边界。至关重要的是，在将相应的上界或下界添加到变量状态后，我们需要遍历20已存在的与约束变量相对的边界，以确保它们与新的边界保持一致：
1 | case (Variable(lhs), rhs) => |
Note that there is something deeply non-trivial happening here: we
install the new upper bound rhs before recursing into the
lhs.lowerBounds. This turns out to be essential — without
it, recursive constraining calls which would get back to
lhs would miss this new upper bound, failing to constrain
it. Another subtlety is that new bounds may very well appear in
lhs.upperBounds and lhs.lowerBounds while we
are recursing. This subtlety is briefly discussed further in Section
5.3.1.
Finally, if all other options have failed, we report an error that the two types cannot be constrained:
1 | case _ => err("cannot constrain " + lhs + " <: " + rhs) |
注意，这里发生了一些深刻的非平凡的事情：我们在递归进入
lhs.lowerBounds 之前安装新的上界
rhs。这被证明是至关重要的——如果没有它，递归约束调用将会返回到
lhs
时会错过这个新的上界，从而无法对其进行约束。另一个微妙之处是，在我们递归期间，新的界限很可能会出现在
lhs.upperBounds 和 lhs.lowerBounds
中。这个微妙之处在第 5.3.1 节中有所简要讨论。
最后，如果所有其他选项都失败了，我们报告一个错误，说明这两种类型无法被约束：
1 | case _ => err("cannot constrain " + lhs + " <: " + rhs) |
In this subsection, we saw the core of the Simple-sub type inference algorithm, which distills what we argue is the “simple essence” of Dolan’s type inference approach. However, we are not quite done yet. We still need to produce user-readable type representations (next section) and to support polymorphism and recursion through let bindings (Section 3.5).
3.3 User-Facing Types Representations
Where did union, intersection, top, bottom, and recursive types go?
It turns out these are not really core to the type inference approach, and are more like emergent properties of type pretty-printing and simplification. They only come up once we try to display friendly type expressions to users, after type inference has done the gist of its job.
3.3.1 Constraining Type Variables Indirectly. Remember that we have been constraining type variables, but that type variable constraints are not part of the syntax that MLsub and Simple-sub are supposed to output. The “trick” is to indirectly encode these constraints through the use of union and intersection types (recall the examples given in Section 2.3.1).
在这一小节中，我们看到了简易子类型推断算法的核心，这提炼了我们认为是Dolan类型推断方法的“简单本质”。然而，我们尚未完成。我们仍需生成用户可读的类型表示（下一节）并通过let绑定支持多态和递归（第3.5节）。
3.3 面向用户的类型表示
并集、交集、顶、底和递归类型去哪儿了？
事实证明，这些并不是类型推断方法的核心，更像是类型美观打印和简化的涌现属性。它们在我们尝试向用户展示友好的类型表达式时才会出现，在类型推断完成其核心工作之后。
3.3.1 间接约束类型变量。请记住，我们一直在约束类型变量，但类型变量约束并不是MLsub和Simple-sub应该输出的语法的一部分。“技巧”在于通过使用并集和交集类型间接编码这些约束（回忆第2.3.1节中给出的例子）。
3.3.2 Targeted Type Syntax. In order to produce user-friendly type representations in the tradition of MLsub, we target the type syntax tree presented in Figure 5.
1 | enum Type { |
Fig. 5. The type syntax targeted as the end result of type inference.
3.3.3 Type Coalescing Algorithm. In order to produce immutable Type values from our inferred SimpleType internal representation, we need to go through a process we refer to as type coalescing, whose goal is to replace the positive occurrences of type variables with a union of their lower bounds, and their negative occurrences with an intersection of their upper bounds.
3.3.2 目标类型语法. 为了生成符合用户友好的类型表示，遵循MLsub的传统，我们的目标是图5中呈现的类型语法树。
1 | enum Type { |
图5. 作为类型推断最终结果的目标类型语法。
3.3.3 类型合并算法. 为了从我们推断的SimpleType内部表示中生成不可变的Type值，我们需要经历一个我们称之为类型合并的过程，其目标是用其下界的并集替换type变量的正出现，用其上界的交集替换负出现。
We define a PolarVariable type synonym which associates a type variable state with a polarity. The algorithm starts by initializing an empty mutable map called recursive, whose goal is to remember which type variables refer to themselves through their bounds, assigning them a fresh type variable which will be used when constructing the corresponding RecursiveType value:
1 | type PolarVariable = (VariableState, Boolean) // 'true' means 'positive' |
The (VariableState, Boolean) keys of the recursive map include the polarity in the right-hand side to make sure we produce only polar recursive types (those whose variables occur with the same polarity as the types themselves); this turns out to be necessary for principality [Dolan 2017].
Then, we define a worker function go which calls itself recursively in a straightforward manner, but makes sure to keep track of the type variables that are currently being coalesced, and to keep track of the current polarity — whether we are coalescing a positive (polar == true) or negative (polar == false) type position:
我们定义了一个 PolarVariable 类型同义词，它将 类型变量 状态与 极性 关联起来。算法首先初始化一个空的可变映射 recursive，其目的是记住哪些 类型变量 通过它们的边界引用自身，并为它们分配一个新的类型变量，该变量将在构造相应的 RecursiveType 值时使用：
1 | type PolarVariable = (VariableState, Boolean) // 'true' 表示 'positive' |
递归映射的 (VariableState, Boolean) 键在右侧包含极性，以确保我们只生成 polar 递归类型（这些类型的变量与类型本身的极性相同）；这被证明对于首要性是必要的 [Dolan 2017]。
然后，我们定义一个工作函数 go，它以直接的方式递归调用自身，但确保跟踪当前正在合并的类型变量，以及跟踪当前极性——我们是合并正类型 (polar == true) 还是负类型 (polar == false) 的位置：
1 | def go(ty: SimpleType, polar: Boolean)(inProcess: Set[PolarVariable]): Type |
The interesting case is the following.21
In the code below, vs.uniqueName, is an attribute defined
in the VariableState class, which holds a name unique to
vs.
1 | case Variable(vs) => |
1 | def go(ty: SimpleType, polar: Boolean)(inProcess: Set[PolarVariable]): Type |
We first check whether the variable is already being coalesced. If it
is, we look up the 'recursive' map: if this map already contains an
entry for the variable, we simply return it; otherwise, we create a new
fresh TypeVariable and update the map using
getOrElseUpdate.
If we are not coalescing a recursive variable occurrence, we look into the bounds of the variable. Depending on the current polarity, we recurse into the lower or upper bounds. Then, if the recursive
map now contains an entry for the variable, it means the variable was recursive. In this case, we wrap the result in RecursiveType with the variable found in the map.
We conclude the algorithm by calling go on the top-level type ty with an empty inProcess:
1 | } |
我们首先检查变量是否已经被合并。如果是，我们查找“recursive”映射：如果该映射已经包含该变量的条目，我们直接返回；否则，我们创建一个新的
TypeVariable 并使用 getOrElseUpdate
更新映射。
如果我们不是在合并一个递归变量的出现，我们将查看变量的界限。根据当前的极性，我们递归进入下限或上限。然后，如果递归
映射现在包含该变量的条目，这意味着该变量是递归的。在这种情况下，我们用在映射中找到的变量包装结果为
RecursiveType。
我们通过在顶级类型 ty 上调用 go 并传入一个空的 inProcess 来结束算法：
1 | } |
This algorithm does produce some unnecessary variables (variables which could be removed to simplify the type expression); we see how to simplify type representations in Section 4.
3.4 Examples
Now is a good time to pause and exemplify some crucial aspects of Simple-sub.
3.4.1 Recursive Types.
The reason for having recursive types in the user-facing type syntax has now become quite obvious: we need them in order to “tie the knot” when we are trying to coalesce type variables which appears in the coalescence of their own bounds.
For instance, consider the possible inferred representation
Function(Variable(s), Variable(t)), where
s = new VariableState(Nil, Nil) and
t = new VariableState(Nil, Function(Variable(s), Variable(t))) :: Nil.
Notice that there is a cycle in the upper bounds of t;
therefore, the coalescing algorithm turns this SimpleType
representation into the user-facing type
FunctionType(TypeVariable("s"), RecursiveType("t", FunctionType(TypeVariable("s"), TypeVariable("t")))),
which corresponds to \(\alpha \rightarrow
(\mu\beta.\alpha \rightarrow \beta)\) (and which will then be
simplified to \(\tau \rightarrow
(\mu\alpha.\tau \rightarrow \alpha)\)).
该算法确实会产生一些不必要的变量（可以通过去除这些变量来简化类型表达）；我们将在第4节中看到如何简化类型表示。
3.4 示例
现在是暂停并举例说明 Simple-sub 的一些关键方面的好时机。
3.4.1 递归类型。
在用户可见的类型语法中引入递归类型的原因现在变得相当明显：我们需要它们来“打结”，当我们尝试将出现在自身边界的类型变量合并时。
例如，考虑可能推断出的表示
Function(Variable(s), Variable(t))，其中
s = new VariableState(Nil, Nil) 和
t = new VariableState(Nil, Function(Variable(s), Variable(t))) :: Nil。注意
t 的上限中存在一个循环；因此，合并算法将此
SimpleType 表示转换为用户可见的类型
FunctionType(TypeVariable("s"), RecursiveType("t", FunctionType(TypeVariable("s"), TypeVariable("t"))))，这对应于
\(\alpha \rightarrow (\mu\beta.\alpha
\rightarrow \beta)\)（然后将简化为 \(\tau \rightarrow (\mu\alpha.\tau \rightarrow
\alpha)\)）。
3.4.2 Example of Type Inference.
To facilitate our understanding of the typing and coalescing algorithms, we now unroll the execution of a type inference run. Consider the term twice = \(\lambda f. \lambda x. f(f x)\), which takes a function f and some x as parameters, and applies f twice on x.
1 | typeTerm(λx. λx. f (f x))(empty) |
3.4.2 类型推断的示例
为了帮助我们理解类型和合并算法，我们现在展开一次类型推断的执行过程。考虑项 twice = \(\lambda f. \lambda x. f(f x)\)，它以一个函数 f 和一些 x 作为参数，并在 x 上调用 f 两次。
1 | typeTerm(λx. λx. f (f x))(empty) |
After this process, we end up with two upper bounds on \(\alpha\), namely
Function(\beta, \gamma) and
Function(\gamma, \delta). We next see how the type
coalescing algorithm unrolls from this inferred SimpleType
representation. We omit the details of some of the less interesting
sub-executions, and by a slight abuse of notation we use \(\alpha\) to denote \(\alpha.uniqueName\):
1 | coalesceType(function(α, function(β, δ))) |
在这个过程中，我们得到两个对 \(\alpha\) 的上界，即
Function(\beta, \gamma) 和
Function(\gamma, \delta)。接下来，我们将看到类型合并算法如何从这个推断的
SimpleType
表示中展开。我们省略一些不太有趣的子执行的细节，并通过轻微的符号滥用使用
\(\alpha\) 来表示 \(\alpha.uniqueName\)：
1 | coalesceType(function(α, function(β, δ))) |
Finally, we will see in Section 4 that this type can be compacted to \(\alpha \sqcap (\beta \sqcup \gamma \rightarrow \gamma \sqcap \delta) \rightarrow \beta \rightarrow \delta\), and then simplified to \((\beta \sqcup \gamma \rightarrow \gamma) \rightarrow \beta \rightarrow \gamma\), since \(\alpha\) occurs only negatively (thus can be removed) and \(\delta\) and \(\gamma\) co-occur negatively (thus can be merged into a single variable).
3.5 Let Polymorphism and Recursion
3.5.1 Let Polymorphism.
In traditional ML languages, local let bindings may be assigned polymorphic types. This requires keeping track of generalized typing schemes which are to be instantiated with fresh variables on every use, and making sure that we are not generalizing those type variables which occur in the environment, which would be unsound.
One way of determining which type variables to generalize is to scan the current environment, looking for references to the type variables in question. However, that is quite inefficient (it adds a linear-time operation in an important part of the algorithm).
最后，我们将在第4节看到，这种类型可以压缩为 \(\alpha \sqcap (\beta \sqcup \gamma \rightarrow \gamma \sqcap \delta) \rightarrow \beta \rightarrow \delta\)，然后简化为 \((\beta \sqcup \gamma \rightarrow \gamma) \rightarrow \beta \rightarrow \gamma\)，因为 \(\alpha\) 仅以负面形式出现（因此可以被移除），而 \(\delta\) 和 \(\gamma\) 在负面形式中共现（因此可以合并为一个变量）。
3.5 Let多态性和递归
3.5.1 Let多态性。
在传统的 ML 语言中，局部 let 绑定可以被赋予多态类型。这需要跟踪广义 类型方案，这些方案将在每次使用时用新变量 实例化，并确保我们不对环境中出现的类型变量进行泛化，这将是不安全的。
确定哪些类型变量需要泛化的一种方法是扫描当前环境，寻找对相关类型变量的引用。然而，这种方法效率相当低下（它在算法的一个重要部分增加了线性时间操作）。
Efficient generalization in ML. A better approach is to use levels. The idea is that all fresh type variables created inside the right-hand side of a let binding are first assigned a higher level, which indicates that they should be generalized. However, the level of a variable is lowered when the variable “escapes” through a constraint into the enclosing environment, preventing its future generalization (see the web article by Kiselyov [2013] for an excellent resource on the subject).
Simple-sub typing with levels. We can use the same idea to achieve let polymorphism in Simple-sub, though we have to be a little more careful, because we do not merely unify type variables as in ML, but instead we constrain their bounds. Our idea is to make sure that lower-level type variables never refer to higher-level ones through their bounds, and to enforce that property by duplicating type structures as needed, when it would otherwise be violated by the addition of a bound.
We first need to add a lvl field to type variable
states:
1 | class VariableState(val level: Int, |
1 | var lowerBounds: List[SimpleType], |
在机器学习中的高效泛化。 一种更好的方法是使用层次。这个想法是，在let绑定的右侧创建的所有新类型变量首先被分配一个更高的层次，这表明它们应该被泛化。然而，当变量通过约束“逃逸”到封闭环境中时，变量的层次会降低，从而防止其未来的泛化（参见Kiselyov [2013] 的网络文章，这是一个关于该主题的优秀资源）。
带层次的简单子类型。 我们可以使用相同的想法在Simple-sub中实现let多态，尽管我们必须更加小心，因为我们并不仅仅像在ML中那样“统一”类型变量，而是约束它们的边界。我们的想法是确保低层次的类型变量通过它们的边界 never 引用高层次的类型变量，并在需要时通过复制类型结构来强制执行该属性，以防止由于添加约束而违反该属性。
我们首先需要向类型变量状态添加一个lvl字段：
1 | class VariableState(val level: Int, |
1 | var lowerBounds: List[SimpleType], |
and to update freshVar correspondingly:
1 | def freshVar(implicit lvl: Int): Variable = |
Next, we add an implicit lvl parameter to the
typeTerm function, and we make sure to type the right-hand
sides of let bindings with a higher level than the current one:
1 | def typeTerm(trm: Term)(implicit ctx: Ctx, lvl: Int): SimpleType = trm match { |
并相应地更新 freshVar：
1 | def freshVar(implicit lvl: Int): Variable = |
接下来，我们在 typeTerm 函数中添加一个隐式的
lvl 参数，并确保让绑定的右侧类型使用比当前高的级别：
1 | def typeTerm(trm: Term)(implicit ctx: Ctx, lvl: Int): SimpleType = trm match { |
Notice that in the context used to type the body of the let binding,
we wrap the right-hand side type into a PolymorphicType
wrapper, which is defined at the end of Figure 6. A polymorphic type
wraps a simple type body, but additionally remembers above which level
the type variables that appear in body are to be considered universally
quantified. Its in instances method copies body, replacing
the type variables above level with fresh variables at level
lvl (a task performed by freshenAbove, whose
implementation is too boring to warrant taking space in this paper).
In order to make PolymorphicType and
SimpleType type-compatible, we create a common base trait22 TypeScheme, as shown in
Figure 6. This trait contains two abstract methods: one to instantiate
the type at a given level, and one to compute the level of the type. The
latter is implemented in SimpleType by a field which is
lazily evaluated, to avoid needless recomputation; this field is used to
remember the maximum level of any type variables contained in the
type.
Finally, we adapt typeTerm to instantiate the types
associated with variable names in ctx:
1 | type Ctx = Map[String, TypeScheme] |
请注意，在用于输入 let 绑定主体的上下文中，我们将右侧的类型包装在
PolymorphicType 包装器中，该包装器在图 6
的末尾定义。多态类型包装一个简单类型主体，但额外记住在主体中出现的类型变量应被视为普遍量化的级别。它的
in instances 方法复制主体，替换级别以上的类型变量为级别
lvl 的新变量（这项任务由 freshenAbove
执行，其实现过于无聊，不值得在本文中占用空间）。
为了使 PolymorphicType 和 SimpleType
类型兼容，我们创建一个共同的基类特 trait23
TypeScheme，如图 6
所示。该特含有两个抽象方法：一个用于在给定级别实例化类型，一个用于计算类型的级别。后者在
SimpleType
中通过一个懒惰求值的字段实现，以避免不必要的重新计算；该字段用于记住类型中包含的任何类型变量的最大级别。
最后，我们调整 typeTerm 以实例化与 ctx
中变量名相关联的类型：
1 | type Ctx = Map[String, TypeScheme] |
1 | sealed trait TypeScheme { |
1 | sealed trait TypeScheme { |
Constraining with levels. The next step is to make sure that variables of higher level do not escape into the bounds of variables of lower level. We do that by adding guards in the constraining algorithm, preventing it from happening:
1 | def constrain(lhs: SimpleType, rhs: SimpleType) |
使用层级进行约束。 下一步是确保较高层级的变量不会逃逸到较低层级变量的边界中。我们通过在约束算法中添加保护措施来防止这种情况发生：
1 | def constrain(lhs: SimpleType, rhs: SimpleType) |
1 | def extrude(ty: SimpleType, pol: Boolean) |
Fig. 7. Type extrusion algorithm.
1 | def extrude(ty: SimpleType, pol: Boolean) |
图 7. 类型挤出算法。
Naturally, we also need to handle the cases where there is a level
violation. In such cases, we make a copy of the problematic type up to
its type variables of wrong level (including their bounds) using the
extrude function, which returns a type at the right level
that mirrors the structure of the original type:
1 | case (lhs @ Variable_, rhs0) => |
自然，我们也需要处理存在级别违规的情况。在这种情况下，我们使用
extrude
函数复制到其错误级别的类型变量（包括它们的边界）的有问题的类型，该函数返回一个在正确级别的类型，反映了原始类型的结构：
1 | case (lhs @ Variable_, rhs0) => |
The extrude function is defined in Figure 7. Its goal is
to make a copy of the problematic type such that the copy has the
requested level and soundly approximates the original type. If
a variable vs needs to be copied as part of an extruded
type, two new variables should be created, one for each of vs's bounds
(unless of course the variable occurs strictly positively or strictly
negatively, in which case one of the two bounds can be discarded). This
way, we essentially create a conservative approximation of vs in the
result of the extrusion, and any later instantiation of vs (created at
every point the nested let binding is used) will be able to receive
additional constraints independently, as long as these constraints are
within the extruded approximating bounds of vs.
extrude 函数在图 7
中定义。它的目标是复制有问题的类型，使得该副本具有请求的级别并且能够合理地
近似 原始类型。如果需要将变量 vs
作为外延类型的一部分进行复制，则应创建两个新变量，一个用于每个vs的界（当然，除非变量严格正向或严格负向出现，在这种情况下可以丢弃两个边界中的一个）。通过这种方式，我们基本上在挤出的结果中创建了vs的一个保守近似，并且任何后续对vs的实例化（在每次使用嵌套let绑定时创建）都能够独立地接收额外的约束，只要这些约束在vs的挤出近似边界之内。
extrude recursively traverses its argument type tree up to its subtrees of acceptable levels. When it finds a type variable vs with the wrong level, it creates a copy nvs of the faulty type variable at the requested level lv1 and registers the necessary constraints. This works because nvs has a level lower than vs, satisfying the invariant on levels. We have to recursively extrude the bound of vs to place it in the nvs copy, but this bounds may form cycles. To avoid going into an infinite extrusion loop, we keep a cache c of the variables already being extruded, along with the polarity of that extrusion. In other words, extrude copies not only type trees, but also the potentially-cyclic subgraphs of type variable bounds which are rooted in these type trees.
extrude 递归遍历其参数类型树直到可接受级别的子树。当它发现一个级别错误的类型变量 vs 时，它在请求的级别 lv1 创建一个故障类型变量 nvs 的副本，并注册必要的约束。这是可行的，因为 nvs 的级别低于 vs，满足级别不变量。我们必须递归地 extrude vs 的边界以将其放置在 nvs 副本中，但这些边界可能会形成循环。为了避免进入无限 extrusion 循环，我们保持一个已经被 extruded 的变量的缓存 c，以及该 extrusion 的极性。换句话说，extrude 不仅复制类型树，还复制这些类型树的类型变量边界的潜在循环子图。
Let polymorphism in MLsub. In contrast to the approach presented here, Dolan uses an equivalent “lambda-lifted” type system, which associates to let-bound variables entire typing environments, in the typing context. While this can make for a slicker specification, it is rather counter-intuitive and thus harder to understand, creates many useless type variables (which need to be simplified later), and needlessly duplicates constraints, which causes inefficiencies [Pottier 1998, Chapter 16.2].
3.5.2 Recursive Let Bindings. Finally, supporting recursive let bindings is done in the usual way, by typing the right-hand side of the let binding with, in the context, a name bound to a type variable which is later checked to be a supertype of the actual right-hand side type (see Figure 8).
3.6 Summary
We summarize the final typing and constraining algorithms in Figures 8 and 9, respectively.
MLsub 中的 Let 多态性。 与此处提出的方法不同，Dolan 使用了一种等效的“lambda-lifted”类型系统，它将 let 绑定变量与整个类型环境关联，在类型上下文中。虽然这可以使规范更加简洁，但它相当直觉上不易理解，因此更难以把握，产生许多无用的类型变量（稍后需要简化），并不必要地重复约束，这导致效率低下 [Pottier 1998, Chapter 16.2]。
3.5.2 递归 Let 绑定。 最后，支持递归的 let 绑定是通过以通常的方式进行的，即在上下文中使用一个绑定到类型变量的名称对 let 绑定的右侧进行类型检查，该类型变量稍后被检查为实际右侧类型的超类型（见图 8）。
3.6 总结
我们在图 8 和图 9 中分别总结了最终的类型和约束算法。
Overall, Simple-sub looks more like traditional type inference algorithms than Dolan’s biunification, and it completely eschews the complexities of bisubstitution and polar types. Yet, as we confirm experimentally in Section 6, both algorithms produce equivalent results. This shows that bisubstitution and polar types are not, in fact, essential to type inference with subtyping and principal types in the style of MLsub.
4 SIMPLIFYING TYPES
As it is, the algorithm shown in the previous section infers types which often contain redundancies in their structures, as well as type variables which could be removed or unified. An important component of type inference when subtyping is involved is to simplify the types inferred, so as to make them compact and easy to comprehend [Pottier 1998]. If we did not perform any simplification, the inferred types would usually grow linearly with the size of the program!
总体而言，Simple-sub 更像传统的类型推断算法，而不是 Dolan 的双重统一，并且完全避免了双重替换和极性类型的复杂性。然而，正如我们在第六节中通过实验确认的，两个算法产生的结果是等价的。这表明，双重替换和极性类型实际上不是在 MLsub 风格中进行带有子类型及主要类型的类型推断所必需的。
4 简化类型
如前所述，前一节中展示的算法推断出的类型通常在结构上包含冗余部分，以及可以删除或统一的类型变量。当涉及子类型时，类型推断的一个重要组成部分是简化推断出的类型，以使其紧凑且易于理解 [Pottier 1998]。如果我们不进行任何简化，推断出的类型通常会随着程序大小的增加而线性增长！
In this section, we explore the design space and tradeoffs of type simplification (Section 4.1); we recall how MLsub performs automaton-based simplification (Section 4.2); we explain the ideas behind Simple-sub’s more basic approach to simplification, which turns out to be sufficient most of the time — and sometimes better (Section 4.3); and we describe an intermediate representation to facilitate the application of these ideas (Section 4.4).
4.1 Type Simplification Tradeoffs
Part of the appeal of algebraic subtyping is that it produces compact principal types, which are easy to read, unlike previous approaches to subtype inference. However, this comes at a cost: it requires making simplifying assumptions about the semantics of types. These assumptions hold in MLsub, but may not hold in languages with more advanced features.
在本节中，我们探讨类型简化的设计空间和权衡（第4.1节）；我们回顾MLsub如何执行基于自动机的简化（第4.2节）；我们解释Simple-sub更基本的简化方法背后的想法，这种方法在大多数情况下被证明是足够的——有时甚至更好（第4.3节）；我们描述了一种中间表示，以促进这些想法的应用（第4.4节）。
4.1 类型简化的权衡
代数子类型的吸引力部分在于它产生紧凑的主类型，这些主类型易于阅读，不像以前的子类型推断方法。然而，这是有代价的：它需要对类型的语义做出简化假设。这些假设在MLsub中成立，但在具有更高级特性的语言中可能不成立。
1 | def typeTerm(trm: Term)(implicit ctx: Ctx, lvl: Int): SimpleType = trm match { |
Fig. 8. Full specification of term typing in Simple-sub.
1 | def typeTerm(trm: Term)(implicit ctx: Ctx, lvl: Int): SimpleType = trm match { |
图 8. Simple-sub 中术语类型的完整规格说明。
For instance, MLsub considers the types
(int → int) ∧ (nat → nat) and
int ∪ nat → int ∧ nat to be equivalent, although the latter
intuitively contains strictly less information. This assumption
is sound, because MLsub programs cannot distinguish between the two
types — program which works with one will also work with the other.
However, the equivalence would not hold in a language which, for
example, used intersection types to encode overloading.
As another example, MLsub does not distinguish between the types
{ tag : 0; payload : str } ∪ { tag : 1; payload : int } and
{ tag : 0 ∪ 1; payload : str ∪ int }, where 0 and 1 denote
singleton literal types (trivial to add to our type system). But in
languages like JavaScript which support flow typing [Pearce 2013;
Tobin-Hochstadt and Felleisen 2010], the former holds more information,
since the different types of payload could be extracted separately by
first matching on the tag.¹⁴
例如，MLsub认为类型(int → int) ∧ (nat → nat)和int ∪ nat → int ∧ nat是等价的，尽管后者在直观上包含的信息严格少。这个假设是合理的，因为MLsub程序无法区分这两种类型——处理一种的程序也可以处理另一种。然而，在一种使用交集类型来编码重载的语言中，这种等价关系就不成立了。
作为另一个例子，MLsub并不区分类型{ tag : 0; payload : str } ∪ { tag : 1; payload : int }和{ tag : 0 ∪ 1; payload : str ∪ int }，其中0和1表示单元素文字类型（很容易添加到我们的类型系统中）。但在支持流类型的语言如JavaScript中[Pearce
2013; Tobin-Hochstadt and Felleisen
2010]，前者包含更多信息，因为不同类型的负载可以通过首先匹配标签分别提取。24
These simplifying assumptions are not necessary for principal type inference — they are merely a requirement of MLsub’s simplification and subsumption checking approaches (note that subsumption checking is outside the scope of this paper). While they are implied by Dolan’s algebraic construction of subtyping, making them inescapable in his system, these assumptions can actually
这些简化假设对于主类型推断并不是必要的——它们仅仅是MLsub的简化和涵蓋性检查方法的要求（请注意，涵蓋性检查超出了本文的范围）。虽然它们是由Dolan的子类型代数构造隐含的，使得它们在他的系统中不可避免，但实际上这些假设可以
1 | def constrain(lhs: SimpleType, rhs: SimpleType) |
Fig. 9. Full specification of subtype constraining in Simple-sub.
be separated from the type inference specification — we see a syntactic interpretation of subtyping in Section 5 which does not imply them, the understanding being that the system can be completed with more rules as desired, to achieve the simplification potential described in this section.
4.2 Type Simplification in MLsub
图9. Simple-sub中子类型约束的完整规范。
与类型推断规范分开 — 我们在第5节中看到了一种子类型的语法解释，该解释不意味着它们，理解是系统可以根据需要添加更多规则，以实现本节中描述的简化潜力。
4.2 MLsub中的类型简化
Thanks to the simplifying assumptions described in the previous subsection, MLsub can represent types as finite-state automata, where the states are type variables and where the edges, which are labelled, represent relations between these type variables. There are four sorts of labels on any edge between two type variables \(\alpha\) and \(\beta\): an “is-a” label indicate that \(\alpha\) is a subtype of \(\beta\); a “consumes” label indicate that \(\alpha\) is a function which takes some \(\beta\) in parameter; a “produces” label indicate that \(\alpha\) is a function which returns some \(\beta\) as a result; and finally, a “contains-L” label indicate that \(\alpha\) is a record which contains a field named \(L\) of type \(\beta\). The starting state of the automaton represents the root of the type expression.
This clever representation allows one to simplify types by reusing well-known existing techniques from the domain of automata theory: type automata can be made deterministic (“is-a”-labelled
由于前一小节中描述的简化假设，MLsub 可以将类型表示为有限状态自动机，其中状态是类型变量，边缘（带标签）表示这些类型变量之间的关系。在任何两个类型变量 \(\alpha\) 和 \(\beta\) 之间的边缘上有四种标签：一个“is-a”标签表示 \(\alpha\) 是 \(\beta\) 的子类型；一个“consumes”标签表示 \(\alpha\) 是一个以某个 \(\beta\) 为参数的函数；一个“produces”标签表示 \(\alpha\) 是一个返回某个 \(\beta\) 作为结果的函数；最后，一个“contains-L”标签表示 \(\alpha\) 是一个包含名为 \(L\) 的字段类型为 \(\beta\) 的结构体。自动机的起始状态表示类型表达式的根。
这种巧妙的表示允许通过重用自动机理论领域中的现有技术来简化类型：类型自动机可以被制作成确定性的（“is-a”标签）
edges are seen as \(\epsilon\) edges, so type automata are initially non-deterministic) and then minimized, to achieve simplification. However, this is a quite heavy and expensive approach. We found that in practice, a more straightforward simplification algorithm was often sufficient. We describe such an algorithm in the rest of this section.
4.3 Type Simplification in Simple-sub
Our simplification approach hinges on two main ideas: co-occurrence analysis and hash consing.
4.3.1 Co-occurrence Analysis. Co-occurrence analysis looks at every variable that appears in a type in both positive and negative positions, and records along which other variables and types it always occurs. A variable \(v\) occurs along a type \(\tau\) if it is part of the same type union ... \(\sqcup v \sqcup\) ... \(\sqcup \tau \sqcup\) ... or part of the same type intersection ... \(\sqcap v \sqcap\) ... \(\sqcap \tau \sqcap\) ...
Based on this information, we can perform three kinds of simplification:
边被视为 \(\epsilon\) 边，因此类型自动机最初是非确定性的) 然后经过最小化，以实现简化。然而，这是一种相当繁重和昂贵的方法。我们发现，在实践中，通常更直接的简化算法就足够了。我们将在本节的其余部分描述这样的算法。
4.3 在 Simple-sub 中的类型简化
我们的简化方法依赖于两个主要思想：共现分析 和 哈希一致性。
4.3.1 共现分析。 共现分析查看在类型中以正面和负面位置出现的每个变量，并记录它与其他变量和类型的共同出现情况。如果一个变量 \(v\) 出现在类型 \(\tau\) 旁边，则它是同一类型并的一个部分 ... \(\sqcup v \sqcup\) ... \(\sqcup \tau \sqcup\) ... 或同一类型交集的一个部分 ... \(\sqcap v \sqcap\) ... \(\sqcap \tau \sqcap\) ...
基于这些信息，我们可以进行三种简化：
Removal of polar variable. First, we want to remove type variables which appear only positively (or negatively) in a type expression. For instance, consider the type inferred for \(\lambda x.x + 1\), which is currently \(\alpha \sqcap \text{int} \rightarrow \text{int}\) (because the typing of lambda expressions always assigns a type variable to the parameter). The variable \(\alpha\) in this type is redundant since it only occurs in negative position — whichever \(\alpha\) the caller may pick, the function will still require the argument to be an int, and it will still produce an int as a result. So we can simply remove \(\alpha\) and obtain the simplified type \(\text{int} \rightarrow \text{int}\).
As another example, the type of a function which uses its argument as an int but never terminates, \(\text{int} \rightarrow \alpha\), can be simplified to \(\text{int} \rightarrow \perp\).
去除极性变量。 首先，我们想要去除在类型表达式中仅以正面（或负面）出现的类型变量。例如，考虑函数 \(\lambda x.x + 1\) 推断出的类型，目前是 \(\alpha \sqcap \text{int} \rightarrow \text{int}\)（因为 lambda 表达式的类型总是将类型变量分配给参数）。这个类型中的变量 \(\alpha\) 是多余的，因为它只出现在负面位置——无论调用者选择哪个 \(\alpha\)，函数仍然要求参数是 int，并且结果仍然是 int。因此，我们可以简单地去除 \(\alpha\)，得到简化后的类型 \(\text{int} \rightarrow \text{int}\)。
作为另一个例子，一个使用其参数作为 int 但永不终止的函数类型 \(\text{int} \rightarrow \alpha\) 可以简化为 \(\text{int} \rightarrow \perp\)。
Unification of indistinguishable variables. We have previously mentioned that a type such as \(\text{bool} \rightarrow \alpha \rightarrow \beta \rightarrow \alpha \sqcup \beta\) (the natural type of if-then-else) is equivalent to the simpler type \(\text{bool} \rightarrow \alpha \rightarrow \alpha\). This is true because the positive occurrences of the variables \(\alpha\) and \(\beta\) are "indistinguishable" — whenever an \(\alpha\) is produced, a \(\beta\) is also produced. Therefore, we cannot distinguish the two variables, and they can be unified.
Based on the result of the co-occurrence analysis, we can unify all those variables that always occur together either in positive or in negative positions (or both).
不可区分变量的统一。 我们之前提到过，类型 \(\text{bool} \rightarrow \alpha \rightarrow \beta \rightarrow \alpha \sqcup \beta\)（if-then-else 的自然类型）等价于更简单的类型 \(\text{bool} \rightarrow \alpha \rightarrow \alpha\)。这是因为变量 \(\alpha\) 和 \(\beta\) 的正出现是“不可区分”的——每当产生一个 \(\alpha\) 时，\(\beta\) 也会被产生。因此，我们无法区分这两个变量，它们可以被统一。
根据共现分析的结果，我们可以统一那些总是一起出现在正位置或负位置（或两者）的所有变量。
Flattening of “variable sandwiches”. What we call a "variable sandwich" is an inferred type variable \(v\) which has a type \(\tau\) both as an upper bound and as a lower bound, i.e., \(v \le \tau\) and \(v \ge \tau\). This means that \(v\) is equivalent to \(\tau\). In a coalesced type, this will transpire as \(v\) co-occurring with \(\tau\) both positively and negatively. So we can use the result of co-occurrence analysis to remove variables which are sandwiched between two identical bounds. As an example, we simplify the type \(\alpha \sqcap \text{int} \rightarrow \alpha \sqcup \text{int}\) to just \(\text{int} \rightarrow \text{int}\).
Conceptually, this idea generalizes polar variable removal, which was explained above. Indeed, if a variable never occurs positively, it conceptually occurs both positively and negatively along with the type \(\perp\), so we can replace that variable with \(\perp\) (i.e., remove it from all type unions).
“变量三明治”的扁平化。 我们所称的“变量三明治”是一个推断的类型变量 \(v\)，其类型 \(\tau\) 同时作为上界和下界，即 \(v \le \tau\) 和 \(v \ge \tau\)。这意味着 \(v\) 与 \(\tau\) 等价。在一个合并的类型中，这将表现为 \(v\) 与 \(\tau\) 同时正向和负向共现。因此，我们可以使用共现分析的结果来移除夹在两个相同界限之间的变量。作为一个例子，我们将类型 \(\alpha \sqcap \text{int} \rightarrow \alpha \sqcup \text{int}\) 简化为仅仅 \(\text{int} \rightarrow \text{int}\)。
在概念上，这个思想推广了极性变量的移除，如上所述。实际上，如果一个变量从未正向出现，那么它在概念上同时与类型 \(\perp\) 正向和负向出现，因此我们可以用 \(\perp\) 替换该变量（即，从所有类型的并集中移除它）。
All these transformations are truly simplifications, in the sense that they yield new types which contain fewer subterms but are still equivalent to the original types (i.e., the two types subsume each other). Therefore, these transformations also preserve principality.
4.3.2 Hash Consing. Simple-sub's other simplification approach, hash consing, deals with removing duplicated structures in coalesced type expressions.
Consider the following recursive term:
\[ \text{let } f = \lambda x. \{ L = x ; R = f x \} \text{ in } f \]
The coalesced type inferred for this term would be:
\[ \alpha \rightarrow \{ L : \alpha; R : \mu\beta. \{ L : \alpha; R : \beta \} \} \]
Notice that there is an outer record layer that is redundant. We would like to instead infer:
\[ \alpha \rightarrow \mu\beta. \{ L : \alpha; R : \beta \} \]
所有这些转换实际上都是简化，从这个意义上说，它们产生了包含较少子项的新类型，但仍然与原始类型等价（即，这两个类型可以互相包含）。因此，这些转换也保留了原始性。
4.3.2 Hash Consing. Simple-sub的另一种简化方法hash consing，处理的是在合并的类型表达式中移除重复结构的问题。
考虑以下递归项：
\[ \text{let } f = \lambda x. \{ L = x ; R = f x \} \text{ in } f \]
为这个项推断出的合并类型将是：
\[ \alpha \rightarrow \{ L : \alpha; R : \mu\beta. \{ L : \alpha; R : \beta \} \} \]
注意，这里有一个冗余的外部结构体层。我们希望推断出：
\[ \alpha \rightarrow \mu\beta. \{ L : \alpha; R : \beta \} \]
This can be done by performing hash consing on the types being
coalesced, in the coalesceType function: instead of simply
remembering which variables are in the process of being
coalesced, we can remember whole type expressions; when we reach a type
expression which is already being coalesced, we introduce a recursive
type variable in this position, removing the redundant outer layer of
types like the above.
这可以通过在 coalesceType
函数中对正在合并的类型执行哈希合并来完成：我们可以记住正在合并的整个类型表达式，而不仅仅是哪个
变量
正在被合并；当我们遇到一个已经在合并中的类型表达式时，我们会在这个位置引入一个递归类型变量，从而去除像上述那样冗余的外层类型。
Interestingly, MLsub does not currently perform a comparable simplification, so Simple-sub infers simpler types in examples like the one above.
有趣的是，MLsub 当前并不执行类似的简化，因此在像上述示例中，Simple-sub 推导出更简单的类型。
4.4 An Intermediate Representation for Simplification
4.4 用于简化的中间表示
The above two approaches do not work very well out of the box. First, we cannot perform them on non-coalesced types, since co-occurrence analysis would miss information which only becomes apparent after the bounds are flattened. For instance, if we inferred a type variable \(\alpha\) with upper bounds \(\tau_0 \rightarrow \tau_1\) and \(\tau_2 \rightarrow \tau_3\), only after we flatten these bounds and merge the function types into \(\tau_0 \sqcup \tau_2 \rightarrow \tau_1 \sqcap \tau_2\) do we notice the co-occurrence of \(\tau_0\), \(\tau_2\) and \(\tau_1\), \(\tau_3\). Second, it is awkward to perform the normalization steps necessary for this sort of function type merging on the final coalesced type representation, which is syntactically too loose (it can represent types which do not correspond to inferred types, for instance merging unions and intersections).
1 | case class CompactType vars: Set[CTypeVariable], |
上述两种方法在实际应用中效果并不理想。首先，我们无法对非合并类型执行这些操作，因为共现分析会遗漏在边界被扁平化后才显现的信息。例如，如果我们推断出一个类型变量 \(\alpha\)，其上界为 \(\tau_0 \rightarrow \tau_1\) 和 \(\tau_2 \rightarrow \tau_3\)，只有在我们扁平化这些边界并将函数类型合并为 \(\tau_0 \sqcup \tau_2 \rightarrow \tau_1 \sqcap \tau_3\) 后，我们才会注意到 \(\tau_0\)、\(\tau_2\) 与 \(\tau_1\)、\(\tau_3\) 的共现。其次，在最终的合并类型表示上执行这种函数类型合并所需的标准化步骤是尴尬的，因为它的语法过于松散（它可以表示与推断类型不对应的类型，例如合并并集和交集）。
1 | case class CompactType vars: Set[CTypeVariable], |
For these reasons, we introduce an intermediate
CompactType representation between SimpleType
and Type, in which to perform simplification more easily.
The CompactType representation, shown above, corresponds to
a normalized representation of types where all the non-recursive
variable bounds are coalesced. The recVars field of
CompactTypeScheme records the bounds of recursive type
variables (which we cannot coalesce, as they are cyclic).
The compactType function to convert a
SimpleType into a CompactTypeScheme is
straightforward and looks like the coalesceType function
shown earlier. The simplifyType function is slightly more
complicated, as it has to perform a co-occurrence analysis pass followed
by a rewriting pass. Finally, hash consing is done as part of the
coalesceCompactType function. We do not show the
implementations of these functions here for lack of space, but they can
be seen in the code associated with the paper.
5 FORMALIZATION OF SIMPLE-SUB
So far, we have appealed to an intuitive understanding of subtyping, eschewing a more explicit characterization. In this section, we make our intuition more formal by giving a syntactic account
出于这些原因，我们引入了一种介于 SimpleType 和
Type 之间的中间 CompactType
表示，以便更容易地进行简化。上述的 CompactType
表示对应于类型的标准化表示，其中所有非递归变量的界限都进行了合并。CompactTypeScheme
的 recVars
字段记录了递归类型变量的界限（我们不能合并它们，因为它们是循环的）。
将 SimpleType 转换为 CompactTypeScheme 的
compactType 函数很简单，类似于前面显示的
coalesceType 函数。simplifyType
函数稍微复杂一些，因为它需要进行共现分析遍及和重写遍及。最后，哈希一致性作为
coalesceCompactType
函数的一部分完成。由于篇幅限制，我们在此不展示这些函数的实现，但可以在与论文相关的代码中看到它们。
5 SIMPLE-SUB 的形式化
到目前为止，我们已经依赖于对子类型的直观理解，避免了更明确的表述。在这一节中，我们通过提供一个语法账户使我们的直观理解更加正式。
\[ \text{S-REFL} \quad \frac{}{\tau \leq \tau} \]
\[ \text{S-TRANS} \quad \frac{ \Sigma \vdash \tau_0 \leq \tau_1 \quad \Sigma \vdash \tau_1 \leq \tau_2 }{ \Sigma \vdash \tau_0 \leq \tau_2 } \]
\[ \text{S-WEAKEN} \quad \frac{H}{\Sigma \vdash H} \]
\[ \text{S-ASSUM} \quad \frac{\Sigma, \triangleright H \vdash H}{\Sigma \vdash H} \]
\[ \text{S-HYP} \quad \frac{H \in \Sigma}{\Sigma \vdash H} \]
\[ \text{S-REC} \quad \frac{}{\mu\alpha.\,\tau \equiv [\mu\alpha.\,\tau / \alpha]\tau} \]
\[ \text{S-OR} \quad \frac{ \forall i, \exists j,\ \Sigma \vdash \tau_i \leq \tau'_j }{ \Sigma \vdash \bigsqcup_i \tau_i \leq \bigsqcup_j \tau'_j } \]
\[ \text{S-AND} \quad \frac{ \forall i, \exists j,\ \Sigma \vdash \tau_j \leq \tau'_i }{ \Sigma \vdash \bigcap_j \tau_j \leq \bigcap_i \tau'_i } \]
\[ \text{S-FUN} \quad \frac{ \triangleleft\Sigma \vdash \tau_0 \leq \tau_1 \quad \triangleleft\Sigma \vdash \tau_2 \leq \tau_3 }{ \Sigma \vdash \tau_1 \to \tau_2 \leq \tau_0 \to \tau_3 } \]
\[ \text{S-RCD} \quad \frac{}{ \{ l_i : t_i \}^i \equiv \bigcap_i \{ l_i : t_i \} } \]
\[ \text{S-DEPTH} \quad \frac{ \triangleleft\Sigma \vdash \tau_1 \leq \tau_2 }{ \Sigma \vdash \{ l : \tau_1 \} \leq \{ l : \tau_2 \} } \]
\[ \begin{aligned} &\triangleleft(\Sigma, H) = \triangleleft\Sigma, H \\ &\triangleleft(\Sigma, \triangleright H) = \triangleleft\Sigma, H \\ &\triangleleft\epsilon = \epsilon \end{aligned} \]
Fig. 10. Declarative subtyping rules of Simple-sub. These only cover part of the relationships present in Dolan’s algebraic construction of types [Dolan 2017]. More subtyping rules can be added to give desirable properties to the system (such as distributivity of unions, intersections, and type constructors), but they are not strictly required for principal type inference. Note that by convention, we consider that an empty union is ⊥ and an empty intersection is T, so these rules cover things like int ≤ T.
of the minimal subtyping relationship required to make the type inference algorithm of Section 3 sound and complete. We state the corresponding theorems and sketch how to carry out their proofs. The complete proofs are outside the scope of this (already quite long) paper.
\[ \text{S-DEPTH} \quad \frac{ \triangleleft\Sigma \vdash \tau_1 \leq \tau_2 }{ \Sigma \vdash \{ l : \tau_1 \} \leq \{ l : \tau_2 \} } \]
\[ \begin{aligned} &\triangleleft(\Sigma, H) = \triangleleft\Sigma, H \\ &\triangleleft(\Sigma, \triangleright H) = \triangleleft\Sigma, H \\ &\triangleleft\epsilon = \epsilon \end{aligned} \]
图10. Simple-sub 的声明性子类型规则。这些仅涵盖了Dolan的类型代数构造中存在的关系的一部分[Dolan 2017]。可以添加更多的子类型规则，以赋予系统所需的特性（例如，并集、交集和类型构造子的分配性），但这些对于主类型推断并不严格必要。请注意，根据约定，我们认为空并集是⊥，空交集是T，因此这些规则涵盖了 int ≤ T 这样的情况。
的最小子类型关系，以使第3节的类型推断算法是可靠和完整的。我们陈述相应的定理并概要说明如何进行证明。完整的证明超出了本文（已经相当长）的范围。
We restrict ourselves to the non-let-polymorphic version of Simple-sub for simplicity.25
5.1 A Syntax-First Definition of Subtyping
Figure 10 presents the minimal subtyping rules necessary to perform sound and complete type inference in Simple-sub. The general subtyping judgement has the form \(Σ \vdash τ_0 ≤ τ_1\) and includes a subtyping context \(Σ\) made of subtyping hypotheses of the form \(τ_2 ≤ τ_3\), possibly prefixed with a \(▷\) symbol. We use \(Σ \vdash τ_0 ≡ τ_1\) as a shorthand for \(Σ \vdash τ_0 ≤ τ_1 ∧ Σ \vdash τ_1 ≤ τ_0\). When \(Σ\) is empty, we omit the \(Σ \vdash\) and just write \(τ_0 ≤ τ_1\) and \(τ_0 ≡ τ_1\).
我们将自己限制在 Simple-sub 的非 let-polymorphic 版本，以简化问题。26
5.1 类型子项的语法优先定义
图 10 展示了在 Simple-sub 中执行声称和完整类型推断所需的最小子项规则。一般的子项判断形式为 \(Σ \vdash τ_0 ≤ τ_1\)，并包含由子项假设构成的子项上下文 \(Σ\)，假设的形式为 \(τ_2 ≤ τ_3\)，可能以 \(▷\) 符号为前缀。我们使用 \(Σ \vdash τ_0 ≡ τ_1\) 作为 \(Σ \vdash τ_0 ≤ τ_1 ∧ Σ \vdash τ_1 ≤ τ_0\) 的简写。当 \(Σ\) 为空时，我们省略 \(Σ \vdash\)，只写 \(τ_0 ≤ τ_1\) 和 \(τ_0 ≡ τ_1\)。
Note that Figure 10 only presents a subset of all the rules one may want in an actual system. In particular, type simplification and subsumption checking (to determine whether one type signature is at least as general as another) require rules to merge type constructors like function types, so that for instance the equivalence \((τ_0 → τ_1) ∩ (τ_2 → τ_3) ≡ τ_0 ∪ τ_1 → τ_2 ∩ τ_3\) holds (see the related discussion in Section 4.1). On the other hand, we do not expect rules like distributivity of unions over intersections to be actually useful in a pure MLsub-style system, since unions and intersections are normally kept separate (unions occurring strictly positively, and intersections strictly negatively); however, they could come in useful in a generalized system.
请注意，图10仅呈现了在实际系统中可能需要的所有规则的一个子集。特别是，类型简化和子类型检查（以确定一个类型签名是否至少和另一个类型签名一样一般）需要规则来合并类型构造，如函数类型，因此例如等式 \((τ_0 → τ_1) ∩ (τ_2 → τ_3) ≡ τ_0 ∪ τ_1 → τ_2 ∩ τ_3\) 成立（参见第4.1节中的相关讨论）。另一方面，我们不希望如交集上的并集的分配律这样的规则在纯MLsub风格的系统中实际上有用，因为并集和交集通常保持分开（并集严格正向出现，交集严格负向出现）；但是，在一个广义系统中，它们可能会有用。
5.1.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-REC rule, which substitutes a recursive types within itself to expose one layer of its underlying definition. However, as remarked by Amadio and Cardelli [1993], the S-REC rule alone is not sufficient to derive valid inequalities like \(μα_0. τ → τ → α_0 ≤ μα_1. τ → α_1\) because
these types, although equivalent, never unfold to the precise same syntactic representation. This motivates the next paragraph.
5.1.1 子类型递归类型
我们对子类型的语法描述的一个结果是，我们并不将类型定义为一些生成关系上的不动点，如在[Dolan 2017；Pierce 2002]中所做的那样。相反，我们必须考虑到我们操控的是有限的语法类型树，其中递归类型必须手动展开以推导出关于它们的信息。这就是S-REC规则的目的，它在自身内部替换递归类型，以揭示其基本定义的一层。然而，正如Amadio和Cardelli [1993]所指出的，单独的S-REC规则不足以推导出有效的不等式，例如\(μα_0. τ → τ → α_0 ≤ μα_1. τ → α_1\)，因为
这些类型虽然是等价的，但从未展开成完全相同的语法表示。这激励了下一段。
5.1.2 Subtyping Hypotheses. We make use of the environment Σ to store subtyping hypotheses, to be leveraged later using the S-HYP rule. We have to be careful not to allow the use of a hypothesis right after assuming it, which would obviously make the system unsound. In the specification of their constraint solving algorithm, Hosoya et al. [2005] use two distinct judgments ⊢ and ⊢' 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, using ◁ to remove all ▷ occurrences from the set of hypotheses, thereby unlocking them for use by S-HYP.
5.1.2 子类型假设。 我们利用环境 Σ 来存储子类型假设，以便稍后通过 S-HYP 规则使用。我们必须小心不要在假设后立即使用该假设，这显然会导致系统的不健全。在他们的约束求解算法的规范中，Hosoya 等人 [2005] 使用两个不同的判断 ⊢ 和 ⊢' 来区分可以使用和不能使用假设的地方。我们采取一种不同但相关的方法。我们的 S-Assum 子类型规则类似于 Appel 等人 [2007] 所描述的 Löb 规则，它使用“later”模态 ▷ 来延迟假设的适用性——通过将此符号放在假设前面，我们防止其被 S-HYP 立即使用。我们在通过函数或结构体构造函数时消除 ▷，使用 ◁ 从假设集中移除所有 ▷ 出现，从而解锁它们以供 S-HYP 使用。
These precautions reflect the “guardedness” restrictions used by Dolan [2017] on recursive types, which prevents usages of α that are not guarded by → or { ... } in a recursive type µα. τ. By contrast, our restriction is not a syntactic one, and contrary to Dolan we do allow types like µα. α — this type unfolds into itself by S-REC — and µα. α ∩ α, about which no useful assumptions can be leveraged, since they never go through a function or record constructor.
5.1.3 Example. As an example, let us try to derive the following inequality, which states that the type of a function taking two curried τ arguments an arbitrary number of times is a special case of the type of a function taking a single τ argument an arbitrary number of times:
\[ \mu\alpha_0. \tau \to \tau \to \alpha_0 \le \mu\alpha_1. \tau \to \alpha_1 \]
To facilitate the development, we use the shorthands τ₀ = μα₀. τ → τ → α₀; τ₁ = μα₁. τ → α₁; and H = τ₀ ≤ τ₁. We start by deriving that the respective unfoldings of the recursive types are subtypes; that is, that τ → τ → τ₀ ≤ τ → τ₁ (1). Note that for conciseness, we omit the applications of S-WEAKEN in the derivations below:
这些预防措施反映了Dolan [2017]对递归类型使用的“受限性”限制，这防止了在递归类型µα. τ中使用未被→或{...}保护的α。相比之下，我们的限制不是一个语法上的限制，与Dolan不同，我们确实允许像µα. α这样的类型——这个类型通过S-REC展开成它自己——以及µα. α ∩ α，关于这些类型没有可用的有用假设，因为它们从未经过函数或结构体构造器。
5.1.3 示例. 作为一个例子，让我们尝试推导以下不等式，它指出一个函数接受两个柯里化τ参数任意次数的类型是一个函数接受单个τ参数任意次数的类型的特例：
\[ \mu\alpha_0. \tau \to \tau \to \alpha_0 \le \mu\alpha_1. \tau \to \alpha_1 \]
为了方便发展，我们使用简写τ₀ = μα₀. τ → τ → α₀; τ₁ = μα₁. τ → α₁; 以及H = τ₀ ≤ τ₁。我们开始推导递归类型的相应展开是子类型；也就是说，τ → τ → τ₀ ≤ τ → τ₁ (1)。请注意，为了简洁，我们在下面的推导中省略了S-WEAKEN的应用：
\[ \begin{tikzcd}[column sep=2.8em, row sep=2.8em] \begin{array}{c} \text{REFL} \\ H \vdash \tau \le \tau \end{array} & \begin{array}{c} \text{FUN} \\ \frac{H \vdash \tau \le \tau}{H \vdash \tau \to \tau_0 \le \tau \to \tau_1} \end{array} & \begin{array}{c} \text{HYP} \\ \frac{(\tau_0 \le \tau_1) \in H}{H \vdash \tau_0 \le \tau_1} \end{array} & \begin{array}{c} \text{REC} \\ H \vdash \tau \to \tau_1 \le \tau_1 \end{array} & \begin{array}{c} \text{TRANS} \\ \frac{H \vdash \tau \to \tau_0 \le \tau_1}{\vdash H \vdash \tau \to \tau \to \tau_0 \le \tau \to \tau_1} \end{array} \\ \multicolumn{5}{c}{(1)} \end{tikzcd} \]
Then, we simply have to fold back the unfolded recursive types, using REC and TRANS:
\[ \begin{tikzcd}[column sep=2.8em, row sep=2.8em] \begin{array}{c} \text{REFL} \\ H \vdash \tau \le \tau \end{array} & \begin{array}{c} \text{FUN} \\ \frac{H \vdash \tau \le \tau}{H \vdash \tau \to \tau_0 \le \tau \to \tau_1} \end{array} & \begin{array}{c} \text{HYP} \\ \frac{(\tau_0 \le \tau_1) \in H}{H \vdash \tau_0 \le \tau_1} \end{array} & \begin{array}{c} \text{REC} \\ H \vdash \tau \to \tau_1 \le \tau_1 \end{array} & \begin{array}{c} \text{TRANS} \\ \frac{H \vdash \tau \to \tau_0 \le \tau_1}{\vdash H \vdash \tau \to \tau \to \tau_0 \le \tau \to \tau_1} \end{array} \\ \multicolumn{5}{c}{(1)} \end{tikzcd} \]
然后，我们只需使用 REC 和 TRANS 将展开的递归类型折叠回去：
\[ \begin{tikzcd}[column sep=2.8em, row sep=2.8em] \begin{array}{c} \text{TRANS} \\ \frac{\begin{array}[t]{c} \text{REC} \\ \multicolumn{2}{c}{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau \to \tau \to \tau_0 \end{array}} \end{array}}{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau \to \tau_1 \end{array}} \end{array} & \begin{array}{c} \text{ASSUM} \\ \frac{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau_1 \end{array}}{\tau_0 \le \tau_1} \end{array} & \begin{array}{c} \text{REC} \\ \frac{\begin{array}[t]{c} \vdash H \vdash \tau \to \tau_1 \le \tau_1 \end{array}}{\vdash H \vdash \tau \to \tau_1 \le \tau_1} \end{array} & \begin{array}{c} \text{TRANS} \\ \frac{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau \to \tau_1 \end{array}}{\vdash H \vdash \tau \to \tau_1 \le \tau_1} \end{array} & \begin{array}{c} \text{ASSUM} \\ \frac{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau_1 \end{array}}{\tau_0 \le \tau_1} \end{array} \\ \multicolumn{5}{c}{(1)} \end{tikzcd} \]
5.2 Simplified Algorithms and Mutability
\[ \begin{tikzcd}[column sep=2.8em, row sep=2.8em] \begin{array}{c} \text{传递性} \\ \frac{\begin{array}[t]{c} \text{假设} \\ \multicolumn{2}{c}{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau \to \tau \to \tau_0 \end{array}} \end{array}}{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau \to \tau_1 \end{array}} \end{array} & \begin{array}{c} \text{假设} \\ \frac{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau_1 \end{array}}{\tau_0 \le \tau_1} \end{array} & \begin{array}{c} \text{递归} \\ \frac{\begin{array}[t]{c} \vdash H \vdash \tau \to \tau_1 \le \tau_1 \end{array}}{\vdash H \vdash \tau \to \tau_1 \le \tau_1} \end{array} & \begin{array}{c} \text{传递性} \\ \frac{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau \to \tau_1 \end{array}}{\vdash H \vdash \tau \to \tau_1 \le \tau_1} \end{array} & \begin{array}{c} \text{假设} \\ \frac{\begin{array}[t]{c} \vdash H \vdash \tau_0 \le \tau_1 \end{array}}{\tau_0 \le \tau_1} \end{array} \\ \multicolumn{5}{c}{(1)} \end{tikzcd} \]
5.2 简化算法与可变性
For ease of formal reasoning, we use a simpler definition of type coalescing, shown in Figure 11. In this definition, we refer to TypeVariable(vs.uniqueName) as αvs, and we use αvs+ and αvs- to denote two additional (distinct) unique names, to be used as positive and negative recursive occurrence binders — they serve the purpose of freshVar.uniqueName in the version of type coalescing shown in Section 3.3. Similarly, it is possible to give a simpler (but less efficient) definition of the constrain
function using immutable data structures instead of mutable ones, which is easily proven equivalent; we do not show this simpler version here for lack of space, but assume its existence.
为了方便形式推理，我们使用了一种更简单的类型合并定义，见图11。在这个定义中，我们将 TypeVariable(vs.uniqueName) 称为 αvs，并用 αvs+ 和 αvs- 来表示两个额外的（不同的）唯一名称，作为正递归出现绑定器和负递归出现绑定器——它们在类型合并的版本中起着 freshVar.uniqueName 的作用，如第3.3节所示。类似地，可以使用不可变数据结构而不是可变数据结构给出约束函数的更简单（但效率较低）定义，这很容易证明是等价的；由于篇幅有限，我们在这里不展示这个更简单的版本，但假设它的存在。
The only mutability left in the simplified algorithms is the mutability of type variable bounds. We refer to these bounds collectively as σ, which maps each VariableState instance to its current upper and lower bounds. We write foo(args)ₐ ⇝σ' res to denote the execution of some function foo given bounds σ and having the effect of producing the new bounds σ'. We use the shorthand lbvsσ for vs.lowerBoundsσ and ubvsσ for vs.upperBoundsσ.
5.3 Soundness and Completeness
Our theorems of interest are the soundness and completeness of Simple-sub:
THEOREM 1 (SOUNDNESS). Simple-sub only yields types which comply with the declarative type system: if typeTerm(t)(empty)₀ ⇝σ st for some st and σ, then there exists a type τ such that τ ⊢ t : τ and τ ≤\(^V\) Eσ+[[st]].
THEOREM 2 (COMPLETENESS). *Simple-sub always finds principal type schemes: if τ : t, then typeTerm(t)(empty)₀ ⇝σ st for some st and σ, and \(E_σ^+ \ [[st]] ≤^V τ\).
5.3.1 Soundness. As usual, proving the theorem requires proving a more general lemma.
文本翻译如下：
在简化算法中唯一剩下的可变性是类型变量边界的可变性。我们将这些边界统称为 σ，它将每个 VariableState 实例映射到其当前的上界和下界。我们写 foo(args)ₐ ⇝σ' res 来表示在给定边界 σ 的情况下执行某个函数 foo，并产生新的边界 σ'。我们使用简写 lbvsσ 表示 vs.lowerBoundsσ，ubvsσ 表示 vs.upperBoundsσ。
5.3 声明性与完整性
我们关注的定理是 Simple-sub 的声明性和完整性：
定理 1（声明性）。Simple-sub 仅产生与声明性类型系统相符的类型：如果 typeTerm(t)(empty)₀ ⇝σ st 对于某些 st 和 σ 成立，则存在一个类型 τ，使得 τ ⊢ t : τ 且 τ ≤\(^V\) Eσ+[[st]]。
定理 2（完整性）。Simple-sub 始终找到主类型方案：如果 τ : t，则存在某些 st 和 σ，使得 typeTerm(t)(empty)₀ ⇝σ st，以及 \(E_σ^+ \ [[st]] ≤^V τ\)。
5.3.1 声明性。与往常一样，证明该定理需要证明一个更一般的引理。
We use unifying type coalescing (Figure 12) — a variant of type coalescing which allows proving the soundness lemmas more easily. The crucial property of unifying coalescing is that it instantiates each type variable αvs in a way that makes the positive coalescing of vs a subtype of its negative coalescing, as long as all lower bounds of vs are subtypes of all its upper bounds — i.e., its bounds are consistent. We also denote by τcons σ the fact that the bounds of all variables in σ are consistent.
Lemma 1 (Soundness — General). Assuming \(\vdash_{\text{cons}} \sigma\) and \(\text{typeTerm}(t)(\text{ctx})_\sigma \Downarrow_{\sigma'} \text{st}\), then \(\vdash_{\text{cons}} \sigma'\) and \(\mathcal{E}^-_{\sigma'}[\text{ctx}] \vdash t : \mathcal{E}^-_{\sigma'}[\text{st}]\).
The proof is by induction on the executions of typeTerm, assuming that typeTerm terminates successfully. In the process, we need a number of auxiliary lemmas, most of which we do not show here. The core of the proof actually resides in the proof of sound constraining (Lemma 2).
\[ \mathbf{E}^{\phi}_{\sigma}[\mathrm{Primitive}(n)]\,C = n \]
我们使用 unifying type coalescing（图12）—— 一种类型聚合的变体，允许更容易地证明声学引理。统一聚合的关键性质是，它以一种方式实例化每个类型变量 αvs，使得 vs 的正聚合是其负聚合的子类型，只要 vs 的所有下界都是其所有上界的子类型 —— 即，它的界限是 consistent 的。我们还用 τcons σ 表示 σ 中所有变量的界限是一致的事实。
引理1（SOUNDNESS — 一般）。 假设 \(\vdash_{\text{cons}} \sigma\) 且 \(\text{typeTerm}(t)(\text{ctx})_\sigma \Downarrow_{\sigma'} \text{st}\)，则 \(\vdash_{\text{cons}} \sigma'\) 且 \(\mathcal{E}^-_{\sigma'}[\text{ctx}] \vdash t : \mathcal{E}^-_{\sigma'}[\text{st}]\)
证明是通过对 typeTerm 执行的归纳，假设 typeTerm 成功终止。在此过程中，我们需要几个辅助引理，其中大部分在这里不展示。证明的核心实际上在于 sound constraining 的证明（引理2）。
\[ \mathbf{E}^{\phi}_{\sigma}[\mathrm{Primitive}(n)]\,C = n \]
\[ \mathbf{E}^{\phi}_{\sigma}[\mathrm{Function}(s,t)]\,C = \mathbf{E}^{-\phi}_{\sigma}[s]\,C \to \mathbf{E}^{\phi}_{\sigma}[t]\,C \]
\[ \mathbf{E}^{\phi}_{\sigma}[\mathrm{Record}(fs)]\,C = \bigcap_{(n,t)\,\in\,fs} \{ n : \mathbf{E}^{\phi}_{\sigma}[t]\,C \} \]
\[ \mathbf{E}^{-}_{\sigma}[\mathrm{Variable}(vs)]\,C = \alpha^{-}_{vs} \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\text{if } (vs, -) \in C \]
\[ \mathbf{E}^{-}_{\sigma}[\mathrm{Variable}(vs)]\,C = \mu\alpha^{-}_{vs}.\,\alpha_{vs} \cap \bigcap_{u\in\mathrm{ub}^{vs}_{\sigma}} \mathbf{E}^{-}_{\sigma}[u]\,(C \cup \{(vs, -)\}) \quad\quad\text{if } (vs, -) \notin C \]
\[ \mathbf{E}^{+}_{\sigma}[\mathrm{Variable}(vs)]\,C = \alpha^{+}_{vs} \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\text{if } (vs, +) \in C \]
\[ \mathbf{E}^{+}_{\sigma}[\mathrm{Variable}(vs)]\,C = \mu\alpha^{+}_{vs}.\,\alpha_{vs} \cup \bigsqcup_{l\in\mathrm{lb}^{vs}_{\sigma}} \mathbf{E}^{+}_{\sigma}[l]\,(C \cup \{(vs, +)\}) \quad\quad\text{if } (vs, +) \notin C \]
Fig. 11. Type coalescing, where the metavariable φ is either + or − and ¬(+) = − and ¬(−) = +.
\[ \mathbf{E}^{\phi}_{\sigma}[\mathrm{Function}(s,t)]\,C = \mathbf{E}^{-\phi}_{\sigma}[s]\,C \to \mathbf{E}^{\phi}_{\sigma}[t]\,C \]
\[ \mathbf{E}^{\phi}_{\sigma}[\mathrm{Record}(fs)]\,C = \bigcap_{(n,t)\,\in\,fs} \{ n : \mathbf{E}^{\phi}_{\sigma}[t]\,C \} \]
\[ \mathbf{E}^{-}_{\sigma}[\mathrm{Variable}(vs)]\,C = \alpha^{-}_{vs} \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\text{如果 } (vs, -) \in C \]
\[ \mathbf{E}^{-}_{\sigma}[\mathrm{Variable}(vs)]\,C = \mu\alpha^{-}_{vs}.\,\alpha_{vs} \cap \bigcap_{u\in\mathrm{ub}^{vs}_{\sigma}} \mathbf{E}^{-}_{\sigma}[u]\,(C \cup \{(vs, -)\}) \quad\quad\text{如果 } (vs, -) \notin C \]
\[ \mathbf{E}^{+}_{\sigma}[\mathrm{Variable}(vs)]\,C = \alpha^{+}_{vs} \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\text{如果 } (vs, +) \in C \]
\[ \mathbf{E}^{+}_{\sigma}[\mathrm{Variable}(vs)]\,C = \mu\alpha^{+}_{vs}.\,\alpha_{vs} \cup \bigsqcup_{l\in\mathrm{lb}^{vs}_{\sigma}} \mathbf{E}^{+}_{\sigma}[l]\,(C \cup \{(vs, +)\}) \quad\quad\text{如果 } (vs, +) \notin C \]
图 11. 类型合并，其中元变量 φ 是 + 或 −，并且 ¬(+) = − 和 ¬(−) = +。
\[ \begin{aligned} \mathcal{E}_\sigma^-[\mathrm{Variable}(vs)]\,C &= \mu\alpha_{vs}^-. \bigcap_{u \in \mathrm{ub}^{vs}_\sigma} \mathcal{E}_\sigma^-[\![u]\!]\,(C \cup \{(vs, -)\}) & \text{if } (vs, -) \notin C \\ \mathcal{E}_\sigma^+[\mathrm{Variable}(vs)]\,C &= \mu\alpha_{vs}^+. \mathcal{E}_\sigma^-[\mathrm{Variable}(vs)]\,C \cup \bigsqcup_{l \in \mathrm{lb}_\sigma^{vs}} \mathcal{E}_\sigma^+[\![\ ]\!]\,(C \cup \{(vs, +)\}) & \text{if } (vs, +) \notin C \end{aligned} \]
Fig. 12. Unifying type coalescing. All other cases are exactly like in Figure 11, and are omitted.
LEMMA 2 (SOUNDNESS OF CONSTRAINING). When it succeeds, constraining in consistent bounds ensures that the bounds remain consistent and the coalescing of the constrained types become subtypes: if \(\vdash_{\text{cons}} \sigma\) and constrain(st₀, st₁)ₐ \(\Downarrow\) σ' (), then \(\vdash_{\text{cons}} \sigma'\) and \(\mathcal{E}_{\sigma'}^-[st₀] \le \mathcal{E}_{\sigma'}^+[st₁]\).
\[ \begin{aligned} \mathcal{E}_\sigma^-[\mathrm{Variable}(vs)]\,C &= \mu\alpha_{vs}^-. \bigcap_{u \in \mathrm{ub}^{vs}_\sigma} \mathcal{E}_\sigma^-[\![u]\!]\,(C \cup \{(vs, -)\}) & \text{如果 } (vs, -) \notin C \\ \mathcal{E}_\sigma^+[\mathrm{Variable}(vs)]\,C &= \mu\alpha_{vs}^+. \mathcal{E}_\sigma^-[\mathrm{Variable}(vs)]\,C \cup \bigsqcup_{l \in \mathrm{lb}_\sigma^{vs}} \mathcal{E}_\sigma^+[\![\ ]\!]\,(C \cup \{(vs, +)\}) & \text{如果 } (vs, +) \notin C \end{aligned} \]
图12. 统一类型合并。其他所有情况与图11完全相同，故省略。
引理2（约束的有效性）。 当成功时，在一致的界限内进行约束确保界限保持一致，且被约束类型的合并变为子类型：如果 \(\vdash_{\text{cons}} \sigma\) 且 constrain(st₀, st₁)ₐ \(\Downarrow\) σ' ()，那么 \(\vdash_{\text{cons}} \sigma'\) 且 \(\mathcal{E}_{\sigma'}^-[st₀] \le \mathcal{E}_{\sigma'}^+[st₁]\).
This is proven by induction on executions of the constraining calls. We actually need a stronger induction hypothesis, which relates the subtyping context \(\Sigma\) with the constraining cache, talks precisely about the bounds introduced by each call, and states that existing subtyping relations between coalesced types are not altered by further constraining calls. The Variable cases are quite subtle; when we insert the new bound into the variable’s state, we temporarily break the consistency of the variable’s bounds, but we restore it as an effect of the following recursive calls to propagate the bound. To apply the induction on these recursive calls, we need to loosen the “consistent bounds” premise of the hypothesis, making an exception for those variables which appear as part of the current constraining cache, thus allowing the calls to happen in partially-broken bounds.
5.3.2 Completeness.
Completeness is proven through the following more general lemma:
这通过对约束调用执行的归纳证明。我们实际上需要一个更强的归纳假设，它将子类型上下文 \(\Sigma\) 与约束缓存相关联，准确地讨论每个调用引入的界限，并声明已合并类型之间的现有子类型关系不受进一步约束调用的影响。变量情况非常微妙；当我们将新界限插入变量的状态时，我们暂时打破了变量界限的一致性，但我们会在后续递归调用中恢复它，以传播该界限。为了对这些递归调用应用归纳，我们需要放宽假设中的“一致界限”前提，对那些作为当前约束缓存一部分出现的变量作出例外，从而允许在部分破坏的界限中进行调用。
5.3.2 完整性。
完整性通过以下更一般的引理证明：
LEMMA 3 (COMPLETENESS — GENERAL). *Assuming \(\Gamma \vdash t : \tau\), then for all \(ctx\), \(\sigma\), and type-variable substitution \(\rho\), if \(\rho(E_\sigma^-[ctx]) \equiv \Gamma\) then typeTerm(t)(ctx)ₐ \(\Downarrow\) _σ'_st for some st and \(\sigma'\), and there exists a substitution \(\rho'\) such that \(\rho'(E_{\sigma'}^-[ctx]) \equiv \Gamma\) and \(\rho'(E_{\sigma'}^+[st]) \le \tau\).*
Remark that “there exists a \(\rho'\) such that \(\rho'(\tau_0) \le \tau_1\)” is equivalent to “\(\tau_0 \le^\forall \tau_1\)” by definition of the subsumption relation \(\le^\forall\). Again, the core of the proof resides in lemmas about constraining.
LEMMA 4 (TERMINATION OF CONSTRAINING). *For all st₀, st₁, and \(\sigma\), either constrain(st₀, st₁)ₐ hits an err(...) case and fails, or there exists a \(\sigma'\) such that constrain(st₀, st₁)ₐ \(\Downarrow\) _\(\sigma'\)().*
引理 3 (完备性 — 一般). *假设 \(\Gamma \vdash t : \tau\)，则对于所有 \(ctx\)、\(\sigma\) 和类型变量替换 \(\rho\)，如果 \(\rho(E_\sigma^-[ctx]) \equiv \Gamma\)，则 typeTerm(t)(ctx)ₐ \(\Downarrow\) _σ'_st 对某些 st 和 \(\sigma'\) 成立，并且存在一个替换 \(\rho'\) 使得 \(\rho'(E_{\sigma'}^-[ctx]) \equiv \Gamma\) 且 \(\rho'(E_{\sigma'}^+[st]) \le \tau\)。*
注意，“存在一个 \(\rho'\) 使得 \(\rho'(\tau_0) \le \tau_1\)”根据子类关系 \(\le^\forall\) 的定义等价于“\(\tau_0 \le^\forall \tau_1\)”。再次强调，证明的核心在于关于约束的引理。
引理 4 (约束的终止). *对于所有 st₀、st₁ 和 \(\sigma\)，要么 constrain(st₀, st₁)ₐ 命中 err(...) 情况并失败，要么存在一个 \(\sigma'\) 使得 constrain(st₀, st₁)ₐ \(\Downarrow\) _\(\sigma'\)()。*
LEMMA 5 (COMPLETENESS OF CONSTRAINING). *Constraining succeeds on types whose coalesced forms are subtypes, and it does not alter existing subtyping relationships: for all st₀, st₁, \(\rho\), and \(\sigma\), if \(\rho(E_\sigma^-[st₀]) \le E_\sigma^+[st₁]\), then constrain(st₀, st₁)ₐ \(\Downarrow\) _\(\sigma'\)() for some \(\sigma'\) - i.e., constraining does not yield an error — and for all st₂, st₃, \(\sigma'\) such that constrain(st₂, st₃)ₐ \(\Downarrow _\sigma'\)(), then \(\rho(E_{\sigma'}^-[st₀]) \le E_{\sigma'}^+[st₁]\).*
引理 5 (约束的完整性)。 *限制在其合并形式为子类型的类型上成功，并且不会改变现有的子类型关系：对于所有的 st₀, st₁, \(\rho\), 和 \(\sigma\)，如果 \(\rho(E_\sigma^-[st₀]) \le E_\sigma^+[st₁]\)，则 constrain(st₀, st₁)ₐ \(\Downarrow\) _\(\sigma'\)() 对某个 \(\sigma'\) 成立 — 即，限制不会产生错误 — 并且对于所有的 st₂, st₃, \(\sigma'\)，如果 constrain(st₂, st₃)ₐ \(\Downarrow _\sigma'\)()，则 \(\rho(E_{\sigma'}^-[st₀]) \le E_{\sigma'}^+[st₁]\).*
We prove Lemmas 3 and 5 by induction on typing and subtyping derivations, respectively. The rule S-TRANS causes some trouble: in case the subtyping derivation used it, we get premises which refer to derivations on which we cannot apply the induction, because they do not correspond to recursive constrain calls. S-TRANS can be removed from the system and proven from the other rules only in an empty subtyping context; indeed, \(\Sigma\) could in principle include transitivity-breaking hypotheses, such as \((\top \le \bot) \in \Sigma\). But the subtyping context, which will mirror the constraining cache, will not be empty in the actual inductive proof of (a stronger version of) Lemma 5. The solution is to show that no transitivity-breaking assumptions are ever introduced in the subtyping context during successful constraining, and that the input subtyping relation can always be derived without using S-TRANS; we do this by strengthening the induction hypothesis accordingly.
6 EXPERIMENTAL EVALUATION
我们通过对类型和子类型推导的归纳法证明引理 3 和引理 5。规则 S-TRANS 造成了一些麻烦：如果子类型推导使用了它，我们得到的前提引用了无法应用归纳法的推导，因为它们不对应于递归约束调用。S-TRANS 可以在空的子类型上下文中从系统中删除，并且仅通过其他规则证明；实际上，\(\Sigma\) 原则上可以包含破坏传递性的假设，例如 \((\top \le \bot) \in \Sigma\)。但是，子类型上下文将在引理 5（更强版本）实际归纳证明中反映约束缓存，因此不会为空。解决方案是证明在成功约束过程中，子类型上下文中从未引入破坏传递性的假设，并且输入子类型关系总是可以在不使用 S-TRANS 的情况下推导出来；我们通过相应地加强归纳假设来做到这一点。
6 实验评估
To evaluate the strengths of both the Simple-sub and MLsub implementations, we ran them on 1,313,832 randomly-generated expressions of varying sizes, of which 515,509 turned out to be well-typed and 798,321 turned out to be ill-typed.
Subsumption checking. MLsub provides a subsumption checker, whose goal is to determine if one inferred signature is at least as general as another (i.e., it tests for \(\le^\forall\)). We used MLsub’s subsumption checker to verify that both algorithms produced equivalent result, checking that mutual subsumption held between the two inferred type expressions.
为了评估 Simple-sub 和 MLsub 实现的优劣，我们在 1,313,832 个随机生成的不同大小的表达式上进行了测试，其中 515,509 个被证明是良类型的，798,321 个被证明是错误类型的。
subsumption检查。 MLsub 提供了一个 subsumption checker，其目标是确定一个推断的签名是否至少与另一个一样一般（即，它测试 \(\le^\forall\)）。我们使用 MLsub 的归纳检查器来验证两个算法产生的结果是相同的，检查两个推断类型表达式之间的互归纳是否成立。
Generated expressions. We considered random expressions making use of integer literals, lambdas, applications, record creations, field selections, recursive let bindings, and non-recursive let bindings. We used at most five different variable names and at most three different field names per expression. We stochastically generated well-scoped expressions without shadowing, using a depth-first search with an exponential decrease in probability of recursing into non-leaf subexpression. This generated 1,313,832 expressions of sizes ranging from 1 to 23, the majority (about a million) being in the 10–15 range. The code used for generating and testing these expressions can be found online in the mlsub-compare branch of the repository, as well as in the archived artifact of this paper.
生成的表达式。 我们考虑了随机表达式，使用整数字面量、lambda、函数调用、结构体创建、字段选择、递归 let 绑定以及非递归 let 绑定。每个表达式中我们最多使用五个不同的变量名和三个不同的字段名。我们随机生成了无变量遮蔽的良作用域表达式，使用深度优先搜索，并在递归到非叶子子表达式的概率上以指数方式递减。如此生成的表达式总计 1,313,832 个，大小范围从 1 到 23，大多数（约一百万个）在 10–15 范围内。用于生成和测试这些表达式的代码可以在在线的 mlsub-compare 仓库分支中找到，也可以在本文的档案工件中找到。
Bugs found in MLsub. We found several bugs in MLsub: a
variable shadowing bug — the expression
let rec x = (let y = x in (fun x -> y)) in x gets
assigned the wrong type a -> a because of the shadowing
of let-bounds variable x;27 a
type comparison bug due to a typo (which had already been fixed in
another branch of the project); and a simplification bug, giving (for
instance) to the record expression
{u = 0; v = {w = {w = 0}}} the wrong type
{u : int, v : (rec a = {w : a})}. Because of the latter
bug, to carry out the tests successfully, we had to disable MLsub’s
simplifier (but the Simple-sub simplifier was still enabled).
Summary. We were able to make sure that Simple-sub and MLsub agreed on type inference for more than a million randomly-generated expressions. Systematic testing turned out to be a surprisingly useful tool for detecting small mistakes which would have otherwise gone unnoticed.
7 CONCLUSIONS AND FUTURE WORK
在MLsub中发现的错误。
我们在MLsub中发现了几个错误：一个变量遮蔽错误——表达式
let rec x = (let y = x in (fun x -> y)) in x 由于遮蔽了
let-bound 变量 x 而被赋予了错误的类型
a -> a；28 一个由于 TYPO
引起的类型比较错误（该错误已经在项目的另一个分支中修复）；以及一个简化错误，使得（例如）结构体表达式
{u = 0; v = {w = {w = 0}}} 被赋予了错误的类型
{u : int, v : (rec a = {w : a})}。由于后一个错误，为了成功进行测试，我们不得不禁用
MLsub 的简化器（但 Simple-sub 的简化器仍然启用）。
总结。 我们能够确保 Simple-sub 和 MLsub 在超过一百万个随机生成的表达式上的类型推断一致。系统化测试被证明是一个令人惊讶的有效工具，用于检测那些否则会被忽视的小错误。
7 结论与未来工作
Algebraic subtyping and its realization in MLsub demonstrated a very promising new technique for inferring compact principal types in the presence of implicit subtyping. In this paper, we presented a simpler foundational view of MLsub’s type system, which does not require notions of bisubstitution or polar types, and slightly departs from the focus on algebra first. This new understanding lead us to more approachable type inference specification and implementation. We showed the design of Simple-sub, which achieves principal type inference and reasonable simplification in just 500 lines of code, to serve as an inspiration to future type systems and programming languages designers.
代数子类型及其在MLsub中的实现展示了一种在隐式子类型存在时推导紧凑主类型的新技术，前景非常可观。本文提出了一个更简单的MLsub类型系统的基础视角，该视角不需要双替代或极性类型的概念，并且在一定程度上偏离了代数优先的重点。这一新理解使我们能够制定更易于接近的类型推导规范和实现。我们展示了Simple-sub的设计，它在仅500行代码内实现了主类型推导和合理简化，以此激励未来的类型系统和编程语言设计者。
There is still much to be explored among the possibilities offered by algebraic subtyping, and by the new Simple-sub algorithm in particular. Polymorphic variants, a very useful language feature [Garrigue 1998], are the dual of polymorphic record types. A simple form of polymorphic variants (i.e., without default match cases and without nested patterns) can be handled in our system in exactly the same way as we have shown for records. Both variants and records can also be extended easily to support row variable for extensibility, yielding a powerful system; moreover, such a system would still be simple and natural to use thanks to subtyping, which usefully complements row polymorphism [Pottier 1998, Chapter 14.7]. Finally, we have been prototyping extensions for more advanced features which also benefit from subtyping, such as first-class polymorphism.
8 ACKNOWLEDGMENTS
I would like to thank Stephen Dolan and Alan Mycroft for their responsiveness and help in testing MLsub, and for their feedback on the paper; Paolo G. Giarrusso for his insightful suggestions; the paper’s shepherd Tom Schrijvers; and the anonymous reviewers for their useful comments.
REFERENCES
仍有许多可能性等待我们去探索，特别是代数子类型和新的 Simple-sub 算法。多态变体，这是一个非常有用的语言特性 [Garrigue 1998]，是多态结构体类型的对偶。我们系统中可以以 完全 相同的方式处理多态变体的简单形式（即，没有默认匹配案例和嵌套模式），就像我们展示的结构体一样。变体和结构体也可以很容易地扩展以支持行变量，从而实现可扩展性，产生一个强大的系统；此外，得益于子类型，这样的系统仍然会简单自然，且实用地补充了行多态性 [Pottier 1998, Chapter 14.7]。最后，我们一直在为更高级特性原型开发扩展，这些特性也受益于子类型，例如一等公民多态性。
8 致谢
我想感谢 Stephen Dolan 和 Alan Mycroft 对 MLsub 测试的响应和帮助，以及他们对论文的反馈；感谢 Paolo G. Giarrusso 的深刻建议；感谢论文的指导 Tom Schrijvers；感谢匿名评审对其有用评论的贡献。
参考文献
Roberto M. Amadio and Luca Cardelli. 1993. Subtyping Recursive Types. ACM Trans. Program. Lang. Syst. 15, 4 (Sept. 1993), 575–631. https://doi.org/10.1145/155183.155231
Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. Springer International Publishing, Cham, 249–272. https://doi.org/10.1007/978-3-319-30936-1_14
Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, and Jérôme Vouillon. 2007. A Very Modal Model of a Modern, Major, General Type System. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Nice, France) (POPL ’07). Association for Computing Machinery, New York, NY, USA, 109–122. https://doi.org/10.1145/1190216.1190235
Roberto M. Amadio 和 Luca Cardelli. 1993. 子类型递归类型. ACM Trans. Program. Lang. Syst. 15, 4 (1993年9月), 575–631. https://doi.org/10.1145/155183.155231
Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, 和 Sandro Stucki. 2016. 依赖对象类型的本质. Springer International Publishing, Cham, 249–272. https://doi.org/10.1007/978-3-319-30936-1_14
Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, 和 Jérôme Vouillon. 2007. 现代主要通用类型系统的非常模态模型. 在 第三十四届年度 ACM SIGPLAN-SIGACT 编程语言原理研讨会会议录 (法国尼斯) (POPL ’07). 计算机协会, 纽约, NY, 美国, 109–122. https://doi.org/10.1145/1190216.1190235
Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyen. 2016. Set-theoretic types for polymorphic variants. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). Association for Computing Machinery, Nara, Japan, 378–391. https://doi.org/10.1145/2951913.2951928
Giuseppe Castagna and Zhiwu Xu. 2011. Set-Theoretic Foundation of Parametric Polymorphism and Subtyping. (2011), 94–106. https://doi.org/10.1145/2034773.2034788
Nathanaël Courant. 2018. Safely typing algebraic effects (Gagallium Blog). http://gallium.inria.fr/blog/safely-typing-algebraic-effects/. Accessed: 2020-06-30.
Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’82). Association for Computing Machinery, Albuquerque, New Mexico, 207–212. https://doi.org/10.1145/582153.582176
Stephen Dolan. 2017. Algebraic subtyping. Ph.D. Dissertation.
Stephen Dolan and Alan Mycroft. 2017. Polymorphism, subtyping, and type inference in MLsub. ACM SIGPLAN Notices 52, 1 (Jan. 2017), 60–72. https://doi.org/10.1145/3093333.3099882
Giuseppe Castagna, Tommaso Petrucciani, 和 Kim Nguyen. 2016. 多态变体的集合论类型. 收录于 第21届ACM SIGPLAN国际函数编程会议（ICFP 2016）论文集. 计算机协会, 日本奈良, 378–391. https://doi.org/10.1145/2951913.2951928
Giuseppe Castagna 和 Zhiwu Xu. 2011. 参数多态性和子类型的集合论基础. (2011), 94–106. https://doi.org/10.1145/2034773.2034788
Nathanaël Courant. 2018. 安全类型化代数效应 (Gagallium Blog). http://gallium.inria.fr/blog/safely-typing-algebraic-effects/. 访问时间: 2020-06-30.
Luis Damas 和 Robin Milner. 1982. 函数程序的主要类型方案. 收录于 第9届ACM SIGPLAN-SIGACT编程语言原理研讨会论文集（POPL ’82）. 计算机协会, 新墨西哥州阿尔伯克基, 207–212. https://doi.org/10.1145/582153.582176
Stephen Dolan. 2017. 代数子类型. 博士论文.
Stephen Dolan 和 Alan Mycroft. 2017. MLsub中的多态性、子类型和类型推断. ACM SIGPLAN通知 52, 1 (2017年1月), 60–72. https://doi.org/10.1145/3093333.3099882
Joshua Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism. SIGPLAN Not. 48, 9 (Sept. 2013), 429–442. https://doi.org/10.1145/2544174.2500582
Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation. 268–277.
Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2008. Semantic Subtyping: Dealing Set-Theoretically with Function, Union, Intersection, and Negation Types. J. ACM 55, 4, Article 19 (Sept. 2008), 64 pages. https://doi.org/10.1145/1391289.1391293
Jacques Garrigue. 1998. Programming with polymorphic variants. In ML Workshop, Vol. 13. Baltimore, 7.
Roger Hindley. 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc. 146 (1969), 29–60. https://doi.org/10.2307/1995158 Publisher: American Mathematical Society.
Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. 2005. Regular Expression Types for XML. ACM Trans. Program. Lang. Syst. 27, 1 (Jan. 2005), 46–90. https://doi.org/10.1145/1053468.1053470
Joshua Dunfield 和 Neelakantan R. Krishnaswami. 2013. 完整且简单的双向类型检查用于更高阶多态性. SIGPLAN Not. 48, 9 (2013年9月), 429–442. https://doi.org/10.1145/2544174.2500582
Tim Freeman 和 Frank Pfenning. 1991. ML 的细化类型. 载于 ACM SIGPLAN 1991 编程语言设计与实现会议纪要. 268–277.
Alain Frisch, Giuseppe Castagna 和 Véronique Benzaken. 2008. 语义子类型: 用集合理论处理函数、并集、交集和否定类型. J. ACM 55, 4, Article 19 (2008年9月), 64页. https://doi.org/10.1145/1391289.1391293
Jacques Garrigue. 1998. 使用多态变体编程. 载于 ML Workshop, 第13卷. 巴尔的摩, 7.
Roger Hindley. 1969. 组合逻辑中对象的主类型方案. Trans. Amer. Math. Soc. 146 (1969), 29–60. https://doi.org/10.2307/1995158 出版社: 美国数学学会.
Haruo Hosoya, Jérôme Vouillon 和 Benjamin C. Pierce. 2005. XML 的正则表达式类型. ACM Trans. Program. Lang. Syst. 27, 1 (2005年1月), 46–90. https://doi.org/10.1145/1053468.1053470
DeLesley S. Hutchins. 2010. Pure Subtype Systems. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Madrid, Spain) (POPL ’10). Association for Computing Machinery, New York, NY, USA, 287–298. https://doi.org/10.1145/1706299.1706334
Oleg Kiselyov. 2013. Efficient generalization with levels (Okmij Blog). http://okmij.org/ftp/ML/generalization.html#levels. Accessed: 2020-06-30.
Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci. 17, 3 (Dec. 1978), 348–375. https://doi.org/10.1016/0022-0000(78)90014-4
Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg Beach, Florida, USA) (POPL ’96). Association for Computing Machinery, New York, NY, USA, 54–67. https://doi.org/10.1145/237721.237729
DeLesley S. Hutchins. 2010. 纯子类型系统。载于 第37届年度 ACM SIGPLAN-SIGACT 编程语言原则研讨会论文集 （西班牙马德里）(POPL ’10)。计算机协会，纽约，纽约，美国，287–298。 https://doi.org/10.1145/1706299.1706334
Oleg Kiselyov. 2013. 带级别的高效泛化 (Okmij 博客). http://okmij.org/ftp/ML/generalization.html#levels. 访问时间：2020-06-30。
Robin Milner. 1978. 编程中类型多态性的理论。 计算机与系统科学杂志 17, 3 (1978年12月)，348–375。 https://doi.org/10.1016/0022-0000(78)90014-4
Martin Odersky 和 Konstantin Läufer. 1996. 将类型注解付诸实践。载于 第23届 ACM SIGPLAN-SIGACT 编程语言原则研讨会论文集 （美国佛罗里达州圣彼得堡海滩）(POPL ’96)。计算机协会，纽约，纽约，美国，54–67。 https://doi.org/10.1145/237721.237729
David J. Pearce. 2013. Sound and Complete Flow Typing with Unions, Intersections and Negations. In Verification, Model Checking, and Abstract Interpretation (Lecture Notes in Computer Science), Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.). Springer, Berlin, Heidelberg, 335–354. https://doi.org/10.1007/978-3-642-35873-9_21
Benjamin C. Pierce. 2002. Types and programming languages. MIT press.
François Pottier. 1998. Type Inference in the Presence of Subtyping: from Theory to Practice. Research Report RR-3483. INRIA. https://hal.inria.fr/inria-00073205
Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (Tucson, AZ, USA) (PLDI ’08). Association for Computing Machinery, New York, NY, USA, 159–169. https://doi.org/10.1145/1375581.1375602
David J. Pearce. 2013. 带有联合、交集和否定的声音和完整流类型。载于 Verification, Model Checking, and Abstract Interpretation (Lecture Notes in Computer Science), Roberto Giacobazzi, Josh Berdine 和 Isabella Mastroeni (编). Springer, Berlin, Heidelberg, 335–354. https://doi.org/10.1007/978-3-642-35873-9_21
Benjamin C. Pierce. 2002. 类型与编程语言. MIT press.
François Pottier. 1998. 存在子类型时的类型推断：从理论到实践. 研究报告 RR-3483. INRIA. https://hal.inria.fr/inria-00073205
Patrick M. Rondon, Ming Kawaguci 和 Ranjit Jhala. 2008. Liquid Types. 载于 Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (Tucson, AZ, USA) (PLDI ’08). Association for Computing Machinery, New York, NY, USA, 159–169. https://doi.org/10.1145/1375581.1375602
Andreas Rossberg. 2015. 1ML – Core and Modules United (F-Ing First-Class Modules). In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Vancouver, BC, Canada) (ICFP 2015). Association for Computing Machinery, New York, NY, USA, 35–47. https://doi.org/10.1145/2784731.2784738
John Rushby, Sam Owre, and Natarajan Shankar. 1998. Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Trans. Softw. Eng. 24, 9 (Sept. 1998), 709–720. https://doi.org/10.1109/32.713327
Sam Tobin-Hochstadt and Matthias Felleisen. 2010. Logical Types for Untyped Languages. SIGPLAN Not. 45, 9 (Sept. 2010), 117–128. https://doi.org/10.1145/1932681.1863561
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (Gothenburg, Sweden) (ICFP '14). Association for Computing Machinery, New York, NY, USA, 269–282. https://doi.org/10.1145/2628136.2628161
Andreas Rossberg. 2015. 1ML – Core and Modules United (F-Ing First-Class Modules). 在 Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Vancouver, BC, Canada) (ICFP 2015). 计算机协会，纽约，NY，USA, 35–47. https://doi.org/10.1145/2784731.2784738
John Rushby, Sam Owre, 和 Natarajan Shankar. 1998. Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Trans. Softw. Eng. 24, 9 (1998年9月), 709–720. https://doi.org/10.1109/32.713327
Sam Tobin-Hochstadt 和 Matthias Felleisen. 2010. Logical Types for Untyped Languages. SIGPLAN Not. 45, 9 (2010年9月), 117–128. https://doi.org/10.1145/1932681.1863561
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, 和 Simon Peyton-Jones. 2014. Refinement Types for Haskell. 在 Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (Gothenburg, Sweden) (ICFP '14). 计算机协会，纽约，NY，USA, 269–282. https://doi.org/10.1145/2628136.2628161
OCaml 在这些打破原则的特性上一直相对保守，显著的例外是 GADTs 和多重结构体字段，但 Haskell 在这方面的采用更为宽松，以增强表达能力。↩︎
OCaml 在这些打破原则的特性上一直相对保守，显著的例外是 GADTs 和多重结构体字段，但 Haskell 在这方面的采用更为宽松，以增强表达能力。↩︎
例如，OCaml 使用行类型使对象类型和多态变体更灵活，避免了显式强制转换的需求，这在某种程度上类似于隐式子类型 [Pottier 1998]；而 Haskell 可以使用类型类来模拟子类型，如 lens 和 optics 库所示，这两个库都是围绕子类型类比设计的。↩︎
例如，OCaml 使用行类型使对象类型和多态变体更灵活，避免了显式强制转换的需求，这在某种程度上类似于隐式子类型 [Pottier 1998]；而 Haskell 可以使用类型类来模拟子类型，如 lens 和 optics 库所示，这两个库都是围绕子类型类比设计的。↩︎
从操作的角度来看，Simple-sub 与 MLsub 的图形实现有许多相似之处，尽管这两种算法仍然相当不同——尤其是，MLsub 在其约束图中将正节点与负节点分开（而 Simple-sub 没有这种分离），并且 MLsub 生成的类型变量比 Simple-sub 多得多。↩︎
从操作的角度来看，Simple-sub 与 MLsub 的图形实现有许多相似之处，尽管这两种算法仍然相当不同——尤其是，MLsub 在其约束图中将正节点与负节点分开（而 Simple-sub 没有这种分离），并且 MLsub 生成的类型变量比 Simple-sub 多得多。↩︎
我们对于代数子类型的可扩展性属性是否如其作者所宣传的那样有用，除了它的简化结果之外，存在一些疑问。首先，实际的编程语言设计上已经具有可扩展的类型系统，因为它们允许用户定义数据类型，而来自封闭世界形式演算的子类型悖论通常不会在这些环境中出现或造成问题。其次，扩展编程语言的核心类型语义的情况极为罕见，因此在设计类型系统时，这种情况可能并不值得优化。↩︎
我们对于代数子类型的可扩展性属性是否如其作者所宣传的那样有用，除了它的简化结果之外，存在一些疑问。首先，实际的编程语言设计上已经具有可扩展的类型系统，因为它们允许用户定义数据类型，而来自封闭世界形式演算的子类型悖论通常不会在这些环境中出现或造成问题。其次，扩展编程语言的核心类型语义的情况极为罕见，因此在设计类型系统时，这种情况可能并不值得优化。↩︎
有趣的是，OCaml 编译器支持递归类型，但默认情况下只允许它们作为对象类型的一部分，因为它们可能导致意外情况——在某些情况下推断出递归类型，而不是报告明显的错误。在基于 MLsub 的实际语言中，可以对递归类型的推断施加类似的限制。↩︎
有趣的是，OCaml 编译器支持递归类型，但默认情况下只允许它们作为对象类型的一部分，因为它们可能导致意外情况——在某些情况下推断出递归类型，而不是报告明显的错误。在基于 MLsub 的实际语言中，可以对递归类型的推断施加类似的限制。↩︎
⁶从这个意义上说，
int\(\sqcup\)string类似于 \(\tau\)，尽管 MLsub 不认为这两种类型是等价的。↩︎⁷请注意，Java的几个特性远远超出了MLsub所能表达的范畴（例如，多态方法和泛型类层次结构），因此MLsub确实是比我们假设的结构化类型Java严格少的表达能力。↩︎
⁶从这个意义上说，
int\(\sqcup\)string类似于 \(\tau\)，尽管 MLsub 不认为这两种类型是等价的。↩︎⁷请注意，Java的几个特性远远超出了MLsub所能表达的范畴（例如，多态方法和泛型类层次结构），因此MLsub确实是比我们假设的结构化类型Java严格少的表达能力。↩︎
⁸实际上，在真实的Java中，下界规范 inexplicably 仅支持通配符类型参数——这显然是一个疏漏。有关Java中类型边界的更多详细信息，请参见 https://docs.oracle.comjavase/tutorial/java/generics/bounded.html 和 https://docs.oracle.comjavase/tutorial/java/generics/lowerBounded.html。↩︎
⁸实际上，在真实的Java中，下界规范 inexplicably 仅支持通配符类型参数——这显然是一个疏漏。有关Java中类型边界的更多详细信息，请参见 https://docs.oracle.comjavase/tutorial/java/generics/bounded.html 和 https://docs.oracle.comjavase/tutorial/java/generics/lowerBounded.html。↩︎
⁹正如 Dolan 和 Mycroft [2017] 所解释的，这种类型与更自然的 \(\forall \alpha, \beta\) 一样一般。 \(bool \to \alpha \to \beta \to \alpha \sqcup \beta\)。↩︎
⁹正如 Dolan 和 Mycroft [2017] 所解释的，这种类型与更自然的 \(\forall \alpha, \beta\) 一样一般。 \(bool \to \alpha \to \beta \to \alpha \sqcup \beta\)。↩︎
¹¹Scala 语法 (
foo(a,_,c)) 是对 lambda 抽象 (x => foo(a, x, c)) 的一种简写。↩︎¹¹Scala 语法 (
foo(a,_,c)) 是对 lambda 抽象 (x => foo(a, x, c)) 的一种简写。↩︎¹²在 Scala 中，
opt.fold(t)(f)通过对包含的值调用函数f来折叠opt选项，如果选项为空，则评估默认的thunk t。MutMap的map.getOrElseUpdate(k, t)方法在map中查找一个键k；如果未找到该键，则评估thunk t并用该值更新map；否则，返回与该键关联的值。↩︎¹³在Scala中，sealed trait 类似于只能由同一文件中定义的类型实现的 interface。↩︎
¹³在Scala中，sealed trait 类似于只能由同一文件中定义的类型实现的 interface。↩︎
¹⁴一些方法在面对这种更高级的推理形式时实现了完整的类型推断 [Castagna et al. 2016]，但它们通常缺乏主类型属性（它们生成一组可能的类型而不是单个最通用的类型），而且它们自然不支持相同程度的简化。↩︎
¹⁵我们对let多态性的实现可以单独证明是正确的，方法是显示它在每个使用地点的效果与复制let绑定定义相同（这就是let多态性的语义[Damas和Milner 1982]）。↩︎
¹⁵我们对let多态性的实现可以单独证明是正确的，方法是显示它在每个使用地点的效果与复制let绑定定义相同（这就是let多态性的语义[Damas和Milner 1982]）。↩︎
¹⁶我们发现这一点是因为，在早期的测试尝试中，我们生成了包含遮蔽的表达式。↩︎
¹⁶我们发现这一点是因为，在早期的测试尝试中，我们生成了包含遮蔽的表达式。↩︎