揭秘类型（及一些悖论的解惑）

# 类型解惑（兼论去悖论化） 来源：https://sifter.org/~simon/journal/20260814.html [<< (https://sifter.org/~simon/journal/20240308.h.html)|上一篇 (https://sifter.org/~simon/journal/20260720.html)|目录 (https://sifter.org/~simon/journal/index.html)|下一篇 (https://sifter.org/~simon/journal/index.html)|>> (https://sifter.org/~simon/journal/indexh.html)] ## 2026年8月14日，星期五 #### *类型解惑（兼论去悖论化）* \[编程语言理论，类型论，认识论\] 这更像是《类型理论之倦》(https://sifter.org/~simon/journal/20140330.html) 的补遗，因此你或许想先从那里读起，但我会尽量让本文保持自包含： 我长久以来一直在纠结“类型”究竟是什么、意味着什么、又增添了什么。最终我意识到，它（对于一个充分的理论基础而言）什么也没增添——这解释了我多年的困惑。但有一个挥之不去的问题始终未能解决，近来我突然想通，并将在下文概述。 关于它（几乎）什么也没增添，其历史背景是：计算机科学和数学界的学者们构建了各种系统，这些系统要么过于严苛，要么过于想当然，于是不得不引入更多机制来修补由此引发的问题。 例如，罗素悖论 (https://en.wikipedia.org/wiki/Russell%27s_paradox)，其根源在于一个假设：你能写下的每个公式都有一个明确的定义值。这几乎和忽视“f(x) = not f(x)”无解一样荒谬，只是后者还差一步修补而已：如果你愿意应用同样的机制——它禁止“f(x) = not f(x)”作为一个可接受的规则——那么它同样会禁止罗素的公式。值得注意的是，这一现实，在概念上，恰恰是普通聪明人对此问题的第一反应——而学者们通常会用一堆晦涩和迂回的方式来搪塞，尽管他们本身是对的。（典型学者掌握着一些关于此问题的复杂、晦涩、形式化的答案，但由于他们自身的晦涩表述，却未能意识到这些答案恰恰就是普通人的第一反应。）没什么好看的，继续前进吧。 与此同时，Curry-Howard对应 (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)，远非两个先前无关的事物之间神秘的相似性，它仅仅是承认：那些嫁接到编程语言上的类型系统，只是重新引入了之前从这些语言中剥离掉的一些关系逻辑。 这些不太光彩的总结给我们的教训是：最好先找出问题的根源 (https://sifter.org/~simon/journal/20121123.h.html)。纠正先前的错误，总是比为其打补丁要好。 这与“类型”概念息息相关，因为它承载了太多包袱（部分是为了解决上述那些并非真正问题的问题）。它似乎非常重要，承载着很多重量，是“正确性”和代码分解（如类）等概念的核心。因此，暗示它并非必要或有用，表面上看似乎有点荒谬。 但我们只需梳理一些历史，更简单地重建事物，就能得到一个更简单、更通用的概念。（消除已学之物竟比学习新知耗时更长，这令人不安。我感觉自己整个职业生涯都在努力清理大脑中那些本应被视为理所当然的垃圾。） 首先，正如在《类型理论之倦》中所指出的，“类型”的几乎所有功能，都可以轻而易举地被一个恰当的关系表示所涵盖。也就是说，与其说类型是一个无用的概念，不如说它是一个已存在的概念：类型，以其最一般的形式，等同于关系成员资格。我在这里混合了两种范式（关系逻辑、集合成员资格）只是为了避免对论点过度约束：可以称之为集合成员资格，也可以称之为谓词函数上的真值，这无关紧要——它是一个常见且直观的概念。“水果”是一个“类型”。“大于Y的值”也是一个类型。我们倾向于认为前者是类型而后者不是，主要出于实用性原因（后文将述），但它们在认识论上是同一种结构。 历史上，“值”与“类型”的关键分野在于：值是程序运行时可以可靠计算出的东西。类型是程序编译时可以可靠计算出的东西。这里的关键在于，计算的表示和规则*可以*在这里被完全统一（例如关系逻辑），但历史上并未统一，这是因为这两组东西在实际应用中的角色不同。 此外，随之而来的是，如果我们开始模糊编译与执行之间的界限，这种实践性的边界也会瓦解，我们立即能更好地通过完全放弃它并坚持单一、统一的表示来受益，这种表示不区分类型和值。 因此，这就是我反对将类型视为特殊构造的论点，体现在多个方面：我们通常用类型所做的一切仍然存在，只是现在作为普通的事实和规则存在于关系逻辑中，与其他所有事物处于同等地位。 但有一个重要的例外。我认为，正是这一点，使得“类型”（作为一个特殊构造）的概念得以锚定，避免了早已飘然远去： 当我们重新审视我上面的定义，即*类型是程序编译时可以可靠计算出的东西*，这意味着别的东西：它是程序编写时已知的东西。也就是说，它是程序员本人所知道的。诚然，它只是已知信息的一个子集——这再次强烈暗示我们最好转向更通用的表示。但尤其重要的是，这是一个非常容易确定的子集：类型逻辑，通常来说，相当简单（如果我们剥离所有代码细节，只留下类型信息，那么即使类型尚未在各处显式声明，我们面对的也是一个非常基础的数据流问题）。而这个易于推断（在编写代码或编译时）的、关于我们关系真理的子集，为我们的代码创建了一个*隐式上下文*。这个上下文进而提供了“类型”最终、实际、虽然有些微不足道但确实特殊的功能：它让我们在语法层面消除*语言*的歧义。 例如，它让我们写下“length”这个词，并让编译器——就像程序员本人或阅读代码的人一样——知道我们指的是计数还是几何量。我应该在此强调，将这个问题留到运行时解决的代码应该是不可编译的：如果你在编写代码时都不知道你指的是哪种含义的length，那么你不知道你在写什么，编译器也不知道。不要将此与*派发*混淆，派发可能根据对象的具体情况以不同的方式执行计算。我们这里要解决的是我们正在计算*什么*（含义），而不是*如何*计算。 我们在实践中，例如C++或Java风格的静态类型中看到这一点，其价值仅仅是语言的压缩：允许我们在不同（尽管常常相似的）上下文中复用同一个词表示不同的含义。 在这里，重要且有用的一点是看清这个明确的功能划分： 基于静态类型的含义消除，*完全*是为方便交流而设的功能，实质上是语法糖，让我们通过在不同上下文中复用令牌来少写一点代码。这是一点点代码压缩，仅此而已。这就是“类型”所服务的唯一真正特殊功能。 但现在看到这一点后，我们不再需要限制什么可以算作类型，除了一个属性：它必须在编译时可确定（即在我们知道参数/数据之前，它本身在代码中就是显而易见的）。也就是说，原则上，我们可以使用*任何东西*作为上下文消歧器，无需将自己限制在整齐的类型层次结构之类的东西中。我们通常这样做，只是因为在设计一个规则或过程时，什么是通常容易确定的这一实践现实，以及我们的语言（包括自然语言和数学语言）是如何围绕此演化而来的。 其他一切——以及我们通常归因于类型的所有繁重工作——现在只是照常的关系逻辑。并未消失，并非无用，只是不再是特例。所有相同的模式仍然适用，只是现在没有了那条横亘中间的限制性分界线。