Ron Minsky：类型及其对软件的重要性

Jane Street 的许多工作都使用 OCaml，但我认为求职者不必一开始就是函数式编程专家或交易专家。我们的软件涵盖市场数据和交易、配置、监控、研究、清算、分布式系统和安全。

今晚我想谈谈静态类型和动态类型，而不是让这场常见的争论更加激烈。选择编程语言很难用科学方法定论：现实中的问题往往很复杂，需要多人花费数年时间解决。

让学生在一个学期里参与研究，比随机分配经验丰富的团队，用不同语言工作六年容易得多。因此我的论述主要依靠经验和直觉，带有我所做过工作的偏见，请大家审慎看待。

人们常把 Python、Lisp 和 JavaScript 等动态语言与易上手、快速编写脚本联系起来，同时认为静态类型语言严肃、快速，有时却不够友好。这些类别内部差异很大，从 Fortran、Java 到 OCaml、Haskell 和 Rust 都在其中。

Fortran 和 Lisp 都可以追溯到 20 世纪 50 年代。Fortran 因数值计算性能而闻名，Lisp 则为早期人工智能研究人员提供了灵活性。这些历史印象至今仍影响人们对语言的看法。

值是程序中流动的数据：整数、字符串、列表，或者在许多语言中出现的函数。变量是值的名称。同一个变量在不同调用中或执行过程的不同阶段，可以指向不同的值。

变量属于程序文本；表达式将变量和其他语法组合成计算。类型对值进行分类，例如整数、字符串和浮点数。即使在动态类型语言中，值也有类型。

按照我在这里使用的区分方式，静态类型还会给变量和表达式赋予类型。变量的类型约束说明它在各种执行情况下能指向哪类值；像 x 加 y 这样的表达式也有类型。

从历史上看，类型的一个用途是提高性能。在 Python 中，加法可能意味着整数加法、浮点加法或字符串拼接。运行时需要判断使用哪种操作；如果编译器已知操作数是整数，就能选择相应的机器操作。

动态运行时也可以花很大力气优化常见情况。编译器可以观察到操作数通常是整数，检查这一假设，再走快速路径。以我的经验，这些优化可能比较脆弱，代码变化后性能也就不那么容易预测。

类型还有助于人理解程序。它可以告诉程序员和协作者，什么样的数据会流经一个函数。这是性能之外的另一项好处，但并不意味着类型没有代价。

类型化程序可能更加冗长。举个具体例子：一个小函数接收浮点数，返回它的整数部分和余数。在 Python 中，返回一个数对就能把它写成很短的函数。

早期 Java 没有一种通用数对类型，能让两个元素分别采用不同类型，因此需要新建类、构造函数和访问器来表达结果。后来 Java 引入泛型，允许使用可复用的数对，这个例子也就短了许多。

类型系统的表达能力会影响额外代码的数量。如果不能直接表达一种自然的数据结构，程序员可能需要绕路。更好的抽象可以缩小差距，但无法消除所有取舍。

用 OCaml 实现同一个函数也很简洁。类型推断让编译器根据操作推导函数类型，因此程序员不必为每个变量写注解。编辑器仍然可以显示：它接收一个浮点数，返回一个整数和一个浮点数。

类型推断和表达能力强的类型可以减轻冗长问题，但类型化语言有时仍需要明确提供信息。它们也增加了学习内容：程序员既要理解计算本身，也要理解类型系统施加的约束。

再看求列表长度。Python 提供通用的长度函数，对整数求长度时会报错。OCaml 通常使用 List.length 和 String.length 等函数，需要更明确地指定对象。

Haskell 提供更通用的长度函数，可以处理可折叠结构。这种通用性很有用，但类型和错误信息也可能更难理解。不同类型系统在表达能力和概念复杂度之间作出了不同选择。

寻找合适的平衡是语言设计问题。类型系统应有足够的表达力，让程序简洁，同时也应容易理解，包括程序未能通过类型检查时给出的解释。有些语言在这方面做得比其他语言更好。

对于小任务，类型可能拖慢进度。写一个简短的 Python 程序，或许比在 OCaml 中先想清楚相应类型更快。如果某个类型系统无法自然地表达程序员想做的事，它也可能妨碍设计。

代价会随语言和任务变化。一些经验丰富的程序员会有意在某些工作中选择动态语言，因为它们让某些设计更容易实现，而特定的静态类型系统表达起来可能很别扭。这是实实在在的取舍。

我支持类型，首先是因为性能，但发现错误也很重要。人们有时只依据能力有限的类型系统来评判类型，低估了更丰富的系统可以表达什么。在 OCaml 等语言中，对缺失值的不同处理方式可以避免普通的空指针错误。

假设一个函数比较两个字典，报告两个字典都有、但值不同的键。一个 Python 版本错误地报告了只存在于第一个字典中的键：第二次查找返回 None，程序随后将它与已有值比较。

这看上去像逻辑错误，而不是典型的把浮点数传给要求整数的函数。但在 OCaml 版本中，查找返回的是 option。直接把 option 和整数比较，就无法通过类型检查。

修正方法是匹配两种情况：如果查找返回 None，就什么也不做；如果返回 Some value，就比较这个值。类型明确指出了值可能缺失，迫使这段程序处理这种情况。

这个小例子无法展示大规模工作中的所有好处，但它表明，有用的类型系统捕获的不只是基本类型不匹配。经过仔细设计，它也能暴露涉及计算含义和结构的错误。

类型签名还可以传达信息。与普通文字文档不同，类型会与程序一起接受检查，因此代码变化时，它不会以同样的方式悄悄过时。信息更丰富的类型可以传达使用者需要了解的更多结构。

类型还能指导重构。修改系统的一处后，类型检查器会指出其他不再匹配的地方。实习生有时会惊讶：做了大量改动，并逐一解决随之出现的错误之后，程序居然仍然能运行。

并非所有类型系统都同样擅长这件事。类型也可以编码不变量，也就是程序演进过程中应始终成立的事实。计算机能检查这些事实后，程序员就可以把更多注意力放在它无法检查的问题上。

工具也能从类型信息中受益。理解程序结构的工具可以提供代码导航、补全等帮助。这也是类型在 JavaScript 生态中越来越受重视的原因之一。

不要用遇到过的最弱类型系统来评判所有类型系统。Python 与 Java 的比较并不能涵盖全部设计空间。可以探索其他语言，但要记住：快速易用的脚本和大型、对正确性要求很高的系统，可能需要不同的选择。

关于证据，我不会自称社会科学专家。挖掘开源代码库也许能为真实工作提供有用线索，但不同项目和程序员对语言的选择并非随机。这些选择偏差很难消除。

针对初学者错误的研究，也可能得出与经验丰富的程序员需求不同的结论。建议撤销最小改动，对新手也许合理；但经验丰富的开发者可能正是有意作出这项改动，更希望获得如何更新其余代码的指引。

我特别看重的功能之一是类型推断：它减少使用阻力，同时保留类型系统的其他好处。类型推断在越来越多的语言中出现，C++ 和 C# 也有相应形式。

另一个是代数数据类型，尤其是和类型。积类型把字段组合在一起，表示“这个并且那个”；和类型描述不同选择，表示“这个或者那个”。结合穷尽的情况分析，它能直接建模不同的可能性。

好的语言理念进入主流可能需要很长时间。垃圾回收出现了几十年才在主流语言中普及。2017 年，我认为和类型也有类似的问题：尽管很实用，使用仍然不够广泛。

有人问 Jane Street 使用 OCaml 的方式如何改变，我会先从语言本身说起。一等模块让我们把模块系统中的单元和接口作为值传给函数或存入数据结构，从而写出更清晰的模块化程序。

广义代数数据类型，也就是 GADT，后来也展现出我们没有预料到的用途。它看上去主要是给编译器作者使用的功能，但我们发现它在系统编程和需要控制内存布局的高性能代码中同样有价值。

我们也更擅长类型驱动设计：在库接口中放入更多不变量和结构，让库更容易理解、正确使用和修改。一个限制也可以视作关于库应如何使用的共享知识。

早期 OCaml 系统规模还不大，即使我有很多东西要学，也能把它们建起来。随着组织扩大，这门语言相对冷门的代价也显现出来。我们投入文档、编辑器功能、编译器和优化工作，还建立了专门的工具与编译器团队。

我希望有一门具备这些功能的主流语言，设计时不必过度受既有生态系统的牵制。Scala、F# 和 Swift 融合了不同领域的理念。集成带来了好处，但这种组合也可能增加复杂度。

我认为 OCaml 相对独立，因而设计更简单：它与 Unix 和 C 集成，而不是深度融入大型托管生态系统。当然，这种选择也有代价，加入 JVM 这样的生态系统有明显好处。

设想一个高吞吐量的数据包处理系统：内存区域直接从网卡接收数据。程序读取位、修改结构、重复操作，而不是为每条消息分配新对象。挑战是让这种底层结构依然容易编程。

GADT 可以让程序逐步细化已知信息：首先知道字节包含 TCP 数据包，接着知道包里是 Nasdaq 消息，最后知道这条消息代表添加订单。接口可以像层层嵌套的选项和组合字段一样自然，同时避免传统表示可能需要的分配。

渐进式类型带来相关的设计挑战：如何在保留现有动态语言习惯用法的同时，为它增加静态检查？最终结果必须协调两种风格，细节可能变得复杂。

Typed Racket 是一个出色的例子。Racket 的数值塔允许算术运算自然地在整数、大整数、有理数和复数之间转换。要精确建模这些行为，类型系统可能变得极其复杂，包括许多不同的数值情况。

静态类型系统是保守的近似，因此一些动态语言习惯用法不容易纳入其中。有些渐进式类型系统有意接受不健全性，以便更容易采用并改善工具支持。这是重要的妥协：如果编译器无法信任类型声明，就不能以同样的方式安全地依赖它进行优化。

我的经验法则是：类型化语言可能在小规模任务中拖慢速度，却能在大规模工作中提高速度。Jane Street 也会花时间进行审查和质量控制，尤其是会向交易所发送订单的软件。这是另一项有意偏向正确性的选择。

如果参加一场短期交易竞赛，参赛者可能只有 12 小时针对模拟交易所建立原型，我通常会推荐 Python。对于 Jane Street 生命周期更长的系统，我当时主要在 Java 和 OCaml 之间选择，而我发现 OCaml 做这类工作更快、更容易。

类型不能取代测试。它们可以自动捕获部分错误，减少需要手工检查的情况，但重要行为仍然需要测试。Jane Street 投入了许多精力降低测试基础设施的使用难度，因为阻力会让人们不愿做必要的测试。

对于一些简单、类型正确的程序，少数例子似乎就能让行为清晰起来。这并不能证明所有 bug 都已消失。更准确地说，类型可以充分约束行为，使精心选择的测试更有效。

一种常见的不变量涉及字段之间的依赖。如果对象的标签表示情况 A，可能必须填写一个字段；如果是情况 B，则需要另一个字段。单靠积类型无法干净地表达所有这种关系，但和类型能把每种选择与它所需的数据绑定在一起。

这些数据约束也可以表示程序状态的事实：例如，某个状态可能要求会话标识符已经建立。把这种关系编码进去，可以减少必须靠人工维持的协调工作。

另一个例子是区分不可信的用户输入与已经为数据库做过引用处理的字符串。使用不同的抽象类型，可以要求显式转换之后，函数才接受需要引用处理的数据。类型检查器由此帮助程序在各处追踪这一属性。这个例子说明的是类型层面的不变量；安全访问数据库仍取决于正确使用查询和转义机制。