note: downstream crates may implement trait `std::clone::Clone` for type `&mut _`
It made me wonder if impl !Trait would make sense just from a diagnostics and documentation perspective: errors like “the core crate has promised that &mut _ will never be Clone”, and a place in rustdoc to, say, explain why Option doesn’t have a Display impl.
I would expect it to be semver-compatible to add a new negative impl for a trait you didn’t impl before, but semver-breaking to remove such a promise. The usual coherence restrictions would apply.
It seems like it’d have interesting RFC implications, too: It’d be possible, for example, to RFC that String will neverimpl Termination (though I expect such a thing would be quite rare).
Hmm, the compiler could potentially auto-propagate !Copy promises, and thus be able to confidently say “this cannot be Copy, so you must borrow or clone here” instead of "it was moved because it doesn’t implement Copy" and thus implying that you should try adding that to the type.
The diagnostic improvements are nice, but for anything to do with semver, the !Copy promise should be opt-in, since the author may want to later change the internals of their type even if those are currently !Copy. For example, consider transitioning from an opaque error type that contains a String to one that contains a Copy enum of possible causes.
Good point! I guess that weakens that part of the idea somewhat, since diagnostics could already check whether it'd be possible to implement Copy for a type.
Cool proposal, especially w.r.t. improved diagnostics!
I’m just wondering about 1 thing, and it’s something better aimed at people who’ve worked on the compiler: at what point does negative reasoning lead to problems that are co-NP in nature?
Where we really want to be careful is if we start introducing "negative where clauses", as that can lead to negative cycles -- i.e., to prove that T: !Trait, we have to prove that T: !OtherTrait, which in turn requires us to prove that T: !Trait.
Classic example from logic would be something like this:
A :- not B
B :- not A
This is tricky. If B is false, then A is true -- but then B is true. (In Rust terms, "A" here might be some Rust predicate like u32: SomeTrait.)
In principle, the solving algorithm (SLG) that Chalk uses is complete for the Well-founded Semantics and can handle such situations. It would, in this case, assign A and B both the result of "undefined" -- neither true nor false.
However, SLG assumes "non-floundering" executions -- this implies that there are no unbound inference variables that appear in negative predicates. This is similar to the rules we have around impls that prevent you from having inference variables that don't appear in the impl header (i.e., impl<A> Foo for u32 { } is illegal because A is not constrained). There are also interactions with some of the other extensions that chalk uses, like forall clauses and so forth that I don't fully recall. =)
All of this is not to say we can't have negative trait impls, but we would need to look carefully at the patterns that arise. And of course semver considerations as well.
It’s only a contradiction in classical logic where everything is strictly true or false. Part of what makes the trait system interesting is that in addition to “definitely impls Trait” and “definitely does not impl Trait”, you also need “we don’t know if it impls Trait” to deal with things like the possibility of the impl being added in the future.
The real question is whether introducing “negative where clauses” and other forms of negative reasoning would produce situations where we genuinely want to accept negative cycles like that and do something useful with them. That, I have no idea.
Well, it's not quite a contradiction -- even setting aside questions of semver, classical logic, and so forth!
What A :- not B is saying is: "one way to prove that A is true is by B being false". Similarly B :- not A. This does not imply that this is the only way to prove that A is true -- it's just one way.
So, for example, given the rules above, A and B could both be true -- but you would need some further rules (perhaps added by other impls) to justify that.
Just going by those two impls, you cannot say that A is true or B is true but you also cannot say that either one is definitely false. Or, to put it another way, you would be justified in concluding that A is false, but you are equally justified in concluding that B is false!
The problem is that whichever of those conclusions you try to reach, you then wind up proving up disqualifying the other. So the problem here is not no solutions, it is rather that you have multiple, equally valid, contradictory solutions -- you could either say that (A, not B) or (not A, B). But we are trying to answer a simpler question: is A true or not? And we can't answer that without also answering something about B.
(There are other ways to evaluate logical programs. e.g., with Answer Set Programming, you actually get back multiple sets of answers... so in this case you would get something like [(A, not B), (B, not A)]. But we have now reached the limit of my knowledge about ASP, since I never dug that far into it -- it didn't seem appropriate for a setting like Rust.)
My brain wants to translate this into classical logic and comes out not with a contradiction but with the two lines being equivalent (in classical logic):
"A :- not B" translated to classical logic is
"A follows from not B" which is equivalent to
"not B implies A" which is the contrapositive of and so equivalent to
"not A implies B" which is equivalent to
"B follows from not A", which translated out of classical logic is
"B :- not A'"
If my translations to and from logic are valid, I'd expect this to be a contradiction in classical logic:
A :- not B
B :- A
I'm not sure what that means for Well-founded Semantics. If we can prove not B we can prove A and thus we can prove B, so B can't be false, but I don't know enough about WfS to say if that means B is definitely undefined, or whether we know anything about A.
As I wrote in this comment, it's not really about a contradiction. Just that we justify either a true or a false answer given that set of rules (but maybe we could with more rules).
translate to the following classical logical statement (TeX syntax)
\not B \implies A
\not A \implies B
Thus if we can prove either A or B false we know the other to hold, but it is equally valid for either or both to be true, as the implication is monodirectional.
I see, thanks for explaining this. So in a sense it’s more like a form of trinary predicate logic.
So, as long as there are no additional constraints being imposed, would it be valid to just pick one at random? Or is it indeed more appropriate to see the solution as the set of all valid answers?