Given how lifetime works, I would expect what is now written as
fn f<'a> (x: &'a str, y: &'a str) -> &'a str
to be instead written as something like
fn f<'a, 'b> (x: &'a str, y: &'b str) -> &'a∧'b str
Here 'a∧'b is supposed to mean the meet of 'a and 'b.
What is the rationale for the current notation? For example, is there aspect that the current notation is conveying naturally or effectively?
What do you mean by the "meet of 'a and 'b"?
The coercions you are allowed to do depend on the variance of the type in the lifetime. How would you write
fn f<'a>(x: fn(&'a str), y: fn(&'a str)) -> fn(&'a str)
These are not simply different notations; these are actually different function signatures. When you call the first f(), if the two references you supply have different lifetimes, then they are coerced to have shorter, equal lifetimes (which is possible because &'x str is covariant in x, i.e. &'short str is a subtype of &'long str when 'long: 'short). This coercion is an operation performed by the calling code, not by f.
If -> &'a∧'b str were a thing that is possible to write, then the lifetime shortening would be happening within the function itself. This is arguably superior to what we have because it might allow more cases of higher-order function usage, but it is different and would require a quite different implementation in the compiler.
This is enlightening. I didn't know there is coercion happening. So I may paraphrase the current notation as follows:
'a where the lifetime of the first argument is at least as long and the lifetime of the second argument is also at least as long, the function guarantees a result whose lifetime is at least as long.Under that statement, if the caller uses the result at a time that exceeds either argument's lifetime, then the result is not guaranteed to be alive, thus rejected by the compiler.
You can say essentially that; it's written
fn f<'a: 'r, 'b: 'r, 'r> (x: &'a str, y: &'b str) -> &'r str
It's just not useful to do so, because the variance in & means that, in effect, does the same thing as just
fn f<'a> (x: &'a str, y: &'a str) -> &'a str
Note that it's not a coercion, it's full subtyping, which is much more powerful.
Like all mathematics article on Wikipedia, it is reference material assuming you already know the field. I tried reading it, and it was nonsense to me (with a bachelor in computer engineering and master in robotics).
If you want to explain to people who know set theory but never even heard of order theory you need to find some other reference.
No, that is not correct. The function does not accept arguments with two different lifetimes. It accepts two arguments with one lifetime, and returns a value with the same lifetime as the inputs. The function is generic over exactly one lifetime parameter <'a>; it never sees more than one lifetime involved in any call to it.
The coercion of longer lifetimes to a suitable single lifetime 'a is the (implicit) responsibility of the code calling the function, not the function itself. The coercion happens to the references before they are passed to the function.
My preferred way to explain this signature
fn f<'a>(x: &'a str, y: &'a str) -> &'a str
is that uses of the returned value keep the associated input borrows active. Both *x and *y remain borrowed so long as the return value is in use, because they are both associated with the same lifetime. If any use of the referents conflicts with being borrowed for that duration, or if the arguments at the call site cannot be coerced to that lifetime, you get a borrow checker error.
Due to variance, the lifetime is not determined by what you pass in.[1] The lifetime in the type of the arguments at the call site do not determine what the lifetime in the return type will be. Instead, the use of the returned value determines what the lifetime will be. I.e. how long the referents must remain borrowed.
By framing it this way, we are no longer tempted to say things like
'a will get the concrete lifetime that is equal to the smaller of the lifetimes of x and y"[2]And instead can reason in a way that more closely matches how the borrow checker actually works.
though what you pass in may result in a borrow check error ↩︎
If I understand the explanation correctly, then it suggests that we understand lifetime annotation as a notation of dependence. A returning reference marked by 'a may at most depend on arguments marked by the same name. I was happily reading the lifetime annotation that way, but ran into difficulty reading 'b: 'a. Under the dependence idea, is there a way to read 'b: 'a, such that for
fn g<'a, 'b> (x: &'a str, y: &'b str)
-> &'a str where 'b: 'a
we can see that returning a reference of lifetime 'b is sound?
The function does not return a reference type with a lifetime 'b. It returns a reference type with a lifetime 'a. But it is sound for the function body to coerce a &'b str to an &'a str, for example by returning the y value.
So perhaps your real question is, how can we read 'b: 'a such that it is clear that *y remains soundly borrowed, should the function body happen to return the y value?
One possibility is to read it as "if 'a is active, 'b is active".
Using the returned value keeps 'a active, and 'a being active keeps 'b active, so the borrows of both referents are still kept active by uses of the returned value.
Thanks for everyone who tries to help me navigate through the problem. I now see how to understand the current notation with subtyping, and I also feel that the dependence reading may still have the potential to be made precise.
Possibly as a final comment, I would like to add a few words about the second lifetime annotation idea in the initial post. Although there may be implementation subtleties, the idea may still has some merits. For example, we may write
fn h<'a,'b> (x: &'a str, y: &'b str) -> &'a+'b str
to express that the result has a lifetime of either that of 'a, or that of 'b, exclusively. Or we may write
fn k<'a,'b> (x: &'a str, y: &'b str) -> &'a∨'b str
to express that the result has a lifetime as the union of 'a and 'b. For the moment this annotation idea may be far away from implementation, but it probably doesn't harm to think about them.