+ + 集合论类型与渐进式类型检查：Elixir 类型系统设计原则详解

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

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

¶一、论文讨论的不是 Typespec 的小修补

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

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

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

¶二、为什么简单的并集类型不够用

先看一个函数：

1
2
3

$ (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 时，类型检查器无法确认结果一定是整数：

1	integer_value + negate(integer_value)

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

1 2	$ (integer() -> integer()) and (boolean() -> boolean())

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

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

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

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

1	{integer() or string(), boolean()}

与：

1	{integer(), boolean()} or {string(), boolean()}

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

¶三、函数元数必须进入类型语义

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

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

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

1	(t1, ..., tn) -> t

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

这一点看似基础，实际影响很大。guard 分析、函数应用检查和多子句函数的重载行为都依赖于准确的 arity 信息。

¶四、参数多态与局部类型推断

集合论类型并不排斥参数多态。论文用 map/2 和 reduce/3 说明这一点：

$ ([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 类型元素的列表。

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

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

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

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

1	tree(a) = (a and not list()) or [tree(a)]

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

1	tree(a) -> [a]

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

¶五、guard 是类型信息，而不只是运行时条件

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

例如：

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

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

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

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

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

person 必须是 map；
person 必须定义 age 字段；
age 的值必须是整数。

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

¶5.1 类型收窄

考虑：

1
2
3

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 有两个逻辑分支：

1 2	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 可以是任意值。因此第一条子句的返回类型是：

1	{term(), boolean()} or {integer(), term()}

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

¶六、当 guard 无法被类型精确表达时，系统使用上下近似

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

1	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 的值。

例如：

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 都已经被第一条子句捕获。因此第一条子句的：

1 2	potentially accepted type = map() or list() surely accepted type = list()

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

¶七、穷尽性检查和冗余分支检查

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

论文定义：

1
2
3

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

函数却只处理：

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

仍有一种输入没有实现：

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

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

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

这两种能力分别对应：

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

¶八、统一理解 record 与 dictionary

Elixir 的 map 有两个常见用途：

1	person.age

把 map 当成 record；

1	person[key]

把 map 当成 dictionary。

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

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

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

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

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

1	%{age: integer(), ...}

如果字段可能缺失：

1	%{optional(:age) => integer()}

此时：

1	person.age

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

1	person[:age]

的结果类型是：

1	integer() or nil

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

1	%{foo: integer(), bar: integer()}

那么：

1	m[:foo] + m[:bar]

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

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

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

1
2
3

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

它表示：

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

固定 singleton key 的声明优先于更宽泛的 key domain。这一点使类型系统能够表达结构化数据与动态字典混合的实际用法。

¶九、渐进式类型检查：dynamic() 的作用

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

论文引入：

dynamic()

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

例如：

1 2	$ dynamic() -> _ def foo1(x), do: ...

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

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

1 2	$ (dynamic() -> dynamic()) -> _ def foo2(fun), do: ...

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

1	foo2({7, 42})

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

¶十、普通函数箭头与 strong arrow

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

考虑两个身份函数：

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

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

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

1	integer() -> integer()

运行时行为却不同：

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

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

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

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

于是：

1 2	$ 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。

类型语法包括：

1
2
3

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

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

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

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

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

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

¶十二、编译器集成原则

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

¶12.1 不改变 Elixir 表达式语法

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

论文选择：

1
2
3

or
and
not

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

1	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 检查和已有函数契约中逐步提取可靠的类型信息。

¶参考资料

Giuseppe Castagna, Guillaume Duboc, José Valim, “The Design Principles of the Elixir Type System”, arXiv:2306.06391v3, 2024。论文摘要页；PDF。
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。
论文中提到的 Typex 原型：typex.fly.dev。
CDuce 项目：cduce.org。
WhatsApp eqWAlizer：github.com/WhatsApp/eqwalizer。
Erlang Typespec 文档：erlang.org/doc/reference_manual/typespec.html。
Gleam：gleam.run。

+ +

¶一、论文讨论的不是 Typespec 的小修补

¶二、为什么简单的并集类型不够用

¶三、函数元数必须进入类型语义

¶四、参数多态与局部类型推断

¶五、guard 是类型信息，而不只是运行时条件

¶5.1 类型收窄

¶5.2 复杂 guard 的环境分裂

¶六、当 guard 无法被类型精确表达时，系统使用上下近似

¶Potentially accepted type

¶Surely accepted type

¶七、穷尽性检查和冗余分支检查

¶八、统一理解 record 与 dictionary

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

¶九、渐进式类型检查：dynamic() 的作用

¶十、普通函数箭头与 strong arrow

¶十一、形式化核心：Core Elixir 与双向类型检查

¶十二、编译器集成原则

¶12.1 不改变 Elixir 表达式语法

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

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

¶十三、尚未完成的部分

¶13.1 类型重建与 occurrence typing

¶13.2 Row polymorphism

¶13.3 消息传递

¶13.4 Behaviours

¶十四、与 Dialyzer、eqWAlizer 和 Gleam 的关系

¶Dialyzer

¶eqWAlizer

¶Gleam

¶十五、如何评价这套设计

¶参考资料

¶参考文献

¶参考文献

¶一、论文讨论的不是 Typespec 的小修补

¶二、为什么简单的并集类型不够用

¶三、函数元数必须进入类型语义

¶四、参数多态与局部类型推断

¶五、guard 是类型信息，而不只是运行时条件

¶5.1 类型收窄

¶5.2 复杂 guard 的环境分裂

¶六、当 guard 无法被类型精确表达时，系统使用上下近似

¶Potentially accepted type

¶Surely accepted type

¶七、穷尽性检查和冗余分支检查

¶八、统一理解 record 与 dictionary

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

¶九、渐进式类型检查：dynamic() 的作用

¶十、普通函数箭头与 strong arrow

¶十一、形式化核心：Core Elixir 与双向类型检查

¶十二、编译器集成原则

¶12.1 不改变 Elixir 表达式语法

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

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

¶十三、尚未完成的部分

¶13.1 类型重建与 occurrence typing

¶13.2 Row polymorphism

¶13.3 消息传递

¶13.4 Behaviours

¶十四、与 Dialyzer、eqWAlizer 和 Gleam 的关系

¶Dialyzer

¶eqWAlizer

¶Gleam

¶十五、如何评价这套设计

¶参考资料