Extending `for<'a>` construct

The goal: Allow bounded universal quantification;

The core problem current form has is that when inference tries to select a lifetime that'd fit for<'a> ... bound it always ends up with 'static, which is very limiting.

The imagined syntax:

for<%list_of_introduced_parameters; %list_of contraints> %bound

An example

for<'c; 's: 'c> F: Fn(&'c Connection,&'s SqlStr) // 's is defined in containing scope

Semantics

This construct signifies that its following bound is generic over all lifetimes that statisfy a %list_of_constraints - the bold is the difference with current form.

EDIT: Two ways of reading this:

First one is left to right: "for all 'c, 's shall outlive 'c" => from this 's = 'static and 'c still has no constraint of it. This way doesn't fit us.

Second way is right to left: "exists 's => exists a set of lifetimes A, such that for any 'a є A holds the following: 's : 'a". This is the intended semantics.

Example motivation:

Sabrina's recent post - it has great example in the very beginning:

fn print_items<I>(mut iter: I)
where
	I: LendingIterator,
	for<'a> I::Item<'a>: Debug, //(1)
{
	while let Some(item) = iter.next() {
		println!("{item:?}");
	}
}

With this extension, we could write it correctly:

fn print_items<'i,I>(mut iter: I)
where
	I: LendingIterator + 'i,
	for<'a; 'i: 'a> I::Item<'a>: Debug,  //(2)
    //this means that for every lifetime that doesn't outlive the iterator,
    //`Item: Debug` is true.
{
	while let Some(item) = iter.next() {
		println!("{item:?}");
	}
}

The core point is that in this line:
print_items::<WindowsMut<'_, _, 2>>(windows_mut(&mut [1, 2, 3]));
the argument's associated lifetime isn't infered (and forced) to be 'static by (1) and instead is only forced to be 'i by (2).

Also, there are examples of APIs that are otherwise impossible here.

1 Like

Minor note: for<'a, 'b: 'a> should introduce two lifetimes, 'a and 'b. What you want is more for<'a> where 'b: 'a, which will require parentheticals, but should work.

A few potential ways of writing it:

where
    for<'a> where 'i: 'a, => I::Item<'a>: Debug,
    for<'a> (where 'i: 'a,) I::Item<'a>: Debug,
    for<'a> (I::Item<'a>: Debug where 'i: 'a,),
    for<'a> (I::Item<'a>: Debug) + 'i: 'a,
4 Likes

I think the syntax from the blog post also could be used (it also feels very intuitive to me and i once tried to use it like this, without knowing that it did not exist):

where
    for<'a where 'i: 'a> I::Item<'a>: Debug,

This lists the constraints right at the definition site, which i think is advantageous over

It also might be better for the parser, because it could reuse the existing where-clause parsing when it encounters the keyword inside of the <>.

3 Likes

If you do want to introduce multiple lifetimes, does one where go at the end?

    for <'a, 'b where 'i: 'a, 'j: 'b>

What do 'b and 'i mean in these examples if they are never introduced?

If all lifetimes are introduced (which I suppose they must?), then the already existing for<'a, 'b: 'a> syntax is enough to express everything.

My assumption with for<'a, 'b: 'a> was that it would introduce both 'a and 'b (be for<'a> for<'b: 'a>) like with other lifetime introducers (e.g. impl<'a, 'b: 'a>).

The 'i example was implicitly attached to fn print_items<'i, I>(mut iter: I) (from the OP).

2 Likes

That's indeed better!

Yes, only one where here - it serves as readable delimiter.

No, lifetimes are introduced before where, after it we put constraints on them.

Maybe we even want a must use property, so that bounds coming after where in for<.. where ..> must use (all of) introduced in clause lifetimes.

I think it's reasonable to require the bounds to only put constraints on/involving the introduced lifetimes, but I think requiring all of the introduced lifetimes to be bounded is unnecessary (and can be sidestepped anyway with 'a: or 'a: 'static).

1 Like

See also the discussion around issue 25860, which has another alternative syntax:

where
    for<'a> where<'i: 'a> I::Item<'a>: Debug,

Personally, I like the symmetry between the for and where.

1 Like

I agree, we still could later drop this requirement, but for the moment this seems good. (i think you meant 'static: 'a)

Hmm I find this syntax a little bit confusing, because it suggests, that such a where can also be used without the for (IIUC this is not possible/mentioned in the post).

True, that is a potential issue. But I still see it as the most visually consistent option overall:

  1. for<...> where ... (sep) Bounds: it can be difficult to tell apart the where bounds from the trait bounds at a glance. Also, it can introduce confusion between the inner and outer where.
  2. for<...; ...> Bounds: the syntax difference between , and ; is a bit too subtle for my liking.
  3. for<... where ...> Bounds: this is workable, but it seems weird to see the lone where keyword inside the angle brackets. Currently, the only keywords within angle brackets are from trait objects (Box<dyn Trait>) and HRTBs (impl<T: for<'a> Trait<'a>> ...), both of which are visually attached to the following trait name.
  4. for<...> where<...> Bounds: my preferred syntax. The angle brackets help distinguish the inner where from the outer where. No special parsing is needed for the interior of the brackets, since they contain an ordinary list of lifetime bounds. As you mentioned, there's a risk that the where could be seen as independent from the for, but I think this can be mitigated with a good error message.

Of course, I'd always be open to a new option. I recall the debates over how to name the let ... else construct, going through various permutations of unless let and if !let and if not let, before the current name was proposed and quickly adopted for the RFC.

  1. also seems like it might be difficult for the parser (and really should not be used IMO)
  2. yes definitely too subtle When comparing 3 and 4, look at how it looks with many bounds:
for<
    'a,
    'b,
    'c,
    'd,
    'e,
    'f,
    where
        'a: 'b,
        'c: 'f,
        'd: 'e,
> fn foo(...);
// vs
for<
    'a,
    'b,
    'c,
    'd,
    'e,
    'f,
> where<
    'a: 'b,
    'c: 'f,
    'd: 'e
> fn foo(...);

In option 3, i like that the > of the for is in front of fn, but the additonal indentation is not really nice (maybe indent the where by -1 and do not indent the bounds by +1). In option 4, i do not like the distance between the end of the for<> and fn. But overall I like option 4 more than putting the bounds even further away from the for. I think they should stay relatively close and be unambiguously connected.

(Realistically, something has gone wrong if you're juggling that many lifetimes at once...)

3 Likes

Yes this might be a bit excessive, but if you use lifetimes with longer names, the construct would also be need to be indented (or if you set your linewidth to something short). So I think we need to consider it.

Reallistically, the only difference here is > and < around the where:

VS

And thus,

if we take fuller single line example:

  • impl<'b,T: for<'a where 'b: 'a > Trait> ...
  • impl<'b,T: for<'a> where<'b: 'a > Trait> ...

Isn't the first cleaner? The same applies for the multiline case.

Lets just gauge the general opinion on this. If someone comes up with a different syntax that has majority support/introduces other benefits, then we can just use that, otherwise this could be baked into some rfc.

  • impl<'b,T: for<'a where 'b: 'a > Trait> ...
  • impl<'b,T: for<'a> where<'b: 'a > Trait> ...
  • something else entirely

0 voters

This of course assumes that adding the possibility for these bounds is indeed a welcome change (I think the majority of posts here reflect that it is).

This has the disadvantage of being inconsistent with where bounds in other contexts, eg.

    struct Foo<T> where T: Debug   // not Foo<T> where<T: Debug>
1 Like

If the only thing for<> constraints could do would be putting bounds on introduced parameters, I'd prefer for<where>. But something that gives me pause is the possibility of it being more general, for example perhaps some way to declare free closure lifetimes or otherwise drive capture inference. That is, things that might read weird within a for<>.

I grant it's a rather vague concern, given that I haven't imagined or seen proposed any good way to declare these sorts of things at all.

3 Likes

Made pull request into RFC repo, thanks for participating.

Hmm that is an interesting point... But when we would have exists<> then we could also allow a where inside that one. Granted you would need to write multiple where, but when we reach that point, allowing a where<> might also not be too far fetched (you would allow multiple where clauses at different points, but I think that is not really a bad thing).

Nice, what I am also wondering, are we going to allow for<'a: 'b> as a shorthand for for<'a where 'a: 'b>? I think this seems very natural considering you can do it in impl<'a: 'b> and at type-def.

Edit: Of course this makes only sense, if we allow for<'a where 'a: 'b> in the first place