2022 年，我们宣布了为 Elixir 添加集合论类型（set-theoretic types）的计划。2023 年 6 月，我们发表了一篇关于 Elixir 类型系统设计的获奖论文，并说明我们的工作已从研究阶段过渡到开发阶段。
随着 Elixir v1.20 的发布，我们完成了第一个开发里程碑：在不引入类型注解的情况下，对每一个 Elixir 程序执行类型推断并渐进地进行类型检查。这意味着 Elixir 能够越来越多地报告死代码和已证实的错误（verified bugs）——即那些如果执行就必然会在运行时失败的类型违反。Elixir 能够高效地发现现有程序中的已证实错误，无需开发者额外负担，并且误报率极低。
在这篇公告中，我们将解析类型系统的目标、dynamic() 类型在 Elixir 中的含义，以及它如何发现已证实的错误。特别地，我们的实现在 "If T: 类型缩小基准测试"中表现良好。Elixir 通过了 13 个类别中的 12 个，表明它能够从普通的 Elixir 代码中恢复精确的类型信息，并利用这些信息在动态类型程序中找出已证实的错误。
该类型系统的实现得益于 CNRS 与 Remote 的合作。开发工作目前由 Fresha 和 Tidewave 赞助。
类型，在我的 Elixir 里？
我们的目标是引入一个类型系统，它具有以下特性：
健全（sound）——类型系统推断和分配的类型与程序的行为保持一致。
渐进（gradual）——Elixir 的类型系统包含 dynamic() 类型，当变量或表达式的类型在运行时被检查时可以使用此类型。在没有 dynamic() 的情况下，Elixir 的类型系统表现为静态类型系统。
对开发者友好——类型通过基本的集合运算（并集、交集、补集）来描述、实现和组合（因此这是一个集合论类型系统），并附带清晰的错误信息。
在现有语言中引入类型系统是一项复杂的变更。因此，我们的第一个里程碑是在不引入类型注解的情况下实现类型系统，但仍然通过发现死代码和已证实的错误来为开发者提供价值。这是通过 dynamic() 类型实现的——在 Elixir 中，它与其他渐进类型语言中的对应类型截然不同。我们来详细解析一下。
dynamic() 类型
许多渐进类型系统都有 any() 类型，从类型系统的角度来看，它通常意味着"什么都行"，因此不报告任何类型违反。而 Elixir 的渐进类型被称为 dynamic()，它具有两个重要特性：兼容性（compatibility）和缩小（narrowing）。
在静态类型系统中，当你有一个形如 integer() or binary() 的类型并调用某个函数时，该函数必须接受这两种类型。然而，由于类型系统无法精确捕捉所有程序的意图，这可能导致误报。例如，考虑下面这段简单的代码：
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 的类型是 integer() or binary()，操作符 / 只接受数字，而 String.upcase 只接受二进制/字符串，但上面的程序是有效的，并且在运行时不会抛出异常。然而，类型系统仍然会报告两个违反，因为传递给 / 和 String.upcase 的类型不是所接受类型的子类型。
虽然上述程序可以通过更好的编写方式消除类型违反，但类型系统总会拒绝一些有效的程序。如果 Elixir 在现有代码库中引入太多误报，就会迅速侵蚀对类型系统的信任。因此，Elixir 的渐进类型系统会将上面的 value_or_error 变量标记为类型 dynamic(integer() or binary())，这意味着该类型在运行时要么是 integer() 要么是 binary()。
当使用 dynamic() 类型调用函数时，Elixir 只有在提供的类型与接受的类型不相交（disjoint）时才会发出类型违反。在上面的程序中，尽管 / 只期望数字，但 dynamic(integer() or binary()) 可以是 integer()，由于接受类型与提供类型不相交，因此没有类型违反。然而，如果我们把程序改成这样：
value_or_error =
if value > 1 do
value
else
"not well"
end
Map.fetch!(value_or_error, :some_key)
因为 Map.fetch! 期望一个映射（map）数据结构，而 value_or_error 在运行时只能是整数或二进制，所以接受类型与提供类型不相交，这就变成了一个违反。这就是兼容性属性，它解释了 Elixir 如何只报告已证实的错误。
然而，如果我们根本找不到很多错误，只报告已证实的错误也没什么用。我们通过确保 Elixir 的动态类型可以被缩小来解决这个问题。看看这段代码：
def add_a_and_b(data) do
data.a + data.b
end
在上面的程序中，data 初始为 dynamic() 类型。然后我们在加法运算符中使用 data.a 和 data.b，因此 Elixir 会将 data 变量精炼为类型 %{..., a: number(), b: number()}，这意味着它是一个映射，同时具有 a 和 b 字段，且值均为数字（并且可能还有其他任何字段，因此有开头的 ...）。因此，如果你忘记选择 .b 字段而写了下面这样：
def add_a_and_b(data) do
data.a + data
end
data 会先被缩小为形如 %{..., a: number()} 的映射，然后被尝试用作 number()，这就会发出一个违反。
换句话说，Elixir 中的 dynamic() 类型实际上像一个范围（range）一样工作，它可以在程序使用过程中被精炼，一旦类型检查超出范围就会报告违反。这与其他渐进类型系统形成了对比，后者使用动态类型丢弃所有类型信息。
在幕后，我们的类型推断和类型检查算法表现得就像我们将所有参数类型都注解为 dynamic() 一样。一旦我们引入用户提供的类型注解，只要不使用 dynamic()，Elixir 的类型系统就会像任何静态类型语言一样工作。而当你跨越静态-动态边界时，我们开发了新的技术，确保我们的渐进类型是健全的，无需额外的运行时检查。
守卫、子句等的类型检查
此版本背后的大部分工作是引入对多种结构的类型检查和缩小。我们来看一些例子。
在守卫方面，我们可以推断并集、交集和补集：
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 键的映射，表示为 %{..., foo: dynamic()}。注意开头的 ... 表示映射可能还有其他键。
def example(x) when not is_map_key(x, :foo)
上面的代码推断出 x 是一个不包含 :foo 键的映射，其类型为 %{..., foo: not_set()}。因此，在函数体内使用 x.foo 会引发一个类型违反。
你还可以使用对数据结构大小进行断言的表达式：
def example(x) when tuple_size(x) < 3
Elixir 会正确地跟踪该元组最多有两个元素，因此访问 elem(x, 3) 会发出一个类型违反。对于映射和列表，我们将大小检查转换为空性检查。换句话说，Elixir 可以查看复杂的守卫，推断类型，并利用这些信息在代码中发现错误。
对于 case 和条件语句等结构，Elixir 会利用前一个子句的信息来精炼后续子句：
case System.get_env("SOME_VAR") do
nil -> :not_found
value -> {:ok, String.upcase(value)}
end
System.get_env("SOME_VAR") 返回 nil 或 binary()。由于第一个子句匹配 nil，类型系统知道 value 不再可能是 nil，因此它必须只是 binary()，这使得第二个子句也能通过类型检查而不发生违反。跨子句的缩小还帮助类型系统在现有代码库中发现冗余子句和死代码。
此外，我们对标准库中许多处理元组和映射的函数进行了类型化。更多详情请参阅 发布说明。
编译时间改进
Elixir v1.20 再次提升了编译时间，尤其是在具有多个核心的机器上运行的应用中。尽管 BEAM 语言的编译总体上已经很高效，但我们的合成基准测试现在将 Elixir 的构建工具列为其中最快的。如果你想贡献更多示例和场景，请开启讨论，以便我们提供透明的基准测试套件和结果。
它还引入了一个名为 :module_definition 的新编译器选项，用于指定模块定义是 :compiled（默认值）还是 :interpreted。这可能会改善大型项目的编译时间，并且不会影响写入磁盘的 .beam 文件，只会影响 defmodule 内部内容的执行方式。你可以在 mix.exs 中设置 elixirc_options: [module_definition: :interpreted] 来启用它。阅读文档以了解更多信息。
下一步是什么？
我们面临的最大问题是：Elixir 何时会引入利用集合论类型的新类型签名？正如我最近在 ElixirConf EU 2026 主题演讲中所讨论的，我们面前仍有研究工作和开发工作。我们只会在以下条件满足时引入类型签名：
我们对 Elixir v1.20 中类型系统的性能感到满意（我们已经做了大量 优化 工作）；
我们能够高效地实现递归类型；
我们能够高效地实现参数化类型；
我们能够高效地实现将映射的键值对作为可枚举类型进行遍历（我们仍在研究可行的解决方案）。
一旦这些问题得到解决，我们将开始探索和讨论类型化的结构体定义，并最终讨论类型签名。像往常一样，我们会通过新闻和 Elixir 论坛让社区了解最新进展。
我们感谢所有尝试发布候选版本、运行基准测试并向我们提供反馈的人！试试 Elixir v1.20 吧，别忘了修复它能免费发现的所有错误！
