Is GAT actually as powerful as HRTB?

language design
1

It seems like you can use Generic Associated Types to get the exact functionality that Higher Ranked Trait Bounds provide, with a little extra type-level indirection. Or without (all of) the jargon, you can use #![feature(generic_associated_types)] to be generic over using Rc or Arc, so long as you're okay with using Type<RcProvider> rather than Type<Rc>.

[playground]

#![feature(never_type)]
#![feature(generic_associated_types)]
#![allow(incomplete_features)]

/*!

We want:

```not_rust
struct UsesRc< R: { Arc or Rc } > {
    inner: R< u32 >,
}
```

Unfortunately, this requires higher kinds...
or does it?

GAT can be used to get this exact behavior,
if you squint a little...

*/

use std::{rc::Rc, sync::Arc, ops::Deref};

pub trait RProvider {
    type R<T>: Deref<Target=T> + Clone;
}

pub struct RcProvider(!);
pub struct ArcProvider(!);

impl RProvider for RcProvider {
    type R<T> = Rc<T>;
}

impl RProvider for ArcProvider {
    type R<T> = Arc<T>;
}

pub struct UsesRc< R: RProvider > {
    pub inner: R::R< u32 >,
}

Is there something I'm missing that makes "full" HRTB more powerful than GAT, or is this actually just HRTB-behind-type-indirection? (One downside of GAT-as-HRTB is that that the provider indirection structs have to be actively defined by the implementer of the trait for coherence to work out. Full HRTB wouldn't need the extra type, thus sidestep that extra coherence check.)

4 Likes
2

This.

By definition, this can have strong implications for safety, depending on what you're doing. (see also Any being a safe trait despite the intended user of the methods on the Any trait (not the inherent impl) being unsafe code.)

3

(FWIW, I think Any being a safe trait was a mistake. IIRC the stabilization of Any::type_id, or some other type_id, was delayed because you could implement it in safe code to cause unsoundness.)

How exactly does GAT-as-HRTB have safety implications? It's obviously harder to use, as there's an extra middleman, but it's no harder (theoretically) than implementing a trait you don't own for a type you don't own. In fact, it's easier: you can always define your own "provider" type to hook up whatever concrete you want into a GAT-as-HRTB trait.

If this actually has safety implications, that's something that should be discussed, because GAT-as-HRTB works just fine (with the GAT feature as currently implemented), and if there's a potential safety hole in it, we need to plug it.

I'm not interested in this constant amount of extra syntactic salt to use GAT-as-HRTB over full HRTB. I'm interested in actual differences in the expressivity of the two.

(To your benefit, Soni: if GAT-as-HRTB is shown equivalent to HRTB, one of the primary arguments against HRTB -- difficulty for the trait solver -- disintegrates, as it already solves the problem for GAT-as-HRTB.)

5 Likes
4

I was confused by this post at first, so I thought it would be good to clarify: this isn't what higher rank trait bounds means. Higher rank trait bounds just means that the parameter is introduced within the bound, and the feature already exists (restricted to lifetimes): it's for<'a>. Higher rank polymorphism is not the same as higher kinded polymorphism.

Here's a primer on the difference, though it discusses higher rank types, not trait bounds: Higher-rank and higher-kinded types | Stephan Boyer

But you're right, we've always known that GATs are equally as powerful as higher kinded polymorphism, though - as you've identified - you have to use this indirection from a type to a type operator (the GAT). This is less convenient for many circumstances, obviously, but avoids other problems Rust would encounter with higher kinded polymorphism (the currying problem). I believe Niko's blog series on this from 2016/2017 explains all of this well.

14 Likes
5

The main difference is that you can't actually make a generic impl for an AnyA<'a> that "just works". You can make an impl for references, an impl for static types, and then leave the rest up to users (thus requiring AnyA to be an unsafe trait).

As for the currying problem mentioned by @withoutboats, aka

fn foo<'a>(x: &dyn AnyA<'a>) {
  if let Some(x) = x.downcast_ref::<for<'a> &'a str>() { println!("1"); }
  if let Some(x) = x.downcast_ref::<for<'a> &'static str>() { println!("2"); }
}

foo(&"bar"); // does this print 1 or 2?

there is a syntax hack we can use, by learning from GATs: GATs require you to make type families, which means they force you to be explicit about the family. So we can fix the issue by simply requiring going through a generic binding, e.g.:

foo(&"bar" as &dyn (<for<'a> &'static str as AnyA<'a>>)); // must print 2, clearly!

Granted, it's slightly more verbose than using a type family. But there's no reason you can't have this, where you want/need the expressivity; and GATs, where you'd rather have less verbosity.

6

I was curious if you could have something similar for types, although I'm not sure it would technically be an "HRTB".

Something like:

for<B> impl<A> MyTrait<B> for A { ... }

...which would describe a trait impl with a generic parameter, but where the impl is the same regardless of the type used as the generic parameter, which presently isn't possible because otherwise the type would be unconstrained.

7

How is that different from this, which compiles today:

trait MyTrait<B> {}
impl<A,B> MyTrait<B> for A {  }
8

I think the non-existing syntax you want is

impl<A> for<B> MyTrait<B> for A { ... }

which binds like

impl<A> (for<B> MyTrait<B>) for A { ... }

so the generic parameter B isn't in-scope for the actual implementation.

Putting the for before the impl is basically a long-hand for what the generic on the impl itself actually means.

4 Likes
9

This is patently NOT the currying problem. Niko's blog series spells out the currying problem.

10

How's it not? And why's nobody linked those yet, anyway?

11

sent to you 16 days ago: Niko's blog
pls. don't rush, pls. don't gloss over, pls. read carefully this time, all 4 parts
leaving as a challenge for you to find which part is talking about currying

1 Like
12

Sorry, that wasn't the greatest example.

Here's an example of some code that doesn't compile today due to an unconstrained type parameter:

trait Foo {}
trait Bar<T> {}
impl<A, B: Bar<A>> Foo for B {}

I was curious if this could be resolved using something like this hypothetical syntax (borrowing from @Nemo157's suggestion):

trait Foo {}
trait Bar<T> {}
impl<B> Foo for B 
where
    B: for<A> Bar<A>
{}
2 Likes
13

Yeah, currying is exactly what we thought it was. We just didn't describe it in formal terms but in practical terms.

The problem is solved by being explicit. Make all non-GAT HKTs require explicitness and you have it completely solved. No need for inference/currying if you simply refuse to support it!

14

This could be alleviated with some very basic GAT helper trait (actually, a set of trait to cover arities):

trait TypeConstructor1 { type T<_0> : ?Sized; }
trait TypeConstructor2 { type T<_0, _1> : ?Sized; }
// etc.

// and some ergonomic type aliases
type Feed1<T_, A0    > = <T_ as TypeConstructor1>::T<A0    >;
type Feed2<T_, A0, A1> = <T_ as TypeConstructor2>::T<A0, A1>;
// ...

and then have something like

#[derive(TypeConstructor)]
struct Arc<T>...

doing the expected thing for some type Arc_.

From there, any downstream library could write their own type aliases:

trait RProvider : TypeConstructor1 {
    type R<T> : Deref<Target = T> + Clone;
}
impl<RC_> RProvider for RC_
where
    RC_ : TypeConstructor1,
    for<T> // <- no `for<T>` yet...
        Feed1<RC_, T> : Deref<Target = T> + Clone
    ,
{
    type R<T> = Feed1<RC_, T>;
}

If we had:

  • those for<T> higher order bounds (that is, HRTB but with types rather than just lifetimes),
  • potentially trait aliases for these versions with added bounds to show better intent (but does not seem paramount),
  • the #[derive(TypeConstructor)] automagically applied to all type definitions (with a way to handle any arity),
  • and the sugar to be able to:
    • write Rc rather than Rc_,
    • write Thing<T> rather than Feed1<Thing, T>,

then we'd have HKTs. When you stare at that list, besides the type-generic HRTB (for<T> ...), everything is mostly sugar and convenience (but for the impossibility to forget to derive(TypeConstructor)). This last point does indeed hurt in practice because of coherence: should a user library try to provide this, there should be only one such canonical library all the crates ought to turn to, based on cooperation and stuff, à la serde.

So I am mostly agreeing with you :grinning_face_with_smiling_eyes:, but I just wanted to mention that regarding coherence, there could be a decoupling between some universal serde-like crate providing the TypeConstructor definitions, and then freedom for downstream crates to provide their own specialized aliases :slightly_smiling_face:

1 Like
15

@dhm: one anecdotal point of evidence: I am a generic Java guy, I hoped I was somewhat smart :slight_smile: however I'm not a functional programmer at all and advanced Haskell is inpenetrable to me.

  • I can understand Niko's blogs (mostly)
  • I understand what @CAD97 wrote in the 1st post of this topic just fine
  • when I try to parse your code from post number 14 - unfortunately still haven't grokked it :frowning:

Maybe I'm old, maybe I'm dumb.. But there you have it.. Re age: active developer rather far from retirement :-]

2 Likes
16

Hey, yeah, I spitted out this code without much context :sweat_smile:, and I'm still not pleased with the naming I have used (which I think plays an important role to better express these semantics), so there are plenty of legitimate reasons to find my code unreadable :grinning_face_with_smiling_eyes: . I'd gladly go in more detail to help people grok this generic verbiage, but I don't think IRLO is the right place for that.

On the other hand, I think it can lead to a very interesting URLO thread, so if you feel like it, @atagunov, we can open a thread on URLO and we can there try to dissect the different patterns at play, here (btw, I personally hope you undo the deletion of your post, since it mentions code intelligibility which is not something to be overlooked. In a way, you have already helped answer the OP: even if GAT may be as powerful as HKTs, the level of trait indrection required to achieve that severly hinders the readability of the code).

Like with most code patterns, though, it's mostly a question of getting used to this form of programming (in this instance, type-level programming exclusively), which may involve Rust the language for its backing syntax, but is not like the usual Rust out there, so the brain needs some training to "read" these things :upside_down_face:

17

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