Gleam 的 case 穷尽性检查——一位粉丝的深入探索

# 一个粉丝眼中的 Gleam case 穷尽性检查 Source: https://oyster.pckt.blog/gleam-case-exhaustiveness-as-a-fan-fd4whyp 抉择，抉择。就在写下这段文字的同时，我脑子里还在同时权衡着好几层嵌套的决定，不过都是为了接下来10分钟怎么过日子。我算得上幸运，因为摆在我面前的这些选择，都是为了让自己更舒适一些——每一件看似琐碎，却都牵扯着复杂的连锁反应。天开始放晴了；我要不要伸手从包里掏出帽子戴上？如果戴，要不要顺便也拿出本子画点什么？如果要画，面对眼前这座美丽城市的无限可能，我该画点什么？而我选择了写这篇文章——与此同时冒着晒伤的风险，也让这个世界少了一幅涂鸦。 计算机的首要职责之一就是做决定，而我们今天的话题，正是追踪编译器在判断一个程序想要处理的每种选择是否都已覆盖时所能采取的步骤。Gleam 的编译器是一件精美而庞大的工程杰作，我想带大家在 Gleam City 的一条小巷里散散步：它关于 case 穷尽性检查的逻辑。 在一门名为 [Gleam](https://gleam.run/) 的编程语言中，我们可以使用 [case 表达式](https://tour.gleam.run/flow-control/case-expressions)。在这个语言子集中，`compiler-core/src/exhaustiveness.rs` 的职责是确保 `case` 中出现的每一个模式都能覆盖 subject（被匹配值）可能取到的每一个值，反过来，也检查是否存在某个分支因为前面的分支已经匹配了同样的情况而永远不会被执行到。在 Gleam 程序编译时就替我们把这一切都解决了，而不是等到程序运行时因为某个未处理的值直接崩溃——这用户体验真是太棒了！ ```gleam pub fn to_string(is_cool: Bool) -> String { case is_cool { True -> "cool" False -> "uncool" } } ``` 如果你删掉 `False` 分支，这段代码就不会编译通过——这是既定事实。而对我来说，`exhaustiveness.rs` 中最特别的地方在于：它会尽力告诉用户究竟缺了*哪一个*分支，如果它能做到的话。它会礼貌地通知我：`"The missing patterns are: False"`。提供这样的提示信息绝非易事，这充分体现了 Gleam 对用户友好性的执着追求。 虽然带类型的函数式编程语言自上世纪70年代起便如杂草般野蛮生长，但与我们讨论的这个文件相关的理论（至少对我而言）要追溯到大约1984-85年，源自 [Lennart Augustsson](https://en.wikipedia.org/wiki/Lennart_Augustsson) 关于模式匹配编译的论文，标题为 [《Compiling Pattern Matching》](https://www.cs.tufts.edu/~nr/cs257/archive/lennart-augustsson/patmatch.djvu)。 > 题外话：如果你读了那篇论文，也许你会像我一样好奇，Augustsson 先生是不是把 "matching" 拼成了 "mathing"，因为这个错误出现了好几次。毕竟，这确实是一个相当"mathy"（数学味十足）的话题。我想这里面肯定藏着某个关于我们大脑模式匹配的笑话。 Augustsson 提出了一个我认为是后续工作的基石的框架：首先按 case 表达式中每个分支的**首层构造器**对分支进行分组，然后为子部分引入新的变量，接着对这些子部分重复此过程！这是一篇精彩的读物，不过略显晦涩。论文的后半部分详细介绍了如何将这些子部分转化为实际的 [LML](https://foldoc.org/LML) 指令，例如当某个子部分匹配不上任何东西时，在嵌套的 case 迷宫中为默认分支生成字面跳转（GOTO？）。换句话说，每次落入默认分支都会强制重试，直到运行时抵达最顶层的默认分支（即匹配失败）——这才算把整个嵌套结构递归完。 > 题外话：用自己的 ML 方言是一件巨大的炫技…… 当我观察 Gleam 的 `Decision::Switch` 的行为时，我能感受到 Augustsson 那"子部分匹配不上任何东西就跳转"的幽灵般的存在。与古老的历史不同，Gleam 是编译型的，因此 `Switch` 的默认分支是一个实际静态类型数据结构中的节点（而非运行时规则）。他们还将 Augustsson 的跳转原本承担的两个职责拆分开了：`Switch`（继续重试，在嵌套结构中其他地方继续匹配）和 `Decision::Fail` 作为一种类型，而非在所有选项都用完时隐式发生。最精彩的组合拳是：在整棵决策树构建完成后，在*编译期*就找到一个 `Fail`，这证明了我们最初的 case 表达式是不穷尽的。精确地知道 `Fail` 发生在哪里，就引导我们来到 `missing_patterns.rs`——它沿着决策树反向回溯，找到那个永远不会匹配的具体场景，从而将其呈现给用户。站在巨人的肩膀上——这个关于运行时断言以发现哪些跳转最终会失败的概念！ 那个永远不会匹配的具体场景，年轻人称之为"见证"（witness），而 [Luc Maranget](https://pauillac.inria.fr/~maranget/)（点击链接，做好被猫吓一跳的准备）在他2007年的论文 [《Warnings for pattern matching》](http://moscova.inria.fr/~maranget/papers/warn/warn.pdf) 中称之为"反例"（counter-example）。我们稍后再回来谈 witness。 > "程序员在面对'非穷尽匹配'警告时，有时会相当恼火。提供一个'未匹配值'的例子，不仅有助于说服他们自己确实写了非穷尽匹配，还能帮助他们修正代码。" —— Luc Maranget，2007 据我以一种天真的函数式编程人类学家的角色进行田野调查所得出的结论，1990年代是函数式编程的黄金时代：Augustsson 的 LML 后来成为了 [Haskell HBC](https://github.com/haskell-implementations/hbc) 的一部分；我们见证了 [Clean](https://en.wikipedia.org/wiki/Clean_%28programming_language%29)（95年）、[OCaml](https://ocaml.org/)（96年）、[Erlang](https://www.erlang.org/)（98年开源）等语言的诞生。在我看来，到了21世纪之交，关于 case 表达式树规模方面的研究似乎已经到顶了（这一点我有意没有深入展开），研究焦点转向了如何让诊断信息更易用，以及如何让我们能匹配的模式更加丰富。由此引出了 Maranget 的论文！他提出的寻找 witness 的方法如下（抱歉又跑了趟题，但这实在太有意思了）： 1. 构建一个矩阵，其中 subject 为列，case 分支的模式为行。 2. 聚焦于某一列。（我说"某一列"而非"第一列"，因为我们天然地会递归进行，先在脑中把这个设定好。） 3. 这一列中的构造器是否覆盖了该类型的所有可能？ - 如果没有，那就是缺了一个构造器！带着缺失的构造器进入步骤4。（不过，像数字和字符串这种老式类型的构造器太多了，多到不可能一一列出，所以对于这类类型我们需要一个"其他所有情况"的分支。想象一个字符串的 case 表达式长这样 `{"a" -> "my answer 1", "aa" -> "my answer 2", .. 无穷无尽}`。） - 如果覆盖了，那至少是好的！对每一个构造器执行步骤4。 - 如果这一列完全为空，跳过这一列，回到步骤2处理下一列。 4. 针对某个给定的构造器，"打进去"一层——对其进行特化（specialize），进入其中。`MyType(r), rest...` 变为 `r, rest...`。我们实际上已经进入了一个新的矩阵！ 5. - 如果这个内部矩阵已经没有行了：我们暂定找到了一个 witness，存下来然后继续。（……对其他需要执行步骤4的构造器同样处理。） - 如果这个内部矩阵有行但没有列，那就完成了！ - 其他情况：回到步骤2。 6. 重复！（持火把的人请放下叉叉——每次迭代实际上都会消耗某些东西，模式*一定会*用完的。）如果我们最终留下了 witness，瞧，这就是我们的缺失模式。如果没有 witness，那这个 case 就结案了。（明白了吧？） "这过山车可真够刺激的。Gleam 是怎么实现这个矩阵的呢？"读者好奇地问道。首先，我得说——你这股拿着棒棒糖、戴着旋转帽的元气劲儿真不错；其次，妙就妙在：Gleam 并没有用矩阵！相反，Gleam 将 case 分支表示为一个分支列表（branch list），每个分支本身又是一个检查列表，每个检查字面上就是 `[变量] is [模式]`，这种风格类似于 [Jules Jacobs 的笔记](https://julesjacobs.com/notes/patternmatching/patternmatching.pdf)和 [Yorick Peterse 的实现](https://github.com/yorickpeterse/pattern-matching-in-rust)。 说到树的构建和 Maranget，他的另一篇论文与我们的主题更加相关，事实上它在今天的 Gleam 代码中被引用了（两次！）。[《Compiling Pattern Matching to good Decision Trees》](https://www.cs.tufts.edu/~nr/cs257/archive/luc-maranget/jun08.pdf)（Maranget，2008，比刚讨论的那篇晚一年）处理的是，你猜到了——如何以保证编译后决策树性能不低于 [OCaml 的回溯编译器](http://moscova.inria.fr/~maranget/papers/opt-pat.ps.gz)（这不就是 Augustsson 那个嵌套跳跃式 case 迷宫吗？）的方式来*编译*决策树。回溯的优势："代码规模有线性保证"。回溯的劣势："可能会多次扫描子项"。Maranget 展示了我们可以通过明智地选择分支构建为树的顺序来降低树的深度。 尽量优先选择以下列： - 首行是构造器模式的列（之所以说"模式"而非仅仅是"构造器"，是因为不光是 `True` 或 `Circle` 这种简单类型，还包括 `Ok(x)` 和 `Ok(False)` 等） - 该列中通配符（wildcard）最少的列。 - 我们即将创建的开关节点（switch-node）上子节点数最少的列。 - 结构体字段数最少的列。 - 该列需要测试的最大行数最少的列。既然迟早要测试，不如早点搞定。 - 在分支列表中越早需要用到该列的。 - 该列中的模式越晚才退化为非构造器形式的列。 最后一种列优选方法在实践中的做法是：对于给定的列，逐个单元格向下看。每个单元格要么有一个构造器（比如 `[]` 或 `[x, ..rest]`），要么该单元格并不特别关心（即 `_, r`）。我们会数到第一个"不关心"的出现位置，然后按计数对各列排序，以此来构建决策树！ 虽然 Gleam 不是以表格形式构建决策逻辑，而是构建整棵决策树（在我看来，用矩阵的方式其实也能行，但这样做我们可以免费获得诊断信息*以及*为 JavaScript 后端打下的基础），至于下一步该测试哪一个的引擎，似乎是 Maranget 和 Jacobs 两种策略的结合：选择构造器数量最少的变量的类型（比如列表有2种，int 有无穷种），如果平局，则选择被剩余检查引用次数最多的变量。明智的选择能确保决策树更小，因为如果不这样做，像下面这样： ```gleam case a, b { Some(x), 1 -> "one" None, 2 -> "two" _, _ -> "buckle my shoe" } ``` 的自然结果是，最后一个分支会被复制很多次，就像这样： （假设我们先按 `a` 来分裂决策树） ``` - Some: 分支 1，加上分支 3 的一个副本 - None: 分支 2，加上分支 3 的一个副本 ``` 然后 ``` - Some: - b 为 1: 分支 1，分支 3 的副本 - b 为其他: 分支 3 的副本 - None: - b 为 2: 分支 2，分支 3 的副本 - b 为其他: 分支 3 的副本 ``` 于是我们的"buckle my shoe"分支就有了4个副本，尽管其中一些副本事后本来就是无用的——比如当 `a` 和 `b` 为 `Some, 1` 时，分支 1 已经匹配了，所以我们可以确定分支 3 的那个副本永远不会被触发。决策树越小，就越容易遍历并找到一个在编译期就可见的死胡同，它不仅证明了*存在*未处理的模式，还能通过向上回溯到树干来找出我们究竟缺了哪个具体的模式。 我在阅读 `exhaustiveness.rs` 时觉得最有趣的部分，是那些我在任何论文中都找不到的功能（注意我并不是在断言这些内容绝对不在任何论文中，只是给自己留个余地，以防是我的搜索技能不够好）。让我们来看几个这样的例子： ```gleam case s { "lewis" <> rest -> ... } ``` 这引入了一整类全新的情况，因为字符串可以是其他字符串的子集！我们习惯了 case 表达式中某个条件为真的处理方式，对吧？在此之上，我们还有[内联守卫](https://tour.gleam.run/flow-control/guards)，这让树的构建变得相当困难： ```gleam case s { "lewis" <> rest if rest == " likes" -> "lewis likes gleam" "lew" <> rest -> "lew-" <> rest _ -> "idk" } ``` 在这种情况下，当我们把这棵决策树遍历到某个位置后，无法回头重新尝试： - `s` 是不是以 "lewis" 开头？ - 是的 - 分支 1：守卫为 true："lewis likes gleam" - 守卫为 false：*糟糕了！* - 不是 - `s` 是不是以 "lew" 开头？ - 是：分支 2 - 不：分支 3 注意那个"糟糕了"。我们*仍然必须*尝试分支 2，因为我们知道 "lew" 是 "lewis" 的子集。"你怎么知道的？"你问。Gleam 的做法是：在同一层级上遍历时，记住它已经见过的字符串前缀，这样它就可以将任意一个更短的前缀添加到每个更长前缀的"糟糕了"区域中，让我们在已经深入遍历之后仍能对其进行测试。 - `s` 是不是以 "lewis" 开头？ - 是的 - 分支 1：守卫为 true："lewis likes gleam" - 守卫为 false：*把分支 2 复制到这里！现在我们就可以检查它了。* - 不是 - `s` 是不是以 "lew" 开头？ - 是：分支 2 - 不：分支 3 作为参考，请在 `compiler-core/src/exhaustiveness.rs` 中查看 `overlap_candidates` 和 `descendant_candidates`。当我翻阅提交历史时，可以说这个字符串前缀的新颖做法经过了反复打磨才达到如今的良好状态，我敢打赌在它完全定稿之前，这里还有更多值得探索的地方。如果我错了——事实上确实存在某篇论文涵盖了基于守卫和前缀/子集的匹配——请告诉我！不过这丝毫不影响这个功能的酷炫程度。 位数组（bit array）逻辑：虽然[《Efficient Manipulation of Binary Data》](https://user.it.uu.se/~kostis/Papers/JFP_06.pdf)处理了具有可变段大小的位数组匹配，但 Gleam 似乎在与其他类型的穷尽性检查的配合下又推进了几步。编译器会检查某个模式是否不可能被匹配，并在遍历过程中记住某个测试是否已经执行过。它还会决定是否需要生成代码来统一/调和 JavaScript 和 BEAM 的行为差异——例如，如果它检测到给定的位数组长度变量*可能是负数*（准确地说，是它无法确保它*绝不可能*为负数），就会发出直接跳过而非 `raise` 的代码，同样地，它也知道 `NaN` / `Infinity` 实际上不会匹配到浮点段。 类型收窄（Type-narrowing）：以此为例： ```gleam pub fn area(s: Shape) -> Float { let shape = Circle(67.0) case shape { Circle(r) -> 3.14 *. r *. r } } ``` 我们的编译器会因为缺少了 Shape 可能拥有的其他所有形状而报错吗？Square、Rhombus，这些只是我强大的大脑能想到的几种形状。（掌声。）Gleam 的编译器记住了名为 `shape` 的 Shape 的具体实例化，确切地知道它永远只可能是 Circle，所以对这个表达式很满意。不仅如此，如果我们*确实*在这里处理了 Square 之类的分支，它还会恰当地提醒我们添加了一个死分支。这也适用于这样的场景： ```gleam pub fn describe(s: Shape) -> String { case s { Circle(r) -> { case s { Circle(_) -> "round and awesome" } } Square(side) -> "four sides and boring" // ... 我的其他形状 } } ``` 内层对 `s` 的 case 不会因为没有处理 Square 的情况而产生警告。是不是很妙！编译器似乎充分利用了……