Changing the `impl Trait for .. { }` syntax

[nikomatsakis]

@troplin

And I don't understand why being co-inductive precludes having supertraits and members. Why can't every impl (or trait if you like) be co-inductive?

Right now, if you have trait Foo: Bar, and you know that T: Foo, you get to assume that T: Bar. But if you have a coindutive trait, that would be unsound -- basically you can construct a self-supposed cycle to "prove" that T: Foo and then you just get to assume that T: Bar. See Cyclic traits allow arbitrary traits to be synthesized · Issue #29859 · rust-lang/rust · GitHub for several examples exploring this. This is why supertraits don't make sense -- or at least would have to work quite differently than non-auto-traits.

As for having members, the reason is similar: the impl's definition of those members might well make use of this recursive reasoning, and it might never bottom out, but there is no easy place for us to check that except at monomorphization time. We might be able to allow members I guess under various restrictions, but again they would work quite differently than non-auto-traits.

@troplin

To put it differently, IMO the trait itself consists only of the operation/items and the semantic meaning that it implies.

I see that POV, but I still think that being an auto trait is really a property of the trait itself. If you read through the code, for example, you'll find we have a predicate "trait-is-auto-trait" (note: not "impl-is-auto-impl") and that we have to treat auto traits differently in lots of places. So basically adding this impl to a trait changes the trait itself in ways that no other impl does. It's not that we just have some special case where we say "when we are looking at a .. impl, do things a bit differently than we would for other impls".

[troplin]

@nikomatsakis

If you read through the code, for example, you'll find we have a predicate "trait-is-auto-trait" (note: not "impl-is-auto-impl") and that we have to treat auto traits differently in lots of places.

I'm not familiar with the compiler codebase but I think this is just a simplification in the compiler. As implemented, a trait can have either only inductive impls or only co-inductive impls. But I imagine that you also could have traits with both, inductive and co-inductive impls.

[troplin]

@nikomatsakis

Right now, if you have trait Foo: Bar, and you know that T: Foo, you get to assume that T: Bar. But if you have a coindutive trait, that would be unsound -- basically you can construct a self-supposed cycle to "prove" that T: Foo and then you just get to assume that T: Bar.

I think co-induction should not extend to supertraits, e.g. in the example from Cyclic traits allow arbitrary traits to be synthesized · Issue #29859 · rust-lang/rust · GitHub

trait Magic: Copy {}
impl<T: Magic> Magic for T {}

fn copy<T: Magic>(x: T) -> (T, T) { (x, x) }

supertraits should be treated separately for matching as if they were written as:

trait Magic: Copy {}
impl<T: Magic+Copy> Magic for T {}

Which would be sound again.

[petrochenkov]

auto trait Foo {}

What do people think about: auto trait Foo; as an alternative syntax?

Auto traits are extremely rare, no need to introduce a syntactic inconsistency to save a couple of characters.

pub trait Foo: Auto {}

The "auto" property is not related to trait inheritance at all, seems like going too far to avoid a contextual keyword.

impl Auto for Send {}

Just rephrasing of impl Send for .. {}, still makes the impl special, not the trait.

I think both a keyword on the trait decl and a supertrait are non-ideal because they would prevent Rust from ever having traits which are automatically implemented with a negative polarity.

auto trait !Foo {}

[jethrogb]

Just to be clear: this syntax change is supposed to only work for auto traits? Or also for other marker traits with no members? Think Zeroable, Eq, Copy etc.

[nikomatsakis]

@jethrogb

Just to be clear: this syntax change is supposed to only work for auto traits?

Which syntax change are you referring to?

[nikomatsakis]

@petrochenkov

Auto traits are extremely rare, no need to introduce a syntactic inconsistency to save a couple of characters.

You persuaded me. auto trait Foo { }. We could (orthogonally) discuss whether a ; can be allowed (for all traits with no members, presumably).

[sfackler]

I always initially read impl Trait for .. {} as implementing Trait for RangeFull, so I’d be on board with something like auto trait.

[Uther]

Since {} are mandatory for other empty blocs(if, while, for, …), it seems consistent to me to require them for empty traits too.

[withoutboats]

They’re not required for empty structs, which is probably a better comparison. But this is orthogonal to the syntax for auto traits.

[jethrogb]

@nikomatsakis

Which syntax change are you referring to?

Yeah, not sure, from the topic intro it sounded like you wanted to get rid of impl Trait for ... {} but after re-reading it sounds more like you want to get rid of trait Trait {}? What's the impl-plan for auto traits then?

[aturon]

I agree entirely with @petrochenkov’s comment. I tend to find conservatism around (contextual) keywords very difficult to understand: whether or not we use a distinct keyword, the concept exists in the language. And in general I think it’s better to have clear names and ways to state concepts, rather than trying to map a large number of concepts into a too-small keyword space.

In short: auto trait Foo {} please!

[Halt]

Don’t sure whether it’s still actual, but…

Personally I think, that new keyword is almost always a poor idea.

The way I see it, all syntax richness may be split into two parts: declarations and annotations. Declarations work on the very same semantic level that programmer uses when thinking about the problem. For example, fn, trait, mod declare things, they all have very explicit and distinct meaning within the language.

On the other hand, annotations actually are meta information that affect how compiler interprets the code. They’re not a part of the code itself. We may say, that annotations declare ideas, not things. Actual things arise later, when compiler (or human) interprets that ideas.

All of the following annotations are not the code, they are comments to the interpreter:

• #[derive(Debug)]
• #[inline]
• #[cfg(test)]
• #[test]

A rule of thumb is that after interpretation of the syntax, all annotations may be removed, and it would not cause any problem, because during interpretation phase we’ve already introduced all things, like auto-generated methods, provided trait impls for auto traits and removed unnecessary ones (in case of test or cfg).

Following this logic we may say, that auto trait is also an idea, not a thing. Therefore, it should be introduced on a lexical level as annotation:

#[auto_trait]
trait Foo {}