揭开MLsub的神秘面纱--代数子类型化的简单本质

注：这篇网络文章是一篇论文的较旧版本，现已作为ICFP珍珠出版。你可以在这里找到那份报纸的预印本。

代数子类型化是有子类型化的全局类型推理的一种新方法。它扩展了传统的Hindley-Milner类型推理，同时保留了主体类型属性-也就是说，它总是可以为任何给定的表达式推断出最通用的类型。这种方法是由斯蒂芬·多兰(Stephen Dolan)和艾伦·麦克罗夫特(Alan Mycroft)共同开发的，作为他的博士论文的一部分。

在MLsub类型推理机中实现了代数子类型。然而，MLsub的设计似乎比用于传统ML语言的简单统一算法要复杂得多。事实证明，MLsub很难掌握，即使对于像我这样已经熟悉编译器和类型系统的人也是如此。

由于对这种情况不满意，我想深入了解代数子类型化方法。除了形式主义，它到底有什么特别之处？在两极统一和极地类型的奇怪概念背后隐藏着哪些简单的概念？

本文就是对这些问题的回答。我提出了代数子类型化的另一种算法，称为Simple-SUB。SIMPLE-SUB可以在500行以下的代码中高效实现(包括解析、简化和美观的打印)，而且我认为它比MLsub看起来更熟悉，也更容易理解。

本文旨在减少形式主义，便于新类型系统和编程语言的潜在设计人员使用。

ML语言家族包括标准ML、OCaml和Haskell，它们是围绕一种强大的“全局”类型推理方法设计的，这种方法植根于Hindley和Milner的工作，后来由Damas密切形式化。在这种方法中，类型系统设计得足够简单，可以从术语中明确推断类型，而不需要任何类型注释的帮助。也就是说，对于任何未注释的术语，总是可以推断出包含可以分配给该术语的所有其他类型的主体类型。例如，术语$\lambda{x}。{x}$可以分配类型$\mathsf{bool}\to\mathsf{bool}$和$\mathsf{int}\to\mathsf{int}$，但这两个类型都包含在多态类型$\forall a.\a\to a$中，也写为'；a-&&39；a；a，这是此术语的主要类型。

Hindley-Milner(HM)类型推理与更受限制的“本地”类型推理方法形成对比，后者可以在Scala和C#等语言中找到，这些语言通常要求程序员显式注释变量类型。另一方面，放弃主体类型属性允许这些类型系统更具表现力，并支持面向对象和一级多态性等功能。请注意，在实践中，即使像OCaml和Haskell这样的ML语言也采用了表达式类型系统特性，这些特性在使用时会破坏主体类型属性。1个

子类型化是一种富有表现力的功能，它允许将类型结构化为层次结构(通常是子类型网格)，并且可以根据此层次结构透明地细化或加宽类型。这让我们可以表达这样一个事实，即某些类型比其他类型更精确(包含更多信息)，但仍然具有兼容的运行时表示，因此它们之间不需要强制。例如，在NAT类型是INT的子类型的系统中，可以在期望INT列表的地方透明地使用NAT列表，而不必对列表的所有元素应用强制函数。可以使用有些繁重的类型系统机制模拟子类型(OCaml和Haskell偶尔也会这样做2)，但是对子类型的一流支持带来了更简单的类型签名和更好的类型推理的好处。

长期以来，人们普遍认为普遍存在的隐式子类型阻碍了令人满意的全局类型推理。事实上，以前的推断子类型的方法不支持主体类型，或者导致推断包含复杂约束集的大型、笨重的类型方案，使得程序员难以理解它们。

代数子类型是由Dolan和Mycroft引入的，它是一种ML风格的类型系统，支持子类型和全局类型推理，同时生成紧凑的主体类型。这里，紧凑是指这样一个事实，即推断的类型是相对简单的类型表达式，没有任何可见的约束，使得程序员很容易理解它们。这是通过仔细设计底层子类型格的语法和语义来实现的，允许简化类型推理算法的约束解析过程中的假设。

然而，Dolan为实现代数子类型而提出的二合一算法对于许多专家和非专家来说都是相当难理解的。事实上，从表面上看，它看起来与传统上用于HM型系统的常用算法J有很大的不同：它需要几个额外的概念，如双取代和极型，使得它看起来更复杂。

值得庆幸的是，事实证明，代数子类型允许使用一种类型推断算法，我称之为Simple-SUB，该算法与熟悉的算法J非常相似，而且比二统一(或者至少比基本语法驱动的二统一形式)效率高得多。3在本文中，我展示了推断代数子类型实际上非常简单，并且可以在300行以下的Scala代码中完成。实际上，大部分复杂性来自于简化推断的类型表示形式，我们将在稍后讨论这一点。

虽然我们展示的实现是用Scala编写的，但是可以直接转换成任何其他函数式编程语言。

本文的目标是将代数子类型重塑为一个更简单的模型，允许更多有前途的类型系统和编程语言设计人员从这种方法提供的深刻见解中受益。

让我们首先简要回顾一下什么是代数子类型和MLsub，哪些不是，并尝试评估它们的表达能力。

MLsub的术语语法如下所示。我省略了布尔文字和if-Then-Else，因为它们很容易被类型化为基元组合符。我还只使用了一种形式的变量$x$，这对我们的使用就足够了(出于技术原因，Dolan的MLsub形式主义将lambda绑定变量与let绑定变量区分开来)。

MLsub的类型语法(总结如下)包括布尔值、函数类型、记录类型、类型变量、TOP$\TOP$(所有值的类型-所有类型的超类型)、BOOT$\BOT$(没有值的类型-所有类型的子类型)、类型UNION$\SQCAP$、类型交集$\SQCAP$和递归类型$\MU{\alpha}。{\tau}$。

虽然大多数MLsub类型形式都是常见的，并不令人惊讶，但有两种类型需要我们特别关注：集合论类型(更具体地说是并集和交集类型)和递归类型。

对于第一次近似，并和交集类型可以用集合论术语来理解：类型项$\tau_0\sqCup\tau_1$(分别为$\tau_0\sqCup\tau_1$)。$\tau_0\sqcap\tau_1$)表示以下值的类型：两者)类型为$\tau_0$或(分别。和)类型为$\tau_1$。

MLsub使用这些类型间接约束推断的类型变量；例如，为术语$\lambda{x}推断的一种类型。{\set{l=x-1\，；\；r=x}}$可以是$\alpha\sqcap\mathsf{int}\to\set{l：\mathsf{int}\，，\；r：\alpha}$。该类型反映了这样一个事实，即在结果记录的$r$字段中返回$\alpha$类型的原始参数，因为输入类型$\alpha$结束于该位置，而且该参数应该能够被视为$\mathsf{int}$，通过函数类型左侧的交集$\alpha\sqcap\mathsf{int}$表示。跟踪精确的参数类型$\alpha$很重要：以后可以用比$\mathsf{int}$更具体的类型替换它，例如$\alpha=\mathsf{nat}$，这将使我们获得$\mathsf{nat}\to\set{l：\mathsf{int}\，；\；r：\mathsf{nat}}$。

另一方面，可能存在一些类型签名，其中某些$\alpha$变得无法与$\mathsf{int}$区分。例如，考虑术语$\lambda{x}。{\mathsf{if}\\mathsf{true}\\mathsf{Then}\{x-1}\\mathsf{Else}\{x}}$，其简化推断类型将仅为$\mathsf{int}\to\mathsf{int}$，因为看似更精确的类型$\alpha\sqcap\mathsf{int}\to\alpha\sqcap\mathsf{int}$实际上并不包含。

代数子类型的美妙之处在于，这种推理适用于任意的变量流和高阶函数；例如，前面的示例可以通过传入函数$f$来表示$\cdot-1$操作，如$\lambda{f}。{\lambda{x}。{\set{l=f x\，；\；r=x}}$，其类型可推断为$(\beta\to\Gamma)\to\alpha\sqcap\beta\to\set{l：\Gamma\，，\；r：\Alpha}$。将此函数应用于参数$(\lambda{x}。{x-1})$生成与原始示例相同的类型(简化后)。

递归类型$\µ\alpha。\tau$表示我们可以任意多次展开的类型；例如，$\µ\alpha。{\top\to\alpha}$等同于$\top\to(\µ\alpha.。{\top\to\alpha})$，相当于$\top\to(\top\to(\µ\alpha.。{\top\to\alpha}))$等)，并且是可以无限应用于任何参数的函数类型(因为所有子类型都是$\top$，并且该类型展开到接受$\top$参数的函数)。因此，递归类型在概念上是无限的-如果我们完全展开它，它将展开为一个无限深的树$\TOP\TO(\TOP\TO(\TOP\TO…))。$。如果这听起来让人困惑，那完全没问题。我们将了解如何理解递归类型，并在本文后面直观地了解为什么需要它们。

我们在上面给出的类型定义中有一个很大的“问题”：这些类型实际上不能在类型表达式中自由使用。MLsub类型的真正语法分为正类型和负类型。具体地说，并集和底部是正类型(并且不能出现在负位置)，而交点和顶部是负类型(并且不能出现在正位置)。

正位置对应于术语输出的类型，而负位置对应于术语作为输入接受的类型。例如，在$(\tau_0\to\tau_1)\to\tau_2$类型中，$\tau_2$类型处于正位置，因为它是主函数的输出，而函数类型$(\tau_0\to\tau_1)$处于负位置，因为它被视为主函数的输入。另一方面，作为输入的函数返回的$\tau_1$处于负位置(因为它是由调用者通过参数函数提供的)，而$\tau_0$处于正位置(因为它是由主函数在调用参数函数时提供的)。

这些极性限制意味着我们在上面看到的类型的完整语法实际上不能按原样使用；程序员不能在他们自己的类型批注中编写违反极性区分的类型。事实上，在MLsub中，您不能表示接受整数或字符串的函数的类型：此类型应该是$\mathsf{int}\sqCup\mathsf{string}\to\tau$，但是$\mathsf{int}\sqCup\mathsf{string}$在负值位置是非法的。另一方面，MLsub可以将合法类型$\tau\to\mathsf{int}\sqCup\mathsf{String}$分配给可以返回整数或字符串…的函数。不是很有用的东西，因为我们不能消费这样的价值观！

令人惊讶的是，这一切归根结底是MLsub语言从根本上并不比结构化Java更具表现力！要理解这一点，请回想一下，Java允许用户使用类型变量来量化类型，还允许用子类型和超类型绑定这些类型变量。我们的见解是，当在适当的极性使用并集和交集时，它们只是间接绑定类型变量的一种方式。

$<；\alpha\mathsf{\textbf{super}}\，\\mathsf{Prime}\mathsf{\textbf{扩展}}\，\\mathsf{nat\；\&；\；odd}>；(\alpha)\to\set{l：\mathsf{int}\，；\；r：\alpha}$。

这意味着$\alpha$应该是$\mathsf{Prime}$的超类型，也是$\mathsf{nat}$和$\mathsf{odd}$的子类型。

有趣的是，MLsub的递归类型可以通过F-有界多态性表示，Java也支持这种多态，允许您将类型变量绑定到包含类型变量本身出现的类型。

读了Dolan的论文和论文，人们可能会认为代数子类型的全部内容是：

然而，我认为这不是了解这里正在发生的事情的最有帮助的方式。

使类型的语义足够简单，使得所有推断的子类型约束都可以简化为对类型变量的约束；

记录所有相关类型变量上的结果约束，这可以用传统的方式来完成(我们稍后会看到)；

使用交集、并集和递归类型来表示类型变量受到间接约束的类型(无需单独的约束规范)。

在我看来，后一点更像是一种“巧妙的伎俩”，并没有真正比传统的方法有任何根本的优势。相反，如果一个类型变量多次出现，则其上的MLsub样式约束将重复，这可能会导致更大的类型表达式。

$\forall\alpha.\\alpha\sqcap\{\x：\mathsf{int}\，；\；x：\mathsf{bool}\\}\to\alpha\sqcap\{\x：\mathsf{int}\，；\；x：\mathsf{bool}\\}\to\alpha\sqcap\{\x：\mathsf{int}\，；\；x：\mathsf{bool。

$\forall\alpha\leq\{\x：\mathsf{int}\，；\；x：\mathsf{bool}\\}.\\alpha\to\alpha$。

现在我们已经对MLsub中的实际情况有了一个直观的了解，让我们设计一个可以利用这种直觉的新算法。

下面是SIMPLE-SUB算法。为简单起见，我将从描述不带let多态性的版本开始，稍后再添加let多态性。

我们将在本文其余部分使用的术语语法的Scala实现直接派生自上一个表，只是我添加了一个整型文字的结构：

ENUM TERM{CASE LIT(值：INT)//42 CASE Var(名称：字符串)//x CASE LAM(名称：字符串，RHS：TERM)//FUN x->；T Case App(lhs：Term，RHS：Term)//s t Case Rcd(field：List[(String，Term)])//{a：0，b：true，...}Case Sel(Receiver：Term，fieldName：String)//T.A Case Let(ISREC：Boolean，Name：String，RHS：Term，Body：Term)}。

代数数据类型在新的Scala3枚举语法中给出，但是可以使用Scala2密封的类层次结构等价地表示。

正如我在前面提到的，不需要IF-THEN-ELSE功能，因为我们可以只添加一个作为组合符：我的解析器实际上解析形式为$\mathsf{if}\{e_0}\\mathsf{Then}\{e_1}\\mathsf{Else}\{e_2}$的代码，就好像它是写成$\mathsf{if}\e_0\e_1\e_2$一样，我从一个上下文开始进行类型检查，该上下文将类型$\forall\alpha.\\mathsf{bool}\分配给‘$\mathsf{if}$’标识符to\alpha\to\alpha$。4.。

SIMPLE-SUB算法的出发点是认识到联合、交集、顶部、底部和递归类型都不是MLsub类型的真正核心，并且更接近其约束处理的紧急性质。

因此，我们将重点介绍类型变量、基元类型构造函数、函数类型和记录类型作为算法的基石；它们的Scala语法如下所示：

枚举SimpleType{case变量(st：VariableState)case原语(name：string)case函数(lhs：SimpleType，rhs：SimpleType)case Record(field：List[(String，SimpleType)])}

类型变量的状态仅由为其记录的所有边界给出：

请注意，我们使用可变变量来保存算法的当前状态-随着算法的进行，这些列表将发生变化。

为了现在执行类型推断，我们所需要做的就是累积和传播出现在不同类型之间的约束，将它们分解，直到它们归结为对类型变量的约束，我们可以通过改变它们记录的边界来约束它们。

类型推理的核心函数是typeTerm，它将类型分配给CTX类型上下文中的给定术语。它将得到约束函数的补充，强制将一种类型约束为另一种类型的子类型，如果这是不可能的，则会引发错误。我们已将typeTerm中的ctx参数设为隐式，以便在不更改时不必将其显式传递给每个递归调用：

Type ctx=Map[String，SimpleType]def typeTerm(Term：Term)(隐式CTX：CTX)：SimpleType=...。Def constrain(lhs：SimpleType，rhs：SimpleType)=...。

我们将使用两个小帮助器函数chresVar和err，分别生成新类型变量和引发错误：

Def resresVar()：Variable=Variable(new VariableState(Nil，Nil))def err(msg：string)：Nothing=抛出新异常("；type error："；+msg)。

现在我们已经建立了所有前提，我们可以开始编写基本类型推理算法的核心：

Def typeTerm(Term：Term)(隐式ctx：ctx)：SimpleType=Term Match{//整数文字：CASE LIT(N)=>；primitive("；int"；)。

GetOrElse方法用于访问给定键处的CTX映射，指定在找不到该键的情况下要执行的thunk：

//变量引用：case Var(Name)=>；ctx。GetOrElse(name，err("；Not Found："；+name))//记录创建：case rcd(Fs)=>；Records(fs.。Map{case(n，t)=>；(n，typeTerm(T))}。

为了对lambda抽象进行类型化，我们创建一个新变量来表示参数类型，并在当前上下文中键入lambda的主体，其中扩展了从参数名到这个新变量的绑定：

//lambda抽象：case Lam(name，body)=>；val param=resresVar()function(param，typeTerm(Body)(ctx+(name-gt；param)，LVL))。

对于类型化应用程序，我们同样引入一个新变量来表示我们正在应用的函数的结果类型：

最后，记录访问会产生一个约束，即接收方(选择左侧的表达式)是具有适当字段名称的记录类型：

//记录字段选择：case Sel(obj，name)=>；val res=resresVar()constrain(typeTerm(Obj)，ord((name，res)：：nil)res}

可以看到，基本的MLsub类型推理算法实际上与传统的HM样式类型推理算法J非常相似，一点也不复杂！

首先，请注意，随着类型推断的进行，使用可变变量更新的类型变量界限很可能会形成循环。我们必须使用一个缓存变量(最初为空)来说明这一点，该变量会记住已经进行或正在进行的所有类型比较，从而避免重复工作和无限递归：

定义约束(lhs：TypeShape，rhs：TypeShape)(隐式缓存：MutSet[(TypeShape，TypeShape。

.