1 files changed, 20 insertions, 20 deletions
diff --git a/source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.md b/source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.md
index ac95c087..7314854a 100644
--- a/source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.md
+++ b/source/_posts/集合论类型与渐进式类型检查：Elixir-类型系统设计原则详解.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 则利用已有运行时检查，避免类型系统为了保证安全而自动改变代码执行方式。