Generalising HRTBs

language design
1

There's some code I've been mucking around with (nothing particularly solid yet) where it would be useful to be able to write something like the following (note T is not a lifetime variable):

trait MyTrait1<T> { ... }

trait MyTrait2 where
  for<T> Self : MyTrait1<T> { ... }

So when I do:

impl MyTrait2 for u32 { ... }

The compiler checks for the impl:

impl<T> MyTrait1<T> for u32 { ... }

This doesn't seem too difficult, because just writing a function:

fn<T> f() where u32 : MyTrait1<T> {}

Will perform the same check for a generic impl, so to do this I don't need to perform anything the typechecker isn't already capable of.

Just wondering whether has been done, or it's in progress (so I don't reinvent the wheel) or if it isn't any tips of where I should start poking around the code to do this would be appreciated.

Alternatively if there is something obviously unsound about this if that could be explained I'd appreciate that also before I go down a rabbit hole that just breaks things.

2 Likes
2

Is there anything you can express with this that you can't already? I don't feel like you can outside of the presence of generalized associated types (i.e., associated type ctors).

The usual GAT formulations tend to include a for<T> construct, fwiw.

1 Like
3

Yes generalized HRTB is sufficient for writing HKT (at least a major subset; even without GAT), while GAT is not.

1 Like
4

There’s nothing I can’t express in nightly (in stable I’ve got some issues as I can’t name Fn types) but basically I end up with horrifically long “where” clauses particularly when I combine functions. Having this for all syntax would clean the code up, as instead of having individual where clauses for each particular usage in a function the for clause would cover them all.

5

I think generalized HRTBs are doable and would be nice to have, but there's some complexity you're not considering. Users would want the ability to put bounds in the for:

for<T: Debug> Self : MyTrait1<T>

(The current lifetime-only implementation doesn't support bounds; for<'a, 'b: 'a> Foo<'a, 'b> is an error.)

But then what if you want constraints that can't be expressed in that form, and normally require a where clause? We might need some kind of new syntax:

for<T where Bar<T>: Debug> Self : MyTrait1<T>

Though it's not strictly necessary, as users could use trait aliases instead...

trait BarDebug = where Bar<T>: Debug;
[..]
for<T: BarDebug> Self : MyTrait1<T>

...but that seems ugly.

Also, allowing trait bounds in HRTBs means they could be nested, letting you write extremely confusing type signatures:

for<T: for<U: for<V> Trait<V>> Trait<U>> Trait<T>

I'm personally fine with that; we have plenty of ways to write confusing signatures as it is. But others might object to the perceived complexity.

2 Likes
6

Thanks for your reply @comex, you bring up some really interesting points.

I haven't touched the Rust compiler before so I think I'll just start with unbounded foralls, although bounded foralls would have their uses. But one thing at a time.

I'll dig around and try to make a PR that's a proof of concept, although at that stage I'll probably need other's help to clean it up.

I've been poking around reading the Rustc guide but any other pointers appreciated.

7

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