From 9feaefdf4f6e4dd53ade997aaeb108ec44a134de Mon Sep 17 00:00:00 2001 From: "Somhairle H. Marisol" Date: Thu, 20 Aug 2026 21:08:39 +0800 Subject: refine: make Elixir paper blog more natural --- ...216\237\345\210\231\350\257\246\350\247\243.md" | 40 +++++++++++----------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git "a/source/_posts/\351\233\206\345\220\210\350\256\272\347\261\273\345\236\213\344\270\216\346\270\220\350\277\233\345\274\217\347\261\273\345\236\213\346\243\200\346\237\245\357\274\232Elixir-\347\261\273\345\236\213\347\263\273\347\273\237\350\256\276\350\256\241\345\216\237\345\210\231\350\257\246\350\247\243.md" "b/source/_posts/\351\233\206\345\220\210\350\256\272\347\261\273\345\236\213\344\270\216\346\270\220\350\277\233\345\274\217\347\261\273\345\236\213\346\243\200\346\237\245\357\274\232Elixir-\347\261\273\345\236\213\347\263\273\347\273\237\350\256\276\350\256\241\345\216\237\345\210\231\350\257\246\350\247\243.md" index ac95c087..7314854a 100644 --- "a/source/_posts/\351\233\206\345\220\210\350\256\272\347\261\273\345\236\213\344\270\216\346\270\220\350\277\233\345\274\217\347\261\273\345\236\213\346\243\200\346\237\245\357\274\232Elixir-\347\261\273\345\236\213\347\263\273\347\273\237\350\256\276\350\256\241\345\216\237\345\210\231\350\257\246\350\247\243.md" +++ "b/source/_posts/\351\233\206\345\220\210\350\256\272\347\261\273\345\236\213\344\270\216\346\270\220\350\277\233\345\274\217\347\261\273\345\236\213\346\243\200\346\237\245\357\274\232Elixir-\347\261\273\345\236\213\347\263\273\347\273\237\350\256\276\350\256\241\345\216\237\345\210\231\350\257\246\350\247\243.md" @@ -7,9 +7,9 @@ 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] +论文的核心判断是：Elixir 需要静态类型检查，但类型系统不能脱离 Elixir 的语言习惯重新设计一套陌生语言。它必须理解多子句函数、函数 arity、模式匹配、guard、map、协议、动态代码和 BEAM 的运行时行为。作者因此没有选择一套简单的“类型标签”，而是把集合论类型、局部类型推断、类型收窄和渐进式类型检查组合在一起，构成一套逐步集成到 Elixir 编译器中的设计方案。[1] -## 一、论文讨论的不是 Typespec 的小修补 +## Elixir 为什么需要另一套类型系统 Elixir 已经有 Typespec，也可以使用 Dialyzer 分析代码。问题在于，Typespec 的声明并不会由 Elixir 编译器完整验证，Dialyzer 则采用 success typing：它只在能够证明某处存在问题时报告警告，从而尽量避免误报。这种策略适合分析规模庞大的既有代码，却会放过一部分潜在错误。 @@ -17,7 +17,7 @@ Elixir 已经有 Typespec，也可以使用 Dialyzer 分析代码。问题在于 这项工作属于语言设计和类型理论研究，不是一篇以 benchmark 为中心的实验论文。论文给出了 Core Elixir 的形式化类型规则，介绍了原型实现，并列出未来的编译器集成路线；作者也明确承认，大规模代码库上的性能、警告质量和社区接受度仍需要后续实现验证。[1] -## 二、为什么简单的并集类型不够用 +## `or` 不够用：集合论类型怎样表达函数行为 先看一个函数： @@ -66,9 +66,9 @@ $ (integer() -> integer()) and 表示同一个值集合。语义子类型通过集合包含关系定义，因此类型检查器可以识别这种等价性，而不需要依赖类型表达式的表面语法。[1] -## 三、函数元数必须进入类型语义 +## 函数 arity 也属于类型 -在 Elixir 中，函数元数不是附属信息。`foo/1` 和 `foo/2` 是两个不同的函数，`is_function(value, 2)` 也可以在运行时检查函数是否接受两个参数。 +在 Elixir 中，函数 arity 不是附属信息。`foo/1` 和 `foo/2` 是两个不同的函数，`is_function(value, 2)` 也可以在运行时检查函数是否接受两个参数。 传统的一元函数类型系统往往把多参数函数编码为接受 tuple 的函数。例如，二元函数可能被表示成接受 `{x, y}` 的一元函数。这种编码无法准确表达 Elixir 的 arity，也无法正确处理 `is_function/2`。 @@ -80,11 +80,11 @@ $ (integer() -> integer()) and 形式化定义中的函数空间使用 $n$ 元输入，而不是单个输入集合。类型子型关系首先要求元数相同，然后比较各个参数域和返回域。不同元数的函数类型交集为空集，这与 Elixir 的运行时语义一致。[1] -这一点看似基础，实际影响很大。guard 分析、函数应用检查和多子句函数的重载行为都依赖于准确的 arity 信息。 +guard 分析、函数应用检查和多子句函数的重载行为都依赖于准确的 arity 信息。 -## 四、参数多态与局部类型推断 +## 参数多态与局部类型推断 -集合论类型并不排斥参数多态。论文用 `map/2` 和 `reduce/3` 说明这一点： +论文用 `map/2` 和 `reduce/3` 说明集合论类型如何支持参数多态： ```elixir $ ([a], (a -> b)) -> [b] @@ -117,7 +117,7 @@ tree(a) -> [a] 这种类型表达能力对处理 Elixir 的通用集合函数很重要。单纯把所有值都近似成 `term()`，会迅速丢失输入元素与输出元素之间的关系。 -## 五、guard 是类型信息，而不只是运行时条件 +## 从 pattern 和 guard 中提取类型 Elixir 程序大量依赖 guard。论文的一个核心工作，是把 guard 分析纳入类型系统，而不是只把 guard 当成无法理解的运行时黑箱。 @@ -174,7 +174,7 @@ def baz(_, _), do: nil 系统不能简单地把 `x` 和 `y` 各自标成一个 union 类型，而需要为 `or` 的两个分支建立不同的类型环境，再合并分支结果。论文的 guard 分析规则从左到右处理 guard，并考虑 Elixir guard 的求值顺序和可能失败的表达式。[1] -## 六、当 guard 无法被类型精确表达时，系统使用上下近似 +## guard 无法精确表达时怎么办 类型系统无法表达所有运行时谓词。例如： @@ -214,7 +214,7 @@ surely accepted type = list() 这足以判定第二条子句是冗余的，因为 `length/1` 只对 list 有意义，而所有 list 已经被前一条子句处理。[1] -## 七、穷尽性检查和冗余分支检查 +## 模式匹配还能检查什么 模式匹配的价值不只在于解构数据，也在于它能够给出完整的控制流信息。 @@ -248,7 +248,7 @@ def handle(r) when r.message == :timeout, do: "Timeout" - exhaustivity checking：检查是否覆盖所有可能输入； - redundancy checking：检查是否存在永远无法匹配的分支。 -## 八、统一理解 record 与 dictionary +## map 同时承担 record 与 dictionary Elixir 的 map 有两个常见用途： @@ -335,9 +335,9 @@ type t() = %{foo: atom(), - `bar` 可以缺失，存在时是 atom； - 其他 atom key 对应 integer。 -固定 singleton key 的声明优先于更宽泛的 key domain。这一点使类型系统能够表达结构化数据与动态字典混合的实际用法。 +固定 singleton key 的声明优先于更宽泛的 key domain，因此同一个 map 类型可以同时表达结构化字段和动态字典键。 -## 九、渐进式类型检查：dynamic() 的作用 +## `dynamic()` 为旧代码留下迁移路径 Elixir 已经存在大量动态代码。若要迁移这些代码，类型系统必须允许静态部分和动态部分共存。 @@ -373,7 +373,7 @@ foo2({7, 42}) 因为 tuple 不是函数，即使函数参数的其他细节是动态的。 -## 十、普通函数箭头与 strong arrow +## strong arrow 如何利用已有的运行时检查 这是论文最关键、也最容易被忽略的部分。 @@ -417,7 +417,7 @@ def foo3(x), do: {id_weak(x), id_strong(x)} 这套设计解决了一个工程问题：传统 sound gradual typing 通常需要编译器在动态代码与静态代码交界处插入 cast。本文方案要求类型系统不改变 Elixir 的编译结果，因此它改为分析现有的 guard、模式匹配和 BEAM 检查，利用已经存在的运行时行为完成安全性推断。[1] -## 十一、形式化核心：Core Elixir 与双向类型检查 +## Core Elixir：把这些规则写成类型系统 论文没有直接形式化整个 Elixir，而是定义了一个 Core Elixir。其表达式包括： @@ -456,7 +456,7 @@ $$ 论文把 guard 的类型分析拆成多个子环境，以处理 `or` 分支以及前置 guard 失败后的求值路径。类型系统还区分能够保证穷尽性的规则和只能给出 warning 的近似规则：如果只能使用 potentially accepted type 判断覆盖范围，系统会提示 case 可能在运行时没有匹配分支。[1] -## 十二、编译器集成原则 +## 类型系统怎样进入 Elixir 编译器 论文提出了几项明确的集成要求。 @@ -494,7 +494,7 @@ JSON.Encoder.t() and XML.Encoder.t() 论文认为，优先支持大多数 Elixir 习惯用法，比立即实现高成本的完整类型重建更实际。类型重建会带来复杂的约束求解和多轮代码分析，因此应当在语言常用结构得到支持后再推进。 -## 十三、尚未完成的部分 +## 论文没有解决的部分 论文没有把类型系统包装成已经完成的工程产品。作者列出了一系列尚未完成的研究方向。 @@ -522,7 +522,7 @@ map 删除和更新操作需要 row polymorphism，才能表达“保留所有 这要求类型系统处理模块类型、抽象类型、参数化 behaviour 以及更复杂的存在类型关系。 -## 十四、与 Dialyzer、eqWAlizer 和 Gleam 的关系 +## 它与 Dialyzer、eqWAlizer 和 Gleam 有什么不同 ### Dialyzer @@ -536,7 +536,7 @@ eqWAlizer 支持泛型、局部类型推断、类型收窄和渐进式类型， Gleam 选择一套从 ML 家族继承而来的静态类型路线，拥有 Hindley–Milner 类型推断和有限的 row polymorphism。它从语言设计之初就选择静态类型；本文方案则直接面对现有 Elixir 代码库，优先解决逐步迁移与语义兼容问题。[1] -## 十五、如何评价这套设计 +## 这套设计的边界 这套方案的理论优势很明确。交集箭头可以表达多子句函数的输入输出对应关系；guard 分析可以把 Elixir 的控制流信息转化为类型信息；开放 map 类型可以同时处理 record 和 dictionary；strong arrow 则利用已有运行时检查，避免类型系统为了保证安全而自动改变代码执行方式。 -- cgit v1.2.3