Cylic trait implementations: motivation · baby stepsNB. This page is part of the series "Cyclic Trait Impls".<br>Click here to see all posts.<br>Lately I’ve been thinking about cyclic trait implementations. This is a problem that I’ve been trying to understand for years and years and I finally feel like I’m geting somewhere. I’m going to try to write out a series of blog posts documenting those explorations and, hopefully, culminating in a design that could be RFC’d. In this first post, I want to talk about one of the interesting questions, what I am going to call “internal” vs “external” proofs. I know that this material can seem abstract, so I’m going to try and connect it to “real Rust” as much as possible! This particular blog post is an introduction, explaining the general problem and giving some motivation for why we care.<br>What are cyclic trait implementations?<br>Right now in Rust we require most traits to have non-cyclic, or inductive, implementations. To explain what I mean, let’s consider this trait:<br>trait Dump {<br>fn dump(&self);
Now imagine that we have an impl of this for i32:<br>// Impl I<br>impl Dump for i32 {<br>fn dump(&self) {<br>println!("{self}");
A simple impl for Rc and `Option:<br>// Impl RC<br>implT> Dump for RcT><br>where<br>T: Dump,<br>fn dump(&self) {<br>T::dump(self)
// Impl Opt<br>implT> Dump for OptionT><br>where<br>T: Dump,<br>fn dump(&self) {<br>if let Some(v) = self {<br>T::dump(v)
and finally a recursive List type that has an impl as well:<br>struct ListT> {<br>value: RcT>,<br>next: OptionRcListT>>>,
// Impl L<br>implT> Dump for ListT><br>where<br>T: Dump,<br>fn dump(&self) {<br>Dump::dump(&self.value);<br>if let Some(n) = &self.next {<br>Dump::dump(n);
If I try to show that List: Debug, I do that by<br>Applying “impl L” to show that List: Debug if i32: DebugThen applying “impl I” to show that i32: Debug
There’s no cycle here – that is, I didn’t have to use impl L to show that impl L is valid.<br>Cyclic logic sounds bad, but it can be exactly what you want<br>Now, when I said that “the impl L didn’t have to use the impl L to show that it is valid” that might not have sounded suspicious to you. In fact, it’s a pretty natural idea. After all, generally when you try to establish a logical argument, you aren’t allowed to use cyclic reasoning. That is, you can’t say: I know that Niko likes Rust because Niko lists Rust. So, in the same sense, it seems natural that I should not be able to say “I know that List implements Dump because List implements Dump”.<br>But actually, it would sometimes be really useful to say exactly that. One example is so-called “perfect derive”. In our Dump impl above, we had one where-clause, T: Dump. And if you were to create a custom derive for Dump and write #[derive(Dump)], the impl I showed is typically exactly what you would get. But it’s not necessarily what you want. Consider what you get with #[derive(Clone)]:<br>// Impl LC1<br>implT> Clone for ListT><br>where<br>T: Clone, // {<br>fn dump(&self) {<br>List {<br>value: Clone::clone(&self.value),<br>next: Clone::clone(&self.next),
Here, the derive is going to create an impl that requires T: Clone. But if you look closely, you’ll see that all the fields only use Rc, so in fact, we should be able to clone a List even without T: Clone! But how is the compiler to know this?<br>You might think that the compiler could do some super smarty-pants analysis on the fields to figure it out. And, in a way, it can: that is what cyclic trait solving is all about. The thing is, while the compiler can do that, the derive cannot – the derive doesn’t have access to the definitions of other types and so forth, and clearly we would need to know things about Option and Rc to figure out whether T: Clone is required here.<br>But what we could do is to generate a different impl. Instead of adding T: Clone for each type parameter, we could add a where-caluse for each field type. This makes sense: after all, we are just going to be calling Clone on every field, so it’s quite logical to say that the impl is valid if every field is cloneable:<br>// Impl LC2<br>implT> Clone for ListT><br>where<br>RcT>: Clone,<br>OptionRcListT>>>: Clone,<br>// .. as above ..
Under this formulation, we can see that all we have to be able to do is to clone an Rc and clone an Option>, neither of which require that T: Clone.<br>This idea is called perfect derive<br>We call this idea [perfect derive][] and it’s been a goal for a while. The thing is, cyclic reasoning is tricky to get right. The Clone example is actually an easy one: that one doesn’t really require cyclic reasoning:<br>To show that List: Clone we have to show that…Rc: Clone, which is easy because impl Clone for Rc doesn’t have any where-clauses1<br>Option>>: Clone uses the impl Clone for Option where T: Clone impl which requires…Rc>: Clone, which is again easy
But it’s not so easy for Dump<br>But if we use...