Elixir v1.20 发布：引入渐进式类型系统，从动态语言迈向静态检查

背景

Elixir 长期以来以其动态特性和灵活性著称，但在大型项目中，缺乏静态类型检查往往导致运行时错误难以追踪。早在 2022 年，Elixir 核心团队便宣布了一项旨在为 Elixir 添加集合论类型（set-theoretic types）的重大努力。2023 年 6 月，团队发表了一篇获奖论文，详细阐述了 Elixir 类型系统的设计，并指出相关工作已从理论研究阶段正式转入开发阶段。

随着 Elixir v1.20 的发布，这一进程迎来了第一个重要的开发里程碑。该版本实现了在不引入显式类型注解的情况下，对每个 Elixir 程序进行类型推断和渐进式类型检查。这一举措标志着 Elixir 开始能够自动识别死代码（dead code）和经过验证的 bug（verified bugs），即那些如果执行必然会在运行时失败的类型违规。

此次发布得益于 CNRS 与 Remote 的合作，开发工作目前由 Fresha 和 Tidewave 赞助。

核心内容

Elixir v1.20 的核心在于引入了一套全新的类型系统，其设计目标、dynamic() 类型的独特性以及具体的类型推断机制如下：

类型系统的三大目标

Elixir 团队致力于构建一个具备以下特性的类型系统：

1. 健全性（Sound）：类型系统推断和分配的类型必须与程序的实际行为保持一致。
2. 渐进性（Gradual）：系统包含 dynamic() 类型，用于在运行时检查变量或表达式的类型。在没有使用 dynamic() 的情况下，Elixir 的类型系统表现得如同静态类型系统。
3. 开发者友好（Developer Friendly）：类型通过基本的集合运算（并集、交集和否定）进行描述、实现和组合，即“集合论类型系统”，并提供清晰的错误信息。

第一里程碑：无注解的价值

引入类型系统是一项复杂的工程。因此，v1.20 的首要里程碑是在不引入类型注解的前提下，通过类型系统为开发者提供价值。具体表现为自动发现死代码和经过验证的 bug。这通过 dynamic() 类型实现，其机制与其他渐进式类型语言截然不同。

dynamic() 类型的独特性：兼容性与收窄

许多渐进式类型系统使用 any() 类型，这在类型系统视角下往往意味着“无所不包”，通常不会报告类型违规。而 Elixir 的 dynamic() 类型具有两个关键属性：兼容性（Compatibility）和收窄（Narrowing）。

1. 兼容性：避免误报

在静态类型系统中，如果函数接受 integer() 或 binary()，调用时必须严格匹配。但这可能导致误报（False Positives）。

例如，以下代码在运行时是有效的：

def percentage_or_error(value) when is_integer(value) do
  value_or_error =
    if value > 1 do
      value
    else
      "not well"
    end
  
  # ... 更多代码 ...
  
  if value > 1 do
    value_or_error / 100  # 期望数字
  else
    String.upcase(value_or_error) # 期望字符串
  end
end

虽然 value_or_error 的类型是 integer() or binary()，且 / 运算符只接受数字，String.upcase 只接受二进制/字符串，但程序逻辑保证了在 / 调用时 value_or_error 必为整数，在 String.upcase 调用时必为字符串。

如果采用严格的静态检查，这会报告两个类型违规。为了保持对现有代码库的信任，Elixir 将 value_or_error 标记为 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 结构，而 value_or_error 运行时只能是整数或二进制，两者类型不相交，从而触发违规。这就是 Elixir 如何仅报告“经过验证的 bug”。

2. 收窄：提升检测能力

仅报告验证过的 bug 还不够，系统必须能发现足够多的 bug。Elixir 通过类型收窄（Type Narrowing）解决此问题。

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

在此代码中，data 初始类型为 dynamic()。当使用 data.a 和 data.b 时，Elixir 会将 data 细化（refine）为类型 %{..., a: number(), b: number()}，暗示它是一个包含 a 和 b 字段且值为数字的 Map。

如果开发者错误地写成：

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

data 首先被细化为 %{..., a: number()}，随后尝试将其作为 number() 使用，这将触发违规。

简而言之，Elixir 中的 dynamic() 类型有效工作像一个范围（Range）。随着程序的使用，该范围会被不断细化；一旦类型检查超出该范围，就会报告违规。这与那些使用 dynamic 丢弃所有类型信息的其他渐进式类型系统形成鲜明对比。

底层机制

在幕后，类型推断和检查算法表现得如同将所有参数类型标注为 dynamic()。一旦引入用户提供的类型注解，只要不使用 dynamic()，Elixir 的类型系统将表现得像任何静态类型语言。团队开发了新技术，确保在跨越静态-动态边界时，渐进式类型保持健全性，而无需额外的运行时检查。

类型守卫、子句及其他构造

v1.20 的很大一部分工作是将类型检查和收窄引入到多个语言构造中：

• 守卫（Guards）：可以推断并集、交集和否定。
  • 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：Elixir 会正确跟踪元组最多有两个元素，因此访问 elem(x, 3) 将触发违规。对于 Map 和 List，大小检查被转换为空值检查。
• Case 和条件语句：
  • Elixir 利用前一个子句的信息来细化后续子句。例如，在 case System.get_env("SOME_VAR") do nil -> ... value -> ... end 中，value 分支会被细化为非 nil 类型。

关键要点

• 渐进式类型系统：Elixir v1.20 引入了基于集合论的渐进式类型系统，支持静态和动态类型的混合使用。
• 无注解即有用：即使不添加任何类型注解，新