Universal quantification for types

[Ekleog]

Currently, we have for <'a>. I was thinking of expanding it into for <T: Trait>.

The use case is the following:

trait Trait {}

// This is implementation detail
struct Foo<T>(T);
impl<T> Trait for Foo<T> {}

// This is public API, foo takes a type and a closure that takes a Trait as input
pub fn foo<T, F: Fn(Foo<T>)>(t: T, f: F) {
    f(Foo(t))
}

(playground link)

Here, I don't want to expose the fact that F must take a Foo<T>. I want to expose the fact that F must take any Trait. But there's no way I can think of to encode this assertion in the Rust type system, currently.

So I was thinking of adding for <T: Trait> bound on types. As was pointed out to me, eg. for <T: Trait> Fn(T) wouldn't be object-safe. But I think that's something that could be useful nonetheless, as exposed by the corrected signature for foo below:

pub fn foo<T, F: for <P: Trait> Fn(P)>(t: T, f: F)

The actual use case that made this idea emerge was with tokio::Stream: I have a function like this:

pub fn bar<
    Stream,
    HandleErr,
    Callback: Fn(MapErr<Stream, HandleErr>) -> MapErr<Stream, HandleErr>
>(
    stream: Stream,
    err_cb: HandleErr,
    callback: Callback
)

Actually, this is a lucky case. Indeed, had I not directly passed the err_cb into stream.map_err, but instead passed eg. a closure, I'd have been completely unable to write the type… and would have had to re-write the closure type by hand just to be able to type it.

So, with the proposed for <T: Trait> idea, the function would look like this:

pub fn bar<Stream, HandleErr, Callback: for <S: Stream> Fn(S) -> S>(...)

What would be possible to pass into it would be (resuming with the toy example above):

// Template functions:
fn baz<T: Trait>(t: T) { }
foo(baz);

// If type inference permits, closures where the body uses only functions from `Trait`
foo(|x| ());

So if that's technically possible I think it'd be great. But I'm not sure it is? I guess it'd require monomorphization of the argument inside of the function body before knowing the size of the said argument, at least.

Anyway, would be glad to hear any opinion on this idea :)

[Ekleog]

So about the technical argument, I guess it'd require monomorphization of the argument inside of the function body before knowing the size of the said argument, at least. Which could cause issues with eg. mutually recursive functions both taking the same for <T: Trait> Fn(T) argument.

I think this could be solved by monomorphizing above the two functions at the same time, but that'd require monomorphizing in the call graph at a starting point and then computing the size, so no simple “take the number of monomorphs in this function and add the number of monomorphs for all called functions”, it'd have to be done cleanly, eg. propagating a set of the monomorphs in the call graph and then taking it as the argument.

Edit: OK, so I should start thinking before I send comments: the above was a discussion of how to make the proposed types object-safe, even though I explicitly mentioned they shouldn't be.

So for the actual technical reasoning: in my mind, it's all about closure inference. The same behaviour can currently be replicated using a trait Foo { fn bar<T: Trait>(&self, t: T); }, so for almost everything (for the Fn-like traits at least, not sure it'd have a use outside of these) all the work apart from closure inference should be, from my never-really-touched-the-rustc-code point of view, light (basically some syntactic sugar).

However, for closures there is a need to actually type them, and auto-deriving all traits that could potentially match a closure sounds like something that wouldn't scale well across large code bases (or would it?). So I'm thinking of a kind of “adversarial typechecking” (there must be an actual word for this in type theory, I just don't happen to know it): take the closure type and what you're trying to match it against, and, if it matches, then it's all good.

So, for an example:

fn foo<F: for <T: Iterator> Fn(T)>(f: F) {}
fn bar<F: for <T: Future> Fn(T)>(f: F) {}

let closure = |x| { x.next(); }
// closure has type [closure], that doesn't derive any trait

foo(closure);
// Here, type to match closure with for <T: Iterator> Fn(T). As it's a closure type,
// this needs proving that the closure indeed verifies this. We use the same code
// as for when verifying a fn baz<T: Iterator>(t: T) { t.next(); } typechecks.
// It does typecheck, so allow that

bar(closure);
// Same thing here, but fn quux<T: Future>(t: T) { t.next(); } doesn't typecheck.
// So that's a type error

Did I miss another difficulty?

[Centril]

For reference, this is what you get with {-# LANGUAGE RankNTypes #-} in Haskell. Some reading:

• https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html

Iirc, Haskell deals with RankNTypes by not monomorphizing things. cc @glaebhoerl on this.

[glaebhoerl]

(Sorry, I didn't read the previous two comments in detail, just responding with what I know per the cc:)

for<T> in where clauses would actually correspond to QuantifiedConstraints; iirc, there's nothing stopping that from being implemented in Rust on the code generation side at least. If you could pass generic functions around by value, e.g. fn foo(bar: fn<T>(T) -> T), that would indeed correspond to RankNTypes. I haven't actually tried to think through what happens if you try to make a trait object out of a for<T> bound, so not bar: fn<T> but bar: for<T> Fn (in Haskell, this would be putting a quantified constraint on an existential type variable, though I don't know if the particulars match up with Rust's trait objects in every detail), but it seems quite plausible that it would also be RankNTypes-alike.

To implement you RankNTypes you need either type erasure (what GHC does, and what Rust does for lifetimes), or intensional polymorphism (what Swift does - pass sizes, alignments, etc. around at runtime). (In both cases, trait vtables would also be passed at runtime.) I think the choices Rust has made (such as "DST" over "SST", and having specialization) make it rather non-trivial to retrofit it with either of those in a clean way, but it's been a long time since I was actively thinking about these things so I can't remember all the details. (And, e.g., the idea of ?DynSize wasn't around back then, I don't know whether that could maybe play a role.)

[Ekleog]

Hmm, so with your comment I think what I'm looking for is the equivalent QuantifiedConstraints? As the idea was not to try to make the for <T> Trait<T> types object-safe (that'd be a separate issue, that'd have to be taken along with making trait Foo { fn bar<T>(t: T); } object-safe).

[kupiakos]

This looks to be a duplicate of #1481