Automatically implement some traits for !

[canndrew]

This RFC assumes the !-type RFC as a prerequisite.

Rendered

[glaebhoerl]

What about writing

impl !MyTrait for ! { }

instead of the attribute?

The double ! is a bit funky, but in general I'm uncomfortable with attributes which have language-level semantic effects (besides macro attributes), and in this case we luckily have just the right in-language syntax for it already.

[Virtlink]

Why not the other way around? Opt-into implementing !.

#[derive(!)]
trait Debug {
    // ...
}

Then there would be no surprise that a trait implements !, and the user would get an informative error if the trait has static methods, associated types, or any other reason the ! auto-implementation cannot be derived, which is nice. Also, it would be more consistent with auto-implementations for structs, such as Debug, that are opt-in even if the majority of structs is expected to implement it.

Finally, I don't like that my program's behavior is influenced by seemingly unrelated changes, such as adding a static method causing the ! auto-impl to be lost. This will get confusing very quickly, especially to new users.

[canndrew]

@glaebhoerl

What about writing...

Good point. That's a much better way of doing it.

@Virtlink

Why not the other way around?

Because it would be too intrusive having to appear on most traits for something that rarely gets used. In practice, I think most people will just leave it off and then their traits won't be implemented for ! even though they should be.

Then there would be no surprise that a trait implements !

Remember that this is all dead code and that these impls don't do anything. I don't think the compiler needs to be at all picky if someone wants to use ! somewhere where's there's only one thing they could possibly mean. By contrast #[derive(Debug)] actually does something, it generates real code and there may be reasons people don't want to use that code. Also ! already has similar magically lenient behaviour where things Just Work. We don't make people write:

let x: u32 = match opt {
    Some(y) => y,
    None => panic!("ahh") as u32,
}

and the user would get an informative error if the trait has static methods, associated types, or any other reason

They could still get this error message anyway if the trait isn't explicitly implemented for ! and the implementation can't be derived.

[withoutboats]

I'm moderately in favor of #1216 because if we have ! in the return position I think it makes sense to have it everywhere, but I'm very wary of a proposal like this. I'm inclined, without demonstrable use cases, against even providing impls for ! for any trait in the standard library. Just because it can be done in theory doesn't mean it should be; why would a user want to pass ! as a Hasher and so on? Is that code we would consider idiomatic? Does it express its intent with clarity and accomplish its purpose parsimoniously? ! is already a hard concept to teach, I don't want to see it have even more complexity.

[canndrew]

@withoutboats

why would a user want to pass ! as a Hasher?

Why not? ! is a perfectly valid Hasher. A Hasher is something that you can feed data into then finish to create a u64. If you have a ! (you don't) then you can feed data into it and finish it (because ex falso quodlibet). Here's a completely contrived use-case for !: Hasher. Suppose I have a trait:

trait PreHasher {
    type H: Hasher;
    fn into_hasher(self) -> io::Result<Self::H>;
}

But then I want to make a dummy implementor of this trait which always errors.

struct ErroringPreHasher;

impl PreHasher for ErroringPreHasher {
    type H = !;
    fn into_hasher(self) -> io::Result<!> { ... }
}

Why shouldn't this be allowed?

@Virtlink

Finally, I don't like that my program's behavior is influenced by seemingly unrelated changes, such as adding a static method causing the ! auto-impl to be lost.

Well, changing the definition of a trait will already break all the users of that trait in most cases. And presumably the user will get an error message telling them why the impl couldn't be derived.

[kennytm]

Nit: "... to learn that ! implements their trait"

[canndrew]

Thanks. Fixed.

[withoutboats]

Why shouldn't this be allowed?

Because special cases aren't necessarily special enough to break the rules. You don't need to convince me that this RFC is sound, I can see that. What I don't agree is that the use case for adding these special rules justifies the additional complexity of the language in having these special rules.

[aturon]

I largely agree with @withoutboats. I also want to raise a specific area of nervousness: we've talked about possible extensions to the trait system like negative bounds or mutually-exclusive traits, and the latter in particular would need to be done carefully if we also had auto-implementation. I also feel uneasy about the fact that this would only apply to some/most traits -- it feels like nontrivial complexity for something that will probably be pretty obscure in practice.

More broadly, though, I'm inclined to reach a decision on #1216, get some experience using it, and then determine from that experience how well-motivated this RFC is. I think it'd be premature to reach a decision on this RFC until then. (And on that note, think we should postpone this RFC for the time being.)

[nikomatsakis]

I agree with @withoutboats that I don't yet see strong reasons to add such impls. It seems like something we could do over time (and on a piecemeal basis) if we chose, perhaps eventually adopting a more automatic proposal like this.

I am overall nervous about this proposal in a number of ways. First, the interaction with other parts of the (already complex) trait system, as @aturon pointed out, but also the fact that we can't write these "automatic" impls for all traits, only a kind of random subset that doesn't align with other things in the language (it sort of aligns with object-safe, I suppose, since -- like objects -- it requires an instance of the type for the impl to make sense and be usable).

It also may be a subset that continues to evolve: e.g., what about associated constants? Other sorts of associated items?

[withoutboats]

@aturon's point about negative bounds seems particularly apt. Why should !: Hasher but not !: !Hasher? There's also only one unique impl of !Hasher for ! (indeed, there's only one unique negative impl of any trait for any type). Regardless of whether or not the complexity is justified, this proposal just seems like incorrect behavior in light of these sort of extensions.

The right implementation of this proposal seems to me to be some sort of special rule in which ! meets any trait bound, with some defined semantics that amount to "its always !" for every sort of associated item (for example, any associated function evaluates to !). I still don't think there's evidence that this is worth the complexity, but I think it would be more correct than this proposal.

[kennytm]

@aturon The mutually exclusive trait links back to here, do you mean #1148?

[aturon]

@kennytm Yes, I do. Fixed, thanks!

[canndrew]

More broadly, though, I'm inclined to reach a decision on #1216, get some experience using it, and then determine from that experience how well-motivated this RFC is. I think it'd be premature to reach a decision on this RFC until then. (And on that note, think we should postpone this RFC for the time being.)

I whole-heartedly agree.

It also may be a subset that continues to evolve: e.g., what about associated constants? Other sorts of associated items?

If they can't be inferred then the impl as a whole can't be inferred.

The right implementation of this proposal seems to me to be some sort of special rule in which ! meets any trait bound, with some defined semantics that amount to "its always !" for every sort of associated item (for example, any associated function evaluates to !).

Maybe I don't understand what you're proposing here but this doesn't sound right at all. If a trait has static methods or associated types/constants then the compiler has no idea how the user might want to define them for !. For examples, here's how I might impl some traits like this for !

/// Types that have a dual type
trait Dual {
    type D: Dual
}

impl Dual for () {
    type D = !;
}

impl Dual for ! {
    type D = ();
}

/// Format the name of a type
impl DebugTypename {
    fn fmt(f: &mut fmt::Formatter) -> fmt::Result;
}

impl DebugTypename for () {
    fn fmt(f: &mut fmt::Formatter) -> fmt::Result {
        write!(f, "()")
    }
}

impl DebugTypename for ! {
    fn fmt(f: &mut fmt::Formatter) -> fmt::Result {
        write!(f, "!")
    }
}

The whole point of this RFC is that it only works in cases like Hasher where the user really has no freedom at all in how to define the impl.

[withoutboats]

The whole point of this RFC is that it only works in cases like Hasher where the user really has no freedom at all in how to define the impl.

But in the presence of negative impls, a user does have a choice - they could impl Hasher or !Hasher. This RFC already proposes making an arbitrary choice for the user.

[joshtriplett]

I ran into some concrete use cases for this recently. I wanted to call a noreturn function (declared with -> !) in a context that wanted the return value to implement a particular trait. This would have made that possible.

This seems entirely safe due to Rust's guarantee that code involving ! can never run. Unlike Haskell's diverging types like undefined (of type a, any type without restriction), ! cannot ever show up at runtime, and if you misuse it you'll get a compile-time error, not a runtime error. Given that, 👍 on this RFC.

[golddranks]

Regarding the issue about negative / positive impls, has anyone with sufficient knowledge in type theory (which I certainly don't have) considered the possibility that ! implemented BOTH negative and positive traits, if the negative ones would be conceived some day? Sounds totally unsound, but I wonder if the special properties of ! (I.e. doesn't contain values at all) make it all good.

[kennytm]

@joshtriplett Can't you cast the result to a concrete type that impl that trait? Something like

fn main() {
    let f: u32 = panic!(""); // <- u32: Clone
    f.clone();
}

[DemiMarie]

@golddranks I am not so sure – in dependently typed languages the mere existence of a diverging value often allows one to obtain a proof of anything, which allows one to coerce incompatible types; at runtime, the diverging proof term has been erased, but the unsafe cast hasn't, resulting in undefined behavior.

I don't think this is an issue for Rust or for any reasonable future extension – but it would take someone with experience in type theory to say for certain.

[glaebhoerl]

@drbo (I don't know whether or how this relates to @golddranks's suggestion; just for the record.)

in dependently typed languages the mere existence of a diverging value often allows one to obtain a proof of anything, which allows one to coerce incompatible types

This is true even in non-dependently-typed languages such as Rust. If you obtain a "value" of ! (or enum Never { }) at runtime, that is undefined behavior. (From a type-theoretical perspective it's something like the canonical example of it.) This is why you can always "return" panic!() from a function, no matter what type it returns.

What's different about dependently typed languages (although note that this is a human-created coincidence, not a fundamentally required property of them) is that most of them aim to be not just type-safe, but also logically consistent. What this means is that an expression of type ! (or False, or Void, or Zero, or Bottom, or ⊥) cannot even type-check. There is no panic!, nor loop { }, nor fn f() -> T { f() }, nor any other way of getting out of your promise to produce a value of type T where you said you would produce a value of type T.

[DemiMarie]

Actually, the difference is that in dependently typed languages, the bottom
type can be used to prove equality of any two types, allowing for
unsoundness. At runtime, the proof term is erased, so the mere fact that a
term has the bottom type leads to unsoundness, even if the term would go
into an infinite loop at runtime (which is well-defined behavior).
On Jun 24, 2016 6:26 AM, "Gábor Lehel" notifications@github.com wrote:

@drbo https://github.com/drbo (I don't know whether or how this relates
to @golddranks https://github.com/golddranks's suggestion; just for the
record.)

in dependently typed languages the mere existence of a diverging value
often allows one to obtain a proof of anything, which allows one to coerce
incompatible types

This is true even in non-dependently-typed languages such as Rust. If you
obtain a "value" of ! (or enum Never { }) at runtime, that is undefined
behavior. (From a type-theoretical perspective it's something like the
canonical example of it.) This is why
https://en.wikipedia.org/wiki/Principle_of_explosion you can always
"return" panic!() from a function, no matter what type it returns.

What's different about dependently typed languages (though note that this
is a human-created coincidence, not a fundamental property of them) is that
most of them aim to be not just type-safe, but also logically consistent.
What this means is that an expression of type ! (or False, or Void, or
Zero, or Bottom, or ⊥) cannot even type-check. There is no panic!, nor loop
{ }, nor fn f() -> T { f() }, nor any other way of getting out of your
promise to produce a value of type T where you said you would produce a
value of type T.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
#1637 (comment), or mute
the thread
https://github.com/notifications/unsubscribe/AGGWB4MJl075l-98a8obTE7Li8Pr_jnqks5qO7DagaJpZM4IuE8z
.

[glaebhoerl]

Okay, I think I understand what you're saying: unlike in Rust, which uses strict evaluation everywhere, the dependently typed language doesn't (always) evaluate the given term to normal form, because it assumes that, due to logical consistency, one has to exist anyways, and so computing it would be needless busywork? (I suppose "the proof term is erased" is another way of saying the same thing, I hadn't made the connection.) This sounds like basically the same issue that Richard Eisenberg describes for GHC's type families.

(Again though, I think this is a property of the dependently typed languages that happen to exist and are popular, not something that necessarily follows from being dependently typed?)

[digama0]

I second @golddranks's suggestion that ! implements all trait bounds, both positive and negative, if it can do so uniquely. In the example of the RFC:

pub trait Consumable {
    fn consume(&self);
}

pub trait Edible: !Poisonous {
    fn nourish(&self);
}

pub trait Poisonous: !Edible {
    fn sicken(&self);
}

impl<T> Consumable for T where T: Edible {
     fn consume(&self) { self.nourish() }
}

impl<T> Consumable for T where T: Poisonous {
     fn consume(&self) { self.sicken() }
}

there is no problem with T = ! here, because neither implementation of consume(self: &!) is callable. However it might be that the type parameter is not used:

pub trait MyTrait {
    fn do_it();
}

pub trait Marker {}

impl<T> MyTrait for T where T: Marker {
     fn do_it() { println!("Called on Marker"); }
}

impl<T> MyTrait for T where T: !Marker {
     fn do_it() { println!("Called on !Marker"); }
}

In this case !, which cannot auto-impl MyTrait, is given two distinct impls from its auto-impls !: Marker and !: !Marker. Thus MyTrait::do_it::<!>() is a compile error, being ambiguous, so you have to use UFCS <MyTrait as Marker>::do_it::<!>() (if I wrote that correctly). I can see a potential problem if this is used in macro expansion, because for any other type that would be an unambiguous expression, but I think this speaks more to the problems of having negative impls than anything else.

I have a background in proof theory, and the "type impls trait" judgement is like a provability assertion, which composes nicely. In contrast, unprovability assertions do not, which reflects the fact that later trait impls can cause a !Trait bound to be lost. The RFC resolves this by considering ?Trait bounds as well, which correspond to the classification of mathematical statements as provable, refutable, or independent. The RFC mentions:

It goes without saying that it would be a coherence violation for a single type to implement both Trait and !Trait.

The mathematical equivalent here is that of an inconsistent system. It should not be a surprise that ! is inconsistent: after all that's the whole point. In general, there is no innate problem with letting arbitrary types implement both Trait and !Trait, but this will cause issues in code that is not expecting it, so it makes sense to warn on seeing this, which ! will opt-out of. (One way this differs from a mathematical inconsistent theory is that there is no rule A + !A -> B. Type-theoretically, that's because !A has the wrong signature: instead of being empty, it should be a function from impls of A to impls of B. Needless to say Rust isn't really in a position to support this.)

The linked RFC is also not clear on how far "reverse deduction" is permitted for trait bounds. If impl B for T where T: A, then logically we should also have impl !A for T where T: !B. But if that is so then something like impl A for Vec<T> where T: A should also be reversible to impl !A for T where Vec<T>: !A which diverges if you throw it into your type inference algorithm.

My view is that negative impls (at least with the given RFC) are type-theoretically unsound, and ! just makes this more obvious.

[withoutboats]

In general, there is no innate problem with letting arbitrary types implement both Trait and !Trait, but this will cause issues in code that is not expecting it, so it makes sense to warn on seeing this, which ! will opt-out of.

I don't know what you mean by "innate" but the problem with allowing types to implement both Trait and !Trait is that our coherence algorithm would treat these traits as disjoint.

My view is that negative impls (at least with the given RFC) are type-theoretically unsound, and ! just makes this more obvious.

To me this conclusion is non sequitur from the rest of your post, could you elaborate?

I suggest we discuss this further on #1658, where it would be much more on topic than on this RFC's discussion thread.

[digama0]

@withoutboats I'll just give a quick response, my post got away from me a bit there.

I don't know what you mean by "innate" but the problem with allowing types to implement both Trait and !Trait is that our coherence algorithm would treat these traits as disjoint.

I was trying to reason out the logical consequence of a type for which T: Trait + !Trait is provable. It's all well and good to say "just crash if you find this" but that's outside the type system, and searching for a contradictory bound is quite nonlocal (you are basically trying to prove the system is consistent).

My view is that negative impls (at least with the given RFC) are type-theoretically unsound, and ! just makes this more obvious.

To me this conclusion is non sequitur from the rest of your post, could you elaborate?

Roughly, the notion not(T: A) has not been clearly defined in any of the negative bound proposals. Logically this should be a deduction rule that allows you to prove any trait bound given T: A, i.e. causing inconsistency; but a plain marker trait does no such thing.

Anyway, I'll stop here and migrate to #1658 (which I should note differs from the proposal that I was referencing above).

[canndrew]

There's a compromise position that I think everyone could support: what if we allowed trait impl method definitions to be omitted when they have an argument of an uninhabited type? For example:

trait MyTrait {
    fn static_method();
    fn non_static_method(self);
}

impl MyTrait for ! {
    fn static_method() {}
    // non_static_method can be omitted because it's uncallable
}

This would allow you to impl !: Hasher by simply writing

impl Hasher for ! {}

Of course this still comes with the problem that people will need to explicitly say that they want the impl which is largely what this RFC was trying to avoid.

[digama0]

@canndrew This method also requires explicit impls, which means that you can't "fix someone's oversight" if, say, libstd didn't decide to impl Hasher for !. But maybe wrapper structs can make up for this, as they do in idiomatic Rust.

[canndrew]

@digama0 I would still want the full form of this RFC (It think, and only if it's compatible with other future features like negative trait bounds). The good thing about the compromise idea though is that it's forwards-compatible with this RFC.

[withoutboats]

@canndrew I still don't see the motivation. Why should we expect that implementing traits for ! is a common enough occurence that we want a special case sugar to make it involve less boilerplate? This carries real costs - language complexity, implementation complexity, documentation, so on. It seems to me that we need to have experience with ! as a type before we can determine if there's justification to add any special support for implementing traits for it.

[digama0]

It is true that as long as the trait impl is being written out, there isn't
much difference between just implementing all the methods the trait, and
this is such a weird corner case that adding special support to the
language will likely feel like cruft. Also, the implementations are as simple as

impl Trait for ! {
    fn foo(&self) -> u32 { self }
}

since ! is Copy and elements of ! coerce to anything.

[canndrew]

It seems to me that we need to have experience with ! as a type before we can determine if there's justification to add any special support for implementing traits for it.

Agreed. I also agree that in the presence of negative impls this whole thing is questionable. But without negative impls I can't see why you'd want the compiler to not just assume the impls.

! can implement so many traits, but I don't expect library authors will actually write out all these impls. They won't think to, or they won't bother, or they'll think something like

why would a user want to pass ! as a Hasher?

And then when people want to use the impls they won't be there.

But yes, this is all very hypothetical and we need to implement ! first to see how valid these concerns are.

[aturon]

The lang team has moved the ! RFC into FCP, but want to reiterate that we feel this RFC is premature. Assuming we can land the basic changes to !, we'll have dealt with the back-compat issues, leaving the motivation for this RFC to be based solely on experience with ! as a type in practice. As such, we'd prefer to close this RFC and wait until we've actually gained that experience and, as a community, feel the need to take this extra step.

@canndrew, you've previously agreed with this sentiment. Would you be willing to close out this RFC for now, to be potentially reconsidered later if the lack of trait impls turns out to be a significant problem in practice?

[nagisa]

@aturon what does lang team plan to do about || -> ! {} in case this is closed? Especially now that FnOnce::Output has been made stable.

EDIT: eh, wrong RFC, never mind me.

[eddyb]

@nagisa Isn't that handled by #1216?

[canndrew]

@aturon Sure.

[canndrew]

I've opened an RFC for the more conservative "compromise position" here