Blog post: Maximally minimal specialization: always applicable impls

10

Hmm… Seems similar to the ideas in the "Can we make a knob" section from Aaron's post that you linked. But as he said:

But saying that you can never repeat a type within a specialization would be very restrictive.

Also reminds me of Haskell's type-parameter roles, which I compared to Rust's situation recently. In fact, I believe that requiring a particular impl to be "always applicable" is equivalent (in some formal sense) to requiring that all its type parameters be representational (AKA parametric), versus nominal. And putting #[specialization_predicate] on a trait is equivalent to requiring that its Self 'parameter' is parametric. However, Niko's proposed rules provide more flexibility than Haskell's in some cases, which I think is sound, as I'll describe later.

In both languages, we want a generic definition to stay representationally equivalent if you change one of its parameter between two types/lifetimes that are themselves representationally equivalent. In both languages, there's a specific language feature that provides a "base case" for representational equivalence - if two different struct definitions happen to have the same field types, that doesn't count; we only care about a case where the language guarantees that two types have the same representation.

  • In Haskell, that's newtype: newtype A = B defines a type A which is equivalent to B. The closest Rust equivalent would be something like #[repr(transparent)] struct A(B);. Importantly, Haskell lets you coerce between any two types with a representational equivalence guarantee. So you can coerce between A and B, and also between Foo A and Foo B if Foo's parameter is representational. (This was originally an accidental consequence of GeneralizedNewtypeDeriving, but later became an explicit feature.)

  • In Rust, that's lifetimes. Trans's blindness to lifetimes effectively allows you to coerce from Foo<'a> to Foo<'anonymous>, though it's not as general as Haskell's coercion mechanism.

So let's look at Haskell's rules for inferring representational versus nominal. To copy and paste from the GHC wiki page:

Next, we descend into each defining equation of the type family and inspect the left-hand and right-hand sides. The right-hand sides are analyzed just like the fields of a data constructor; see the ​Role inference section above for more details.

This example isn't on that page, but if you write something like

type family Foo x where
    Foo x = Bar x

where Bar is an existing type family, Foo's parameter inherits the representational/nominal decision from Bar. So if Bar's parameter is nominal, Foo's parameter is implied to be nominal, and ditto for representational.

This is roughly equivalent to "Condition 1: Relies only on implied bounds." By default, type parameters to Rust traits are nominal (i.e. not required to be parametric), including the Self 'parameter', so adding random trait bounds to an always-applicable impl would force its parameters to be nominal as well, contradicting the requirement that they be representational. But since marking a trait as #[specialization_predicate] asserts that its Self parameter is representational, it's okay to depend on those.

How is a restriction on bounds equivalent to a restriction on the right-hand side? Well, type families aren't the same as traits - they're basically a type-to-type lookup table, most directly analogous a trait with one associated type, which happens to be implemented for all types. As it happens, Haskell has a much much closer equivalent of traits, namely typeclasses, and they can even have associated types. But GeneralizedNewtypeDeriving has a blanket ban on typeclasses with associated types, regardless of representational-ness, so I can't use those as an example.

But there's a pretty simple transformation to simulate a predicate trait using a type family. This code:

trait SomeTrait {}
impl SomeTrait for isize {}

could be implemented as:

// define two types named True and False
data True
data False
// and the lookup table:
type family IsSomeTraitImplemented x where
  IsSomeTraitImplemented Int = True
  IsSomeTraitImplemented _ = False

And then if you want to add a "bound",

trait AnotherTrait {}
impl<T> AnotherTrait for T where T: SomeTrait {}

could be

type family IsAnotherTraitImplemented x where
  IsAnotherTraitImplemented x = IsSomeTraitImplemented x

(and you could define an "and" combinator if you wanted to simulate multiple bounds, etc.)

So the "bound" T: SomeTrait turns into a type expression IsSomeTraitImplemented x on the right-hand side.

Anyway, continuing on with the Haskell rules:

The more interesting analysis comes when inspecting the left-hand sides. We want to mark any type variable that is scrutinized as nominal. By "scrutinized", we mean a variable that is being used in a non-parametric fashion. [..]

To accomplish this, we check for any occurences of the either of the following sorts of scrutinization:

[I'm going to quote these out of order:]

  1. Type patterns that are syntactically equal are all marked as nominal. For instance:

    type family Eq w x y z where
  Eq a b (Either b a) c = a

    Here, we have two variable names that are used in multiple places: a and b. As a result, the type variables which they inhabit (w, x, and y) are all marked as nominal.

That's easy: it corresponds to "Condition 3: Each type parameter can only be used once."

  1. A type pattern that is not a single type variable. For instance, all of these equations provde examples of type patterns which do scrutinize a particular type variable:

    type family Inspect x where
  Inspect Int          = Bool
  Inspect (Either a b) = a
  Inspect (f a)        = a

    Any type variable that is scrutinized in this fashion (x in the above example) is marked as nominal.

This is the part where Niko's proposed rules are more flexible.

For lifetime parameters, this is covered by "Condition 2: Fully generic with respect to lifetimes." Similarly to how the above disallows Inspect Int = Bool, using a concrete type where we want a type parameter, an always-applicable impl can't say impl SomeTrait for Foo<'static>, using a concrete lifetime where we want a lifetime parameter.

But Niko's rules do allow for a more direct equivalent to the above example: we could impl SomeTrait for isize, and separately impl<A, B> SomeTrait for Either<A, B>. This is safe, though, and I think it would be safe in Haskell as well - i.e. Haskell is being overly conservative. After all, in both languages we know that Int and Either a b cannot possibly be representationally equivalent:

  • In Haskell, that's because Int is not a newtype of Either or vice versa; they are distinct data types. (Though there may be backwards-compatibility concerns, generally speaking, in allowing code to make these kinds of assumptions. It's unlikely that Int's implementation would ever be changed into a newtype of Either, but you could imagine that happening for other pairs of types...)
  • In Rust, that's because isize and Either<A, B> are not identical barring lifetimes. (No backwards-compatibiliy concerns here, since there's no newtype feature. Transparent structs don't count, because the type system doesn't treat them specially.)

Therefore, it should be fine for Inspect Int and Inspect (Either a b) to also not be representationally equivalent. (edit: but I might be missing something, in which case I’d love to be corrected.)

Is there a point to this post?

Maybe. If Niko's plan is equivalent in some sense to a simplified version of type roles, then that suggests it's on good theoretical ground. And it opens the possibility of moving toward a more full-featured version, either now or (more likely) as a backwards-compatible extension.

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

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.

So perhaps, even if they are equivalent, that should be regarded as an unfortunate coincidence rather than a path for future exploration. :wink:

6 Likes