Rust 编译器 trait 求解器中的 Goals 与 Clauses：从逻辑程序设计到余归纳推理

Rust 编译器 trait 求解器中的 Goals 与 Clauses从逻辑程序设计到余归纳推理【免费下载链接】rustEmpowering everyone to build reliable and efficient software.项目地址: https://gitcode.com/GitHub_Trending/ru/rust导读Rust 的 trait 系统本质上是一套逻辑推理系统——类型检查器会生成需要证明的goal目标而程序中的 trait、impl 声明则被翻译成已知为真的clause子句求解过程即在这些子句之上做深度优先搜索。本文基于 rustc-dev-guide 的 goals-and-clauses.md 章节系统讲解 goal/clause 的语法元结构、六种核心领域目标domain goal的语义以及归纳/余归纳证明的区别并结合本仓库 rustc 源码rustc_type_ir、rustc_trait_selection等 crate给出实现层面的印证。读完本文你将理解 Rust trait 求解器证明什么、依据什么、如何判定循环的完整逻辑骨架为后续阅读规范查询、规范化与求解器实现打下基础。一、逻辑程序设计视角下的 Goal 与 Clause在逻辑程序设计logic programming术语中goal目标是你必须证明的东西待求解的问题clause子句是你已知为真的东西可用的规则。正如 lowering-to-logic.md 所描述的Rust 的 trait 求解器基于遗传 Harrophereditary Harrop, HH子句的一个扩展。HH 子句是对传统 Prolog Horn 子句的推广——标准 Horn 子句不允许在目标goal的体body中出现全称量化forall与蕴含if而类型检查泛型函数恰恰需要这两种能力。例如把一个 trait 及其 impl 声明映射为类 Prolog 规则trait Clone { } impl Clone for usize { } implT Clone for VecT where T: Clone { }对应Clone(usize). Clone(Vec?T) :- Clone(?T).其中A :- B表示若 B 为真则 A 为真。要证明Clone(VecVecusize)就递归地应用规则先证Clone(Vecusize)再证Clone(usize)有直接 impl成立而Clone(VecBar)则因没有Clone(Bar)的规则而失败。这套目标驱动、规则匹配、递归下潜的过程就是 trait 求解的最朴素形态。二、Goals 与 Clauses 的元结构在 Rust 求解器中goal 与 clause 的形式如下注意两者互相引用是递归定义Goal DomainGoal // 领域目标见下文 | Goal Goal | Goal || Goal | existsK { Goal } // 存在量化 | forallK { Goal } // 全称量化 | if (Clause) { Goal } // 蕴含 | true // 平凡为真 | ambiguous // 永远无法证明 Clause DomainGoal | Clause :- Goal // 若可证明 Goal则 Clause 为真 | Clause Clause | forallK { Clause } K type // 一种kind | lifetime几个要点true表示平凡成立ambiguous表示永远无法证明在求解器里对应未知/不成立的结果而不是错误。existsK、forallK中的K可以是类型或生命周期这反映了 Rust 中泛型参数与生命周期参数的统一抽象。这些目标的证明过程本质上是深度优先搜索depth-first search细节可参考论文A Proof Procedure for the Logic of Hereditary Harrop Formulas即上文的 pphhf 参考文献。本仓库的 rustc-dev-guide 中还专门有 resolution.md 一章讨论求解与规范化流程可配合阅读。从源码结构看这套抽象在 rustc 中的落点是通用 goal/clause 骨架定义于 compiler/rustc_type_ir/src/solve/mod.rs其中的Goal结构体位于该文件第 394 行附近QueryInput在第 456 行附近GoalSource在第 422 行附近谓词种类clause/predicate 的原子形态定义于 compiler/rustc_type_ir/src/predicate_kind.rs原文档同时指出在 chalk 项目中对应的定义位于chalk-ir/src/lib.rschalk 是 rustc 的 trait 求解器原型实现也是本仓库 chalk.md 章节的主题。Clause 的折叠形式与 DomainGoal 的地位对上面的 clause 定义稍作展平可以看到任何 clause 最终都可写成forallK1, ..., Kn { DomainGoal :- Goal }也就是说DomainGoal 永远是 clause 的 LHS左部——在最细粒度上trait 求解器最终要证明的就是某个 DomainGoal。这一观察决定了 DomainGoal 是整个逻辑的核心原子。三、TraitRef 与 Projection定义 DomainGoal 的前置概念在给出 DomainGoal 的完整集合之前需要先引入两个简单表述。Trait referencetrait 引用由 trait 名 一组合适的输入P0..Pn构成TraitRef P0: TraitNameP1..Pn例如u32: Display、VecT: IntoIterator都是 trait reference。注意 Rust 表层语法还允许一些 trait reference 之外的东西比如关联类型绑定VecT: IntoIteratorItem T这不在 trait reference 的定义之内。Projection投影由一个关联项引用及其输入P0..Pm构成Projection P0 as TraitNameP1..Pn::AssocItemPn1..Pm例如T as Iterator::Item。投影是 Rust 关联类型associated type在求解逻辑中的表示形态它指向通过某个 trait 实现而得到的类型。四、DomainGoaltrait 逻辑的六种原子目标有了 TraitRef 与 Projection可以给出 DomainGoal 的完整定义DomainGoal Holds(WhereClause) | FromEnv(TraitRef) | FromEnv(Type) | WellFormed(TraitRef) | WellFormed(Type) | Normalize(Projection - Type) WhereClause Implemented(TraitRef) | ProjectionEq(Projection Type) | Outlives(Type: Region) | Outlives(Region: Region)WhereClause指代 Rust 用户实际能在程序中书写的where子句。这个抽象层存在的意义在于有时我们只想处理在 Rust 中真正可写的那些领域目标把它单独抽出来便于约束。下面逐一拆解。4.1 Implemented(TraitRef)例Implemented(i32: Copy)语义若给定输入类型与生命周期上实现了给定 trait则为真。对应 Rust 源码trait 子句。在 predicate_kind.rs 中ClauseKind::Trait(ty::TraitClauseI)的注释明确写着对应where Foo: BarA, B, C即这类子句直接映射到Implemented类目标。4.2 ProjectionEq(Projection Type)例ProjectionEqT as Iterator::Item u8语义给定的关联类型Projection等于Type。它既可以通过规范化normalization证明也可以使用占位关联类型placeholder associated types证明——后者与 rustc-dev-guide 中 hrtb.md更高阶 trait bound讨论的占位/存在变量机制相关。4.3 Normalize(Projection - Type)例NormalizeT as Iterator::Item - u8语义给定的关联类型Projection可以规范化为Type即沿着关联类型定义/impl 一路展开求值。关键性质Normalize蕴含ProjectionEq但反之不成立。因为规范化必须算到底而等值可以只停留在占位符层面。此外一般要证明Normalize(T as Trait::Item - U)还同时要求先证明Implemented(T: Trait)——关联类型的规范化必须以 trait 已实现为前提。源码印证在 predicate_kind.rs 第 30-32 行ClauseKind::Projection的注释描述为where T as TraitRef::Name X大致如此而规范化目标的载体NormalizesTo结构体定义于 compiler/rustc_type_ir/src/predicate.rs第 619 行附近它携带alias要规范化投影与term规范化结果两个字段正是Normalize(Projection - Type)的代码形态。4.4 FromEnv(TraitRef)例FromEnv(Self: Addi32)语义若内部的TraitRef被假定为真——即可以从当前作用域内可见的 where 子句推导出来——则为真。考虑如下函数原文档的经典例子fn loud_cloneT: Clone(stuff: T) - T { println!(cloning!); stuff.clone() }在函数体内我们持有FromEnv(T: Clone)。作用域内 where 子句是嵌套的位于某个 impl 体内的函数体也会继承该 impl 体的 where 子句。这条规则连同下一条被用于实现隐含 boundimplied bounds。在 lowering 部分我们会看到FromEnv(TraitRef)蕴含Implemented(TraitRef)但反之不成立——正是这一非对称性构成了 implied bounds 的基石。更详细的推导见本仓库的 implied-bounds.md 章节那里区分了显式隐含 bound如 ADT 字段推导出的 outlives 约束由inferred_outlives_of查询计算与隐式隐含 bound如fn fooa, T(x: a T)无需声明即可假设T: a。4.5 FromEnv(Type)例FromEnv(HashSetK)语义若内部的Type被假定为良构well-formed——即它是某个函数或 impl 的输入类型——则为真。考虑struct HashSetK where K: Hash { ... } fn loud_insertK(set: mut HashSetK, item: K) { println!(inserting!); set.insert(item); }HashSetK是loud_insert函数的输入类型因此函数体内假定它良构持有FromEnv(HashSetK)。在 lowering 时FromEnv(HashSetK)会蕴含Implemented(K: Hash)因为HashSet的声明带有K: Hash这个 where 子句。于是loud_insert上不必重复书写K: Hash约束——编译器自动假定它成立。这正是 implied bounds 减轻冗余标注的实际收益。4.6 WellFormed(Item)语义给定条目是良构的。良构可以针对不同类型的条目类型WellFormed(Veci32)在 Rust 中为真WellFormed(Vecstr)为假因为str不是Sized。TraitRef如WellFormed(Veci32: Clone)。与 implied bounds 的关系良构性是可以放心假定 FromEnv的前提。回到loud_clone之所以能假定FromEnv(T: Clone)是因为我们同时会对loud_clone的每个调用点验证WellFormed(T: Clone)loud_insert同理每个调用点都会验证WellFormed(HashSetK)。换句话说调用点的良构验证为函数体内部的宽松假定买单。源码印证在 predicate_kind.rs 第 38-39 行ClauseKind::WellFormed(I::Term)的注释是无对应语法T良构——这正好说明 WellFormed 不是用户可书写子句而是求解器内部生成的验证目标。4.7 Outlives(Type: Region) 与 Outlives(Region: Region)例Outlives(a str: b)、Outlives(a: static)语义若左侧的类型/区域比右侧的区域存活得更久outlives则为真。源码印证对应 predicate_kind.rs 中的ClauseKind::RegionOutlives(ty::OutlivesClauseI, RegionI)where a: r与ClauseKind::TypeOutlives(ty::OutlivesClauseI, I::Ty)where T: r。outlives 目标的证明与生命周期推断深度耦合这也是 trait 求解与借用检查的交叉点。五、归纳目标与余归纳目标Coinductive Goals大多数目标在系统中是归纳的inductive不允许循环推理。考虑这样的子句Implemented(Foo: Bar) :- Implemented(Foo: Bar).按归纳语义这条子句毫无用处要证明Implemented(Foo: Bar)就必须递归证明它自己循环往复无穷无尽求解器会在此终止但结论是Implemented(Foo: Bar)不成立/未知。然而部分目标是余归纳的co-inductive允许循环。若Bar是余归纳 trait则上面的规则完全有效它恰恰说明Implemented(Foo: Bar)为真。5.1 Auto traits余归纳的典型用例Rust 中 auto traits 正是余归纳目标的代表。考虑Send与结构体struct Foo { next: OptionBoxFoo }auto trait 的默认规则是Foo是Send当且仅当其字段类型是Send。于是有规则Implemented(Foo: Send) :- Implemented(OptionBoxFoo: Send).可以想见证明OptionBoxFoo: Send会循环地再次要求证明Foo: Send——我们确实进入了循环但没关系即便Foo引用了自身我们仍认为Foo: Send成立无限递归结构在逻辑上自洽。从一般原理上说Rust 在 trait 求解中使用余归纳是为了枚举一个固定的可能性集合。对 auto traits 而言就是枚举从给定起点出发可达的类型集合Foo可达OptionBoxFoo进而可达BoxFoo再到Foo循环闭合。源码中的印证非常具体在 compiler/rustc_trait_selection/src/traits/select/mod.rs 的coinductive_match函数第 1243-1259 行附近中注释明确写道coinductive trait 是指 auto trait 或Sized当求解栈顶的目标cycle[0]是 coinductive trait且回溯路径上的谓词也全是 coinductive trait 时该循环被判定为可接受。同一文件第 139-140 行的注释也区分了两种情形B: AutoTrait需要A: AutoTraitcoinductive 循环OK与C: NonAutoTrait需要A: AutoTrait非 coinductive 循环不行。auto trait 求解器的实现位于 compiler/rustc_trait_selection/src/traits/auto_trait.rs其第 68 行附近的注释同样提醒由于Send的余归纳本质完整且正确的结果实际上……即必须借助 coinductive 处理递归结构。底层判定依据记录在 compiler/rustc_middle/src/ty/trait_def.rs 第 43-50 行附近的is_coinductive字段若 trait 带有#[rustc_coinductive]属性则is_coinductive为真注释还提到未来可能让所有 trait 都变成 coinductive需要更好的证明策略。select/mod.rs第 1249 行正是通过tcx.trait_is_coinductive(data.def_id())读取这一信息。5.2 WellFormed 谓词同样是余归纳的除 auto traits 外WellFormed谓词也是余归纳的。这与它枚举所有情况的用法一致良构性需要递归检查类型的各个组成部分是否良构如WellFormed(Vecstr)需要检查str是否Sized而这些检查之间可能形成循环。将 WellFormed 设为余归纳正是为了支撑 4.6 节描述的 implied bounds 模式——详细论证参见 implied-bounds.md。在coinductive_match的实现中可以看到ClauseKind::WellFormed分支目前只有在启用generic_const_exprs特性时才按余归纳处理第 1251-1256 行这属于求解器实现中仍在演进的细节。六、从目标到求解与求解器实现的衔接理解了 goal/clause 的形态后可以顺带看清它与 rustc 现代求解器的衔接关系目标的载体Goal结构体compiler/rustc_type_ir/src/solve/mod.rs 第 394 行附近是一个带 binder 的目标谓词QueryInput第 456 行附近将目标与参数环境param env打包作为求解查询的输入。这正是把本文的抽象语法落地为具体类型的实现。谓词的枚举PredicateKind与ClauseKindcompiler/rustc_type_ir/src/predicate_kind.rs覆盖了比本文 DomainGoal 更广的形态——除 Trait/Projection/WellFormed/Outlives 外还包括ConstArgHasType、ConstEvaluatable常量求值约束、HostEffectconst 化效果约束、DynCompatibledyn 兼容性、Subtype/Coerce子类型与强制转换、ConstEquate与Ambiguous恒为模糊的标记谓词用于相干性检查中标记 opaque 类型可能相等等。可见现代求解器在六种核心 DomainGoal 之上又为新的语言特性扩展了不少谓词。证明过程的终止归纳/余归纳区分直接决定求解器遇到循环时的行为——归纳循环被当作失败余归纳循环被当作成功。这与 caching.md求解缓存及 canonicalization.md规范化把含推理变量的目标转为规范形式以便缓存与复用共同构成了求解器正确性与性能的支柱。七、未完成章节与延伸阅读原文档作者明确标注本章仍有两块内容待补充Incomplete chapter证明过程proof procedure的详细展开上文提到的深度优先搜索只是概述完整的 HH 公式证明过程需要更系统的描述论文A Proof Procedure for the Logic of Hereditary Harrop Formulas是权威参考。SLG 求解与否定推理negative reasoningSLG线性解析制表求解算法用于处理递归目标与否定是比朴素 DFS 更精细的求解策略。若希望继续深入本仓库 rustc-dev-guide 的 traits 目录提供了完整的相邻章节先读 lowering-to-logic.md 理解声明如何变成子句再读 implied-bounds.md 看 FromEnv/WellFormed 如何支撑隐含 bound之后可依次阅读 canonicalization.md、canonical-queries.md、hrtb.md 与 resolution.md从而拼出 trait 求解的全貌。实现层面核心代码集中在 compiler/rustc_trait_selection/src/traits/ 与 compiler/rustc_type_ir/src/ 两个目录下可直接按文中给出的文件与行号定位关键函数。【免费下载链接】rustEmpowering everyone to build reliable and efficient software.项目地址: https://gitcode.com/GitHub_Trending/ru/rust创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考