From 6c2ebe0799e94df55fbdd8096ae17680c8e4e85e Mon Sep 17 00:00:00 2001 From: i-shm Date: Thu, 20 Aug 2026 13:09:06 +0000 Subject: deploy: 9feaefdf4f6e4dd53ade997aaeb108ec44a134de --- .../index.html" | 40 +++++++++++----------- 1 file changed, 20 insertions(+), 20 deletions(-) (limited to '2026/08') diff --git "a/2026/08/20/\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/index.html" "b/2026/08/20/\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/index.html" index 67afcd19..759a44c8 100644 --- "a/2026/08/20/\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/index.html" +++ "b/2026/08/20/\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/index.html" @@ -301,12 +301,12 @@ mjx-container[display="true"] + br {

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

+

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

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

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

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

-

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

+

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

先看一个函数：

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

@@ -329,15 +329,15 @@ mjx-container[display="true"] + br {

与：

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

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

-

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

-

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

+

函数 arity 也属于类型

+

在 Elixir 中，函数 arity 不是附属信息。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 说明这一点：

+

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

+

参数多态与局部类型推断

+

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

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

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

@@ -348,7 +348,7 @@ mjx-container[display="true"] + br {

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

1
tree(a) -> [a]

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

-

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

+

从 pattern 和 guard 中提取类型

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

例如：

1
def get_age(person) when is_integer(person.age), do: person.age
@@ -373,7 +373,7 @@ mjx-container[display="true"] + br {

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

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

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

-

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

+

guard 无法精确表达时怎么办

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

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

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

@@ -388,7 +388,7 @@ mjx-container[display="true"] + br {

第一条子句可能接受两字段 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()}}
@@ -403,7 +403,7 @@ mjx-container[display="true"] + br {
  • exhaustivity checking：检查是否覆盖所有可能输入；
  • redundancy checking：检查是否存在永远无法匹配的分支。
    • -

    八、统一理解 record 与 dictionary

    +

    map 同时承担 record 与 dictionary

    Elixir 的 map 有两个常见用途：

    1
    person.age

    把 map 当成 record；

    @@ -440,8 +440,8 @@ mjx-container[display="true"] + br {
  • bar 可以缺失，存在时是 atom；
  • 其他 atom key 对应 integer。
    • -

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

    -

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

    +

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

    +

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

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

    论文引入：

    1
    dynamic()
    @@ -454,7 +454,7 @@ mjx-container[display="true"] + br {

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

    1
    foo2({7, 42})

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

    -

    十、普通函数箭头与 strong arrow

    +

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

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

    考虑两个身份函数：

    1
    2
    3
    4
    5
    $ integer() -> integer()
    def id_weak(x), do: x

    $ integer() -> integer()
    def id_strong(x) when is_integer(x), do: x
    @@ -476,7 +476,7 @@ mjx-container[display="true"] + br { 
    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 与双向类型检查

    +

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

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

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

    -

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

    +

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

    -- cgit v1.2.3