Mutually exclusive traits

[withoutboats]

Mutually exclusive traits. Discussed previously on internals.rust-lang.org, but the RFC has been updated in material ways.

Rendered

[llogiq]

Do we require that both traits declare themselves to be negatively bounded by the other? It certainly improves readability, especially in larger source files. If this is the case, the compiler should generate a warning if Edible : !Poisonous, but Poisonous is not bounded by !Edible.

[withoutboats]

Edible: !Poisonous implies Poisonous: !Edible, so there wouldn't be a coherence violation if one denotation was left off. I agree that it is better readability for both to be denoted, and a lint would be good.

[llogiq]

Yes, a lint would certainly be the best way to do this.

[llogiq]

This is a bit unclear to me. So ?Send is implemented for which types? What are the semantics of implementing ?Trait? What about bounding by ?Trait? I'd like the text to either forbid it or specify what it actually means.

[withoutboats]

A type which implements ?Send would not meet the bound T: Send or T: !Send. The only reason to implement ?Send over !Send is if you believe you might one day be able to mark the type Send and don't want that to be backwards incompatible (I don't know if any types that would want this exist; I doubt that they do).

Bounding by ?Trait is not possible and not sensible; all type parameters are bound ?Trait for all traits unless bound otherwise, and that bound means nothing (that is, a type parameter T may or may not implement any particular trait unless it has a bound which declares otherwise).

[llogiq]

So impl ?Send just means that no one should rely on the type being !Send now or in the future. That makes sense. Would you add a sentence to that effect to clarify this paragraph?

[llogiq]

This is a very cool feature, but looks a bit like spooky action from a distance. We should make sure that error messages (e.g. if someone tries to impl Bar for T) reflect the actual reason.

[withoutboats]

I agree with this. If someone attempts to implement as an example, Float and Integer for their type, the error they should get should be to the effect that Float contradicts Integer, not something about !Float or !Integer, which they have not directly used.

[jnicklas]

I think I dislike this feature, and I preferred it being left out in the original draft. With a positive trait bound on a trait I have to manually implement it, I can't see why that would be different with a negative trait bound.

I would expect/prefer an error like:

test.rs:7:1: 7:23 error: the trait `!Bar` is not implemented for the type `SomeType` [E0277]
test.rs:7 impl Foo for SomeType {}
          ^~~~~~~~~~~~~~~~~~~~~~

[llogiq]

Thinking about it a bit more, @jnicklas proposal certainly meshes well with the "make code semantically complete locally" philosophy of Rust (which is also why we only have fn-local type inference). Someone reading SomeType's code or using SomeType somewhere else will probably not have in mind that Foo : !Bar.

Requiring that SomeType : !Bar or impl !Bar for SomeType (which one btw.?) is a small price to pay for that improved readability.

[jnicklas]

It'd definitely be impl !Bar for SomeType {}.

[withoutboats]

I chose to propose that sugar because it seemed like there wasn't enough in the pre-RFC for folks to disagree about. :-) In seriousness, I do think this is good sugar.

It's not actually true that you have to manually implement all positive traits which are bounds, because some are implemented by default through default impls. Default impls currently can only be provided for marker traits, and of the four non-built-in traits in std::marker (Send, Sync, Reflect, and Unsize), three are implemented by default. Negative traits are all marker traits, and while inference is a different mechanism from default impls, it is similar in principle.

If a type implements a trait, it cannot implement a trait which is mutually exclusive with that trait. Implementing that trait is a semantic declaration that this type does not implement traits that are mutually exclusive with the traits it does implement. Mutual exclusion implies that these traits are fundamentally disparate (e.g. Int and Float or Num and Collection), a client should not be expecting that a type which implements Int can be passed where a type is bound Float.

It seems much less of a leaping inference than the leap that Rust already makes in local contexts, which makes this code compile (and which cannot be removed).

pub trait Quux { }

pub struct Foo;
pub trait Bar { }

impl Quux for Foo { }
impl<T> Quux for T where T: Bar { }

[llogiq]

If you want to stand by it, at least extend the Alternatives section to cover @jnicklas' proposal.

I'm currently leaning in favor of explicit stating the impl, because we can later remove the requirement in a backwards-compatible way. Introducing the requirement later would break code.

[llogiq]

I'd like to have "unless T actually has an impl for Trait in addition to 'by default', to clarify the meaning.

[llogiq]

Following @steveklabnik 's comment to my recent RFC submission, you should linebreak your Markdown.

👍 for the proposal

[llogiq]

I'd use code formatting for actual code and add more headers to clarify, like:

	?Trait	Trait	!Trait
Specific impl	by default	impl Trait for T	impl !Trait for T
Explicit impl	impl ?Trait for T	impl Trait for T	impl !Trait for T
Default impl	by default	impl Trait for ..	impl !Trait for ..
Bounds	by default	where T: Trait	where T: !Trait
Explicit bound	where T: ?Sized	by default for Sized

I'm unsure about the "Explicit bound" header, though. Wouldn't that contradict your assertion that being bound by ?Trait makes no sense?

[nrc]

Changed the title to avoid confusion with mutexes

[huonw]

This seems like something that may have some prior art in a language like Haskell (or some variant), so it'd be good to have a look around to see if there's been research/experiments with this somewhere already. I'm just a little nervous that this may have unexpected interactions so it'd be good to get a broader view.

[bbatha]

There's a spelling error here: "under this RFC tahn before" should be "under this RFC than before"

[paholg]

This is very exciting and I hope it goes through.

I would argue strongly in favor of the alternative proposal. If anyone is to use ?Trait, then the main proposal suffers the same backwards incompatibility issues as the alternative, while the alternative maintains its advantages.

I feel I can best illustrate my point with a concrete example. Say that you want to create a linear algebra library as generically as possible, and you want to use * for both pairwise multiplication between vectors and for scalar multiplication. Then, you will likely end up with something like this:

trait Vector {}
struct Vec2<N> { x: N, y: N }
impl<N> Vector for Vec2<N> {}

// pairwise multiplication between vectors
impl<N: Mul<M>, M> Mul<Vec2<M>> for Vec2<N> {
    type Output = Vec2<<N as Mul<M>>::Output>;
    ...
}
// scalar multiplication
impl<N: Mul<T>, T: !Vector> Mul<T> for Vec2<N> {
    type Output = Vec2<<N as Mul<T>>::Output>;
    ...
}

Under the alternative proposal, this is all that is needed and anyone can use your vectors with any type they wish.

Under the main proposal, one would need to impl !Vector for Type {} in order for Type to be useable as a scalar. If Type is defined in a different crate, then this is impossible.

The workaround to this would be to include a second, essentially identical definition for scalar multiplication:

impl<N: Mul<T>, T: ?Vector> Mul<T> for Vec2<N> {
    type Output = Vec2<<N as Mul<T>>::Output>;
    ...
}

This is clearly problematic. In fact, we could even forgo the first definition and only use the second, treating ?Vector as though it means "not Vector"

If creating trait Trait means that a type T must belong to precisely one of Trait, !Trait, or ?Trait, then whichever the default is can (and will) be used as though it means !Trait, so the standard and the syntax should match that.

[llogiq]

@paholg Good point.

If creating trait Trait means that a type T must belong to precisely one of Trait, !Trait, or ?Trait, then whichever the default is can (and will) be used as though it means !Trait, so the standard and the syntax should match that.

The RFC (line 126) proposes that !Trait be the default only within the same crate. Outside we cannot be sure if a type is ever to implement !Trait or Trait, so in order to keep external code compatible, we need to assume ?Trait in external crates.

[paholg]

@llogiq I missed that. I would argue that it is just more confusing, though, and would cause unexpected bugs if a crate is ever split into two.

Within a crate, it's trivial to specify whether a type implements Trait, !Trait, or ?Trait; the default really matters when importing a type from one crate and a trait from another, as you are stuck with it.

[llogiq]

@paholg This rule actually reflects the current coherence rules as far as I understand. So if it really is confusing, we should look into how it is documented and what errors may ensue and make sure that the documentation and error messages clear up any confusion.

However, I see why you'd like to have the default ?Trait globally and reiterate my position that it should at least be noted in the Alternatives section.

[withoutboats]

Under the main proposal, one would need to impl !Vector for Type {} in order for Type to be useable as a scalar. If Type is defined in a different crate, then this is impossible.

Note that the alternative is accessible a la carte by declaring impl !Vector for .. { }. The difference is about default behavior. The main reason the primary proposal is to require an explicit impl of this relation is, as the proposal says, backwards compatibility by default, but there are some others:

• It is already the behavior that Rust assumes (outside of the local crate). Changing this default would not be backwards incompatible, but it make everyone's trait declarations a stronger statement that they would have to learn about and evaluate.
• As the default impl section covers, if a member of a struct contradicts the default impl, the relation is inferred to be ?Trait, rather than the default impl (there are very good reasons for this, otherwise types carrying thread-unsafe data would be Send by default). If this were not the default relation, this would be very confusing. And the uncertainty here cannot just resolve to !Trait if a member contradicts the default impl, because there's really nothing under this proposal that would stop Send from being ThreadLocal, implemented negatively by default, in which case the same soundness violation would occur if it were assumed !ThreadLocal as if it were assumed Send.
• It makes silence a semantic declaration, which is bad in my opinion.

[withoutboats]

I missed that. I would argue that it is just more confusing, though, and would cause unexpected bugs if a crate is ever split into two.

This part of the RFC is a clarification of the current rule, which was arrived at by evolution. Originally, types were !Trait by default throughout the entire system, until the backwards incompatibility of the negative reasoning in this was exposed. Then, it was changed to be a coherence violation but only for external types/traits (presumably because, if you introduce a coherence violation in your own crate, its your responsibility). Then Rust hit 1.0. If Rust were still unstable, this RFC would have also proposed to remove this allowance for implicit local non-overlap, which I find very inelegant and potentially quite confusing, but that would be backwards incompatible. This is the sort of tiny language wart that would be removed in the mythical 2.0, I think.

[jnicklas]

In @paholg's example it'd also be possible to declare a mutually exclusive trait Scalar which is default implemented. This would mean that Vector types would have to implement !Scalar (or have it implemented for them automatically, depending on how that question is resolved). In any case, I think the main proposal is more flexible and easier to understand than the alternative, and I strongly prefer the main proposal.

[withoutboats]

This seems like something that may have some prior art in a language like Haskell (or some variant), so it'd be good to have a look around to see if there's been research/experiments with this somewhere already. I'm just a little nervous that this may have unexpected interactions so it'd be good to get a broader view.

I looked around online & couldn't find anything like this in Haskell, so I asked in #haskell and it hasn't been considered. The only concern anyone in the channel raised had to do with orphan impls, which Haskell allows but Rust does not.

I agree that this seems like something that could have surprising implications. I've tried hard to think of what they could be though and come up empty.

[withoutboats]

Re: Local impls and warbling (using Dirt as my type and Edible as my trait).

It actually is not necessary that local types and traits have the implicit relation Dirt: !Edible, only that impls for Dirt not overlap with impls for T: Edible, because that is currently the only discernment between ?Edible and !Edible. Thus, in a local context, a T where T: ?Trait could not overlap with a T: Trait, while still also not implicitly meeting the bound !Trait. This seems like the better course of action.

EDIT: Actually, if you think of this 'warble' as just another kind of inference (if both type and trait are local, and two impls would overlap otherwise, infer that the type does not impl the trait), declaring the type fully !Trait seems like the better thing to do after all! Hmmm...

[huonw]

I looked around online & couldn't find anything like this in Haskell, so I asked in #haskell and it hasn't been considered. The only concern anyone in the channel raised had to do with orphan impls, which Haskell allows but Rust does not.

Great, thanks for looking into it.

I've tried hard to think of what they could be though and come up empty.

Yeah, I haven't thought of anything either, and I'm sure you've spent more time on it than me!

[Anachron]

I like this RFC, however, I have to admit that I'm afraid this could get too complicated (at least redundant).
What I mean is:

Meltable = !Stone && !Wood && !Water

Then you would have to declare non-meltability to all three types, but in real code this could become messy soon. (Imagine saying that Water is not Meltable, not Burnable, not Flameable and co, instead of saying what it does)

I agree that both types should explicitly say their relationship and I also do not know a solution for this.

[llogiq]

@Anachron as long as Meltable is defined in the current crate, it would negatively bound Water, Stone and Wood by default, unless they explicitly are declared to be Meltable as per the default inference rule.

[Anachron]

@llogiq wouldn't that contradict the rule mentioned in #1148 (comment), that a missing declaration should at least trigger an info?

[llogiq]

That would be a lint, not a hard-and-fast rule. Lints can be deactivated using #[allow(...)]; also as proposed it only requires an explicit X : !Y if an explicit Y: !X is given – else we'd end up requiring any of !X or ?X for each trait available in the current crate on each type specified in the current crate, which would give us a quadratic number of lines of code that can be inferred anyway.

Btw. that comment is not yet part of the RFC if I read it correctly. @withoutboats Shall I send you a PR to that effect?

[nikomatsakis]

So, for some time now, I've been working on a detailed response here. I'm getting closer. But working through some of my thoughts, I encountered a question that I don't quite know the answer to.

Imagine that I have some type Foo that implements a trait Bar:

impl Bar for Foo { .. }

Does Foo: ?Bar now hold, or not? I would assume that it does, and I think it's sort of important that it does, for backwards compatibility reasons. That is, otherwise moving from the default (Foo: ?Bar) to a positive impl (Foo: Bar) is kind of a breaking change. But some of the RFC text made me think that perhaps the intention was otherwise.

To be honest, I'm not sure that thinking of Foo: ?Bar as a kind of predicate is very useful. It seems to me that it is a predicate which is always true (for the backwards compatibility reasons argued above), and hence having it in a where-clause or any other such location is sort of pointless. The only real reason I can see it is as a "generalization" of T: ?Sized, but it's not really a generalization in my view, since the point of that declaration is so that we do NOT add the default T: Sized -- that is, T: ?Sized is not itself saying anything positive, just overriding a default. In a sense, impl ?Trait for Foo, when used with a structural (OIBIT) trait, has a very similar meaning (within the context of this RFC, I mean).

[withoutboats]

Your interpretation is correct. Foo: ?Bar always holds true, no matter what you impl. Every type parameter is implicitly bound ?Bar for every trait except for Sized unless a different bound is specified. There's no reason to support explicit declarations of this bound for traits other than Sized, the relation is only described because it unifies the proposal conceptually.

Similarly, there's no reason to support explicit impls of ?Trait unless Trait has a default implementation.

[nikomatsakis]

So, I'm long overdue in adding some detailed feedback here, and I apologize for that! Let me start by saying that I really like this approach at a high level. I find the motivation compelling. In particular, I think there is a need to finish the story that RFC 1023 began. Currently, negative reasoning is permitted within a crate, but not outside. This was a pragmatic rule at the time but it doesn't seem like the best rule going forward. For one thing, it's not clear that crate authors are aware of the negative reasoning they are using: it's easy to make accidental assumptions. For another, there are plenty of times when you'd be willing to promise never to implement a trait: for example, Rc<T> would happily promise to never implement Copy, but it cannot.

That said, I have some concerns. I'm going to start with a comment that kind of resummarizes the RFC and points out some quibbles with the text itself. I've got another in the works with some deeper concerns around negative reasoning, specialization, etc (not all of which are specific to this RFC). Part of my purpose in resummarizing the RFC is to ensure I am understanding the intention, so please correct me if you think I have something wrong!

Marker traits vs new kinds of predicates

I find some parts of the RFC a bit confusing. Sometimes it seems to use T: ?Trait as a kind of positive declaration that neither T: Trait nor T: !Trait holds, but other times it does not. For example, the RFC states that !Trait and ?Trait "act as if they were marker traits", but I don't think that's quite right -- they are not really traits. They can't be used as objects, nor can they appear in UFCS forms or any other place. Rather, I think they act more like predicates (the things that can appear in a where clause, supertrait list, etc). That is, today we have one kind of trait-related predicate:

where T: Trait<..>

but, under this RFC, we would have two kinds of predicates:

where T: Trait<..>
where T: !Trait<..>

(For now, I've excluded ?Trait from this list since, as we said, it's sort of pointless. I'll add some more detailed thoughts below. Either way, the existing ?Sized can be understood as controlling whether T: Sized is added by default or not, not as its own kind of predicate.)

Furthermore, for non-structural (that is, non-OIBIT) traits, we now have one kind of impl:

impl Trait for T

but we would now have two, a positive and a negative impl:

impl Trait for T { ... }
impl !Trait for T { } // <-- no need for members, maybe we should just write `impl !Trait for T;`

The idea would be that we can prove the predicate T: Trait if we can find a suitable impl Trait for T. Similarly, we can prove the predicate T: !Trait if either: (1) we can find a suitable impl !Trait for T; (2) the trait or type is tagged #[fundamental] and no impl Trait for T is found; or (3) T is within the current crate and there is no impl T: Trait. As @withoutboats noted, number (3) is in some sense unfortunate, but is required for compatibility with the current rules about negative reasoning: probably we would want to add a lint against this. In other words, any time you rely on implicit negative reasoning within your crate, we would add a lint that suggests adding an explicit negative impl. (This is because of my feeling I noted above: that I think negative reasoning is often used by accident.)

Structural traits

Now we come to structural traits. Here we currently have three sorts of impls:

impl StructuralTrait for .. { } // <-- again, no need for members, since structural traits must be empty.
impl StructuralTrait for T { }  // <-- opt-in.
impl !StructuralTrait for T { } // <-- opt-out.

With structural traits today, things are somewhat inverted. To prove that T: StructuralTrait, we search first for an opt-in or opt-out impl. If we can't find one, we fall back to the structural interpretation, walking the struct's (or enum's) members and checking whether all of them are of a type which implements the trait. In other words, you can think of impl StructuralTrait for .. as supplying a default impl for each type, sort of like:

struct Foo { a: Bar, b: Baz }
impl StructuralTrait for Foo where Bar: StructuralTrait, Baz: StructuralTrait { } // sort of

In other words, to determine whether Foo: StructuralTrait holds, we have to go check whether Bar: StructuralTrait holds and Baz: StructuralTrait holds. (In fact, the precise expansion is a bit more subtle and under discussion, but this suffices for now.) There are lots of niggly details here, some of which I think may be relevant to this RFC; I'll get into those in my next comment.

Anyway, this RFC changes the story in two ways. First, it makes a subtle change to the semantics of impl !Trait. Whereas today that just means "do not consider Trait implemented", this makes it an irreversible declaration that Trait will never be implemented. This seems fine to me, though it is subtle. To recover the original semantics, you now use a new kind of impl, that basically applies only to structural traits (or only has utility with structural traits, depending on your POV):

impl ?StructuralTrait for T { }

This ? impl basically means: do not generate the default impl for T that .. would otherwise generate. Therefore, T is not going to implement StructuralTrait for now, but it may in the future.

The second change is that this RFC adds a negative .. impl:

impl !StructualTrait for .. { } // structural, but with a negative bent

My interpretation of the language from this section is that, whereas I described the positive sense as generating a defualt positive impl, this would generate a default negative impl:

struct Foo { x: Bar, y: Baz}
impl !SomeTrait for Foo where Bar: !SomeTrait, Baz: !SomeTrait { }

In other words, to determine whether Foo: !StructuralTrait holds, we have to go check whether Bar: !StructuralTrait holds and Baz: !StructuralTrait holds. If either of those does not hold, then Foo: !StructuralTrait does not hold. Similarly, Foo: StructuralTrait does not hold, because there is no positive impl.

I don't really see the purpose for this form as presented. What I have seen in the thread doesn't seem correct. For example, @withoutboats presents Num as a use-case here and @paholg presents vector vs scalar addition, but I don't think that a structural interpretation is right for either of those: for example, consider the Num case. If I had a type

struct MyThingy { 
    n: SomeNumberType,
    s: String
}

where SomeNumberType: Num, then this would mean that MyThingy: !Num does NOT hold, because it contains a member for which Num holds. That seems...odd? I think what both of these use cases are really asking for is something more like today's #[fundamental] trait (see next section).

Relationship to fundamental

I think what the impl !Trait for .. examples are really asking for is the existing #[fundamental] attribute. This attribute allows negative reasoning around a specific trait or self type. In terms of this RFC, a trait marked as #[fundamental] can be understood as a trait where the absence of an impl Trait for T can be used to prove T: !Trait (or, put another way, we change the default from T: ?Trait to T: !Trait, but since I don't like writing T: ?Trait as a predicate, I wouldn't say it that way).

As I wrote, some of the comments seem to suggest that this is what impl !SomeTrait for .. would do, but I don't believe that is actually the case from the language of the RFC -- and if it IS the case, it seems odd to overload the .. notation for that purpose, since this is quite different from the structural interpretation it implies today.

Anyway, it is great that this RFC provides a somewhat more structured way to think about fundamental. We should maybe consider whether want to devise another syntax for it. (Or maybe just continue with the current unstable attribute.)

When considering a possible alternative syntax, also note that we support fundamental types today. A fundamental type Foo is similar, except that the default is changed to Foo: !Trait is changed for all traits. I think the only fundamental type at present is Box (along with the builtin types like &T).

On the topic of ?Trait

I would prefer not to present ?Trait as a kind of predicate. That is, rather than writing T: ?Trait holds, I would rather say "neither T: Trait nor T: !Trait holds". I think that ?Trait can always be interpreted as opting out of strong, default declarations:

• T: ?Sized means "do not add T: Sized"
• impl ?StructuralTrait for T means "do not add a default impl of StructuralTrait for T".

There are a number of reasons for this. Among them, we know that T: ?Trait ALWAYS holds, so declaring that it does is not very useful. It's kind of confusing, too: if I can write Foo: ?Baz, what does that mean? Is Foo: ?Baz + !Baz a legal combination? What about trait Foo: ?Baz? I think it's better to focus on the two kinds of predicates that have meaning.

Oversimplifying

Just as a general note, most of the my examples above have made some implicit assumptions. For example, we are not talking at all about generic traits, or about blanket impls like impl<T> !Trait for T, etc. I'm not sure what complications might arise when we try to lift those.

!Trait inference

I think that the first form of !Trait "inference" (from the supertrait list) makes sense and I couldn't imagine it otherwise. This seems to follow directly from my interpretation above that T: Trait and T: !Trait are two distinct predicate forms. Therefore, since trait Foo: <Predicate> normally means that if T: Foo then T: <Predicate>, it only makes sense for this to work for both Trait and !Trait predicates.

The second form of inference, however, I like less. This is the !Trait inference based on "an implementation that would otherwise overlap" (the inference based on supertrait bounds like trait Edible: !Poisonous seems fine). For one thing, the language is rather vague and I'm not sure how one would implement it. Actually, in times past I've spent quite some time going down this road, in an effort to improve coherence and infer mutual exclusion, and it never led anywhere good -- iirc it was hard to even specify, and the best I could do meant that if you added any impl anywhere, you potentially had to re-evaluate the coherence properties of all impls everywhere, which would not be good for compilation times nor local reasoning. In any case, this rule also seems to be perpetuating the implicit "crate-based" reasoning around negativeness, but we agreed that this RFC gives us a more principled way to declare negative impls and one that we ought to be taking advantage of.

On that topic, there is a slight difference between the current crate-based reasoning and !Trait impls. That is, the existing system allows me to reason about my local types with precision, but not foreign types. Interestingly, downstream crates cannot take advantage of the negative reasoning that I myself use. That is, if I have a collection of trait impls for MyType that rely on the fact that MyType: !MyTrait, that is legal -- but it's not legal for some consumer to rely on that same fact. If we moved towards these explicit declarations, that would not be the case. It's conceivable one might want to retain the ability to have a "private" negative impl, though I don't know of an obvious good use case for that.

Done.

Whew! Thanks @withoutboats for a thought-provoking RFC. I'm going to post another comment in a bit with some deeper concerns (some of which also arise for specialiation). I feel like we have a lot of promising new ideas (this RFC, specialization, structural traits) but more effort is needed to gel thing into something coherent (no pun intended). Anyway, despite all my quibbles here, I really like the broad outlines of this proposal and I do think this is going in a good direction. Basically, this RFC seems to lay out a good way to rationalize and improve the "#[fundamental]" attribute.

[withoutboats]

Thanks! It's been a few months since I thought about this RFC, this is fun. Any lack of clarity is certainly my fault as author and not the fault of any reader. Especially anything to do with T: ?Trait, which I definitely used in two conflicting ways.

I think what this RFC, structural traits (thank you for this term which is much better than OIBITs!) and specialization are all circling around is this: the relationship between traits and types is well-described in terms of set theory. Traits and type parameters both refer to sets of types. We currently have ∈s (impl) and ⊆ (bounds) but we want to be able to describe more complex relations. And we are restrained by some facts which are external to the 'set nature' of traits:

• No actionable inference should be made on the basis of non-statement (because of backcompat and linkability). This is already violated in an intra-crate context, which is "fine" in that it doesn't violate either of the underlying justifications, but not great.
• For every possible set of declarations, the rules should consistently identify exactly one ∈ statement that has primacy for every type/trait pair (because this is how methods are dispatched, of course).

The goal of this RFC is essentially to introduce disjunction in a manner that is consistent with these constraints (mainly the first one).

I'm going to digest your comments more, especially on #[fundmental], and reply in specific. I really dislike #[fundamental] (I don't think its good design to use attributes to change how the type system works), but I'm not sure if there's a clean way to get the exact behavior #[fundamental] is used for.

[nikomatsakis]

No actionable inference should be made on the basis of non-statement (because of backcompat and linkability). This is already violated in an intra-crate context, which is "fine" in that it doesn't violate either of the underlying justifications, but not great.

Another way to look at this is in terms of 'intuitionistic' vs classical logic. Basically, it is not the case that either T: Trait xor T: !Trait. Rather it is the case that T: Trait nand T: !Trait -- in particular, neither could hold.

I'm going to digest your comments more, especially on #[fundmental], and reply in specific. I really dislike #[fundamental](I don't think its good design to use attributes to change how the type system works), but I'm not sure if there's a clean way to get the exact behavior #[fundamental] is used for.

If the concern is primarily about the syntax, I certainly agree. The attribute was chosen because it the a simple and low-cost way to introduce the notion we needed. But nobody loves it.

That said, there are a lot of places (e.g., Drop, negative impls, perhaps Copy), where we use impl syntax by default and it sort of opens up a lot of generality that we later have to cope with (e.g., "conditional" logic). This is often problematic: e.g., we may well want to say that traits either are fundamental or not, and not say something like "Trait is fundamental if T is Copy but not otherwise". Anyway I have some further thoughts about this but I've not finished writing them up yet (part of what happens is that writing things up prompts me to think more about it and we wind up with a kind of iterative cycle...which sometimes takes a while).

[nikomatsakis]

I wanted to follow up on this discussion about "intuitionistic" vs "classical" logic. The fact that there exist types where neither T: Trait nor T: !Trait holds (in fact, this would be the common case) implies that negative reasoning is not a substitute for specialization.

To see what I mean, imagine that I have two impls like this:

impl<T:!Clone> SomeTrait for T { .. }
impl<T:Clone> SomeTrait for T { .. }

In principle, this seems equivalent to these two impls (which rely on specialization):

impl<T> SomeTrait for T { .. }
impl<T:Clone> SomeTrait for T { .. }

But in fact this is not the case. The reason is that, in the specialization case, we know that SomeTrait is implemented for all T, because of the first impl. But in the negative reasoning case, we DON'T know that SomeTrait is implemented for all T. After all, if I have just some random type:

struct MyStruct { ... }

then I can't say whether MyStruct: Clone holds or not!

What this means is that if I wanted to use methods from SomeTrait, I could not write a function like this:

fn foo<T>(t: &T) { MyTrait::some_method(t); }

I would have to write one of the following:

fn foo<T:MyTrait>(t: &T) { MyTrait::some_method(t); }
fn foo<T:Clone>(t: &T) { MyTrait::some_method(t); }
fn foo<T:!Clone>(t: &T) { MyTrait::some_method(t); }

In any case, I know this RFC explicitly says that specialization is not an alternative, but the wording there didn't explicitly draw out this point about the excluded middle, and I thought it was non-obvious.

Also, as an aside, I don't fully agree with this characterization:

Put in terms of sets, traits declare sets of types; mutually exclusive traits are disjoint sets, and specialized implementations are subsets.

In particular, while this is true of the existing specialization RFC, there exist specialization variants where the subset relationship is not known to hold (and I personally think those variants could be very important for us -- but that's a comment for another RFC).

[nikomatsakis]

So I wrote something: A modest proposal around negative reasoning and auto traits. I've been sitting on this write-up for a long time, hoping to edit it some more, but I've decided just to post it. As the title says, this is a "modest proposal" around negativity. I am not promoting this as an RFC yet -- for one thing, the material on auto traits is not quite right yet, though the differences are kind of in the weeds -- but it outlines my thinking about negativity quite well. Essentially, if we were to ever adopt a !Trait system, this is the one I think we should have. At the moment, I'd say this is the only system that holds together coherently. Note that it is very similar, but not identical, to this RFC.

Frankly, I'm feeling pretty good about that proposal overall. But I know that others on @rust-lang/lang have some reservations. Let me try to summarize what I've heard:

• Is the idea of negative impls layering on more complexity than it's worth?
  • I personally think that negative impls can be explained quite well in terms of semver. That is, you are promising never to implement a trait in the future.
• If the primary motivation is to enable more flexibility in coherence, can we achieve that via specialization?
  • Negativity lets you combine a blanket impl impl<T: Foo> Bar for T with a specific impl impl Bar for Baz so long as Baz: !Foo can be proven.
  • But specialization might let you have those same two impls, using the logic: "currently, they are disjoint; but if Baz does implement Foo, then it will just be a specialization".
  • However, there are some limitations here:
    • The lack of lattice rules for specialization or some similar equivalent is a big one.
    • If the blanket impl doesn't use default items, then this rule would not work
      • And using default items implies we cannot project, so may not be an option.

[withoutboats]

Negativity lets you combine a blanket impl impl<T: Foo> Bar for T with a specific impl impl Bar for Baz so long as Baz: !Foo can be proven.

It also lets you combine multiple blanket impls such as impl<T: Foo> Bar for T and impl<T: Baz> Bar for T if T: !Foo where T: Baz or the inverse can be proven, which is not possible through specialization without lattice impls.

[withoutboats]

An example was posted in the subreddit today for which mutual exclusion would be well-suited, though it would also require another extension to the trait system surrounding Drop. The example was this:

trait Foo { }
impl<T> Foo for T where T: Copy { }
impl Foo for String { }

The compiler disallows this (outside of the standard library) because it won't assume that no future version of String will implement Copy. However, String can't implement Copy in a way backward compatible way because it carries a destructor.

The trait Copy could be said to have the definition trait Copy: Clone + !Drop { }. With something like the RFC proposed here, types with a Drop impl would not overlap with T: Copy. This would also require an inverted structural trait to be feasible: impl !Drop for .. { } (I don't believe these two changes present any backwards compatibility hazards if they are concurrent with introducing negative bounds at all).

However there is a wrinkle in that String does not itself have an implementation of Drop - it isn't !Drop because it has a field which is Drop, but the compiler can't assume that it will never become !Drop based on the rules we've laid out so far. Because Drop is already a very special case trait, it would seem reasonable to me to add one of these two special rules:

• Any type with a destructor meets the bounds Drop.
• Any type with a destructor is known not to meet the bounds !Drop and to never meet that bounds in the future, but is not known to meet the bounds Drop.

Both present a minor backward compatibility hazard in that removing all fields with a destructor is a breaking change. The first allows you to rely on that assumption in more cases.

[nikomatsakis]

We discussed this RFC at the @rust-lang/lang meeting last week. We decided it makes sense to postpone this RFC for the time being, under issue #1053. Essentially, there isn't a lot of active conversation, and it makes sense to wait until the specialization implementation has progressed a bit farther before we make any decision here.

As I wrote in my previous comment, though, I (personally) do think that there will be a role for negative reasoning, and that the broad outlines of this RFC are correct.

[oberien]

Now that specialization is stable and released, what is the status on this RFC?

[sfackler]

Specialization is not stable.

[aturon]

@oberien The ideas of this RFC are definitely something we're keeping in mind, but there are a lot of ways we might try to loosen the rules around coherence, so we're taking things a bit slowly.

We're hoping to get specialization officially stabilized in the next couple of months; it's blocked on some pretty deep implementation work. After that, we can start looking more seriously at various extensions.

[dhardy]

@pitdicker just hit an issue needing negative type bounds or specialization (see here).

[kennytm]

@dhardy If a type cannot simultaneously implement BlockRng<X> and BlockRng<Y> when X ≠ Y, perhaps you should make that generic parameter into an associated type instead.

trait BlockRng {
    type Element;
    type Results: AsRef<[Self::Element]> + Default;
}

impl<R> Rng for BlockRngWrapper<R> 
where
    R: BlockRng<Element=u32>,
    R::Results: AsRef<[u32]> // <-- FIXME why is this line needed?
{ ... }

impl<R> Rng for BlockRngWrapper<R> 
where
    R: BlockRng<Element=u64>,
    R::Results: AsRef<[u64]>
{ ... }

Yes this still emits E0119 "conflicting implementations of trait", but at least we can guarantee that these two impls will never overlap using the more conservative #1672 instead of this RFC.

(I guess all of these needs to wait for the chalk experiment to complete, though)

[newpavlov]

Another example of the need for mutually exclusive trait bound, or negative trait bound, or specialization with lattice rules, or something else in the line. In it I try to write support code which will allow us to use for loops with iterators (including implicit conversion using IntoIterator) and generators through desugaring of:

let result = for value in values {
    // body
};

To:

let generator = IntoGenerator::into_generator(values);
let result = loop {
    match generator.resume() {
        GeneratorState::Yielded(value) => {
            // body
        },
        GeneratorState::Complete(result) => break result,
    }
};

Quite unfortunately it seems this approach is currently impossible...