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

[troplin]

For example, auto traits use a coinductive matching strategy, unlike normal traits, which are inductive.

Me not being a PL theorist, could you explain in a few words what that means? I mean in practice, how they behave differently.

[nikomatsakis]

The trait is special. For example, auto traits use a coinductive matching strategy

Sorry, let me define this. The “coinductive” strategy means that, in short, if you have a cycle, that’s ok. In other words, roughly speaking, to prove that Foo<T>: Send, you get to assume that Foo<T>: Send holds. This is required because of recursive types and so forth. (I plan to try and write-up a blog post on this going into a bit more depth; I’d love to make auto traits less special, I just don’t think it works – but in any case they will always be somewhat special.)

[nikomatsakis]

Heh, yes, just tried.

[nikomatsakis]

Here is a concrete example of how they are different. If you had

struct Foo<T> {
    b: Option<Box<Foo<T>>>
}

you can imagine that the “auto trait” impl is something like

unsafe impl Send for Foo<T>
    where Option<Box<Foo<T>>>: Send
{ }

so if want to show that Foo<T>: Send, we have to first show that Option<Box<Foo<T>>>: Send. But that in turn means we must show Box<Foo<T>>: Send (because that’s what the Option impl will require) and then Foo<T>: Send (because that’s what the Box impl will require).

You might think that we could write the Send impl like so:

unsafe impl Send for Foo<T>
    where T: Send
{ }

except that this doesn’t work for all structs, most notably around associated types:

struct Bar<T: Iterator> {
    x: Option<Box<Bar<T::Item>>>
}

Here the impl would be:

unsafe impl<T: Iterator> Send for Bar<T>
    where T::Item: Send
{ }

but what if we have Bar<Baz> where Baz: Iterator<Item=Bar<Baz>>? Now to prove that Bar<Baz>: Send, we have to show that Baz::Item: Send, and Baz::Item is (again) Bar<Baz>. So we’re stuck.

[nikomatsakis]

(With normal impls, you would get an overflow error. With an auto trait, we consider this OK.)

[troplin]

Ok I think I’ve understood. But I still think that this is a property of the impl, not of the trait itself. It seems to me that the impl is co-inductive, not the trait. 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?

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

[nikomatsakis]

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 https://github.com/rust-lang/rust/issues/29859 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.

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]

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]

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 https://github.com/rust-lang/rust/issues/29859

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]

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

Which syntax change are you referring to?

[nikomatsakis]

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]

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 {}

[nikomatsakis]

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.