OCaml 编译器 - 2021年5月
我很高兴发布“OCaml 编译器开发新闻通讯”的第二期。(这绝非详尽无遗:许多人最终没有时间撰写内容,这也没关系。)
当然,欢迎随时发表评论或提问!
如果您一直在开发 OCaml 编译器,并且想说些什么,请随时在本主题中发布!如果您希望我在下次准备新闻通讯时与您联系(未来某个随机时间点),请通过电子邮件告知我(gabriel.scherer at gmail)。
上一期
Gabriel Scherer 和 Nicolas Chataing(@gasche 和 @nchataing)
[Gabriel 撰写] 我最近与我的实习生 Nicolas Chataing 开展的主要与编译器相关的活动是正在进行的实现变体构造函数拆箱原型的工作,这是 Jeremy Yallop 提议的核心子集(https://github.com/ocaml/RFCs/pull/14)。目前 OCaml 可以“拆箱”一个变体,如果它只有一个构造函数(带有一个参数),
type t = Int of int [@@unboxed]
Jeremy 的想法是支持存在其他构造函数的情况,但构造函数参数的标签(立即值或块构造函数标签)与该类型任何其他值的标签不重叠。
type t = Short of int [@unboxed] | Long of Mpz.t
Nicolas 的原型实现进展顺利,遇到并解决了一些有趣的挑战,并在此过程中进行了一些重构 PR(#10307、#10412、#10428)。
一个关键要素是能够计算 OCaml 类型的“头部形状”,即其值的可能标签集的过近似。我们在执行此操作时遇到了一些工程和研究问题。这应该在代码库的哪个位置计算(注意循环模块依赖关系)?在存在互递归类型的情况下,我们能否以精确的方式计算此信息,而不会冒非终止的风险?
我们从 Leo White 和 Stephen Dolan 提出的通用方法中汲取灵感,该方法建议按需计算这些类型的“类型声明属性”,而不是作为类型声明签名的一部分(请参阅他们对 #10017、#10041 中“立即性”的提议),但我们的属性被更频繁地请求(构造函数的任何出现)并且更细粒度(它对类型参数敏感),因此我们不得不为新问题发明一些解决方案。(一个紧密相关的例子是 get_unboxed_type_representation
,它通过使用燃料避免非终止,我们想要一些比这更好的东西。)
我们在以下简短摘要中讨论了我们对终止的处理(某些)细节:在没有循环的情况下展开 ML 数据类型定义。
Xavier Leroy(@xavierleroy)
我与 Damien Doligez 和 Sadiq Jaffer 合作研究了“安全点”提案(#10039),这是推进集成 Multicore OCaml 所必需的。我将支持插入轮询的静态分析重新表达为反向数据流分析,使它们更容易理解和更健壮。我们还讨论了是否在循环顶部或底部插入轮询。这两种策略都在 PR 的当前状态下实现,Sadiq 目前正在对它们进行基准测试。
所有这一切都重新激发了我对数据流分析的兴趣。我编写了一个通用的反向数据流分析器,它由抽象域和转移函数参数化(#10404)。最初,我打算仅将其用于插入轮询,但我也使用它来重新实现活动性分析,该分析在寄存器分配和死代码消除中起着至关重要的作用。旧的活动性分析的一个问题是,它花费的时间随循环嵌套呈指数增长。新的通用分析器通过避免系统地从抽象域的底部开始不动点迭代,而是从之前找到的不动点开始(如果有),从而避免了这个陷阱。这使得活动性分析在循环嵌套方面呈线性增长,并且在最坏情况下在函数大小方面呈三次方增长,而不是指数增长。
然后,我将相同的技巧应用于这两个预先插入溢出和重新加载的传递(#10414)。这些是“分析和同时转换”传递,因此我无法使用通用数据流分析器,但我可以重用相同的改进不动点迭代策略,再次避免在循环嵌套方面呈指数增长的行为。例如,一个由 16 个嵌套的“for”循环组成的简单函数现在可以在几毫秒内编译完成,而之前则需要几秒钟。
Jacques Garrigue(@garrigue)
本月没有新的 PR,但我一直在处理 4 月份开始的尚未合并的 PR
- #10348 改进了统一期间扩展的方式,以避免一些虚假的与 GADT 相关的歧义错误
- #10364 更改了模式匹配情况主体类型,允许在某些非主要情况下发出警告;它还发现类型检查器内部的一些与主要性相关的错误
- #10337 通过将 type_expr 设为抽象类型(与 Takafumi Saikawa(@t6s)合作)来强制始终操作类型的规范视图
对于最后一个 PR,我们有趣地观察到,虽然这将对 repr 的调用次数增加了高达 4 倍,例如在 stdlib 中导致 4% 的开销,但我们没有看到 Coq 编译性能下降。
我还发现了 GADT 实现中的一个新的主要性错误(再次参见 #10348),幸运的是,这应该不会影响健全性。
在稍微不同的方向上,我开始致力于一个面向 Coq 的后端:https://github.com/COCTI/ocaml/tree/ocaml_in_coq
如果您在 ocamlc 中添加 -coq 选项,您将获得一个 .v 文件而不是 .cmo 文件。它仍处于非常早期的阶段,只能编译核心 ML 程序,包括引用。与 coq-of-ocaml 的主要区别在于,翻译旨在保持健全性:生成的 Coq 代码可以在没有公理的情况下进行类型化和评估,并且应该简化为与源程序相同的 resut,以便 Coq 的类型健全性保证 ocaml 的类型健全性(对于单个程序)。在这一点上,它仅依赖于对 Coq 正性限制的单一放松。
Thomas Refis(@trefis)
最近,Didier Rémy 和我一直在研究模块化显式,这是一种介于核心语言和模块语言之间的小扩展,有助于操作一等函子和通过一个新的构造(暂定)称为依赖函数在核心语言中提供对模块参数的抽象错觉。
此构造最初是在模块化隐式提案的背景下引入的;大致来说,如果您删除该提案的“隐式参数解析”部分,您将得到它。
因此,它是迈向模块化隐式的自然垫脚石,并且已经拥有自己的独立 PR:#9187,由 Matthew Ryan 贡献。
Didier 和我最近一直在关注的是,对该功能及其与一等模块的关系进行更正式的描述,以及一些论点来证明在没有模块化隐式的情况下,将其添加到语言中是合理且可取的。
Stephen Dolan(@stedolan)
我刚刚打开了 #10437,它允许在签名和 GADT 中对类型变量进行显式量词,这是我十几个月前向 OCaml 维护人员承诺的一个小功能。(最终动机是这些显式量词提供了一个放置布局信息的好地方,但我认为它们本身就值得拥有)。
注意:Gabriel 上面提到的 #10017 / #10041 中的按需立即性提案是从实验分支 https://github.com/janestreet/ocaml/tree/layouts 中的类型系统的一部分提取的,该分支还允许对具有给定立即性/布局的类型进行量词:例如,可以编写 type ('a : immediate) t = { foo : 'a }
并让推理等按预期工作。
Sadiq Jaffer(@sadiqj)
安全点 PR #10039 有了一些更新。它现在有一个新的静态分析,由 Xavier Leroy 和 Damien Doligez 编写,并且在所有 64 位平台上都有可工作的代码发射器。
静态分析在循环中对轮询放置具有一定的灵活性。我们已经在 amd64 和 arm64 上进行了基准测试,选择使用在 Sandmark 套件中导致指令和分支略少的选项。除了某些重构之外,我认为 PR 没有其他未解决的问题。
基于安全点,我很快就会有一个属性要提出,这将使具有原子代码块的用户能够安全地迁移到具有安全点的 OCaml 版本。一个草稿 PR 或 RFC 将很快发布。
我还对检测运行时进行了一些工作。该项目的目标之一是能够持续监控在生产环境中运行的 OCaml 应用程序。为此,我正在评估检测运行时的性能开销(启用和禁用),确定减少开销需要哪些工作以及我们如何修改运行时以持续提取指标和事件。
Anil Madhavapeddy(@avsm)
Ewan Mellor 和我正在开发一个 CI,它将使测试对 OCaml 编译器的单个更改集并针对一组 opam 包运行“反向依赖项”变得容易,以精确隔离导致失败的原因。
构建 opam 包可能会遇到各种原因导致失败。这可能包括针对稳定发布的编译器的构建失败,也可能仅在 OCaml 主干上失败(但在发布的编译器上成功),或者仅在 OCaml 主干 + 相关 PR 上失败。我们新的 CI 侧重于对导致包构建失败的这些情况进行分类。拥有这个 CI 应该能够让我们快速确定 PR 的影响以及对包生态系统的潜在回归。一旦 CI 在 OCaml 多核树上稳定下来,我计划将其提交为一个 CI,以针对主线 OCaml 运行。
工作树位于 ocaml-multicore-ci(尽管它被称为“多核 CI”,但实际上它变成了“ocaml-compiler-ci”,我们将在第一次发布之前重命名存储库)。
Florian Angeletti (@Octachron)
本周我一直在做一些工作,为 #10361 中类型声明的基于差异的错误消息添加交换和移动操作。
(以及 OCaml 4.13.0 的第一个 alpha 版本的发布)
PR 的核心思想是在错误消息中比较
type t = { a:int; b:int; c:int; d:int }
与
type t = { a:int; c:int; d:int }
时,最好注意到缺少一个字段,而不是尝试比较字段 b
和 c
。
并且使用为函子差异引入的机制,这很容易实现。我从去年 12 月就开始尝试这个选项,并且随着函子差异 PR 的合并 #9331,我在 4 月份提出了一个 PR #10361。
然而,与函子相比,在类型声明中,我们有一个补充信息:给定位置的字段和构造函数的名称。不使用此信息会导致略微笨拙的错误消息
module M: sig type t = { a:int; b:int } end = struct type t = {b:int;
a:int}
1. Fields have different names, x and y.
2. Fields have different names, y and x.
这里,最好识别出这两个字段已交换。
一种无需增加差异复杂度即可实现此目的的简单方法是,在差异算法生成的最佳补丁上事后识别交换。
通过这种方式,我们可以将之前的错误消息替换为
1<->2. Fields x and y have been swapped.
而不会增加错误分析的成本。
当字段的位置在接口和实现之间发生变化时,也会发生类似的情况
module M: sig
type t = { a:unit; b:int; c:float}
end = struct
type t = { b:int; c:float; a:unit}
end
解释说,可以通过在字段 b
之前添加字段 a
并在 c
之后删除另一个字段 a
来将实现转换为接口是正确的。但总结问题的方式要好得多
1->3. Field a has been moved from position 1 to 3
现在已识别这两种复合移动。
对 OCaml 中的错误消息感兴趣的人也应该看看 Antal Spector-Zabusky 在 #10407 中完成的出色工作,以通过扩展完整错误跟踪来改进模块级错误消息。(这两个 PR 相互补充。)