Higher-ranked trait bounds

[nikomatsakis]

A description of higher-ranked trait bounds, which is the remaining piece needed to make unboxed closures equal to normal closures.

Rendered view.

[P1start]

The current syntax for higher-ranked lifetimes in bare functions is fn<'a>(&'a int), not <'a> fn(&'a int). Perhaps bare functions could stay the same, Fn{,Mut,Once} could use a similar syntax with the sugar (Fn<'a>(&'a int)), and any other trait would have to use the for syntax (for<'a> Foo<&'a int>).

[nikomatsakis]

On Fri, Oct 10, 2014 at 02:06:51PM -0700, P1start wrote:

The current syntax for higher-ranked lifetimes in bare functions is fn<'a>(&'a int), not <'a> fn(&'a int). Perhaps bare functions could stay the same, Fn{,Mut,Once} could use a similar syntax with the sugar (Fn<'a>(&'a int)), and any other trait would have to use the for syntax (for<'a> Foo<&'a int>).

I considered this. The main reason I did not propose it is that it
makes the parsing much more subtle. How do I know whether Foo< is
going to be Foo<A,B> or Foo<'a>(...)? It seems to require quite a
bit of lookahead, particularly if you don't want to rely on the
lifetime vs type distinction (which I don't, for reasons described in
the RFC). I suppose that there is a cover grammar, nonetheless, so
in principle it doesn't require extraordinary lookahead.

Of course, there is also some appeal to having a single syntax that is
uniformly applicable to all types.

In any case I certainly ought to have included a section on it for the
RFC.

[pnkfelix]

should we allow the for <'a> format at the fn definition point as well (in addition to the type expression form)?

i.e. support as an item for <'a> fn(x: &'a mut int) -> &'a mut int { *x = *x + 1; x }

[glaebhoerl]

@pnkfelix That's essentially #122, which was postponed.

[reem]

I suppose that we have for<'a> instead of forall<'a> because it's shorter? I am sympathetic to that claim, but forall makes it clearer that we mean "for all lifetimes 'a" instead of "for some lifetime 'a".

+1 to the proposal overall.

[arielb1]

With the new higher-order lifetimes and the new where clauses, would some version of

trait Iterable<T, 'a> {
    type IT where IT : Iterator<T> + 'a;
    fn iter(self) -> IT;
}

fn test<T>(i: &T) where for<'a> &'a T: Iterable<uint, 'a>

be legal?

[Ericson2314]

Looks good, I eagerly await this feature! 3 questions:

• Currently, are (type- or lifetime-) polymorphic functions subtypes of all possible instantiations, or are the needed type parameters inferred separately from subtyping?
• There are a number of ways to generalize this feature, (type- and lifetime- quantification, higher-rank types, higher rank traits (trait for<'a> MyTrait { .. })). I completely understand not trying to address them all pre-1.0, let alone in one RFC. But has anybody looked into whether the proposed syntax at least generalizes? The for<'a> syntax is very nice; it would be a pity if down the road it didn't work for some reason.
• Rather than relying on the eager/late check, could one (also) explicitly write something like impl for<'late> FnMut(&'late Foo) -> Bar for SomeType { ... }. The ability to display that intent might be useful both to inform readers of the code, and the get the compiler to error why one's impl won't work, rather than silently "downgrade" it.

[nikomatsakis]

On Sat, Oct 11, 2014 at 01:00:48PM -0700, arielb1 wrote:

With the new higher-order lifetimes and the new where clauses, would something like Rust fn test<T>(i: &T) where for<'a> &'a T: Iterable<uint> be legal?

Hmm, so, this was not covered by the RFC, though in principle it is
possible. I remember thinking about this use case at one point before
and forgetting about it, thanks for reminidng me. :)

In any case, to accommodate this requires basically requires only
changing the grammar and definition of late-bound-lifetimes.
Late-bound-lifetimes would thus exclude only those which appear in
where clauses (those could be in principle be permitted too, but it'd
require both support for trait-bounds that are parametric over types
and an extended vesion of the for clause that itself included where
clause).

In the impl itself, there aren't many changes either, as the scope of
the for clause would probably "cover" the self type, even though
without permitting the syntax you suggest, there'd never be a use of a
bound lifetime within the self type.)

[nikomatsakis]

On Sat, Oct 11, 2014 at 01:52:52PM -0700, John Ericson wrote:

Looks good, I eagerly await this feature! 3 questions:

• Currently, are (type- or lifetime-) polymorphic functions subtypes of all possible instantiations, or are the needed type parameters inferred separately from subtyping?

Type parametes are seperate, but higher-ranked fn types are possible
with lifetimes, and they are subtypes of possible instantiations. The
scheme is roughly the same as what is described in the RFC.

• There are a number of ways to generalize this feature, (type- and lifetime- quantification, higher-rank types, higher rank traits (trait for<'a> MyTrait { .. })). I completely understand not trying to address them all pre-1.0, let alone in one RFC. But has anybody looked into whether the proposed syntax at least generalizes? The for<'a> syntax is very nice; it would be a pity if down the road it didn't work for some reason.

I've tried to look ahead and I believe the for syntax scales.
Extensions I think are likely are type quantification (explicitly
discussed in the RFC) and the possible future ability to include not
just universally quantified lifetimes/types but to include "inline"
where clauses (for<'a,'b> where 'a:'b or something). I kind of hope
we never have to add such a feature though.

• Rather than relying on the eager/late check, could one (also) explicitly write something like impl for<'late> FnMut(&'late Foo) -> Bar for SomeType { ... }. The ability to display that intent might be useful both to inform readers of the code, and the get the compiler to error why one's impl won't work, rather than silently "downgrade" it.

I considered this previously, when we were deciding how to handle
fns. We settled on the implicit route. We've been using the eager/late
check for quite some time with no complaints whatsoever, so I feel
pretty good about it overall.

[arielb1]

@nikomatsakis

Nice! Note that if you take the associated type -> fundep desugar, you should get something like

trait Iterable<T, IT, 'a> {
    fn iter(self) -> IT;
}

fn test<T>(i: &T) where for<'a, IT> &'a T: Iterable<uint, 'a, IT>
                                    IT: Iterator<T>+'a

So associated types seems to be a non-conservative extension (is this the right term here?) over fundeps+HRLT. Is this correct? (However, this is not seem to be the same as full 2RT, as IT is a formula with no free type variables).

By the way, aren't "late-bound" lifetimes just lifetime parameters that the impl-ee is bivariant in?

[glaebhoerl]

Looks good to me!

Is there any reason not to allow higher-rank lifetimes on normal structs and enums? E.g.

struct Foo<'a> { ... }

and then

for<'a> Foo<'a>

Edit: Also, I wonder if there's any theoretical difference between &mut for<'a> FnMut(int) and for<'a> &mut FnMut(int).

[arielb1]

@glaebhoerl

Universal quantifiers can always be moved around in a covariant context – so &mut ∀'a &'a T ~ ∀'a &mut &'a T

[glaebhoerl]

Yeah, that's what I figured... it's only the fact that this is a trait, with some form of implicit existential quantification going on, which makes me a bit uncertain. (Probably you're right, I just didn't feel like thinking it all the way through.)

[brson]

Accepted. Discussion. Tracking.

[glaebhoerl]

An interesting question which occurred to me:

Is there a difference between for<'a> Foo<'a> and Foo<'static>? In theory and/or in practice? If yes, what is it? If no, what does that imply?

(Relatedly, my earlier question, "Is there any reason not to allow higher-rank lifetimes on normal structs and enums?", is still open as well.)

[huonw]

Is there a difference between for<'a> Foo<'a> and Foo<'static>? In theory and/or in practice? If yes, what is it? If no, what does that imply?

I think the answer is yes, depending on the variance of 'a in Foo, e.g. substituting 'static into struct Foo<'a>(fn(&'a int) -> &'a int) seems to be quite different to a HRTB.

[glaebhoerl]

Yes, it definitely seems to be different in the contravariant case.

[Ericson2314]

This reminds me, if 'static is the upper bound of all lifetimes, could there be a lower bound? Would higher-ranked lifetimes then only be needed in the invariant case?

[glaebhoerl]

That was one of the next thoughts I had, along with existentially quantified lifetimes (which are nonsensical for the covariant case, but perhaps not for the contravariant one). The lower bound would presumably be the empty lifetime, but given that &'a Foo means that the reference does not outlive the lifetime 'a, a reference with an empty lifetime by definition cannot exist. Maybe it could work somehow in the contravariant case, but it seems weird. Perhaps this is also connected to the discussion I saw at some point over whether 'static is the infinite lifetime, or merely the longest finite lifetime (life of the program) we can get our hands on. Analogously, maybe there is a "shortest lifetime that ever exists in practice", like the lifetime of a temporary? I have no idea. (For the invariant case, maybe there is also some connection to Spellcode's local quantifier, which I've never really managed to wrap my head around.)

(By "contravariant" in the above I mean "expects a reference type as argument"; last time I checked the terminology was accepted as being vice-versa for the lifetimes themselves.)