diff options
| -rw-r--r-- | source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.md | 555 |
1 files changed, 555 insertions, 0 deletions
diff --git a/source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.md b/source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.md new file mode 100644 index 00000000..ac95c087 --- /dev/null +++ b/source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.md @@ -0,0 +1,555 @@ +--- +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 的语言习惯重新设计一套陌生语言。它必须理解多子句函数、函数元数、模式匹配、guard、map、协议、动态代码和 BEAM 的运行时行为。作者因此没有选择一套简单的“类型标签”，而是把集合论类型、局部类型推断、类型收窄和渐进式类型检查组合在一起，构成一套逐步集成到 Elixir 编译器中的设计方案。[1] + +## 一、论文讨论的不是 Typespec 的小修补 + +Elixir 已经有 Typespec，也可以使用 Dialyzer 分析代码。问题在于，Typespec 的声明并不会由 Elixir 编译器完整验证，Dialyzer 则采用 success typing：它只在能够证明某处存在问题时报告警告，从而尽量避免误报。这种策略适合分析规模庞大的既有代码，却会放过一部分潜在错误。 + +论文提出的系统追求更强的类型安全保证。它希望在编译期报告更多类型错误，同时允许项目继续保留未标注的动态代码。类型系统因此必须同时完成两件事：一方面精确表达函数和数据结构的约束，另一方面控制迁移成本，不要求开发者一次性改写整个代码库。[1] + +这项工作属于语言设计和类型理论研究，不是一篇以 benchmark 为中心的实验论文。论文给出了 Core Elixir 的形式化类型规则，介绍了原型实现，并列出未来的编译器集成路线；作者也明确承认，大规模代码库上的性能、警告质量和社区接受度仍需要后续实现验证。[1] + +## 二、为什么简单的并集类型不够用 + +先看一个函数： + +```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] + +## 三、函数元数必须进入类型语义 + +在 Elixir 中，函数元数不是附属信息。`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()`，会迅速丢失输入元素与输出元素之间的关系。 + +## 五、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：检查是否存在永远无法匹配的分支。 + +## 八、统一理解 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。这一点使类型系统能够表达结构化数据与动态字典混合的实际用法。 + +## 九、渐进式类型检查：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] + +## 十二、编译器集成原则 + +论文提出了几项明确的集成要求。 + +### 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/)。 |