嘿,又是一个新的团队公告。但我得承认:如果你关注了RFCs 仓库、Rust zulip,或者在GATs 稳定公告帖上特别细心的话,这**可能**不会让你感到惊讶。事实上,这个“新”团队早在去年五月底就已经正式成立了。
我们现在分享这篇帖子(而不是几个月前或……从未分享)有几个原因。首先,团队在去年十二月初完成了一次为期三天的线下/混合聚会,我们想分享这次会议的目的和成果。其次,现在发布此公告正值团队成立约 7 个月,我们很想分享在这段时间里取得的成就。最后,随着我们步入 2023 年的新年,这是一个分享我们今年及以后预期发展方向的好时机。
背景 - 我们是如何走到这一步的?
过去几年里,Rust 在用户、贡献者、特性、工具、文档等许多方面都取得了显著增长。随着它的发展,人们希望用它做的事情清单也同样快速增长。除了强大且符合人体工程学的特性外,对诸如 IDEs 或语言学习工具等强大工具的需求也变得越来越明显。新的编译器(前端和后端)正在被编写。最重要的是,我们希望 Rust 继续保持其核心设计原则之一:安全。
所有这些点都突显了一些关键需求:能够**知道** Rust 语言应该如何工作,能够相对轻松地通过新特性**扩展**语言和编译器,能够**接入**编译器并查询程序的重要信息,最后能够以易于接受且健壮的方式**维护**语言和编译器。多年来,我们在这些需求上投入了相当多的精力,但尚未完全实现这些关键要求。
更进一步,具体到数字上,目前大约有 220 个已接受但尚未完全实现的语言、编译器或类型特性的开放跟踪问题,其中大约一半至少有 3 年历史,许多甚至更久。这些跟踪问题开放如此之久,不仅是由于带宽不足,更是因为研究这些特性很困难,很大程度上是因为将相关的语义正确地置于更大语言的上下文中很困难;没有人能轻易看一眼就知道需要做什么来完成它们。很明显,我们仍然需要更好的基础来对语言和编译器进行修改。
另一个可能让你震惊的数字是:目前有 62 个开放的不健全性 (unsoundness) 问题。这听起来比实际情况可怕得多:几乎所有这些都是编译器和语言的边缘情况,是由专门进行探索和测试的人发现的;在实践中,这些问题不会出现在你编写的程序中。然而,这些是我们想要解决的边缘问题。
类型团队
接下来,我们不再讨论整个 Rust 语言和编译器,而是关注其中的一小部分。具体来说,这里相关的部分包括类型检查器——大致定义变量如何被赋予其类型的语义和实现,特质求解——决定哪些类型定义了哪些特质,以及借用检查——证明 Rust 的所有权模型始终成立。所有这些可以作为一个整体被认为是“类型系统”。
根据RFC 3254,上述 Rust 语言和编译器的子集现在属于类型团队的职责范围。那么,这具体意味着什么呢?
首先,大约从 2018 年起,就存在一个“特质工作组”,其主要目标是为 Rust 的特质系统(包括 Chalk 特质求解库)创建高效且可扩展的定义和实现。随着时间的推移,特别是在 2021 年下半年到 2022 年,工作组的影响力和职责自然扩展到了类型检查器和借用检查器——它们实际上密切相关,通常很难将特质求解器与另外两者分开。因此,在某些方面,类型团队实质上涵盖了之前的特质工作组。
另一个相关的工作组是polonius 工作组,它主要负责 Polonius 借用检查库的设计和实现。虽然工作组本身将继续存在,但它现在也属于类型团队的职责范围。
现在,尽管特质工作组实质上被合并到了类型团队中,但创建一个**团队**带来了一些好处。首先,像样式团队(以及许多其他团队)一样,类型团队不是一个顶级团队。它实际上(目前来说是唯一一个)拥有**两个**父团队:语言团队和编译器团队。这两个团队都决定将覆盖类型系统的决策权委托给类型团队。
语言团队委托了类型系统设计的某些部分。然而,重要的是,这种设计更多地涵盖类型系统“如何工作”,而不是特性的“感觉”,并期望类型团队在需要时就新的语言扩展提供建议并提出担忧。(这种划分没有严格定义,但通常期望更偏向谨慎)。另一方面,编译器团队委托了定义和维护特质系统实现的责任。
语言团队和编译器团队传统上共同承担的一项特定责任是评估和修复语言中与类型系统相关的不健全性错误。这些问题通常源于实现定义的语言语义,过去需要语言和编译器团队的同步和输入。在大多数情况下,类型团队现在有权在无需任何父团队直接输入的情况下评估和实施修复。重要的是,这适用于技术上**不向后兼容**的修复。虽然修复安全漏洞不在 Rust 的向后兼容性保证范围内,但这些决定不会草率做出,通常需要团队批准,并通过crater 工具评估潜在的生态系统破坏。然而,现在可以在一个团队内完成这项工作,而无需协调两个独立的团队,这使得弥合这些不健全性漏洞变得更容易(我稍后会详细讨论这一点)。
形式化 Rust 类型系统
如上所述,不断发展的 Rust 语言一个几乎必不可少的要素是知道它应该如何工作(并对此有完善的文档)。最近有一些推动 Rust 规范的努力(如 Ferrocene 或 这个开放的 RFC),但是,无论其是否可能集成到更通用的规范中,拥有类型系统的形式化定义将带来巨大的好处。事实上,形式化的存在将允许在没有编译器其余部分的微妙复杂性的情况下,更好地评估潜在的新特性或不健全性漏洞。
早在 2015 年,Rust 1.0 发布后不久,一个名为 Chalk 的实验性 Rust 特质求解器就开始编写。Chalk 的核心思想是将 Rust 特质系统的表层语法和概念(例如 trait、impl、where 子句)转化为一组逻辑规则,可以使用类似 Prolog 的求解器进行求解。然后,一旦这组逻辑和求解器与编译器本身的特质求解器达到一致,计划就是直接替换现有的求解器。与此同时(并继续前进),这个新的求解器可以被其他工具使用,例如 rust-analyzer,它目前就在使用 Chalk。
现在,考虑到 Chalk 的“年纪”以及曾寄予的期望,你可能会忍不住问一句:“Chalk 什么时候能就绪?”——很多人都问过。然而,多年来我们了解到,Chalk 可能不是 Rust 正确的长期解决方案,原因有几点。首先,正如本文中多次提到的,特质求解器只是一个更大类型系统的一部分;对整个类型系统如何协同工作进行建模,比试图分别建模各个部分更能全面了解其细节。其次,**编译器**的需求与**形式化**的需求截然不同:编译器需要高性能的代码,并能够跟踪强大的诊断所需的信息;好的形式化不仅要完整,还要易于维护、阅读和理解。多年来,Chalk 试图两者兼顾,但到目前为止,它都没有做到。
那么,未来的计划是什么?首先,类型团队已经开始着手形式化 Rust 类型系统,目前暂定名为 a-mir-formality。最初的实验阶段是使用 PLT redex 编写的,但正在进行 Rust 语言移植。还有很多工作要做(包括建模更多的特质系统、编写 RFC 并将其移至 rust-lang 组织),但它已经显示出巨大的潜力。
其次,我们已经启动了一项倡议,在源代码树内编写新特质求解器。这个新的特质求解器范围比 a-mir-formality 更有限(也就是说,不打算涵盖整个类型系统)。在许多方面,它预计会与 Chalk 非常相似,但会利用现有编译器和特质求解器的部分内容,以便使过渡尽可能顺利。我们确实希望它在某个时候会被移出源代码树,因此正在以尽可能模块化的方式编写它。在本月早些时候的类型团队聚会期间,我们已经能够详细讨论求解器的预期结构,并且我们已经将其合并到源代码树中。
最后,Chalk 将不再是团队的重点。短期内,它可能仍然是一个有用的实验工具。如前所述,rust-analyzer 使用 Chalk 作为其特质求解器。在 rustc 中,也可以通过不稳定特性标志使用它。因此,新想法目前可以在 Chalk 中实现并在实践中进行实战测试。然而,随着 a-mir-formality 和新的树内特质求解器变得更易用且其接口更易访问,这个好处可能不会持续太久。所有这些并不是说 Chalk 是失败的。事实上,Chalk 教会了我们很多关于如何以逻辑方式思考 Rust 特质求解器的知识,并且当前的 Rust 特质求解器随着时间的推移已经演变得更接近 Chalk 的模型,即使是不完全的。我们预计目前仍将以某种形式支持 Chalk,供 rust-analyzer 使用,并可能供那些有兴趣进行实验的人使用。
弥合不健全性漏洞
正如前面提到的,创建一个新的类型团队并获得语言团队和编译器团队授权的一个巨大好处是,团队能够大部分独立地评估和修复不健全性问题。然而,另一个次要的好处实际上是更好的流程和知识共享,这使得团队成员能够就存在哪些不健全性问题、它们为何存在以及需要如何修复达成一致。例如,在本月早些时候的聚会期间,我们能够回顾所有不健全性问题(重点关注与类型系统相关的问题),确定其原因,并讨论预期的修复方案(尽管大多数修复需要前面章节讨论的先决工作)。
此外,团队已经进行了一些不健全性修复,还有一些正在进行中。我不会详细说明,而是选择以列表形式列出:
- 考虑未规范化类型用于隐式边界 (Consider unnormalized types for implied bounds):在 1.65 版本落地,未发现回退
- 对于不透明类型的 well formedness,既不要求也不暗示生命周期边界 (Neither require nor imply lifetime bounds on opaque type for well formedness):在 1.66 版本落地,未发现回退
- 添加 IMPLIED_BOUNDS_ENTAILMENT lint (Add IMPLIED_BOUNDS_ENTAILMENT lint):将在 1.68 版本落地,是未来兼容 lint,因为发现许多(不健全性)回退
- 检查 ADT 字段的 copy 实现,考虑 regions (Check ADT fields for copy implementations considering regions):当前开放,准备落地
- 在 wfcheck 中规范化之前注册 wf obligation (Register wf obligation before normalizing in wfcheck):当前开放,发现回退,需要额外工作
- 在一致性检查期间将 projections 作为未覆盖类型处理 (Handle projections as uncovered types during coherence check):当前开放,发现一些回退,建议使用未来兼容 lint
- 不在 AstConv 中规范化 (Don't normalize in AstConv):将在 1.68 版本落地,发现 1 个小回退
正如你所见,我们在弥合不健全性漏洞方面正在取得进展。crater 评估发现这些有时会破坏代码。然而,我们尽力缓解这种情况,即使被破坏的代码在技术上是不健全的。
新特性
虽然从技术上讲,提议和设计新特性不属于类型团队的职责范围(这些更多地属于语言团队本身),但在某些情况下,团队会深度参与(即使不是主导)特性设计。
这些可以是小的补充,接近于错误修复。例如,这个 PR 允许比以前编译更多种类的生命周期 outlives 边界。或者,这些 PR 可能是更大、更有影响力的更改,它们不属于“特性”范畴,而是与类型系统紧密相关。例如,这个 PR 使 `Sized` trait 成为 coinductive,这实际上使得更多循环边界能够编译(参见这个测试 了解示例)。
还有一些由类型团队推动的更大特性和特性集,这主要是由于它们与类型系统有很强的交叉。以下是一些例子:
- 泛型关联类型(GATs)- 这个特性早在类型团队成立之前就存在了,也是此列表中目前唯一一个已经稳定的特性。但由于与类型系统的深入交互,团队能够解决其最终稳定路径上出现的问题。有关更多详细信息,请参阅这篇博客文章。
- 类型别名 impl trait (TAITs) - 正确实现这个特性需要对类型检查器有透彻的理解。这个特性已接近稳定。更多信息请参阅跟踪问题。
- Trait 向上转型 (Trait upcasting) - 这个特性相对较小,但与类型系统有一些交互。同样,请参阅跟踪问题 了解该特性的解释。
- Negative impls - 这个特性也早于类型团队,但最近团队一直在研究它。目前仍有一些开放的 bug 和不健全性问题,因此离稳定还有一段距离,但你可以在这里 关注。
- Trait 中返回位置 impl trait (RPITITs) 和 Trait 中异步函数 (AFITs) - 这些特性最近才随着 GATs 和 TAITs 的进展成为可能。它们目前在同一个跟踪问题下进行跟踪。
路线图
最后,让我们将这一切放到一个路线图上。正如往常一样,目标最好是具体、可衡量和有时限的。为此,我们将目标大致分为 4 个阶段:2023 年夏季、2023 年底、2024 年底和 2027 年底(6 个月、1 年、2 年和 5 年)。总的来说,我们的目标是构建一个平台来维护健全、可测试和文档化的类型系统,使其能够支持 Rust 语言所需的新特性。此外,我们希望培养一个可持续的开源团队(类型团队)来维护这个平台和类型系统。
快速提示:这里有些内容在这篇帖子中没有完全解释,但为了完整性起见还是包含了它们。那么,言归正传:
6 个月
- 正在进行的新特质求解器应该可以进行测试
- a-mir-formality 应该能针对 Rust 测试套件进行测试
- TAITs 和 RPITITs/AFITs 都应该稳定或正在走向稳定。
2023 年底
- 新特质求解器取代现有特质求解器的一部分,但未在所有地方使用
- 我们有(团队的)入职计划和新特质求解器的文档
- a-mir-formality 被整合到语言设计流程中
2024 年底
- rustc 和 rust-analyzer 共享新特质求解器
- 里程碑:共享类型 IR
- 我们有一个清晰的 API 用于可扩展的特质错误,至少在内部是可用的
- “亮点特性”
- Polonius 处于可用状态
- 高阶特质边界中的隐式边界(参见这个 issue 了解一个此特性将解决的问题示例)
- 基本能在任何地方使用 `impl Trait`
- 潜在的版次边界变化
2027 年底
- (类型相关)不健全性问题已解决
- 大多数语言扩展易于完成;大型扩展可行
- a-mir-formality 通过 99.9% 的 Rust 测试套件
结论
对于 Rust 来说,这是一个令人兴奋的时期。随着其用户群和受欢迎程度的增长,语言本身也在发展。随着语言的发展,对支持语言的可持续类型系统的需求变得越来越明显。项目组成立了这个新的类型团队来解决这个需求,希望在这篇帖子中,您能看到团队迄今为止取得了很多成就。我们期望这个趋势在未来很多年里都能持续下去。
一如既往,如果您想参与或有任何问题,请访问Rust zulip。