重写Futhark类型检查器

# 重写 Futhark 类型检查器 来源：https://futhark-lang.org/blog/2026-07-21-rewriting-the-type-checker.html 发布于 2026 年 7 月 21 日 本文讲述 Futhark 类型检查器的发展历程，源于我即将合并的一次大规模重构（https://github.com/diku-dk/futhark/pull/2302）。主要面向其他语言设计者，其中包含一些我希望最初就知道的经验教训——尽管我并未深入阅读类型检查相关文献，所以这些内容或许早已是老生常谈。 ### 背景（https://futhark-lang.org/blog/2026-07-21-rewriting-the-type-checker.html#background） 早在混沌初开之时（https://futhark-lang.org/blog/2017-12-27-reflections-on-a-phd-accidentally-spent-on-language-design.html），我们最初设计 Futhark 时，类型系统非常简单：只有标量、数组和元组这些类型，所有函数都是一阶且单态的，没有类型推断。所有函数都必须标注参数和返回类型。从（近乎）一开始就存在的唯一高级特性，是通过一种唯一性类型（https://futhark-lang.org/blog/2022-06-13-uniqueness-types.html）实现的原地更新，尽管当时我们并未真正理解其复杂性。 那时（https://github.com/diku-dk/futhark/blob/48ca2dedf23990e2b0ffd00a26ab32ca4f0ef22c/src/L0/TypeChecker.hs）它真的只是一个类型*检查器*：从已知事实（参数的类型）出发，检查表达式类型是否一致，并跟踪别名来验证原地更新的使用。实现方式是对每个函数进行简单的自上而下单次遍历，在遍历过程中为 AST 节点标注已确定的类型，供后续阶段使用。这正是我在标准编程语言实现课程中学到（并后来自己教学）的同类类型检查器。当你能仅凭此就过关时，这是一个*良好*的设计：易于实现、相当高效、容易理解。当时我们并未真正理解*正确*检查原地更新安全规则所需付出的复杂性，所以这种简单或许只是假象，但那些日子我们依然很快乐。 当然，这种好日子并没有持续太久。我们最终开始添加特性，如记录（https://futhark-lang.org/blog/2017-03-06-futhark-record-system.html）和 ML 风格模块系统（https://futhark-lang.org/blog/2017-01-25-futhark-module-system.html）。到 0.4.0 版本时，我们引入了高阶函数和 Hindley-Milner 风格类型推断（https://futhark-lang.org/blog/2018-04-10-futhark-0.4.0-released.html）。实现是经典的（有些人可能会说过时的）Algorithm W（https://jeremymikkola.com/posts/2018_03_25_understanding_algorithm_w.html）——标准的 Hindley-Milner 类型推断算法。在遍历函数时，我们立即求解类型约束。然而，我们的一些类型系统特性从未与此方法自然契合。我们的记录系统以及唯一性类型，都依赖于能查询当前程序片段的类型并基于此做出决策。这种情况出现在分支中，比如`if a then b else c`的别名取决于`b`和`c`的类型是否能携带别名（基本类型不能）。我们通过向类型变量表示中添加各种额外信息拼凑出了一个实现，但这有些复杂、不易于验证正确性，且调试起来相当繁琐。 后来，当我们添加了合适的大小类型（https://futhark-lang.org/blog/2019-08-03-towards-size-types.html）时，我们通过扩展基础 Hindley-Milner 系统，将大小也视为一种可进行合一化的“类型”来实现。此时系统开始发出吱嘎声。再次考虑分支`if a then b else c`——结果的大小是多少？如果`b`和`c`是数组，我们需要确定它们是否具有相同大小，如果不是，则为结果大小生成一个存在量词。但在我们查看这个`if`时，可能还不知道它们是否是数组！类似情况很多，类型系统具有各种限制和奇怪之处，一个函数的良好类型化程度会以微妙的方式取决于你是否添加了类型注解。不过一个好的特性是，如果你在所有参数上都添加了类型注解（通常被认为是良好的风格），那么事情就会相当可预测地工作。但即便如此，此时对类型检查器进行 hack 已不再那么有趣。 最终，这种设计——单次程序遍历操纵日益复杂的状态——变得不可行。这是当我们开始研究 AUTOMAP（https://futhark-lang.org/blog/2024-06-17-automap.html）时发生的，这是一个（尚未完成）的系统，大致意思是你可以只说`f x`，而不必说`map f x`，让编译器计算出需要多少个`map`。在开发过程中，我们发现 AUTOMAP 必须通过从全局角度审视函数，部分地进行类型检查但不去推断数组的具体大小，确定使类型检查通过所需的最小`map`数量（通过使用 ILP 求解器），然后确定具体大小。这种设计无法融入现有类型检查器，所以我开始将其拆分为多个阶段。 第一个分离的阶段是名称解析（https://github.com/diku-dk/futhark/blob/master/src/Language/Futhark/TypeChecker/Names.hs）。它做你期望的事情：解析程序中的每个名称，实际上是为每个名称分配唯一标识符。这是一个小胜利，但简化了类型检查器一点。下一个阶段是概念上的最终阶段：检查别名和原地更新违规（https://github.com/diku-dk/futhark/blob/master/src/Language/Futhark/TypeChecker/Consumption.hs）。这被证明是*更*有收益的，因为该机制一直受限于必须处理不完整的类型信息。现在它会被提供一个*完全良好类型化的程序*，只需确定是否有任何原地约束被违反（本质上，原地更新在语义上是否可观察）。 现在我们剩下一个核心部分：“项类型检查器”，它同时执行正常的 ML 风格类型推断和大小推断。作为一种权宜之计，为了让 AUTOMAP 研究项目取得进展，我做了一件非常 hacky 的事情：我编写了一个全新的基于*约束*的类型检查器，它不执行大小推断，只执行标准类型推断。我们称之为*无大小类型检查器*。它不即时求解类型方程，而是生成一组*类型约束*（主要是类型相等性），由约束求解器“离线”求解。这种“生成然后求解”的方法使得处理复杂的类型系统特性更加可行，因为你无需基于部分信息做出决策，并且也被格拉斯哥 Haskell 编译器（https://www.youtube.com/watch?v=OISat1b2-4k）和 Flix（https://flix.dev/）所采用。在我们的实现中，我们使用这些约束来驱动 AUTOMAP 求解器，然后*丢弃这些约束并重新运行原始的大小感知类型检查器*（加上 AUTOMAP 提供的一些额外信息）。这种做法*可行*，所有程序都能通过类型检查，但我认为我们的论文（https://futhark-lang.org/publications/oopsla24.pdf）用词“我们的 Automap 启用类型检查器未优化”已经相当客气了。我担心的不仅仅是冗余工作导致的低效，更在于*重复逻辑*导致的不清晰——每个类型检查规则在代码中都被重复了！ ### 新的类型检查器（https://futhark-lang.org/blog/2026-07-21-rewriting-the-type-checker.html#the-new-type-checker） 我仍然对 AUTOMAP 本身抱有希望，但要使其达到可用状态还需要未知数量的实现工作。然而，在这项工作中，我被基于约束的类型检查器的优雅所吸引。核心优势在于你可以推迟决策，直到所有信息都可用。从人类角度来看，当你可以打印出所有约束并进行分析时，调试（或基准测试）也要*容易得多*。不幸的是，我们的实现非常糟糕。去年我开始了在没有 AUTOMAP 的情况下进行基于约束的类型检查的工作（https://github.com/diku-dk/futhark/pull/2302），特别是逻辑重复被最小化。想法是使用无大小类型检查器推断“基础”类型（即不填充数组具体大小的类型），然后进行第二遍仅执行*大小推断*。 主要障碍（也是为什么直到现在才完成）源于与存在量词大小相关的棘手情况，即数组大小的存在量词必须插入在正确的位置。考虑一个带有大小提升类型变量的函数，如下： `` def apply 'a '^b (f: a -> b) (x: a) = f x `` 由于`^b`是大小提升的，它可以被实例化为包含存在量词的类型，在这种情况下意味着`f`可以是一个返回未知大小数组的函数。 如果我们说`apply iota`，那么无大小类型检查器将为`apply`推断出以下类型： `` (f: i64 -> []i64) -> (x: i64) -> []i64 = `` 当我们进行大小推断时，推断出以下带有存在量词（`?\[n\]`）的返回类型非常重要： `` (f: i64 -> ?[n].[n]i64) -> (x: i64) -> ?[m].[m]i64 `` 而不是让返回大小作为一个大小参数一直浮到顶层： `` (f: i64 -> [n]i64) -> (x: i64) -> [n]i64 `` 这个不正确的类型表明`f`返回的数组在调用`f`之前就已经知道，并且不依赖于其参数。这对于*某些*`f`是成立的，但当`f=iota`时不成立。 在旧的类型检查器中，这是通过在合一过程深处对灵活的大小提升类型变量进行一些巧妙（哦不……）的编程来实现的。由于无大小类型检查器现在已预先确定了所有基础类型，*永远不会*遇到灵活类型变量，所以我必须想出一个不同的解决方案。细节过于复杂无法在此详述，但最终是对该问题更显式的处理。仍然存在一些*丑陋*的部分，我认为我们从未为大小推断制定出好的理论，但这些部分现在感染的代码区域比以前小得多。我仍然有一个模糊的想法，也许将来应该基于双向类型检查（https://ncatlab.org/nlab/show/bidirectional+typechecking）而不是完全推断来重做所有大小检查，因为它实际上是一个依赖类型系统。 但那是以后的事。通过这项工作，Futhark 类型检查器现在每个函数经历四个阶段： 1. 解析名称。 2. 使用无大小类型检查器确定基础类型。 3. 执行大小推断。 4. 检查原地更新违规。 （如果我们最终完成 AUTOMAP，它将放在阶段 2 和 3 之间。） 这种设计的一个可爱特性是，如果在阶段*i*遇到错误，我们有来自阶段*i-1*的完整信息来帮助解释错误。这与原始的单遍类型检查器相比是一个很好的变化，在那种情况下，如果出现问题，我们通常*没有*关于尚未遍历的程序部分的信息。我猜想有一个一般原则：将类型系统设计为“分层”是个好主意，每一层都对前一层增加更多限制，这样即使程序在所有层上都不完全类型正确，其含义也能被理解。 我还发现将尽可能多的检查放在主类型检查之后运行的单独阶段中是有用的。例如，Futhark 对高阶函数有限制：你不能从分支或循环中返回它们。以前，我们会在相关的类型变量上装饰此类信息，这使核心推断算法变得复杂，有时还会导致难以理解的错误信息。现在，我们在类型推断之后遍历程序，寻找任何这样的禁止使用。如果发现，很容易找出原因：你告诉用户*这个*表达式不允许，以及*这是*我们为它推断出的类型。 这种方法的一个潜在缺点是效率——做四件事通常比做一件事更昂贵。此外，其中一些阶段在技术上会对函数进行超过一次遍历（特别是大小推断），以检查各种其他问题或更新 AST 装饰。 现在插一句关于编译效率的话。Futhark 从未被设计为快速编译。就个人而言，当我最初开始研究 Futhark 时，我受到诸如 Stalin（https://github.com/barak/stalin）和 MLton（http://www.mlton.org/）等项目的启发，它们以在极长编译时间下实现意想不到的高性能而闻名。我的愿望是让人们评价 Futhark“它确实能生成快速代码，只要你愿意等”。也许我甚至曾想以编译时间不切实际而自豪，就像 Stalin 那样，并且这肯定能作为该语言未被广泛使用的便利借口。（尽管 MLton 作为编译器来说很慢，但硬件的改进使其如今已经相当实用。）然而，自那以后 Futhark 不仅被（少数）其他人使用；我们也自己用它进行并行编程技术的研究（https://futhark-lang.org/blog/2026-06-18-data-parallel-pretty-printing.html）。当你能够从编译器那里得到相当及时的反馈时，做这件事会更有趣。因此，尽管 Futhark 类型检查器按大多数标准来说相当慢，但我们*确实*在一定程度上努力不使其比现在慢太多。 在我最初拆分类型检查器的工作中，我观察到在一个代表性程序（https://github.com/diku-dk/futhark-benchmarks/blob/master/finpar/LocVolCalib.fut）上`futhark check`出现了 20% 的减速，但我通过种种优化将其降低到了大约 -4%（即*加速*）。其中大部分是繁琐的技巧：在进行某项工作之前检查是否真的必要。我本可以也将这些优化添加到旧类型检查器中从而使其更快吗？是的，但我没有。我并不是想做出最快的类型检查器，只是不想让它变得更慢。（但如果有谁想写一个快速类型检查器，请尽管联系！我认为当前的设计使得独立地对组件进行基准测试相当容易。） 作为这项工作的一部分，我还让类型检查器准备好支持递归（尽管之前（https://futhark-lang.org/blog/2016-09-03-language-design.html）有过担忧（https://futhark-lang.org/blog/2026-01-20-why-not-tail-recursion.html）），目前由秘密环境变量`FUTHARK_ALLOW_RECURSION`控制，但那是另一天的故事了。