Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mutually exclusive traits #1148

Closed
wants to merge 5 commits into from

Conversation

withoutboats
Copy link
Contributor

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

Rendered

@alexcrichton alexcrichton added the T-lang Relevant to the language team, which will review and decide on the RFC. label Jun 3, 2015
fn nourish(&self);
}

pub trait Poisonous: !Edible {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@llogiq
Copy link
Contributor

llogiq commented Jun 3, 2015

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

👍 for the proposal

| | impl ?Trait for T | | |
| Default impl | by default | impl Trait for .. | impl !Trait for .. |
| Bounds | by default | where T: Trait | where T: !Trait |
| | where T: ?Sized | by default for Sized | |
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 nrc changed the title Mutex traits Mutually exclusive traits Jun 3, 2015
@nrc
Copy link
Member

nrc commented Jun 3, 2015

Changed the title to avoid confusion with mutexes

@huonw
Copy link
Member

huonw commented Jun 3, 2015

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.


It may be difficult to grok the difference between `!Trait` and `?Trait`. The reason for this difference only becomes clear with an understanding of all the factors at play in the coherence system. Inferred `!Trait` impls and the rarity of `?Trait` impls should make this an unlikely corner of the trait system for a new user to accidentally happen upon, however.

The `impl !Trait for T` syntax overlaps with the syntax of existing negative impls for types with default impls, and has slightly greater semantic content under this RFC tahn before. For each existing negative impl, it will need to be determined whether that type should impl `!Trait` or `?Trait` (that is, whether or not the non-implementation is a guarantee). That said, this change is not backwards incompatible and will not cause any regressions, and existing negative impls are an unstable feature outside of std.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@paholg
Copy link

paholg commented Jun 4, 2015

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
Copy link
Contributor

llogiq commented Jun 4, 2015

@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
Copy link

paholg commented Jun 4, 2015

@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
Copy link
Contributor

llogiq commented Jun 4, 2015

@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
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link

jnicklas commented Jun 4, 2015

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link
Member

huonw commented Jun 4, 2015

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
Copy link

Anachron commented Jun 4, 2015

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
Copy link
Contributor

llogiq commented Jun 5, 2015

@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
Copy link

Anachron commented Jun 5, 2015

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

Consolidated orphan rules stuff and implicit !Trait into a single section on inference
@llogiq
Copy link
Contributor

llogiq commented Jun 5, 2015

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?

@withoutboats
Copy link
Contributor Author

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
Copy link
Contributor

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
Copy link
Contributor Author

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
Copy link
Contributor

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
Copy link
Contributor

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
Copy link
Contributor

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link
Contributor

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
Copy link

oberien commented Feb 11, 2017

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

@sfackler
Copy link
Member

Specialization is not stable.

@aturon
Copy link
Member

aturon commented Feb 11, 2017

@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
Copy link
Contributor

dhardy commented Dec 28, 2017

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

@kennytm
Copy link
Member

kennytm commented Dec 29, 2017

@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
Copy link
Contributor

newpavlov commented Jan 16, 2018

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...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
T-lang Relevant to the language team, which will review and decide on the RFC.
Projects
None yet
Development

Successfully merging this pull request may close these issues.