Shipping specialization: a story of soundness

It can't be. We rely on it for soundness (e.g. in RefMut::map).

I suppose that types that only differ re lifetimes have a common supertype? Can we use that semilattice to prevent lifetime specialization with things like the (T, T) example?

@Ericson2314 Does that idea still work if taking into account invariant type parameters?

:confused: I was sorta thinking there’s very little true invariance in the heart of Rust if the “latent” ontravariance can be used, but custom parameterized nominal types can’t soundly be replaced with their bodies, of course.

But the heart of Rust is &mut and it's invariant. (;

I forgot about that too :O. (In stateful MIR I do point out that splitting the intial and final type gets rid of the invariance, but that doesn’t help here.)

Maybe we should disallow aliasing of type parameters unless we forbid their substition with anything involving invariant lifetimes?!

That gives us leverage to use something like epochs to make trans smarter over time, while still shipping some version of specialization relatively soon.

I may be misunderstanding something, but isn't trans explicitly out of scope of the epochs RFC, which is targeted at front-end changes?

For the final bomb example, since trans knows that the code satisfies typeck, can it switch to treating the associated types as ‘in’ type parameters? So can it use the fact that s: String to select the correct specialization? This is assuming that the issues related to lifetime specialization have already been solved for cases that don’t involve associated types.

Or in other words, can trans treat the final bomb example the same as the following code:

trait Bomb<Assoc: Default> {}

impl<T> Bomb<()> for T {}

impl<T> Bomb<String> for (T, T) {}

fn indirect<T: Bomb<A>, A: Default>() -> A {
    A::default()
}

fn build<T, A1, A2>(t: T) -> A2
    where T: Bomb<A1>,
          (T, T): Bomb<A2>,
          A1: Default,
          A2: Default
{
    indirect::<(T, T), A2>()
}

fn main() {
    let s: String = build("Uh oh");
    drop(s)
}

I’m still learning the details of rust, so hope my posts here aren’t too much noise.

Necropost:

I recently read in a random Hacker News comment about "type roles" in Haskell:

...and it occurred to me that the problem the feature was meant to solve is pretty similar to the soundness hole here.

The compiler expects to be able to use the same trait/typeclass implementations for two types based on the assumption that they have identical representations:

  • Haskell: A newtype versus the type it wraps
  • Rust: Types that differ only in lifetime parameters

This works for normal (parametric) generic code, but is broken by the ability to create a type-to-type 'lookup table':

  • Haskell: …using type families (which are just associated types, in Rust terminology, but because Haskell's type system treats newtypes as separate types, there's nothing preventing you from impl'ing something for a newtype and its base type with different associated types)
  • Rust: …using associated types + specialization (specialization is required because the language has only a single concrete lifetime, 'static, so there's no other way to have two separate impls of the same trait for two types differing only in a lifetime parameter)

Haskell's solution is to differentiate between two 'roles' of type parameters: "representational" parameters, which allow coercions but not lookup, and "nominal" parameters, which allow lookup but not coercions. (By "coercions" I mean the features in first set of bullets, and by "lookup" I mean the second set.)

However, @glaebhoerl once wrote, about the roles feature:

The opinion of many leading members of the Haskell community is that this solution was ill-conceived and brings more complexity than it's worth.

And I'm not really sure what an equivalent feature would look like in Rust, anyway.

“representational” parameters ..., and “representational” parameters,

Probaby one of them should be changed.

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