Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Higher-ranked trait bounds #387

Merged
merged 3 commits into from
Nov 4, 2014
Merged

Higher-ranked trait bounds #387

merged 3 commits into from
Nov 4, 2014

Conversation

nikomatsakis
Copy link
Contributor

@nikomatsakis nikomatsakis commented Oct 10, 2014

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

Rendered view.

## Update syntax of fn types

The existing bare fn types will be updated to use the same `for`
notation. Therefore, `<'a> fn(&'a int)` becomes `for<'a> fn(&'a int)`.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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>).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 }

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@reem
Copy link

reem commented Oct 11, 2014

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
Copy link
Contributor

arielb1 commented Oct 11, 2014

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
Copy link
Contributor

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link
Contributor

arielb1 commented Oct 12, 2014

@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
Copy link
Contributor

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
Copy link
Contributor

arielb1 commented Oct 13, 2014

@glaebhoerl

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

@glaebhoerl
Copy link
Contributor

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
Copy link
Contributor

brson commented Nov 4, 2014

Accepted. Discussion. Tracking.

@glaebhoerl
Copy link
Contributor

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
Copy link
Member

huonw commented Nov 16, 2014

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
Copy link
Contributor

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

@Ericson2314
Copy link
Contributor

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
Copy link
Contributor

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.)

@Centril Centril added A-traits Trait system related proposals & ideas A-typesystem Type system related proposals & ideas labels Nov 23, 2018
@Centril Centril added the A-higher-rank-polymorphism Proposals relating to higher rank (non-prenex) polymorphism. label Nov 23, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-higher-rank-polymorphism Proposals relating to higher rank (non-prenex) polymorphism. A-traits Trait system related proposals & ideas A-typesystem Type system related proposals & ideas
Projects
None yet
Development

Successfully merging this pull request may close these issues.

10 participants