2026年8月21日 [一般类型理论 集合论 记忆] 随着人们年龄的增长，他们变得更聪明，或者至少他们自己认为如此。然后，他们就有责任将积累的智慧传授给年轻一代。莱斯利·朗波特因其在分布式系统和容错方面的成就而闻名。对许多人来说，他更为人熟知的是LaTeX的作者，这是一个让唐纳德·克努斯传奇的TeX排版系统能够为我们其他人所用的著名宏包。随着莱斯利逐渐年迈，他感到有必要写一系列相当古怪的论文，标题如《如何写一个长公式》。另一篇论文被称为《类型被认为是有害的》，这是对规范语言中类型的抨击。这个标题回响了艾德斯杰·迪克斯特拉的一封著名信函，“go to语句被认为是有害的”，该标题（由期刊编辑选择）随后被许多反对许多事物的作者借用了。莱斯利反对类型。但我又是怎么参与进来的呢？ 类型被认为是有害的 莱斯利的论点是，规范语言应该基于无类型形式（某种集合论），而不是有类型形式。他提出了几个支持的论点：无类型形式更灵活；有类型形式会引发许多异常和问题；在验证过程中，我们所认为的规范中的类型错误无论如何都会被检测到。这个论点有一定道理。在1992年，类型系统正处于变革之中，当时这篇笔记被写成。Coq（现在是Rocq）刚刚出现，而马丁·洛夫类型理论也在发生重大变化。至于简单类型理论，早期的HOL实现仅存在了两年左右。任何有类型的演算能够做什么都不清楚。证明助手尚未支持类型类。约翰·哈里森距离引入他获得低预算依赖类型的技巧还有几年，这一技巧足以表达$T^n$。另一方面，朗波特的笔记一团糟。他似乎对任何实际的有类型形式并不熟悉，并且将大部分笔记用于打击稻草人。当他将笔记提交给TOPLAS出版并送给我审稿时，我的判决是拒绝。另一位审稿人大卫·麦克阿尔斯特也得出了相同的结论。本该如此，但编辑安德鲁·阿佩尔有其他想法。“让它更美观”辩论是好的，他说。这些思想值得公开讨论，或者类似的事情。但我们不能在TOPLAS中允许错误。你为什么不和朗波特一起作为共同作者，把论文转变成技术上准确但保持相同精神的东西？我乐意尝试：我对类型系统有一定了解，我还有自己的无类型集合论形式（Isabelle/ZF），很高兴宣传。大卫稍微支持了一下，但很快就退出了。他很聪明。1 莱斯利和我在论文上工作了很长一段时间。这是一种奇怪的非自愿共同创作，但我们还是设法完成了。新论文捕捉到了莱斯利论点的核心，同时包含了更理智的类型运作描述。在此过程中，我亲眼见证了莱斯利无与伦比的TeX精通：一些我从未见过的低级技巧。第二轮评审，天哪 与此同时，安德鲁·阿佩尔辞去了TOPLAS编辑一职。新编辑卡尔·冈特并未获知这篇论文的特殊状态。因此，当论文送到他那里时，他将其送给了新的审稿人。这并非计划的一部分。而新审稿人也决定拒绝这篇论文。其中一份报告混乱不堪。显然，作者在写论文时正遭受一场癫痫发作。那么我联系了卡尔，说等一下，我的拒绝毫无价值，而这个人的拒绝怎么就有效了？而且，他简直就是在发狂。最终，这篇论文还是发表了，附有免责声明，表达对热烈辩论的期望，等等等等等等。我不确定辩论是否真的发生过。回顾 而现在，我们可以问莱斯利的论点在27年后是否依然成立。可以公平地说，远没有那么好。类型系统已经有了相当大的发展，并且在许多规范和验证任务中证明了其价值，其中一些是工业规模的。CompCert验证的C编译器seL4：“全球最可靠和最快的操作系统内核”亚马逊的Nitro隔离引擎。与此同时，在困扰集合论形式的问题上进展甚微。没有类型就没有符号重载，这在理论上是微不足道的（你只需使用很多不同的符号），但在实践中却是个大问题。而且更糟糕的是，能够写出绝对任何东西大多是个犯错误的邀请。验证是一种极其昂贵的发现此类错误的方法，而那些你没有发现的错误可能会使你的证明毫无价值。就我所知，即使是朗波特自己规范语言（TLA+）最终也实施了一些类型限制。所以，实际上，你的规范语言可能应该