Richard Eisenberg 谈依赖类型、OCaml 与 AI 辅助编程

Ron Minsky 介绍了 Richard Eisenberg：他是 Haskell 的资深贡献者、GHC 指导委员会成员和 Haskell Foundation 主席。Eisenberg 已加入 Jane Street 的工具与编译器团队，负责 OCaml 编译器前端的工作。

Eisenberg 在中学任教之后，准备攻读编程语言研究生时首次接触 Haskell。依赖类型让他大为震撼：表达能力足够强的类型可以在实现之前描述预期的程序，让编译器检查实现是否符合要求。

被问及如何通俗解释时，Eisenberg 从效果而非定义说起。只要规格设置得当，支持依赖类型的语言就可以将正确性证明编码进程序，并在每次编译时检查该证明。

以整数列表排序为例。从整数列表到整数列表的函数，这种描述过于宽泛。要求输出按非递减顺序排列更好，但始终返回空列表的函数也满足这一条件。

更完整的规格要求输出既是非递减的，又是输入列表的一个排列。不同的排序算法都能满足同一个类型，编译器可以检查它们的证明。这是依赖类型，因为所要求的输出依赖于具体的输入。

当时 Haskell 还没有完整的依赖类型，但它富有表现力的类型系统吸引了 Eisenberg。在宾夕法尼亚大学，他先后与 Stephanie Weirich 和 Simon Peyton Jones 合作，开始共同研究 Haskell 及其编译器。

他对语言的兴趣更早就萌生了。他小时候学过 BASIC，大约 12 岁时买到一个 Pascal 编译器。他以为手册包含所需的一切，于是花了数小时研究语法图，自学了编程。

后来，Norman Ramsey 的一门编程语言课程重新点燃了他的兴趣。Eisenberg 先在中学教书，之后回校攻读博士。研究期间，他希望编译器支持一个依赖类型的想法；Peyton Jones 鼓励他自己实现，两位合作者都给予了指导。

在 Bryn Mawr College，Eisenberg 可以将开源贡献与学术论文一同计入成果。这让他在研究和教学的同时继续开发编译器，但兼顾三者很不容易。多年教学之后，他决定转向另一个方向。

他加入软件咨询公司 Tweag，继续研究 Haskell 并为编译器做贡献。后来，他希望加入一支紧密协作的团队，并体验另一门语言。Minsky 邀请他加入 Jane Street，最终时机成熟，整个过程大约花了 11 个月。

Eisenberg 最初因自己对金融业的印象以及往返纽约通勤的问题而犹豫。后来他发现这个职位很有吸引力：它包括开放语言的开发和对更广泛生态的贡献，延续了他此前十年的研究兴趣。

Minsky 回到依赖类型的实际成本。证明可能很难构造，定理证明系统也需要大量工程工作。他问，如果证明成为日常编程的一部分，这个过程能否足够方便，同时不妨碍其他工作？

Eisenberg 说，社区仍在努力回答这个问题。他的原则是，高级特性应当可以按需选择：即使语言支持依赖类型，程序员也应能编写简单的列表到列表排序函数，而不必证明每一项性质。

是否证明某个性质，需要权衡成本与收益。证明需要投入，但对于重要且容易出错的组件，它可能减少测试、调试或严重故障的风险。经验与判断有助于确定哪些地方值得获得额外保障。

Minsky 将这称为按需付出：从相对简单的语言开始，需要时再增加能力，而不是让每项工作都承担复杂性。Eisenberg 同意，要维持这一界限很困难；他的 Haskell 工作旨在增加依赖类型特性，同时保留编写简单程序的能力。

在 Jane Street，Eisenberg 更广泛的目标是利用类型组织思路和程序。规格可以在实现之前澄清意图，并让编译器检查实现。理想情况下，检查发生在编译期，而不是在运行时给用户带来成本。

他的具体项目是非装箱类型。想象一条交易记录嵌套在其他结构中：如果采用简单的装箱表示，访问内部字段可能需要依次跟随多个指针，造成缓存未命中。目标是在支持有用的类型结构时，不必承担这一连串分配和间接访问。

Minsky 解释，OCaml 的传统表示有意保持简单：值通常是机器字大小的立即值，或者是堆上分配的块，后者包含一个头部和若干机器字大小的槽位。Eisenberg 认为某些类型结构由此产生的运行时成本是语言设计问题。

Minsky 澄清，非装箱类型并不会让性能细节消失，而是把某些表示方式的选择明确放到类型层面。Eisenberg 同意：程序执行仍有物理模型，程序员需要足够的信息才能设计快速的数据表示。

Minsky 对比了自动优化和性能工程。编译器改进若能让大多数程序快 20%，就是巨大的普遍收益；而给予程序员精确控制，有时能让某个程序快 5 倍、10 倍甚至 100 倍。两种方法都重要，但作用范围不同。

Eisenberg 认为抽象与控制之间始终存在张力。高级语言让程序员不必逐条编写机器指令，但如果隐藏过多执行细节，就可能妨碍性能工程。编译器应利用少量有用的提示生成高效代码，而不必暴露所有底层细节。

非装箱类型也面临按需付出的挑战。Eisenberg 解释，它们可能干扰多态：通用的列表长度函数依赖一个可以代表多种元素类型的类型变量，但某些非装箱表示不符合相同的统一假设。

团队必须找到办法，在物理布局不同的情况下保留有用的多态算法。随着实验推进，他们预计会发现不再适用的编程模式，并想办法绕过这些问题。代码生成可能是解决方案的一部分。

Minsky 解释了其中的机制：使用统一的装箱列表表示时，一段代码就能遍历形状相同的节点。不同的非装箱布局可能需要不同的机器指令，因此恢复多态可能需要针对多种表示生成代码。

Eisenberg 说，当时最好的想法是在编译期生成所需代码。这可能排除一些潜在的编程惯用法，但他预计实际用户很少需要它们。设计仍然很难，团队还需要积累使用经验。

Minsky 将这个项目与 Rust 相比较：Rust 同时提供类型安全和底层内存控制。Eisenberg 强调了一个重要区别：Rust 放弃了垃圾回收。对于许多程序，包括不以微秒级延迟为关键的编译器代码，自动回收非常方便。

Rust 的内存模型要求程序员在整个程序中考虑分配和释放。Eisenberg 希望 OCaml 在大多数应用中保留垃圾回收模型，同时在需要时提供更精细的控制。从这个意义上说，团队正努力保留按需付出的原则。

Minsky 质疑按需付出是否总是最优。渐进类型系统可能因为混合有类型和无类型代码而增加复杂性；有时统一的选择更简单，比如在整门语言中使用类型。对某些应用来说，在所有位置明确控制内存也可能更合适。

Eisenberg 将目标重新表述为多种容易互操作的模式。一个文件或包可以使用普通 OCaml 内存表示，另一个则要求更严格的控制。多语言系统也在解决类似需求，但语言之间的连接可能很困难，每种组合都有自己的问题。

一种可能的设计是让装箱成为显式操作，在普通代码中自动插入。编译器设置可以关闭自动装箱，要求每次分配都显式提出。Eisenberg 强调，这只是一个供实验的想法，并非确定的设计，而且垃圾回收仍会存在。

Minsky 指出 Jane Street 并不拥有 OCaml，必须说服上游维护者接受修改。Eisenberg 认为这种关系有益。OCaml 起源于 Inria，Jane Street 既受益于社区工作，也向社区回馈自己的想法。

团队可以先在内部实验，对设计建立信心，再与更广泛的社区合作，判断它是否适合进入供所有人使用的 OCaml。Eisenberg 以 OCaml 5 的多核支持为例：这项大量工作主要在 Jane Street 之外完成，但公司可以从中受益。

开放协作也能改进具体的修改：Eisenberg 描述了自己向上游提交编译器改进后，从公司外部人员那里获得更好想法的经历。Minsky 将这种流程与 Haskell 开发作比较，后者的早期设计和评估与开源社区结合得更紧密。

Eisenberg 说，内部环境能让团队在语言特性触及成千上万用户之前进行实验。一项公开特性一旦广泛使用，即使设计有缺陷，修改它也可能破坏程序：不喜欢该特性的用户可能仍依赖它，而其他人则可能非常重视它。

在 Jane Street，工程师可以引入特性、从内部使用中学习，再对整个代码库作协调一致的修改。一次“tree smash”可以统一更新代码。他以局部类型和栈分配为例，说明设计如何在使用之后、提交上游之前得到修订。

Minsky 询问，内部测试是否可能让特性过度拟合 Jane Street 的特殊需求。Eisenberg 同意这是实际问题。团队会尽早征求公开反馈，包括向社区介绍非装箱类型和局部分配，以检验这些想法是否有更广泛的价值。

Eisenberg 在学习 OCaml 的同时仍活跃于 Haskell 社区。他注意到的一个区别是接口的位置：Haskell 程序员通常把类型签名放在函数旁边，而 OCaml 常将模块接口放在另一个文件中。他怀疑这会影响文档习惯。

Haskell 的类型类允许一个函数名代表多种操作，这可能让一连串表达式更难理解。OCaml 往往更明确地表明运行时执行的操作。Eisenberg 谨慎地概括：Haskell 常在编译期展示更多信息，OCaml 则常在运行时展示更多。

惰性求值是另一个区别。Haskell 可以推迟计算，直到需要其值时才执行，这可能避免一些工作，却让性能更难预测。OCaml 通常立即执行计算，因此更容易从代码中看出大致的执行顺序。

Minsky 质疑标注和文档的差异究竟来自语言本身还是社区文化。OCaml 允许添加更多标注，接口文件也是放置注释的自然位置。Eisenberg 承认，比较两个编译器可能影响了他的印象：它们的旧代码写于如今的编程实践形成之前。

两门语言处理扩展的方式也不同。Minsky 认为 OCaml 相对保守，而 Haskell 更愿意实验，并通过 pragma 启用特性。Eisenberg 说，他上次统计时 GHC 大约有 150 个扩展，理论上形成了巨大的配置空间。

Eisenberg 将这归因于 Haskell 的历史：它曾是由多个编译器实现的标准。扩展让各实现保留共同核心，同时进行实验。OCaml 则有语言手册和主要实现，而不是同样的标准与多编译器结构。

如今 GHC 已占主导地位，Eisenberg 认为旧扩展系统的理由没有以前充分。用户可能需要写很长的标志列表，新手也难以区分成熟、实验性和有问题的扩展。GHC 指导委员会正在讨论一种更易使用、同时保留向后兼容性的组织方式。

Eisenberg 希望有一个更统一的标准语言，也许可以把实际选择从约 150 个扩展减少到少数几个。他并不指望完全消除扩展：Haskell 的用途太多，直接取消这一机制可能造成社区分裂。

Minsky 转向 AI 辅助编程。Eisenberg 认为这是重要的一步，但不意味着编程语言设计的终结。编程语言是人与计算机之间、人与人之间进行精确沟通的媒介；生成代码又增加了计算机向人沟通的方式。

人仍需要阅读生成的代码，判断它是否实现了预期。Eisenberg 长期主张语言设计应优先优化阅读体验，而非编写体验：简洁的符号也许很巧妙，但单词通常更容易搜索、学习和理解。

如果计算机编写更多代码、人编写得更少，对可读性的要求就会增加。未来的表示方式可能更丰富、更结构化，但 Eisenberg 将其视为精确沟通演进的另一个阶段，而不是抛弃一切、从头开始的理由。

依赖类型可以为 AI 生成的实现提供精确规格。排序例子说明措辞为何重要：输出必须是输入的一个排列，按非递减顺序排列，并包括重复元素。模型可以根据这一规格生成代码，然后检查结果。

Minsky 怀疑人们是否会经常编写精确规格，因为这很困难；他建议让模型起草规格，再由人审阅。Eisenberg 同意起草很难，但提醒说，人仍必须理解并验证规格，否则系统就失去了与预期结果的联系。

Minsky 指出阅读也很难。在代码审查中，有价值的交流常从审查者看不懂杂乱的实现、要求简化开始。AI 助手能否生成真正容易理解的代码，仍是一个开放问题。

Eisenberg 补充说，如果能够严格检查实现是否符合简单而精确的规格，那么实现本身是否简单，对正确性的影响可能就没那么大。依赖类型是一种可能的机制；精化类型和其他方法也可以将规格与实现联系起来。

两人讨论了将语言作为与 AI 助手协作的中间表示，以建立对结果的信心。Eisenberg 认为，当时人们与助手的交互才经历了几个月的快速变化，围绕这种交互从头设计语言还为时过早。现有语言已经支持精确沟通，因此仍是有用的起点。