Blog post: Maximally minimal specialization: always applicable impls

canndrew · 2018-02-10T03:18:42.009Z

Nit: in the blog post

impl<T> From<T> for ! { .. }

should be

impl<T> From<!> for T { .. }

Sgeo · 2018-02-10T07:57:47.830Z

Can HList search by type (without the type inference trick) be implemented with this?

If I recall correctly, I’d need the following impls to work

impl<Head, Tail> Has<Head> for Cons<Head, Tail> { .. }
impl<T, Head, Tail> Has<T> for Cons<Head, Tail> where Tail: Has<T> { .. }
impl<Head, Tail> Has<Head> for Cons<Head, Tail> where Tail: Has<T> { .. }

As far as I understood when last seriously thinking about this, I would need the “lattice rule” for this, and this proposal is a lattice rule that excludes some scenarios?

glaebhoerl · 2018-02-10T11:35:23.390Z

comex:

On the other hand, I’ll again quote @glaebhoerl, regarding Haskell type roles:

(FWIW I haven’t kept up and I don’t know what the current situation is - that was a while ago now. One of the reasons people didn’t like them is that they’re not first class - you can’t talk about things being nominal or representational beyond marking individual type parameters as being one or the other - but also making them first-class seemed too elaborate relative to the benefit. Here are a couple of relevant-seeming links, which themselves appear to be several years old already. In any case, I would ask a GHCer or two before taking my old word as gospel on this. It may still be true but I don’t know.)

asajeffrey · 2018-02-10T18:47:23.431Z

Ooh this is interesting! Linear uses of type variables was the original Generic Java proposal, but turned out not to be sound (http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00849.html). The problem there was the interaction between linearity and subtyping: you can construct a type B<T> <: A<T,T> then use B linearly, but oops it’s non-linear in the supertype.

But yay Rust doesn’t have subtyping except on lifetimes, so reconstructing this example in Rust is tricky to say the least. The nearest I could come to it is:

trait A<'a, 'b> {}
trait B<'a> : A<'a, 'a> {}

impl<'a, 'b> A<'a, 'b> for Foo<'a, 'b> {}
impl<'a, 'b> B<'a> for Foo<'a, 'b> {}

With current Rust this fails to compile (https://play.rust-lang.org/?gist=ccf9c99a2ab26d0899c828b5ae3a255f&version=stable), due to lifetime errors, not overlap.

So the good news is that the obvious attempts to recreate the Java example have failed, another victory for not much subtyping!

asajeffrey · 2018-02-10T21:37:51.446Z

One thing that occurred to me is how much this is related to proof objects for identities in type theory. For example we can code up the semi-decision procedure for type equality:

struct True;
struct False;

where a P:MaybeEq<T,U> acts as a witness for the the semi-decision procedure for type equality, in that if P is True then T == U.

trait MaybeEq<T, U> { fn maybe_cast(x: T) -> Option<U>; }
impl<T> MaybeEq<T, T> for True { fn maybe_cast(x: T) -> Option<T> { Some(x) } }
impl<T, U> MaybeEq<T, U> for False { fn maybe_cast(_: T) -> Option<U> { None } }

The thing rustc can’t do, since this would allow rustc to decide type equality is infer P:

trait DecideEq<U> { type P: MaybeEq<Self, U>; }
impl<T, U> DecideEq<U> for T { type P = False; }
impl<T> DecideEq<T> for T { type P = True; }

This fails the requirements for overlapping impls since the specialization (the True case) uses T twice, where the base impl (the False) case uses T only once.

Code at https://play.rust-lang.org/?gist=b67b1219269348be21831f3e1ce2edbf&version=stable

RReverser · 2018-02-12T10:20:28.662Z

It’s not arbitrary though - as was mentioned above, you only need special-casing for ‘static lifetime, and it’ s pretty easy to distinguish already.

We can already implement some traits only for 'static versions of structs, it would be neat to let them co-exist with impls for any other lifetime for specialization.

rpjohnst · 2018-02-12T20:38:48.894Z

With lifetime inference and constraints it is arbitrary. Special casing 'static might be reasonable but I would like to see some actual use cases for that.

nikomatsakis · 2018-02-12T21:02:49.990Z

arielb1:

This is more like an “inversion principle for impls”, rather than an implied bounds rule (I don’t see any WF bounds here that might be implied).

In terms of the work @scalexm did, the real form of the rule, I believe, would be this:

FromEnv(T: Clone) :- FromEnv(Vec<T>: Clone)

That is, if the environment tells us that Vec<T>: Clone, it also tells us that T: Clone. This is why I called it an implied bounds rule. But it’s not particularly important. I’d prefer not to pursue said changes too eagerly anyway.

nikomatsakis · 2018-02-12T21:09:19.277Z

Hehe, when writing that I was chanting to myself “don’t get it backwards! don’t get it backwards!” So of course I did.

nikomatsakis · 2018-02-12T21:15:07.706Z

RReverser:

It’s not arbitrary though - as was mentioned above, you only need special-casing for ‘static lifetime, and it’ s pretty easy to distinguish already.

First off, just having the borrow checker decide ‘static or not’ is enough to make it arbitrary – it picks the shortest lifetime it can, right now, which means that even if it could have picked 'static, it will try to avoid it unless forced. (This is necessary to avoid nonsense borrowck errors.)

But, secondly, in general you might need to know whether two lifetimes are equal. Consider:

impl<T> Foo for (T, T) { }

and now you have a type (&u32, &u32). Does it apply or not?

Also stuff like this:

impl<T,U> Foo<T> for U
impl<'a, 'b> Foo<&'a u32> for &'b u32 where 'a: 'b

Now if we have &u32: Foo<&u32>, does the specialization apply?

nikomatsakis · 2018-02-12T21:16:45.663Z

asajeffrey:

One thing that occurred to me is how much this is related to proof objects for identities in type theory.

This…took me a while to parse. But that’s a fun example. =)

nikomatsakis · 2018-02-12T21:34:21.103Z

arielb1:

I consider TrustedLen as rather important, and it would have to be marked as a “specialization predicate” (or, as I prefer, a “decidable predicate”).

I agree that this is an important use case, and I certainly agree that we don’t handle it all that well, and it’s certainly that we had hoped to avoid “splitting” traits into “specialization predicates” and “normal traits”. But at this point I don’t think it’s possible to avoid that split.

The fact is that impls can (and frequently do!) include tests that we just can’t test after erasure. Previously we had hoped to find some solution that basically let the choices made pre- and post-erasure diverge: I suspect this is fundamentally unsound, and that is roughly the point of my post.

In any case, even if it can be made sound, it’s always made me pretty nervous. It seems like it implies that figuring out which code will run is pretty non-trivial for users. I am nervous about this, particularly since I think people will use specialization for more than just optimization, but also for semantic choices.

That seems to leave three options:

Stop erasing.
Somehow make all choices at typeck time.
Restrict the set of specialization impls to those that can be decided equally well at typeck time and at codegen time.

We’ve been discussing the first one (“stop erasing”) on this thread. I believe it is quite infeasible. It would also mean that further improvements like NLL are not possible, or at least much more fraught, since they would change runtime semantics. I expect us to make more such improvements. =)

Making all choices at typeck time is, in a sense a variant on the first option. It would mean that generic functions – which often lack the context for such a choice – must push the choice up to their caller. I’m not even sure this can be done, since often the choices will involve compound types that feature regions from within the function. But even assuming it can be made to work, it’s clear that it has the same downsides in terms of the borrowck and regionck suddenly being in charge of making choices about what code executes (it probably avoids some of the monomorphization explosion, since I imagine we would basically be compiling down to a dictionary passing style, and in practice the dictionaries we resolve would wind up being the same).

So that leaves us with the third option, which is basically what I described. (Were there any other specific proposals for how to implement such a test? It’d be interesting to compare, but I don’t recall anyone giving a detailed proposal.)

Am I missing some alternative?

aturon · 2018-02-12T21:37:44.113Z

nikomatsakis:

I believe it is quite infeasible.

Not only that: it doesn’t magically deliver soundness either, because there are still cases where typeck and trans can disagree.

RReverser · 2018-02-13T11:49:56.943Z

Just a side note: apart from TrustedLen, another example where 'static-based specialisation would be helpful is https://github.com/rust-lang/rust/pull/46993 so that one could use String::from and Vec::from on compile-time constants like any other references and API would avoid allocation itself.

jmst · 2018-02-13T15:23:35.073Z

@nikomatsakis I think there might be a further alternative of considering all lifetimes to be distinct and incomparable unless they must be equal because it’s the same type (or if there are some where constraints on lifetimes in scope, although this would require passing this to code generation).

It’s a bit tricky, because applying it to all trait resolution would not be backwards compatible, but it might be possible to only apply it to specialization decisions (in both typechecking and codegen, of course).

Not quite sure how expressive and desirable this would be and not even totally sure whether it can be done soundly (although it seems it can be). It might be the simplest approach if it’s feasible though.

arielb1 · 2018-02-13T19:55:05.972Z

nikomatsakis:

That seems to leave three options:

Sure, and I think some sort of “dispatchable traits” is the sanest way to go forward - it just needs some language design in order to not be terribly ugly.

For some reason I thought we decided on !dispatchability on the RFC, but I can’t find any clear comment talking about that. I should try to ascribe less meaning to lonely unclear RFC PR comments.

RReverser:

Just a side note: apart from TrustedLen, another example where 'static-based specialisation would be helpful is https://github.com/rust-lang/rust/pull/46993

Please no.

There are 2 problems: the first, that the result of lifetime inference are intentionally not precisely specified. For example, with the current version of lifetime inference, the 'static impl would be pretty hard to reach, as

impl From<&'static str> for String { /* .. */ }
fn foo() {
    let t = String::from("hello");
    // ^ subtyping is possible between the literal and the function call, so the compiler can (and with today's
    // implementation, will) infer a stack-local lifetime for the "hello" literal, and this code will still allocate.
}

The second: Rust has lifetime parametricity. This means that if unsafe code passes a lifetime back to user code, e.g. through a for<'a> closure, the unsafe code gets to pick the meaning for that lifetime.

For example, the lifetime passed by Ref::map is supposed to live “as long as the ref lives”:

// Ref::map
fn map<U: ?Sized, F>(orig: Ref<'b, T>, f: F) -> Ref<'b, U> where
    F: for<'r> FnOnce(&'r T) -> &'r U { /* ... */ }

fn foo<'a>(r: &'a RefCell<u32>) -> Option<Ref<'a, u32>> {
    let x = 0;
    let ref_ = r.borrow();
    let ref_ = ref_.map(|inner| {
        // `inner` is an `&u32` that lives as long as the `Ref` lives.

        // If the `Ref` is dropped within `foo`, it lives shorter than `x`,
        // and if it isn't, then it lives longer than `x`, and we have no
        // way of telling which way it is, so we can't precisely specialize
        // within `some_fn`.
        some_fn(foo, &x)
    });
    if random() % 2 == 0 {
        drop(ref_);
        None
    } else {
        Some(ref_)
    }
}

arielb1 · 2018-02-13T19:59:20.361Z

I think there’s a similar example with NLL, even without any unsafe code, where you can have a pair of simultaneously-live lifetimes, that, depending on a branch destination, it is both possible that the first lifetime ends first, that both lifetimes are equal, and that the second lifetime ends first.

That means it is impossible to compare lifetimes at runtime - you could write a “self-referential case” where if you dispatch such that the lifetimes are equal, they will end up as unequal, and vice versa. With associated types being specializable, the way from there to transmute is pretty short.

RReverser · 2018-02-17T11:56:45.936Z

arielb1:

There are 2 problems: the first, that the result of lifetime inference are intentionally not precisely specified.

They’re not at the moment, and part of the thread is exactly about suggestion to change that for 'static lifetime.

arielb1:

The second: Rust has lifetime parametricity. This means that if unsafe code passes a lifetime back to user code, e.g. through a for<'a> closure, the unsafe code gets to pick the meaning for that lifetime.

I’d say this example should be fine and just not using specialisation at all - specialisation is meant purely as optimisation, and can be just omitted for complex examples like you presented while still used for explicitly static values.

I might be wrong, but it seems most of the counterarguments are about complexity of specialisation between any two arbitrary lifetimes - which is indeed hard if not impossible to do - but it still seems that specialising for explicit 'static lifetime should be quite possible and useful.

steven099 · 2018-04-18T18:39:10.632Z

One thing I’m not clear on from the blog post is whether the exception to ‘always applicable’ for specialization predicates (“the exception”) would apply when determining whether a specialization predicate impl itself is valid. Consider:

impl<T> UnconditionalSeek for S<T> where T: UnconditionalSeek { ... }

Does this impl satisfy ‘always applicable’ for the purposes of a implementing a specialization predicate? It does if we’re allowed to ignore the specialization predicate on T in accordance with the exception, but the impl certainly doesn’t apply unconditionally. The reason I’m unsure—aside from the language around the impl being “unconditional”—is because of the parenthetical in:

every one of their impls must be always applicable (our original predicate)

This could be read to imply that specialization predicate impls have to be ‘always applicable’ based on the original version of ‘always applicable’ that existed prior to the introduction of the exception.

It seems as though the version of ‘always applicable’ that includes the exception would be sufficient to make specialization predicates themselves sound, since it still prevents specialization based on lifetimes/type equality. I don’t know if there’s a broader reason why this wouldn’t work though, such as an interaction with associated types.

nikomatsakis · 2019-03-25T08:29:39.386Z

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