Elixir 1.20 的渐进类型系统 — 不写注解也能找到"已验证 bug"，实际是怎么回事

• 引言 — 耗时四年才完成的第一个里程碑
• dynamic() 和 any() 不一样的地方
• 1.20 实际新增了什么
• 把"13 个中通过 12 个"对照一手资料核对了一下
• 编译时间 — "最快"这个说法的实际分量
• 不是白拿的那部分
• 升级之前该知道的事
• 类型签名为什么还要再等一等
• 那么，现在该做什么
• 结语
• 参考资料

引言 — 耗时四年才完成的第一个里程碑

Elixir 团队宣布要把集合论类型(set-theoretic types)引入编译器，是在 2022 年。2023 年，Giuseppe Castagna、Guillaume Duboc、José Valim 在《The Design Principles of the Elixir Type System》中公布了设计原理，宣布项目"从研究走向开发"。到了 2026 年 6 月 3 日，Elixir v1.20 发布，这第一个里程碑就此完成。

这个里程碑可以这样概括 — 完全不引入任何类型注解，对所有 Elixir 程序执行类型推断和渐进式类型检查。 也就是说，即便你一行代码都不改，编译器也能帮你找出死代码和"已验证的 bug(verified bugs)"。这里的已验证 bug，按发布文自己的定义，指的是一旦执行就保证会在运行时失败的类型违规。

本文要剥掉炒作，看三件事：(1) 1.20 实际新增了什么，(2) 把发布文的数字对照一手资料后还剩下什么，(3) 文档里写了、但发布文里没提的权衡。Elixir 1.18 和 OTP 27/28 那个时代整体生态格局，已经在《Modern Elixir & Phoenix 2026》和《Modern Erlang and BEAM 2026》两篇里讲过了，这里只深挖类型系统本身。

dynamic() 和 any() 不一样的地方

按官方文档的说法，Elixir 类型系统的目标有三个 — 可靠性(sound)：推断出的、赋予的类型，要和程序的实际行为一致。渐进性(gradual)：存在 dynamic() 类型，去掉 dynamic() 之后就像一个静态类型系统。对开发者友好：用并集、交集、否定这些基本集合运算来描述类型(所以叫"集合论的")。

这里的核心是 dynamic()。很多渐进类型系统里的 any()，从类型系统的角度看意味着"什么都行"，所以它压根不会报告违规。Elixir 的 dynamic() 不一样。用发布文自己的话说，它有两个性质 — 兼容性(compatibility) 和 收窄(narrowing)。

先看兼容性。照搬发布文自己举的例子。

def percentage_or_error(value) when is_integer(value) do
  value_or_error =
    if value > 1 do
      value
    else
      "not well"
    end
  # ... more code ...
  if value > 1 do
    value_or_error / 100
  else
    String.upcase(value_or_error)
  end
end

value_or_error 要么是整数，要么是二进制串(binary)。/ 运算符只接受数值，String.upcase 只接受二进制串。要是换成一个严格的静态类型系统，这里会报出两处违规。可这段程序在运行时不会抛出任何异常。这是类型系统没能精确捕捉程序意图而产生的误报(false positive)。

Elixir 给这个变量打上 dynamic(integer() or binary()) 这个类型。把 dynamic() 类型的值传给函数时，Elixir 只在提供的类型与允许的类型互不相交(disjoint)时 才报违规。/ 虽然只接受数值，但 dynamic(integer() or binary()) 有可能是整数，两者并不互斥，所以不算违规。而如果把代码改成这样，

value_or_error =
  if value > 1 do
    value
  else
    "not well"
  end

Map.fetch!(value_or_error, :some_key)

Map.fetch! 期望的是一个 map，可这个值在运行时只可能是整数或二进制串。两者互不相交，所以是违规。这就是 Elixir 敢说自己"只报告已验证 bug"的依据。

不过，只报告已验证的 bug、却抓不到多少 bug 的话，那也没什么用。这就轮到收窄登场了。

def add_a_and_b(data) do
  data.a + data.b
end

data 一开始是 dynamic()，但因为看到 data.a、data.b 被用在加法里，就被收窄成 %{..., a: number(), b: number()}(前面的 ... 表示允许有其他键)。所以如果漏写了 .b，写成 data.a + data，data 已经先被收窄成了 map，接下来又要被当数值用，于是就违规了。

一句话概括 — Elixir 的 dynamic() 表现得像一个范围，随代码推进不断收窄，只有当类型检查越出这个范围时才报违规。 这和其他渐进类型系统用 dynamic 类型来丢弃类型信息的方向正好相反。

1.20 实际新增了什么

以CHANGELOG为准，看看 1.20 新增了哪些东西。

守卫推断(guard inference)。 这是本次发布最后补上的一块拼图。

def example(x, y) when is_list(x) and is_integer(y)
# x 是列表，y 是整数

def example({:ok, x} = y) when is_binary(x) or is_integer(x)
# x 是二进制串或整数，y 是以 :ok 开头的二元组

def example(x) when is_map_key(x, :foo)
# x 是带有 :foo 键的 map -> %{..., foo: dynamic()}

def example(x) when not is_map_key(x, :foo)
# x 是不带 :foo 键的 map -> %{..., foo: not_set()}
# 因此函数体里的 x.foo 是类型违规

def example(x) when tuple_size(x) < 3
# 元组最多 2 个元素 -> elem(x, 3) 是违规

否定(not is_map_key)被表示成一个叫 not_set() 的类型，这一点很有集合论类型系统的味道。对 map、列表的大小检查，会被转换成"是否为空"的检查。

函数体全体推断。 到 1.18 为止，只在模式(pattern)上做推断。现在会看函数体。

def sum_to_string(a, b) do
  Integer.to_string(a + b)
end

+ 既接受整数也接受浮点数，但因为结果被传进了一个要求整数的函数，所以 a、b 都被推断为整数。信息在反方向流动。

跨分支推断与 occurrence typing。 case、cond、with 加上了 occurrence typing，前面的分支会收窄后面的分支。

case System.get_env("SOME_VAR") do
  nil -> :not_found
  value -> {:ok, String.upcase(value)}
end

System.get_env/1 要么返回 nil，要么返回二进制串，而第一个分支已经拦住了 nil，所以 value 就只能是二进制串，String.upcase 也就无违规地通过了。附带效果是新增了冗余分支(redundant clauses) 的警告。

跨依赖推断。 这是 CHANGELOG 里 "Perform type inference across applications" 那一项。在 1.20-rc 之前，类型推断只发生在对标准库函数的调用上，调用你自己的依赖模块时，只做类型检查、不做推断。现在，从依赖里推断出的类型信息，会流入你自己应用的推断过程。这是一个让流经编译器的类型信息量大幅增加的改动，Elixir 团队在2026 年 1 月的路线图文章里说过，光是这一步就单独占用了一整个候选发布版本。

事实上，1.20 一共经过了七个候选发布版本(rc.0 到 rc.6)。rc.0 是 2026 年 1 月 9 日，rc.6 是 5 月 21 日，最终发布是 6 月 3 日。1 月的路线图文章当时预告的最终发布时间是"5 月"，所以晚了大约一个月，但对一次类型系统的全面落地来说，这个延期还算说得过去。

把"13 个中通过 12 个"对照一手资料核对了一下

发布文里最抓眼球的数字是这句：

our implementation performs well in the "If T: Benchmark for Type Narrowing" benchmark. Elixir passes 12 of the 13 categories

If-T 是一个真实存在的第三方基准测试，由 Hanwen Guo 和 Ben Greenman 创建(arXiv:2508.03830)，放在犹他大学 PLT 小组的 utahplt/ifT-benchmark 仓库里。它衡量的是类型收窄(occurrence typing)，每个主题都成对准备一个"应该通过类型检查的程序"和一个"不应该通过的程序"。类别正好是 13 个 — positive、negative、connectives、nesting_body、struct_fields、tuple_elements、tuple_length、alias、nesting_condition、merge_with_union、predicate_2way、predicate_1way、predicate_checked。

可发布文在这句话上挂的链接，指向的是仓库的Benchmark Results 表。打开那张表一看 — 根本没有 Elixir 这一列。

截至今天(2026-07-16)核实到的情况是这样。上游结果表涵盖的类型检查器有 Typed Racket、TypeScript、Flow、mypy、Pyright、Sorbet、Luau、MLsem、Typed Clojure、ty、Pyrefly，一共 11 个。仓库目录树(106 个条目)里的语言目录也只有这同样的 11 个，没有 Elixir 目录。在 README 全文里不区分大小写搜索"elixir"，结果是 0 条，无论开放还是关闭的 PR 里，也没有一个提议添加 Elixir。

所以准确地说是这样 — "13 个中通过 12 个"是 Elixir 团队自己测出来的数据，发布文链接的那张结果表并不能支撑这个数字。 这不代表它是错的。而是说，上游没有放出可复现的实现，第三方没法验证。到底是哪一类没通过，也从未公开过(搜索结果摘要里飘着一些指名道姓的说法，但在任何一手资料里都得不到确认，所以本文不引用)。

为了提供背景，把上游表的实际数字抄录在这里，有助于判断这个自测数据的位置。

上游 If-T 结果表(utahplt/ifT-benchmark, v1.1) — 按 13 个类别计
  Typed Clojure : 13/13  (全部通过)
  Typed Racket  : 12/13  (tuple_length 失败)
  MLsem         : 12/13  (connectives 失败)
  Flow          : 11/13
  Pyright       : 11/13
  TypeScript    : 10/13  (nesting_condition、predicate_1way、predicate_checked 失败)
  mypy          :  9/13

  Elixir        : 表里没有(发布文自测 12/13)

如果 12/13 属实，那就意味着和 Typed Racket 同一档次，还领先于 TypeScript。在完全没有注解的代码上做到这种收窄精度，确实算得上令人印象深刻的结果。不过就目前的状态而言，准确的说法应该带上这样的标签：这是作者自己测的，条件和失败项都没公开，也没法拿链接里的那张表来对照。

编译时间 — "最快"这个说法的实际分量

发布文还有另一个说法 — "在我们的合成基准里，Elixir 的构建工具如今是 BEAM 语言里最快的。"

依据是 José Valim 本人的仓库 josevalim/langcompilebench。这是作者自测的数据，仓库自己也说明这些是"合成基准(synthetic benchmarks)"。测量对象是100 个独立模块，各自编译 100 个 hello world 函数，启动应用，再跑一个最小测试套件所花的时间。测试条件是 MacStudio M1，取 5 次的平均值。

基于 Erlang/OTP 28
  Elixir v1.19                        ~0.73s
  Elixir v1.20                        ~0.63s
  Elixir v1.20 (interpreted defmodule) ~0.58s
  Erlang (rebar3)                     ~0.72s
  Gleam v1.14                         ~0.71s

基于 Erlang/OTP 29
  Elixir v1.19                            ~0.65s
  Elixir v1.20-rc.2                       ~0.55s
  Elixir v1.20-rc.2 (interpreted defmodule) ~0.50s
  Erlang (rebar3)                         ~0.64s
  Gleam v1.14                             ~0.67s

照字面读这些数字 — 从 1.19 到 1.20，0.73 秒变成了 0.63 秒，领先 Erlang 的 0.72 秒和 Gleam 的 0.71 秒。这是事实。但同样是事实的是，整个任务只有 0.7 秒左右，差距在 0.1 秒上下。而且这个工作负载就是一堆 hello world 函数，不是真实代码 — 压根就没有能把类型检查跑得吃重的代码。

最诚实的做法，是把作者本人留在仓库里的这段说明原样搬过来。

当然，这不代表同等规模的 Elixir 项目编译起来会比同等规模的 Gleam 或 Erlang 项目快，因为除了编译器本身的原始性能之外，还有更多变量在起作用。(…) 理论上说，rebar3 在这几个里应该表现最好。

换到增量编译，排名就完全反过来了。按同一个仓库自己的分析，关键在于能不能把模块间的依赖区分为编译时依赖和运行时依赖。Erlang(除了极少用到的 parse transform)只有运行时依赖，所以在这几个语言里，增量编译性能是最好的。 改一个文件，就只重新编译那一个文件。Gleam 把所有依赖都当成编译时依赖，所以最差。Elixir 介于两者之间。

langcompilebench 的汇总表
  语言     | 依赖类型                | 是否允许循环 | 每次改动预期的重新编译量
  Erlang   | 仅运行时                | 是           | 最低
  Elixir   | 运行时 + 编译时         | 是           | 中等
  Gleam    | 仅编译时                | 否           | 最高

也就是说，"最快"这个说法，仅限于干净构建的合成基准这个范围；而在开发过程中实际能感受到的增量构建上，同一个仓库自己的结论是 Erlang 领先。这是只读发布文会漏掉的背景信息。

不是白拿的那部分

这些是文档里写了、发布文里却没提的权衡。

dynamic 总是出现在根部。 按官方文档的说明，如果你写一个像 {:ok, dynamic()} 这样的元组，Elixir 会把它重写成 dynamic({:ok, term()})。文档明确指出的缺点是这个 — 没法只让元组、map、列表的一部分是 gradual 的，一旦沾上就整体变成 gradual。 作为交换，dynamic 总是显式地出现在根部，这被当作一个优点提出来 — 它能阻止 dynamic 悄悄渗透进一个静态类型的程序里。这是一个刻意的设计决定，但它确实是拿精度去交换的。

结构体更新在设计上就会产生违规。 这是文档自己举的例子。

user = find_user_by_id(42)
%User{user | name: "John Doe"}

即便 find_user_by_id 在运行时永远返回一个 User 结构体，只要类型系统没法静态证明这一点，就会报出类型违规。用文档自己的话说，"结构体更新就是被设计成这样工作的"。解决办法是在定义变量的同时做匹配。

%User{} = user = find_user_by_id(42)
%User{user | name: "John Doe"}

发布文里"误报率极低"的说法，是一个没有给出数字的厂商自评，这一点得和"还留着这种需要改代码的地方"放在一起看。

interpreted defmodule 是有代价的。 上面基准测试里跑出最快数字的 module_definition: :interpreted 选项，发布文里只提到了它的好处，但 CHANGELOG 里写了缺点。

• 编译期间出错时的堆栈跟踪，精确度可能会下降
• defmodule 内部的匿名函数，参数最多只能有 20 个(用 def 等定义的函数本身仍然支持到 255 个)

默认值是 :compiled，要开启的话，在 mix.exs 里加上 elixirc_options: [module_definition: :interpreted]。.beam 文件本身不会变 — 只是执行 defmodule 内部的方式变了。

升级之前该知道的事

OTP 要求。 1.20 要求 Erlang/OTP 27 及以上，并且与 OTP 29 兼容。如果你还被绑定在 OTP 26 或更低版本上，1.20 压根就不是一个选项。

安全补丁只存在于 1.20。 1.20.1(2026 年 6 月 9 日)修复了 CVE-2026-49762(GHSA-w2h8-8x3g-278p，严重程度 medium，由 Erlang Ecosystem Foundation 发布)。问题出在 Version 模块对整数的无限制解析上。版本字符串里的数字组成部分，被不加长度限制地转换成整数，一旦有一个全是数字、足够大的组成部分，就会触发超线性且不让步(non-yielding)的转换，占住一个 BEAM 调度器；再大一点，就会因为 SystemLimitError 而让进程崩溃。根据 OSV 记录，只需要一个大约 1 兆字节的字符串就够了，而且不需要任何身份验证。 可达路径是 Version.parse/1、Version.parse!/1、Version.match?/3、Version.compare/2、Version.parse_requirement/1，任何把 HTTP 参数或包元数据这类不可信输入传给这些函数的应用都会受影响。修复方式是把数字组成部分限制在 10 进制 14 字节以内。

这里有个重要的点 — 受影响范围是从 1.5.0 一直到 1.20.1 之前的全部版本。可查一下就会发现，2026 年 6 月 9 日之后发布的版本只有 1.20.1 和 1.20.2，根本不存在 v1.19.6 或 v1.18.5 这样的标签。也就是说，要拿到这个漏洞的补丁，除了升到 1.20.1 及以上，没有别的办法。 如果打算继续停留在 1.19 或更低版本，就得按 Elixir 团队的建议，自己限制传给 Version 模块的数据大小。

硬性弃用。 这些是 1.20 里真正开始报警告的项目。

• File.stream!(path, modes, lines_or_bytes) → 参数顺序改为 File.stream!(path, lines_or_bytes, modes)
• 在位模式(bit pattern)里匹配大小时需要用 pin 运算符：<<x::size(^existing_var)>>
• Kernel.ParallelCompiler.async/1 → Kernel.ParallelCompiler.pmap/2
• Logger.*_backend 系列函数 → 改用 handler 方式(想继续用 backend 的话，可以用 :logger_backends 包)
• Logger.enable/1、Logger.disable/1 → Logger.put_process_level/2、Logger.delete_process_level/1
• mix.exs 里的 xref: [exclude: ...] → elixirc_options: [no_warn_undefined: ...]

两处潜在的破坏性变更。 出于安全考虑，字符串、注释以及 ? 后面直接跟原始 CR 换行的写法被禁止了；require SomeModule 不再在编译时展开成该模块本身(在运行时返回模块这一点没变)。CHANGELOG 特意写下后面这一条，是因为像 require(SomeMod).some_macro() 这样的代码可能会被这个改动破坏。

类型签名为什么还要再等一等

最让人好奇的问题 — 什么时候能用编译器强制执行的类型签名，取代 @spec?

发布文给出了四个条件。类型签名只有在下面这些都满足之后才会被引入。

1. 团队对 1.20 的类型系统性能感到满意
2. 能高效实现递归类型(recursive types)
3. 能高效实现参数化类型(parametric types)
4. 能把 map 的键值对遍历高效实现为 enumerable — 发布文明确说明这一项目前仍在研究解法

也就是说，剩下的不只是工程问题，还有尚未解决的研究课题。1 月的路线图文章说，这些问题会在 v1.21(2026 年 11 月)和 v1.22(2027 年 5 月)里去探索，同时自己列出了两个可能让类型系统被证明不实用的风险 — 人体工学(ergonomics)(到目前为止的所有改进，都是在不改动语言本身的前提下在幕后发生的，对开发者体验的影响还没被评估过)和性能(performance)(目前的实现不支持递归类型和参数化类型，而这两者有可能直接冲击性能)。

剩下的里程碑顺序是这样的。第二个是带类型的结构体(typed structs) — 原生定义结构体字段的类型，并让它在整个代码库里传播开来。第三个是集合论类型签名。

这里还有一条安静但分量不小的消息。官方文档明确写道 — 现有的 Erlang Typespec，精度不足以用在集合论类型上，等这个阶段结束，它就会从语言里逐步被淘汰(phased out)，后处理工作会被移到一个独立的库里。 如果你的代码库一直在认真使用 @spec，那就意味着迁移迟早会来。具体时间还没定。

那么，现在该做什么

可以放心升级的情况。 如果你在 OTP 27+ 上，而且上面那份弃用清单是你能承受的范围，升级的理由就很充分。类型检查不是可选项，它就是直接开着的，你不用改代码。得到的东西几乎是白拿的。而且因为 Version 的 CVE 补丁只存在于 1.20.1 及以上，如果你的应用会把外部输入传给 Version 模块，升级实际上就是一个安全问题。

不用着急的情况。 如果你是为了用类型签名而在等，1.20 不是那个版本。至少要等到 v1.21(2026 年 11 月)，现实一点说还要更晚，要是研究课题解决不了，还可能继续往后拖。带类型的结构体也还没到。如果你还被绑定在 OTP 26 或更低版本，那压根升不了。

调整预期。 1.20 能帮你找到的，是"一旦执行就必定崩溃"的违规和死代码。它并不能证明你的类型是对的。既然没有注解，编译器知道的就只有能从代码里推断出来的东西，含糊的地方会一直留在 dynamic() 里，只有互不相交时才会被抓出来。用过 Dialyzer 的人对这个位置应该不陌生，区别在于 Elixir 1.20 是内置在编译器里的，不需要单独运行，也不需要构建 PLT。

升级之后如果警告大量冒出来，多半是真 bug 的可能性很大。发布文最后一句话说的就是这个意思 — "去试试 Elixir v1.20，别忘了把它白送给你的那些 bug 都修一修。"

结语

归纳一下就是这样。Elixir 1.20 确实完成了始于 2022 年的类型系统工作的第一个里程碑，而且是真的 — 不用注解就能对所有程序做渐进式类型检查，dynamic() 不是丢弃类型信息，而是像范围一样随代码收窄，推断能跨越守卫、函数体、分支、依赖流动。代价基本上就只是升级本身。

与此同时，发布文里的两个数字，对照一手资料之后，分量都变小了。If-T 的"13 个里通过 12 个"，是一份自测数据，链接的上游表里连 Elixir 这一列都没有；编译速度第一的说法，来自作者本人的 hello world 合成基准，在一次 0.7 秒的任务里差了大约 0.1 秒，而到了增量构建上，同一个仓库自己把 Erlang 排在了前面。这两个说法都不是假的，但都比只读发布文得到的印象要小。

而真正让人想要的东西 — 类型签名和带类型的结构体 — 还要再等一年多，而且排在 Elixir 团队自己写下的"有可能被证明不实用"的未解决研究课题后面。这份坦诚，也是这个项目坚持了四年依然能保住信任的原因之一。

参考资料

• Elixir v1.20 released: now a gradually typed language (2026-06-03, José Valim)
• Elixir v1.20 CHANGELOG(一手资料)
• Type inference of all constructs and the next 15 months (2026-01-09) — 路线图与 RC 时间表
• Gradual set-theoretic types — 官方文档(v1.20.2)
• The Design Principles of the Elixir Type System — Castagna, Duboc, Valim (Programming journal, 2024, Vol. 8, Issue 2, Article 4)
• If-T: A Benchmark for Type Narrowing — Guo, Greenman (arXiv:2508.03830)
• utahplt/ifT-benchmark — 上游基准与结果表
• josevalim/langcompilebench — BEAM 语言编译时间合成基准
• CVE-2026-49762 / GHSA-w2h8-8x3g-278p — Version 模块的无限制整数解析
• 《Modern Elixir & Phoenix 2026》— 生态格局(相关文章)
• 《Modern Erlang and BEAM 2026》— OTP 与运行时(相关文章)