Lifetime polymorphism brainstorm

Lifetime polymorphism. What do I do?

There are few interwoven issues:

• Do we want lifetimes to be partially ordered or totally ordered?
• We want &'a T to be coercible to &'b T if we know that 'a <: 'b (i.e. 'b' is strictly shorter than 'a).
• We want to express something very similar to stack polymorphism.

The typing of a function is effectively a promise, that:

I (here meaning the function in question) can be called with any stack S, as long as P(S) holds, though this predicate only looks at a small subset of the stack. I might change this subset (push/pop values), but I will not change the rest of the stack. By using forall instantiation, you can give me a continuation that can depend on the rest of the stack, even though I cannot. This continuation can also depend on any changes I have made.

By changing that phrasing slightly, we arrive at what we would like our lifetime polymorphism to achieve:

I (here meaning the function in question) can be called with any lifetime graph L, as long as P(L) holds, though this preducate only looks at a small subset of the graph. I might change this subset (add/remove lifetimes), but I will not change the rest of the graph. By using forall instantiation, you can give me a continuation that can depend on the rest of the graph, even though I cannot. This continuation can also depend on any changes I have made.

Here we run into an issue: With stack polymorphism we could express P(S) as the front S looks like this, while we cannot do this for P(G). In fact no matter who we represent G, we might depend on lifetimes present in the middle of G.

Dead end 1

We tag code blocks with the lifetime graph they require:

code[G = ('a, 'b : 'a)]{r0: ...}

We then allow a coercion from code[G]{...} to code[G']{...} if we can find an embedding of G inside G'. However this is not satisfactory, as we can always find an embedding of G inside G' for any G, G', by mapping every lifetime in G to the same lifetime in G'.

Dead end 2

What if do something similar to stack, i.e. force the element we do care about to structurally be at the "front" of the graph. Would that work?

No, probably not. Let us look at this function:

fn foo<'a, 'b>(x: &'a T1,y: &'b T2) -> T3 {
   [something with x and y]
}

Let us say that we syntactically required the graph to look like 'a : 'b : G. In this case we could never have 'b < 'a, because that graph could not be represented as the above.

Possible solution 1

Ken said that we should consider the idea of not having an object representing the lifetime graph directly, but instead represent it implicitly using the context. I do not see how that would work, but I am open to ideas!

Possible solution 2

Instead of placing the restrictions on the graph when we use it, how about we place the restrictions when we define it? In other words something like this:

forall S, G fulfilling R
  code<G>{sp: code<G>{sp: S}, S}:
    ret

Here R is a set of requirements, that a G should fulfill because it can be used to instantiate it. We are able to coerce a forall G fulfilling R to forall G fulfilling R' as long as R' is more restrictive than R.

Open questions

• How do we handle adding new lifetimes/removing them before calling our continuation? Adding lifetimes is never an issue, but removing lifetimes that are not a the front is an issue. Perhaps we should go with a total order?