[Pre-Pre-RFC] Generic generics (or HKTs for short)

language design
1

Idea

  1. Allow struct Foo<T<'a, U, const N: usize>> { ... }, fn foo<T<...>>, etc.
  2. Usage: Foo::<for<'a, U, const N: usize> Bar<'a, U, N>>.
  3. Unused lifetimes can be omitted: Foo::<for<U, const N: usize> Bar<U, N>>.
  4. Conflict with for<'a> fn(): always disambiguate towards existing semantics, require for<'a> for<> fn. This is because type constructors for fn types are unlikely to be useful in practice, but nevertheless there's no reason not to support them. This is not a problem for dyn types as dyn for<'a> Fn() is the existing syntax and for<'a> dyn isn't allowed.
  5. Interactions with inference: TBD.
  6. Order: TBD. See also Const generics and defaults

Motivation

Rust currently requires Any: 'static. This is all fine and well but with generic generics it is possible to introduce a new kind of Any hereby called AnyA<'a>: 'a. (Note: AnyA<'static> implies AnyA<'static>: 'static implies Any: AnyA<'static> - but Any need not be a subtype of AnyA<'static> for this proposal, nor does AnyA<'a> need to be a part of this proposal(!)).

Its implementation, including TypeConstructorId, is as follows:

#[repr(transparent)]
#[derive(PartialEq, Eq, ...)]
struct TypeConstructorId(TypeId);

impl TypeConstructorId {
  // note: can be expanded with more lifetimes (see point 3 of "idea").
  // IMPORTANT: HKTs used here (1)
  fn of<T<'t_a>>() -> TypeConstructorId {
    // IMPORTANT: HKTs used here (2)
    TypeConstructorId(TypeId::of::<for<'a> fn(T<'a>)>())
  }
}

// IMPORTANT: NO HKTs here!
trait AnyA<'a> where AnyA<'a>: 'a {
  fn type_constructor_id(&self) -> TypeConstructorId;
}

// IMPORTANT: HKTs used here (3)
impl<'a, T<'t_a>> AnyA<'a> for T<'a> where T<'a>: 'a + ?Sized {
  fn type_constructor_id(&self) -> TypeConstructorId {
    // IMPORTANT: HKTs used here (4)
    TypeConstructorId::of::<for<'for_a> T<'for_a>>()
  }
}

impl<'any_a> dyn AnyA<'any_a> {
  // IMPORTANT: HKTs used here (5), also inline bounds on it
  pub fn is<T<'t_a>: AnyA<'t_a>>(&self) -> bool {
    // IMPORTANT: HKTs used here (6)
    let t = TypeConstructorId::of::<for<'for_a> T<'for_a>>();
    let concrete = self.type_constructor_id();
    t == concrete
  }

  // IMPORTANT: HKTs used here (7), also where bounds on it
  pub fn downcast_ref<T<'t_a>>(&self) -> Option<&T<'any_a>>
  where for<'for_a> T<'for_a>: AnyA<'for_a>
  {
    // IMPORTANT: HKTs used here (8)
    if self.is::<for<'for_a> T<'for_a>>() {
      // IMPORTANT: HKTs used here (9)
      // SAFETY: AnyA<'a> doesn't operate on concrete lifetimes, instead
      // it cares about how lifetimes are bound into the type and just
      // carries the concrete lifetime through the type system. You cannot
      // "hide" a lifetime by converting to AnyA. You must pass the lifetime
      // around. With `Any`, the whole type is hidden, but with `AnyA` some
      // details are (intentionally) exposed. Doesn't make it much less
      // flexible tho.
      unsafe { Some(&*(self as *const dyn AnyA<'any_a> as *const T<'any_a>)) }
    } else {
      None
    }
  }
}

In total, this has 9 uses of HKTs:

  1. Function definition that takes HKTs.
  2. This T<'a> is actually an usage of the HKT T<'t_a>, altho this for<'a> fn(...) is existing syntax.
  3. There is a generic lifetime 'a, as well as an HKT T<'t_a>. Note the difference between 'a and 't_a.
  4. Note the for<'for_a> as defined in this proposal.
  5. Same as (1) but with inline bounds.
  6. Same as (4).
  7. Same as (5) but using where. Also note the concrete T<'any_a> in the Option.
  8. Same as (4).
  9. Note the concrete T<'any_a>.

Also note that the trait AnyA<'a> itself doesn't use HKTs, and this whole thing doesn't use any new intrinsics.

Prior discussion

See Generic generics (there may have been other stuff but we don't remember)

Benefits

AnyA<'a> looks particularly interesting if combined with the ability to downcast between traits (i.e. implementing an OOP system on top of Rust). While this proposal isn't about adding AnyA<'a>, nor is it about adding an OOP system on top of Rust, these make good examples/arguments for why this proposal should be implemented.

Drawbacks

There are... a lot of drawbacks to this proposal. HKTs are a monumental undertaking. There are already plenty of bugs related to constraint checking (as in where bounds), and this would likely end up introducing so many more. Additionally, chalk still has a long way to come. Additionally additionally, who knows how this is meant to interact with inference!

Right now this proposal is mostly meant to be for defining the syntax for HKTs in Rust, as well as bringing forward an use-case that can pretty much only be satisfied with HKTs. Many languages get away with not having HKTs after all, but Rust has lifetimes, and they do get in the way: Generic Associated Types (GATs), a strict (and fairly limited) subset of HKTs, exist primarily due to lifetimes, and this use-case also boils down to lifetimes. So much so that, from talking to other Rust users, it seems likely GATs will be stabilized as lifetimes-only long before they'll support other kinds of generics. (Side note: we do, in fact, have a limited form of HKTs today: for<'a> fn() and dyn for<'a>. And you can only use them for... lifetimes. Yep. Sensing a pattern here. :stuck_out_tongue: )

???

So yeah. This is a sorta HKTs proposal. Ah well. >.<

1 Like
2

There is already at least one HKT proposal, not sure how they are related:

They are plenty of similar syntactic proposals. In short, what's substantially different about yours?

1 Like
3

GATs aren't HKTs (in particular the GAT is fixed at the impl Trait whereas this can accept the HKTs at any time) but also, this is heavily based on existing syntax. In fact the use of for<...> to bind the HKTs (e.g., Foo::of::<for<'a> (&'a K, &'a V)>()) is almost entirely based on the syntax for for<'a> fn, altho the point of using it is that it allows naming the HKT parameters without having to name the generic (i.e. without using keyword-based generic arguments, which we don't have). Additionally the syntax for accepting an HKT (that is, fn foo<T<'a>>()) is based on existing syntax for types (struct Foo<T>, trait Bar<'a>, they all put the name, then follow it with <>. impl<T> is slightly special but there's actually no good reason to treat it different with HKTs.).

6

Does this code above

mean that T<'a> is not hiding any lifetimes other than 'a ?

E.g. does

// type constructor that takes lifetime for first reference
// as its single argument
Cell<(&'_ u8, &'b u8)>

qualify to be T<_> above?

If it did qualify then I guess such AnyA would run into the same issue as the retracted RFC 1849 was trying to address: TypeId doesn't encode this other lifetimes ('b in my example) and so TypeId as it is now would permit casting values unsafely.

So it needs to be disqualified somehow. I guess that would need some extra syntax?

  • ..and if you had a way to declare and enforce that,
  • if you had a way to declare and enforce that T does not include any lifetimes other than 'a

then

  • couldn't AnyA be written without HKT?
  • couldn't it be mostly just a copy-paste from Any?

like this:

trait AnyA<'a> {
    fn type_id(&self) -> TypeId; // same as Any
}

// updated..
impl<'a, T: ?Sized> AnyA<'a> for T
       where T : NoOtherLifeTimesExcept<'a> {
    fn type_id(&self) -> TypeId {
        TypeId::of::<T>() // same as Any
    }
}

impl dyn AnyA<'a> {
  fn is<T: Any>(&self) -> bool
      where T : NoOtherLifeTimesExcept<'a> {
     // .. same as Any ..
  }
  fn downcast_ref<T: Any>(&self) -> Option<&T>
      where T : NoOtherLifeTimesExcept<'a> {
    // .. same as Any ..
  }
}
7

Sorry? Can you rewrite this as a type T<'t_a> = ...; that compiles in today's Rust?

How do you expect T to be both 'static and NoOtherLifetimesExcept<'a>? And what is NoOtherLifetimesExcept<'a> - how would you implement that without HKTs?

1 Like
8

I wanted to inquire if the following would compile under AnyA implementation from the first post

struct S<'a, 'b> {a : &'a i32, b : &'b i32}

fn f<'a, 'b>(a : & 'a i32, b : & 'b i32) {
  let s = S{a, b};
  let any = &s as &dyn AnyA<'a>; // is this okay?
}

Thx, I have fixed my code above removing 'static.

NoOtherLifetimesExcept<'a> is a hypothetical reasoning device:

  • would NoOtherLifetimesExcept<'a> be sufficient to implement AnyA?
  • is NoOtherLifetimesExcept<'a> simpler than HKT as proposed in this topic?

If both are true then NoOtherLifetimesExcept<'a> is what

  • the motivating example distils to
  • the motivating example really calls for

As links posted by H2CO show Rust is expected to gain an alternative to vanilla HKT in the form of generic associated types. I understand the reasoning was: GAT cover a number of important use cases HKT could have hoped to solve. Thus your example was interesting to scrutinise: does it really present a use case not covered by GAT? My personal conclusion here is that what your example really calls for is a facility equal in power to my hypothetical NoOtherLifetimesExcept<'a> but not necessarily anything more powerful/flexible.

9

Again, if and only if you can represent it in the form

type T<'t_a> = [...];

in current rust, then it's a valid T<'t_a> for this proposal.

This means these are valid:

type T<'a> = &'static str;
type U<'a> = ();
type V<'a> = (&'a str, &'a str);
type W<'a> = (&'a str, &'static str);

But things like this aren't:

type T<'a> = (&'a str, &'b str);

We don't know how to prove that this is either sound or unsound, whereas HKTs can be formally reasoned about. However, how does this compare to just T: 'a? Also note that TypeId::of doesn't accept lifetimes because you can't monomorphize on lifetimes. (that is, (&'a str, &'static str) is, for all intents and purposes, the same as (&'static str, &'a str). check out the previous thread for more details about this.)

GATs are not HKTs and they solve a different problem. They're just associated types. You don't pass them around like you pass HKTs around. A single trait impl must have statically-known GATs, whereas HKTs allow you to create arbitrary GATs. GATs are just allowing type Foo<'a> in impl Trait for Foo {} and doesn't even require chalk. In particular you can't generically have an useful GAT:

impl<T> Trait for T {
  type Foo<'a> = /* Nothing you can put here can apply to a T<'a> because
    there's no such thing as a T<'a>, there's only a concrete, T, with no
    lifetime parameters. You can have a
    type Foo<'a> = SomethingWithoutLifetimes;
    but that defeats the point. */;
}

HKTs allow you to bind generics against GATs:

fn foo<T, U: Trait<Item=T>>() {} // valid today
fn foo<T<'a>, U: Trait<Item<'a>=T<'a>>() {} // impossible today
10

One still needs to reason to establish that a given AnyA implementation is safe.
My AnyA<'a> implementation should be no more difficult to prove safe than yours.

Given

struct S<'a, 'b> where 'b : 'a  {..}

it's true that

S<'a, 'b> : 'a

but it's not true that

S<'a, 'b> : NoOtherLifetimeExcept<'a> // hypothetical feature
// I'm not advocating this feature just reasoning about it

It is true HKTs can do things that GATs cannot.
But that is beside the point.

There are things they both can do. A careful analysis of the most desired motivating use-cases has shown GATs do cover them in Rust. So Rust will be getting GATs.

I was most interested to examine your usecase to see if it provides motivation for things that HKTs can do and GATs cannot. My conclusion is that it does not. In my view it does provide instead a motivation for a feature similar to NoOtherLifetimesExcept<'a>.

11

Sure, but lifetimes (outside HRTBs - aka HKTs) are erased at monomorphization. How do you reason about something that doesn't even exist (namely the TypeId of T where T isn't 'static). That would be the first step to reasoning about everything else.

If you somehow had some way of having Self<'a> then GATs would mostly solve this (but not entirely). We're not gonna get Self<'a> tho because Self is by definition a concrete type, not a generic type.

With Self<'a> you'd shove type Ctor<'a> = Self<'a>; in a trait and use SuchTrait::Ctor<'a> in place of T<'a>, but otherwise you'd still have the differences with how TypeId gets handled (using TypeCtorId instead and stuff). The trait would be SingleLifetime, not NoOtherLifetimeExcept<'a>, and it'd have Ctor<'a>. This also doesn't cover every case: what if Self has multiple lifetimes, but you want them all to be the same? Self<'a> doesn't handle that, you'd need Self<'a, 'a> instead. But you don't need that with HKTs.

12
  • types are erased from compiled Haskell code yet they are used to reason about code safety
  • reasoning involved in establishing the safety of Rust programming language does rely on lifetimes quite heavily
  • I guess higher-kinded types you'd like to see will be erased from compiled code as well

So how do you reason? I don't think I'll be able to answer your question satisfactorily until I educate myself more and can understand RustBelt papers.. The reasoning which is within my grasp now is quite limited and informal.

13

for<'a> fn(&'static ()) monomorphizes different from for<'a> fn(&'a ()) btw. the difference isn't erased from compiled code, it's just stored separately.

We could potentially have full HKTs with lifetimes-only if things like SingleLifetime, DoubleLifetime, etc existed as auto-traits today. But it'd still be HKTs - since it's just expanding on what HRTBs can apply to by providing some helper traits. At that point might aswell add lifetimes-only HKTs as a language feature tho, rather than a compiler hack.

Edit: actually nvm, you can't specialize on lifetimes so something like &'static str would have the same GATs as &'a str. So you wouldn't have full HKTs, but rather something really similar to full HKTs but with a bunch of broken edge-cases.

14

@Soni I keep reading your feature proposals and coming away with absolutely no idea what you want your proposed feature for. They're always both super specific -- you clearly have some problem that you're trying to solve -- and super abstract -- leaving no clue what the original problem is.

I, and I think a lot of other people here, would be better able to understand the value of each proposal of yours, if it came with concrete use cases. Not just "I want to be able to write AnyA<'a> : 'a" but some actual program, that solves a real-world problem, that would be improved by the availability of the feature.

(In other words, show not just the implementation of AnyA<'a> but some code that uses it to accomplish something, and also how that's either not possible or significantly clunkier in the absence of AnyA<'a>.)

3 Likes
15

They are specific - we want AnyA<'a> because Any can't be polymorphic over lifetimes (since lifetimes are conceptually provenance rather than types, yet they're encoded in the type system... but we digress) - and also abstract - we don't have an use for AnyA<'a> other than it makes us feel happy and looks cool.

We do know others have an use for it tho, but we're bad at keeping track of other ppl's threads. But ppl have wanted to do run-time polymorphism over lifetimes before. After all, at least for actual types, you can always emulate GATs and HKTs using Any. You just can't have lifetimes.

16

I hope you'll understand that "it makes us feel happy and looks cool" does not help me understand whether a proposed new feature would be a useful addition to the language, and I doubt I'm the only one who feels that way.

2 Likes
17

So like, this is how this would be used:

fn foo<'a>(x: &dyn AnyA<'a>) -> Option<&&'a str> {
  x.downcast_ref::<for<'a> &'a str>()
}
foo(&"foo" as &dyn AnyA<'_>)

And we noticed a problem here because technically &'static str is a T<'a> (try it yourself: type T<'a> = &'static str), but so is &'a str.

You'd need some way to specify whether you want the 'static variant, or the lifetime variant. because of overlapping impls/specialization on lifetimes. This is actually brought up in some posts about GATs and HKTs here: Associated type constructors, part 4: Unifying ATC and HKT

On that post it's proposed to be strict so inference still works. Here we propose being lax so you have to explicitly specify what you want. But ofc we didn't think about how to do that, so... oh well :‌/

18

This is still too abstract for me -- I understand what this does (I think) but not why you would need to do that. What's stopping you from passing around &'a str and/or Option<&'a str> or some concrete enumeration, one of whose alternatives holds a string?

(It's possible that Any is a red herring here. Can you come up with an example that doesn't involve "I want to pass around a black box whose contents are unspecified except for their lifetime"?)

2 Likes
19

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