nikomatsakis/a-modest-proposal.md Secret

## a-modest-proposal.md

      
    Raw
  

              a-modest-proposal.md
            
          
    I've been thinking about negative trait bounds a fair amount lately. I
think I'm starting to get a picture of how I see them fitting into our
system. This description is very similar to RFC 1148, but it differs
in a few particulars. It also incorporates some description of auto traits.
First, as in RFC 1148, the idea would be to embrace
"intuitionistic" over classical logic. What this means is that proving
T: Trait and proving T: !Trait are basically the same process: one
can prove T: Trait by finding a suitable impl of Trait, and
likewise one can prove T: !Trait by finding a suitable impl of
!Trait. It is however entirely possible that one cannot prove either
T: Trait or T: !Trait, so this means that !(T: Trait) does not
imply T: !Trait nor vice-versa. In fact, in a sense, Trait and
!Trait are almost completely independent predicates -- but as
we'll see, coherence does ensure that T: Trait xor T: !Trait,
which have an important semantic implications (but doesn't affect what
rustc does in particular).
In this RFC, I will adopt the RFC 1148 notation of writing T: ?Trait to mean that neither T: Trait nor T: !Trait are
provable. Unlike RFC 1148, I don't anticipate making this
something that users can actually type (though one could imagine
allowing impl ?Trait declarations for auto traits in particular).
Second, we would adapt coherence to be based primarily on explicit
negative impls. I put forward an initial proposal that is fully
backwards compatible, but I suspect this is an area where we could get
away with some changes.  In particular, I would like to at minimum
remove #[fundamental].  See
the section on "Negative reasoning in coherence"
for details.
Negative impls

In terms of impls, users would now have the ability to explicitly
implement a "negative impl". This can be understood as a commitment
that the type will never implement the given trait:
impl<...> !Trait<...> for Type { }
These impls don't have any particular restrictions. As today, their
body is always empty (maybe we should just write a ;).
Most parts of the system would treat !Trait basically as if it were
a completely distinct trait from Trait. So if you want to that T: !Trait, you would search for negative impls that cover that case.  If
you want to prove that T: Trait, you would search for positive impls
that cover that case.
Put another way, if you ignore coherence, you could consider:
trait Trait { ... }
impl Trait for T { ... }
impl !Trait for U { }
as being equivalent to introducing a marker trait NotTrait like so:
trait Trait { ... }
trait NotTrait { /* empty */ }
impl Trait for T { ... }
impl NotTrait for U { }
Negative bounds

We can also permit negative bounds of the form T: !Trait. As
described in the previous section, T: !Trait only holds if we can
find a suitable negative impl. (However, we could also drop support
for these bounds, at least for now, which simplifies some aspect of
this proposal; see the
list of "unknowns and variants" at the end.)
Coherence of Trait and !Trait

The only bit of the system that really acts differently is coherence.
We use the term "polarity" to refer to whether an impl is for Trait
(positive polarity) or !Trait (negative polarity).
The coherence rules would ensure that every pair of positive impls
is disjoint. They also ensure that every positive impl is disjoint with
every negative impl.
Note that the coherence rules do not need to ensure that every
negative impl is disjoint with every negative impl. This is basically
analogous to RFC 1268, the RFC we adopted which relaxes the
coherence rules for marker traits. Unfortunately, it carries the same
implementation complications -- if we cannot solve those, then we
should simply have coherence ensure that negative impls are disjoint.

Negative reasoning in coherence (and backwards compatibility)

In general I would like to try to integrate !Trait bounds into
coherence better. This is where things get a bit tricky. Let's first
describe my ideal world. Ideally, to my mind, the coherence overlap
algorithm would rely only on explicit negative impls.
That is, the algorithm for judging overlap might look something like
this (this is an adapted version of what we have today):

Replace all type and lifetime variables with inference variables.
Unify the trait references (if not possible, the impls are disjoint).
Let P be the union of the where clauses on both impls.
Let Q be a set containing the "flat map" of the inverse of the
where clauses in P, as follows:

T: Trait<..> becomes Some(T: !Trait<..>)
T: !Trait<..> becomes Some(T: Trait<..>)
all other where clauses (e.g., T: 'a, 'a: 'b) become None

iow, they have no inverse and cannot be used to prove disjointedness


If we can successfully evaluate any of the where clauses in Q,
then the impls are disjoint.
Otherwise, they may overlap.

However, this procedure has two limitations:

It doesn't understand mutually inconsistent sets of bounds.
It would probably break far too many existing crates to be feasible.
In particular, it doesn't permit any of implied negative logic that
RFC 1023 specified.

Let's look at those two things in detail.
Mutually inconsistent sets of bounds

The other problem with the procedure above is that it will not be able
to handle pairs of impls like the following:
impl<T:Foo> Bar for T { }
impl<T:!Foo> Bar for T { }
These two impls really ought to be considered disjoint, because we
know that T: Foo xor T: !Foo. Unfortunately, the procedure above
will fail, because it will try to prove that T: Foo (and fail) and
then try to prove that T: !Foo (and fail). In particular, we need a
"directional" overlap check, where we consider the preconditions of
one impl, and use those to check for contradictions with the other
impl. This is quite similar to what specialization
does. Alternatively, we could try to adapt the approach specified in
RFC 586 of detecting "mutually inconsistent" bounds in a set of
bounds, but that feels a bit trickier to me (for example, we would
need to ensure that neither impl is inconsistent on its own, as well).
Since this doesn't seem that tricky, I'm just going to assume we
solve this for now. :)
Backwards compatibility

For reference, the rules there was that coherence could use implicit
negative reasoning about a trait reference T: Trait<U..> if that
trait reference met the following critera:

the types [T, ...U] in the trait reference meet the orphan rules; or,
the trait Trait is declared #[fundamental].

There are two ways we could incorporate this kind of reasoning
into the scheme described thus far:

You could extend the notion of T: !Trait<..> to say:

if the types meet the orphan rules, you can deduce that !Trait holds simply
by the absence of a positive impl


Or you could keep !Trait as requiring an explicit impl, but just
allow coherence to use a slightly extended form of negative
reasoning.

I favor the second approach. In particular, I would extend the
algorithm I gave before with another step (step 6 is new):

Replace all type and lifetime variables with inference variables.
Unify the trait references (if not possible, the impls are disjoint).
Let P be the union of the where clauses on both impls.
Let Q be a set containing the "flat map" of the inverse of the
where clauses in P, as follows:

T: Trait<..> becomes Some(T: !Trait<..>)
T: !Trait<..> becomes Some(T: Trait<..>)
all other where clauses (e.g., T: 'a, 'a: 'b) become None

iow, they have no inverse and cannot be used to prove disjointedness


If we can successfully evaluate any of the where clauses in Q,
then the impls are disjoint.
Let R be the set of trait references in P that meet the criteria
from RFC 1023.

Check whether any of those cannot be proven, using today's classical logic.
If so, the impls are disjoint.
However, we issue a deprecation warning suggesting the use of an explicit negative impl.


Otherwise, the impls may overlap.

Note that we continue to permit the same impls as ever, but we issue a
deprecation warning. That is, we are going to try and actively migrate
people to use explicit negative logic (but we are not going to take
the implicit logic away).
There are several reasons that I favor the approach of deprecating implicit
negative logic and containing the damage to coherence rather than
infecting T: !Trait<..> altogether:


Implicit negative logic is easy to do by accident. I suspect we
are accidentally making assumptions about types that we are not
aware we are making. I know I found some cases like that in the
standard library from time to time. Moreover, by adding a
deprecation warning, we may eventually get ourselves into a position
where we can remove the implicit logic altogether (either as part of
a Rust 2.0, or just if we are able to determine that the logic is
not widely used).


Implicit negative logic is dangerous. If we make !Trait use
the implicit logic of specialization, it means that one cannot
understand T: !Trait as being equivalent to T: NotTrait, but
rather one must think of it as a different thing altogether, obeying
much more complex rules. This means that the interactions with the
existing system, and in particular lifetime erasure, become much
less clear; it also means that we must think very carefully about
how it will interact with new features like specialization.

I don't yet have a smoking gun problem, but it seems clear that,
at minimum, specialization would have to consider T: !Trait<..>
very carefully in any kind of "lifetime-parametric" analysis.
Also, most prolog and logic systems have shied away from classical
logic, because it cannot be implemented in a complete fashion.
I'm not sure of the details here, but it seems to me we would be
wise to stay away too. (And implicit negative logic is a kind of
classical logic, since we assume that !(T: Trait) implies
T: !Trait.


Implicit negative logic is challenging to implement. At minimum,
implicit negative logic would make the implementation of region inference
and lifetime erasure much more complex. Today, all of our region bounds
devolve into 'a: 'b relations, which are reflexive (that is, 'a: 'a).
(Equality can be understood as 'a: 'b and 'b: 'a.). This means that
we can implement region inference using fixed-point iteration (well, mostly),
and that we can implement lifetime erasure by just replacing all
lifetimes with 'static. If we allowed implicit negative logic,
though, you could construct irreflexive lifetime relations:
trait Foo<'a, 'b> { }
  
struct LocalType;
impl Foo<'a, 'b> for LocalType where 'a: 'b { }
Now LocalType: !Foo<'x, 'y> is true if 'x: 'y does NOT hold,
which means that 'x must be strictly smaller than y. This
would break a lot of assumptions in the compiler.


Removing fundamental

So far, I haven't proposed anything backwards incompatible. However,
one of the things that makes explicit !Trait impls appealing to me
is that they offer a better alternative to #[fundamental]. I
suspect we could get away with removing #[fundamental] altogether
and just keeping the implicit negative logic around local
types. (Ideally, we'd get rid of that too, but I think that could
break a lot of code. We'll have to test.)
The reason that I think we can remove #[fundamental] is that we were
very parsimonius about applying it. Currently, it is only applied to
three traits in the standard library:

the Sized trait; and,
the closure traits Fn...FnOnce.

Clearly, the special logic around Sized would have to stay: but
that's ok with me. Sized is a very special trait. It does not permit
ANY user-defined impls, and it is always evaluated by the compiler to
a boolean value, essentially (though false might mean "not known to
be Sized).
The special logic around closure traits we could probably remove. The
reason this was added was to support the string patterns API,
which wants to be able to accept either a closure or a constant string
without a problem. So removing #[fundamental] would require us to
add explicit negative impls of FnMut to (at least) the following
implementors of Pattern:

impl<'a, C> Pattern<'a> for CharEqPattern<C> where C: CharEq
impl<'a> Pattern<'a> for char
impl<'a, 'b> Pattern<'a> for &'b [char]
impl<'a, 'b> Pattern<'a> for &'b &'b str
impl<'a, 'b> Pattern<'a> for &'b str
impl<'a, 'b> Pattern<'a> for &'b String

What I don't know is what other traits out there in the wild might be
affected.  That is, anybody can write a trait like Pattern --
unfortunately, RFC 1210 did not require an unstable feature gate to
employ the #[fundamental] attribute. I regret that now, but
luckily we were very parsimonious in applying it, which may be good
enough. The only way to know is to implement it and try it out (well,
actually, some targeted acks through the crates.io sources might be
helpful too).
Interaction with specialization

If/when we add specialization, I don't think it adds any particular
complications. This is precisely because of the fact that !Trait can
be thought of as equivalent to a marker trait NotTrait (but with
added coherence support). If however we were to incorporat
RFC 1023 like logic into !Trait, things get more complicated --
then we'd probably have to consider !Trait, when applied to a
fundamental trait or local types, as being
lifetime-non-parametric. That would be unfortunate.
Refining the auto trait specification

The auto trait RFC differs in several particulars from the
actual implementation, which causes confusion. The most
important one is that it specifies a kind of "fallback" semantics,
where we first look for positive impls, then negative impls, then
finally a default impl. This is basically the "implicit negative
logic" I decried above. What is actually implemented is actually much
more aligned with what you see in this document, but it still contains
some worrisome bugs, such as #23072.
In general, I think auto traits should be considered a kind of
"defaulting" mechanism. That is, if for some given type T, you do
not supply any impls, then we will automatically supply one for
you. This impl will ensure that T: Trait is implemented only if all
the types of all data reachable from T implement Trait.  We never
generate an automatic T: !Trait impl.
The categories of types where a default impl will be generated if
no applicable impl is found are:

Scalar types like i32 etc -- these are just implemented by
default.
Tuples for each arity, like (_,), (_, _), etc -- these are
implemented by default if their component types are implemented.
Reference types &_ and &mut _ as well as pointer types
*const _ and *mut _ -- these are implemented if their referent
is implemented.
Slice types [_] and array types [_; N] for every possible length
-- these are implemented by default if their component types are
implemented.
User-declared struct and enum types S<..> -- these are implemented
by default if their field types are implemented (see the algorithm
below).

Let me give some examples to try and clarify this.
Synthesizing impls: some examples on structs and enums

Let's start with some examples involving user-defined struct and
enum types. I'll use the Send trait as my example of an auto trait
trait (Send happens to be an unsafe trait, so you'll see the
unsafe keyword below, but that is basically orthogonal to the main
point).
As we will see in these examples, the basic intution is that if the
user declares anything about a given struct or enum, then auto trait
traits behave normally for that type, like any other trait. It's only
in the case where the user declares nothing that the auto trait
acts differently.
Here is the most basic example: if we just declare a new struct type,
and nothing else, then we will synthesize an impl for that struct. (In
fact, the precise process by which this impl is synthesized is fairly
subtle, but let's ignore that for now.)
struct StructA<T> {
    vec: Vec<T>
}

// There are no explicit of impls of any polarity for `StructA`,
// and hence this implies the creation of an impl roughly like this:
//
// unsafe impl<T> Send for StructA<T>
//    where T: Send { }
Note that this implies that we can never prove StructA<T>: !Send
because we do not synthesize a !Send impls (though we may of course
fail to prove StructA<T>: Send, if we cannot prove T: Send).
However, if there are any explicit impls for a struct (of any
polarity, and with any type parameters), then no impl is synthesized
at all:
struct StructB<T> { .. }
unsafe impl Send for StructB<i32> { }

// Issue #23072
struct StructC<T> { .. }
impl<T:Default> !Send for StructC<T> { }

// Issue #27554
struct StructD<T> { .. }
unsafe impl<T:Default> Send for StructD<T> { }

// No synthetic impls created for `Struct{B,C,D}`.
Let's look at StructB first. There is one explicit impl, so that
means we can prove StructB<i32>: Send but we can't prove
StructB<T>: Send for any type T != i32. This also implies that the
current behavior for issues #23072 and #27554 is in fact
roughly correct. Consider StructC above -- because of the explicit
negative impl, we can prove that StructC<Foo>: !Send, but only if
Foo: Default. However, since there are now no positive impls at all,
we can never prove StructC<T>: Send for any T (and in particular
it doesn't matter whether T: Default or not). Similarly, for
StructD, we can only prove that StructD<T>: Send if T: Default.
Synthetic impls for things other than structs or enums

When you declare an auto trait, you can also declare impls for the
builtin type constructors (that is, types other than structs or
enums). Those too act to suppress or enable synthetic impls, and the
intution is roughly the same: if you say nothing about some builtin
type cosntructor, then it will follow the default rules, but if you
say anything at all, it acts like any other trait.
The set of builtin type constructors is in fact infinite, and it is
roughly as follows. I will use _ to indicate types; I am
intentionally not giving the types a name since the type constructor
applies regardless of what the type is.

scalars: i32, u32, etc
pointers: *const _, *mut _
references: &_, &mut _ (for any lifetime)
tuples: (_,), (_, _), (_, _, _), ...
slices: [_]
arrays: [_; 0], [_; 1], [_; 2], ...

Let's see some examples to see how this works. For all the examples to
come, I'll assume the impls are declared alongside a simple auto trait
trait MyOibitTrait, declared like so:
trait MyOibitTrait { }
impl MyOibitTrait for .. { }
OK, let's start with scalars. If I say nothing about i32, say, then
it is assumed i32: MyOibitTrait. But I can also pick and choose for
specific scalar types:
impl MyOibitTrait for i32 { }
impl !MyOibitTrait for f32 { }
then we find that while i32: MyOibitTrait still holds, f32: MyOibitTrait does not. Moreover, f32: !MyOibitTrait does hold.
Let's move on to pointers. By default, *const T: MyOibitTrait holds
if T: MyOibitTrait holds. But I might want to override that, as in the
Send trait:
impl<T:!Send> !MyOibitTrait for *const T { }
impl<T:Send> MyOibitTrait for *const T { }
Now there is no synthetic impl for *const T, and hence *const T: MyOibitTrait is only provable if T: Send. Similarly, *const T: !MyOibitTrait is only provable if T: !Send. Otherwise, if T: ?Send, then *const T: ?MyOibitTrait.
Finally, let's talk about tuples, slices, and arrays. We might want to
just prohibit implementing auto traits over these kinds of types,
because there are an infinite set of them. It's not really clear then
how useful it can be to write a specific impl. However, if we did
permit it, it might have the following meaning:
// For whatever reason, MyOibitTrait is always
// implemented for two-tuples:
impl<T,U> MyOibitTrait for (T, U) { }

// But we still generate synthetic impls for other arities:
//
// impl<T> MyOibitTrait for (T,) { } // 1-tuple
// impl<T,U,V> MyOibitTrait for (T,U,V) { } // 3-tuple
// impl<T,U,V,W> MyOibitTrait for (T,U,V,W) { } // 4-tuple
// ...
I guess alternatively we might just lump all tuples together, so if
you write an impl for a 2-tuple, it prevents any impls from being
generated for tuples or other arities (and similarly for array
lengths). That would probably be better.

Unknowns and variants

Let me just note down some unknowns and variants in this proposal:

The entire proposal fits together even without adding explicit where
clauses of the form T: !Trait. That is, we might just add negative
impls (at least to start) and incorporate those into coherence, and
leave negative reasoning out elsewhere.
The precise coherence algorithm that incorporates knowledge of T: Trait xor T: !Trait.  (I don't think, though, that knowing about
this "xor property" is important anywhere outside of coherence.)
Seems fairly non-scary. This point is moot if we drop explicit T: !Trait bounds.
The precise algorithm by which synthetic auto trait impls are created. I
am coming around to the idea of making auto traits purely inductive
but following a kind of "coinductive-like" elaboration procedure:
basically building out a tree of things to prove and stopping
whenever we get to either a user-provided case or a cycle.  This
also seems mostly non-scary at this point, but I haven't had time to
write it up.
We may want a way to impl ?OibitTrait for Type, see section below
for more details.

Auto traits and ?Trait impls

You'll note that there is no way here to supress the generation of a
synthetic impl without also making an affirmative declaration of some
kind. That is, I can either impl OibitTrait for MyStruct or I can
impl !OibitTrait for MyStruct, but either way I am making a future
commitment. Maybe I just want to hold off on that.
In fact, this can be done, but it's kind of hacky. You have to use
a dummy private type as a member of the struct:
struct Dummy;
impl !OibitTrait for Dummy { }

pub struct MyStruct {
    dummy: Dummy
}
(For generic types, one can use a similar hack to impl !OibitTrait for MyStruct<Dummy>.)
To make this more of a first-class declaration, we could permit an
explicit impl of ?MyOibitTrait:
impl ?OibitTrait for Dummy { }
This would suppress all synthetic impls. However, I am not particulary
keen on including this option, for a few reasons:

it suggests that T: ?Trait is a "predicate that can be proven", just
like T: Trait and T: !Trait, but in fact T: ?Trait would be quite
different (and, in particular, it holds because of the absence of impls,
typically).
I'm not sure how often this is necessary; the dummy trick seems not intolerable.