path: root/source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.md

---
title: 集合论类型与渐进式类型检查：Elixir 类型系统设计原则详解
date: 2026-08-20 11:50:00
tags: [Technique]
mathjax: true
---

> 本文解读 Giuseppe Castagna、Guillaume Duboc 与 José Valim 的论文《The Design Principles of the Elixir Type System》。论文提出了一套面向 Elixir 的渐进式类型系统，重点处理集合论类型、语义子类型、模式匹配、guard、map、动态代码与 BEAM 运行时检查之间的关系。

论文的核心判断是：Elixir 需要静态类型检查，但类型系统不能脱离 Elixir 的语言习惯重新设计一套陌生语言。它必须理解多子句函数、函数 arity、模式匹配、guard、map、协议、动态代码和 BEAM 的运行时行为。作者因此没有选择一套简单的“类型标签”，而是把集合论类型、局部类型推断、类型收窄和渐进式类型检查组合在一起，构成一套逐步集成到 Elixir 编译器中的设计方案。[1]

## Elixir 为什么需要另一套类型系统

Elixir 已经有 Typespec，也可以使用 Dialyzer 分析代码。问题在于，Typespec 的声明并不会由 Elixir 编译器完整验证，Dialyzer 则采用 success typing：它只在能够证明某处存在问题时报告警告，从而尽量避免误报。这种策略适合分析规模庞大的既有代码，却会放过一部分潜在错误。

论文提出的系统追求更强的类型安全保证。它希望在编译期报告更多类型错误，同时允许项目继续保留未标注的动态代码。类型系统因此必须同时完成两件事：一方面精确表达函数和数据结构的约束，另一方面控制迁移成本，不要求开发者一次性改写整个代码库。[1]

这项工作属于语言设计和类型理论研究，不是一篇以 benchmark 为中心的实验论文。论文给出了 Core Elixir 的形式化类型规则，介绍了原型实现，并列出未来的编译器集成路线；作者也明确承认，大规模代码库上的性能、警告质量和社区接受度仍需要后续实现验证。[1]

## `or` 不够用：集合论类型怎样表达函数行为

先看一个函数：

```elixir
$ (integer() or boolean()) -> (integer() or boolean())
def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x
```

这个声明只说明输入可以是整数或布尔值，输出也可以是整数或布尔值。它没有表达输入和输出之间的对应关系。因此，当下面的代码调用 `negate/1` 时，类型检查器无法确认结果一定是整数：

```elixir
integer_value + negate(integer_value)
```

论文改用函数箭头类型的交集：

```elixir
$ (integer() -> integer()) and
  (boolean() -> boolean())
```

这个类型表达了两个子行为：整数输入得到整数输出，布尔值输入得到布尔值输出。它比前一个并集类型更精确。

集合论类型把类型理解为值的集合：

- `integer()` 表示所有整数构成的集合；
- `boolean()` 表示 `{true, false}`；
- `t1 or t2` 表示两个集合的并集；
- `t1 and t2` 表示两个集合的交集；
- `not t` 表示集合补集；
- `none()` 表示空集合；
- `term()` 表示所有 Elixir 值。

这种解释使类型运算服从集合论的交换律、结合律和分配律。比如：

```elixir
{integer() or string(), boolean()}
```

与：

```elixir
{integer(), boolean()} or {string(), boolean()}
```

表示同一个值集合。语义子类型通过集合包含关系定义，因此类型检查器可以识别这种等价性，而不需要依赖类型表达式的表面语法。[1]

## 函数 arity 也属于类型

在 Elixir 中，函数 arity 不是附属信息。`foo/1` 和 `foo/2` 是两个不同的函数，`is_function(value, 2)` 也可以在运行时检查函数是否接受两个参数。

传统的一元函数类型系统往往把多参数函数编码为接受 tuple 的函数。例如，二元函数可能被表示成接受 `{x, y}` 的一元函数。这种编码无法准确表达 Elixir 的 arity，也无法正确处理 `is_function/2`。

论文因此直接把元数写入函数类型：

```text
(t1, ..., tn) -> t
```

形式化定义中的函数空间使用 $n$ 元输入，而不是单个输入集合。类型子型关系首先要求元数相同，然后比较各个参数域和返回域。不同元数的函数类型交集为空集，这与 Elixir 的运行时语义一致。[1]

guard 分析、函数应用检查和多子句函数的重载行为都依赖于准确的 arity 信息。

## 参数多态与局部类型推断

论文用 `map/2` 和 `reduce/3` 说明集合论类型如何支持参数多态：

```elixir
$ ([a], (a -> b)) -> [b]
  when a: term(), b: term()
def map([h | t], fun), do: [fun.(h) | map(t, fun)]
def map([], _fun), do: []
```

它的含义是：对于任意类型 `a` 和 `b`，`map/2` 接受 `a` 类型元素的列表，以及一个从 `a` 映射到 `b` 的函数，返回 `b` 类型元素的列表。

调用时不需要显式实例化类型变量：

```elixir
map([1, 4], fn x -> negate(x) end)
```

局部类型推断可以把 `a` 和 `b` 都实例化为 `integer()`，因此结果类型为 `[integer()]`。

论文还用递归类型描述嵌套列表：

```elixir
tree(a) = (a and not list()) or [tree(a)]
```

这个定义允许叶节点是 `a` 类型且不是 list 的值，也允许节点是由其他树组成的 list。于是 `flatten/1` 可以获得如下类型：

```elixir
tree(a) -> [a]
```

这种类型表达能力对处理 Elixir 的通用集合函数很重要。单纯把所有值都近似成 `term()`，会迅速丢失输入元素与输出元素之间的关系。

## 从 pattern 和 guard 中提取类型

Elixir 程序大量依赖 guard。论文的一个核心工作，是把 guard 分析纳入类型系统，而不是只把 guard 当成无法理解的运行时黑箱。

例如：

```elixir
def get_age(person) when is_integer(person.age), do: person.age
```

类型检查器可以从 `person.age` 和 `is_integer/1` 推断：

```text
%{age: integer(), ...} -> integer()
```

这里的 `...` 表示开放 map：map 至少包含 `age` 字段，也可以包含其他字段。

这个推断同时完成了三件事：

1. `person` 必须是 map；
2. `person` 必须定义 `age` 字段；
3. `age` 的值必须是整数。

因此，类型系统可以把 guard 视为对变量类型的约束，并在后续表达式中使用这些约束。

### 5.1 类型收窄

考虑：

```elixir
def negate_alt(x) do
  if is_integer(x), do: -x, else: not x
end
```

如果 `x` 初始类型是 `integer() or boolean()`，类型检查器会在 `do` 分支把它收窄成 `integer()`，在 `else` 分支把它收窄成 `boolean()`。

论文把这种技术称为 narrowing。它也适用于被测试表达式内部的变量，例如 map 字段和 tuple 元素。

### 5.2 复杂 guard 的环境分裂

下面的 guard 有两个逻辑分支：

```elixir
def baz(x, y) when is_boolean(x) or is_integer(y), do: {y, x}
def baz(_, _), do: nil
```

第一种情况是 `x` 为 boolean，`y` 可以是任意值；第二种情况是 `y` 为 integer，`x` 可以是任意值。因此第一条子句的返回类型是：

```text
{term(), boolean()} or {integer(), term()}
```

系统不能简单地把 `x` 和 `y` 各自标成一个 union 类型，而需要为 `or` 的两个分支建立不同的类型环境，再合并分支结果。论文的 guard 分析规则从左到右处理 guard，并考虑 Elixir guard 的求值顺序和可能失败的表达式。[1]

## guard 无法精确表达时怎么办

类型系统无法表达所有运行时谓词。例如：

```elixir
def foo(x) when map_size(x) == 2, do: Map.to_list(x)
```

“所有恰好包含两个字段的 map”是一个运行时集合，但不一定能够用当前类型语法精确表达。

论文因此区分两种近似。

### Potentially accepted type

它是一个上近似，包含所有可能通过 pattern/guard 的值，也可能包含一些实际上不会通过 guard 的值。

在上面的例子中，可以使用 `map()` 作为 potentially accepted type。它比“大小为 2 的 map”更宽，但包含后者的全部值。

### Surely accepted type

它是一个下近似，只包含确定会通过 pattern/guard 的值。

例如：

```elixir
def bar(x) when
  (is_map(x) and map_size(x) == 2) or is_list(x), do: to_string(x)

def bar(x) when length(x) == 2, do: x
```

第一条子句可能接受两字段 map，也接受所有 list。系统无法精确表达两字段 map，但可以确定所有 list 都已经被第一条子句捕获。因此第一条子句的：

```text
potentially accepted type = map() or list()
surely accepted type = list()
```

这足以判定第二条子句是冗余的，因为 `length/1` 只对 list 有意义，而所有 list 已经被前一条子句处理。[1]

## 模式匹配还能检查什么

模式匹配的价值不只在于解构数据，也在于它能够给出完整的控制流信息。

论文定义：

```elixir
result() =
  %{output: :ok, socket: socket()} or
  %{output: :error, message: :timeout or {:delay, integer()}}
```

函数却只处理：

```elixir
def handle(r) when r.output == :ok, do: "Msg received"
def handle(r) when r.message == :timeout, do: "Timeout"
```

仍有一种输入没有实现：

```elixir
%{output: :error, message: {:delay, integer()}}
```

类型检查器可以报告函数定义不完整，并直接指出缺失的输入类型。相比只说“可能存在未匹配分支”，这种警告更适合重构大型代码库。

反过来，如果函数输入类型只允许 map，却增加了一个匹配 tuple 的子句，类型检查器可以报告该分支永远不会执行。

这两种能力分别对应：

- exhaustivity checking：检查是否覆盖所有可能输入；
- redundancy checking：检查是否存在永远无法匹配的分支。

## map 同时承担 record 与 dictionary

Elixir 的 map 有两个常见用途：

```elixir
person.age
```

把 map 当成 record；

```elixir
person[key]
```

把 map 当成 dictionary。

两种访问方式的运行时语义不同：

- `person.age` 要求 `age` 一定存在，否则抛出异常；
- `person[:age]` 允许 key 缺失，此时返回 `nil`。

论文用 required 和 optional 字段标记这种差异：

```elixir
%{required(:age) => integer(), optional(term()) => term()}
```

也可以使用更直观的开放 map 写法：

```elixir
%{age: integer(), ...}
```

如果字段可能缺失：

```elixir
%{optional(:age) => integer()}
```

此时：

```elixir
person.age
```

会触发类型警告，因为 `age` 不一定存在；而：

```elixir
person[:age]
```

的结果类型是：

```text
integer() or nil
```

如果 map 中的字段被声明为必需字段：

```elixir
%{foo: integer(), bar: integer()}
```

那么：

```elixir
m[:foo] + m[:bar]
```

可以被推断为整数运算，因为两个字段都不可能返回 `nil`。

### 8.1 混合记录字段与字典键域

论文允许一个 map 类型同时包含固定字段和动态键域：

```elixir
type t() = %{foo: atom(),
              optional(:bar) => atom(),
              optional(atom()) => integer()}
```

它表示：

- `foo` 必须存在，并且是 atom；
- `bar` 可以缺失，存在时是 atom；
- 其他 atom key 对应 integer。

固定 singleton key 的声明优先于更宽泛的 key domain，因此同一个 map 类型可以同时表达结构化字段和动态字典键。

## `dynamic()` 为旧代码留下迁移路径

Elixir 已经存在大量动态代码。若要迁移这些代码，类型系统必须允许静态部分和动态部分共存。

论文引入：

```elixir
dynamic()
```

它不是普通的顶层类型。`term()` 表示所有值，而 `dynamic()` 表示类型检查器暂时不知道某个表达式的具体类型，并允许它在运行时以不同类型出现。

例如：

```elixir
$ dynamic() -> _
def foo1(x), do: ...
```

函数可以接受任意类型的参数，函数体中每次使用 `x` 时也可以处于不同的动态类型环境。

但 `dynamic()` 不会让类型检查完全失去意义：

```elixir
$ (dynamic() -> dynamic()) -> _
def foo2(fun), do: ...
```

这里仍然要求 `fun` 具有函数类型。下面的调用会被拒绝：

```elixir
foo2({7, 42})
```

因为 tuple 不是函数，即使函数参数的其他细节是动态的。

## strong arrow 如何利用已有的运行时检查

这是论文最关键、也最容易被忽略的部分。

考虑两个身份函数：

```elixir
$ integer() -> integer()
def id_weak(x), do: x

$ integer() -> integer()
def id_strong(x) when is_integer(x), do: x
```

从静态输入输出关系看，它们都像是：

```text
integer() -> integer()
```

运行时行为却不同：

- `id_weak/1` 没有检查输入，传入字符串时可能原样返回字符串；
- `id_strong/1` 通过 guard 检查输入，非整数会匹配失败。

因此，论文把第二种函数视为 strong function，把第一种函数视为 weak function。

strong arrow 的语义是：函数即使收到不属于声明 domain 的动态输入，也必须满足以下条件之一：

1. 返回符合 codomain 的结果；
2. 通过 BEAM 或程序员写出的运行时检查失败；
3. 发散而不返回。

于是：

```elixir
$ dynamic() -> {dynamic(), integer()}
def foo3(x), do: {id_weak(x), id_strong(x)}
```

第一项仍然是 `dynamic()`，因为 `id_weak/1` 没有运行时检查；第二项可以被确定为 `integer()`，因为 `id_strong/1` 要么返回整数，要么在输入错误时失败。

这套设计解决了一个工程问题：传统 sound gradual typing 通常需要编译器在动态代码与静态代码交界处插入 cast。本文方案要求类型系统不改变 Elixir 的编译结果，因此它改为分析现有的 guard、模式匹配和 BEAM 检查，利用已经存在的运行时行为完成安全性推断。[1]

## Core Elixir：把这些规则写成类型系统

论文没有直接形式化整个 Elixir，而是定义了一个 Core Elixir。其表达式包括：

- 常量和变量；
- lambda 与函数应用；
- tuple 与 tuple projection；
- 带类型注解的 let；
- 加法；
- 带 pattern 和 guard 的 case。

类型语法包括：

```text
b ::= int | atom | 1fun | 1tup

t ::= b | c | α | t -> t | {t} | t or t | not t
```

交集可以由否定和并集编码：

$$
t_1 \mathbin{and} t_2 = not\,(not\,t_1 \mathbin{or} not\,t_2)
$$

顶层类型和空类型分别编码为：

$$
term() = int \mathbin{or} atom \mathbin{or} 1fun \mathbin{or} 1tup
$$

$$
none() = not\,term()
$$

类型检查采用双向思想：一部分表达式合成类型，另一部分表达式在给定期望类型的条件下进行检查。case 表达式的类型规则会计算每个 pattern/guard 能够处理的输入区域，并用这些区域生成分支环境。

论文把 guard 的类型分析拆成多个子环境，以处理 `or` 分支以及前置 guard 失败后的求值路径。类型系统还区分能够保证穷尽性的规则和只能给出 warning 的近似规则：如果只能使用 potentially accepted type 判断覆盖范围，系统会提示 case 可能在运行时没有匹配分支。[1]

## 类型系统怎样进入 Elixir 编译器

论文提出了几项明确的集成要求。

### 12.1 不改变 Elixir 表达式语法

类型系统不能要求每个函数参数都增加新语法。Elixir 已经把大量语言结构写在自身宏系统中，因此类型语法也必须遵守现有语言的表达习惯。

论文选择：

```elixir
or
and
not
```

表达集合论中的并集、交集和否定。作者认为，Elixir 开发者更容易理解：

```elixir
JSON.Encoder.t() and XML.Encoder.t()
```

而不是另外引入一套完全不同的符号。

### 12.2 先从隐式类型信息开始

作者规划了三个里程碑。

第一步，类型只在编译器内部使用。开发者暂时不能书写完整类型注解，系统先从 pattern 和 guard 中提取类型信息，用于发现字段名错误和基本类型不匹配。

第二步，为 struct 引入类型注解。struct 是命名且静态定义的 record，能够提供比普通 map 更稳定的字段信息。

第三步，引入函数类型注解。没有显式类型的参数默认使用 `dynamic()`，从而保持旧代码可编译。

### 12.3 类型检查优先于完整类型重建

论文认为，优先支持大多数 Elixir 习惯用法，比立即实现高成本的完整类型重建更实际。类型重建会带来复杂的约束求解和多轮代码分析，因此应当在语言常用结构得到支持后再推进。

## 论文没有解决的部分

论文没有把类型系统包装成已经完成的工程产品。作者列出了一系列尚未完成的研究方向。

### 13.1 类型重建与 occurrence typing

当前系统可以检查某些精确类型，但未必能够自动重建这些类型。例如 `filter/2` 的精确结果类型需要分析谓词函数对元素的判断，并把判断结果传递回元素变量。这需要更强的 occurrence typing 技术。

### 13.2 Row polymorphism

map 删除和更新操作需要 row polymorphism，才能表达“保留所有未知字段，同时删除或更新某一个字段”。集合论类型与 row polymorphism 的结合仍是开放问题。

### 13.3 消息传递

`receive` 已经可以利用 pattern、guard 和 narrowing，但 Elixir 进程之间的消息协议还没有被完整类型化。未来可以引入 mailbox types 或 behavioural types，描述进程接收和发送的消息集合。

### 13.4 Behaviours

论文最后用 `GenServer` 说明 behaviour 类型化的难点。理想的 `GenServer(request, reply)` 类型需要同时描述：

- 对外透明的 option 和 result 类型；
- 每个实现内部不透明的 state 类型；
- 由具体实现决定的 request 和 reply 类型；
- 必须实现或可以省略的 callback；
- `start/3` 的第一个参数必须是兼容的 behaviour 模块。

这要求类型系统处理模块类型、抽象类型、参数化 behaviour 以及更复杂的存在类型关系。

## 它与 Dialyzer、eqWAlizer 和 Gleam 有什么不同

### Dialyzer

Dialyzer 采用 success typing，优先减少误报。论文方案追求更强的 soundness，因此可能报告更多问题。二者代表不同的工程取舍：前者适合在大型动态代码库中保守分析，后者试图提供更强的编译期契约保证。[1]

### eqWAlizer

eqWAlizer 支持泛型、局部类型推断、类型收窄和渐进式类型，但论文方案进一步使用集合论类型、否定类型和 strong arrows，并把 map record 与 dictionary 放在统一类型体系中。[1]

### Gleam

Gleam 选择一套从 ML 家族继承而来的静态类型路线，拥有 Hindley–Milner 类型推断和有限的 row polymorphism。它从语言设计之初就选择静态类型；本文方案则直接面对现有 Elixir 代码库，优先解决逐步迁移与语义兼容问题。[1]

## 这套设计的边界

这套方案的理论优势很明确。交集箭头可以表达多子句函数的输入输出对应关系；guard 分析可以把 Elixir 的控制流信息转化为类型信息；开放 map 类型可以同时处理 record 和 dictionary；strong arrow 则利用已有运行时检查，避免类型系统为了保证安全而自动改变代码执行方式。

工程风险同样明确。类型表达式可能非常复杂，子类型判断可能增加编译成本，更强的 soundness 可能带来更多 warning，而宏、消息传递和 behaviour 仍需要继续研究。论文没有提供大型真实项目上的编译耗时、警告精度和迁移成本数据，因此它应当被看作一套有形式化基础的设计提案和原型路线，而不是已经完成的生产级类型检查器。

这篇论文最重要的贡献，是把问题重新表述为：如何让静态类型适应 Elixir 的运行时和编程风格。它没有要求 Elixir 放弃动态性，也没有把 Elixir 改造成另一门静态函数式语言，而是试图从 pattern、guard、map、BEAM 检查和已有函数契约中逐步提取可靠的类型信息。

## 参考资料

1. Giuseppe Castagna, Guillaume Duboc, José Valim, “The Design Principles of the Elixir Type System”, arXiv:2306.06391v3, 2024。 [论文摘要页](https://arxiv.org/abs/2306.06391)；[PDF](https://arxiv.org/pdf/2306.06391)。
2. Giuseppe Castagna, Guillaume Duboc, José Valim, “The Design Principles of the Elixir Type System”, *The Art, Science, and Engineering of Programming*, 8(2), 2024, Article 4。 [DOI](https://doi.org/10.22152/programming-journal.org/2024/8/4)。
3. 论文中提到的 Typex 原型：[typex.fly.dev](https://typex.fly.dev/)。
4. CDuce 项目：[cduce.org](https://www.cduce.org/)。
5. WhatsApp eqWAlizer：[github.com/WhatsApp/eqwalizer](https://github.com/WhatsApp/eqwalizer)。
6. Erlang Typespec 文档：[erlang.org/doc/reference_manual/typespec.html](https://www.erlang.org/doc/reference_manual/typespec.html)。
7. Gleam：[gleam.run](https://gleam.run/)。