Let us now return to the exchange rule. Remember from before that this rule says that order of variables is irrelevant.
\[\begin{matrix} G_1, y : T_2, x : T_1 \vdash e : T_3 \\ \hline G_1, x : T_1, y : T_2 \vdash e : T_3 \end{matrix}\]Much as Rust allows full control of the contraction rule with the Copy
and Clone
traits
and partial control of the weakening rule with the Drop
trait, I am interested in what would
happen if we allowed control of the exchange rule.
First, we need to understand what it means to not have the exchange rule.
I said before before that it literally means that we must use variables in the order they are given,
like in the stack data structure. Forbidding all uses of variables out of order might be useful for something like files on disk space, where reading in order is cheaper.
We also have the case of Return<T>
, referencing the most recent stack frame in the call stack discipline, where we need to consume
it before any other instances of Return<S>
referencing higher stack frames are called.
Most of the time however we do need random-access,
the ability of machines to access out of order locations in memory. Most situations where
we care about order are the same ones Rust’s lifetime system was designed to prevent: use-after-free bugs.
Rust’s lifetime system is primarily concerned with the relative order between two variables, and all other
exchanges are allowed.
The next question, then, is how do we add back exchange for all but a few selected cases? If we try to use the same approach as the other substructural rules and directly come up with a trait for exchangable types, we run into the issue that there are now two types involved in the exchange, and there is no obvious way to orient the trait around a single type. Besides, this does not really lend itself to most variables being independent of each other. I started from considering that every set of variables would be (implicitly) equipped with a linear ordering — what the lack of exchange normally implies where there is a single ordered sequence the variables can be listed in. Exchange would be modeled as having a choice between multiple orders. However, I was very tempted by how Rust’s lifetime system specifies relative order as a directed acyclic graph of in-type dependencies; each participating variable’s type contains the lifetimes of the variables that it must be used before. This system creates a partial order - some variables are independent of each other and have no particular relative order. What ultimately convinced me is that it turns out there is a theorem that the set of all possible topological sortings of a directing acyclic graph is unique. Thus, in theory the orders specified by directed acyclic graphs should be representable as some choice of linear orders. These choices can be extremely complex, however, so specifying order as a sort of lifetime system should be much more easily usable.
Here is what this might look like as a new lifetime system in Rust-like syntax. For every variable x
that is in
scope, 'x
denotes the lifetime of x
. As in Rust, we can also introduce new lifetimes as type-level parameters;
we however need to be careful that these do not conflict with the names of any variables that will be introduced.
The syntax 'x * 'y
is used to indicate the lifetime that is the intersection of 'x
and 'y
.
Unlike in Rust, passing a lifetime as a type-level parameter does not specify the relative order of the resulting type.
We do still want to support lifetime parameters, but a type constructor is in theory free to do whatever it wants with them.
To specify a value of a type is order-restricted, we instead introduce the syntax 'l ! T
, where 'l
is a lifetime, including interesections of lifetimes. A variable x : 'l ! T
is just like a variable of type T
except that it must be used and consumed
before any of the variables 'l
comes from are used.
In Rust, the type constraint T : 'l
is used much like a trait to assert that all lifetime constraints of T
‘outlive’ 'l
.
More precisely, this is ‘non-strictly outlives’, meaning that T
might be of the same lifetime as 'l
but does not
contain any lifetimes shorter than 'l
.
Because we do not pass in lifetime constraints as parameters to T
, we do not automatically know if T
actually has more
constrained lifetimes inside of it, such as in ('m ! T) : 'l
. Instead, we treat 'l
and other lifetimes as actual traits
(albeit ideally auto-derived) defining the ‘non-strictly outlives’ relation.
trait 'l {
fn outlive<'m>(self : 'l * 'm ! Self) -> 'l ! Self;
}
What this means is that an implementing type T : 'l
can safely ignore any lifetime constraints applied to it that are stricter than 'l
.
Of special importance is the lifetime 'static
, which both in Rust and here is the “no-op” lifetime constraint;
'static ! T
is always just T
.
A type T : 'static
is able to ignore all lifetime constraints applied to it.
trait 'static {
fn outlive<'l>(self : 'l ! Self) -> Self;
}
Most data types will assert outliving at least some known lifetime, allowing most other lifetimes
to be safely ignored. On the other hand, most codata types, like functions,
do not assert outliving any lifetimes, as different instances can have arbitrary lifetimes.
This comes from the former being eagerly evaluated while the latter are lazily evaluated.
Given an unknown function value restricted to some lifetime, we don’t know enough about the function
to know whether the lifetime can be safely ignored, so we must always assume the lifetime is legitimate.
In practice, closure types may often want to get around this by providing an
explicit lifetime constraint, such as FnOnce() -> T + 'static
.
An important exception is Return<T>
; while a data type in other respects it does not assert outliving any
lifetimes. This is how we prevent instances of Return<T>
from escaping the callback they are provided in.
Lifetimes have two structural properties of note:
Extra lifetime constraints can always be added; that is, we always have
fn lower<'m>(self : Self) -> 'm ! Self;
Lifetimes distribute over structs and enums. If a struct or enum is lifetime-constrained, then it can still be destructured, but all of its fields will then have that same constraint added. If constructing a struct or enum from fields with the same lifetime (or more likely, lowered to the same intersection), then we can move the lifetime constraint to the outside.
Where we truly depart from Rust’s lifetime system is the role that they play in function invocation.
In Rust, function arguments and the return type are by default unconstrained by lifetimes, and only argument types with an explicit
or inferred lifetime parameter will be constrained in the function body. Lifetime
constraints on the return type must be explicit. Our system is in a sense the exact opposite. All function arguments
are assumed to have some constraint external to the function body, and we rely on argument types asserting they outlive 'static
or some other known lifetime
in order for those arguments to escape the function invocation. I have taken to calling such types semistatic. The return value is constrained to the intersection of the lifetimes
of all function arguments and the function itself. If we are trying to return a data type, then there too we rely on this data type
being semistatic in order to be able to use it for most expected purposes.
Let me make this a bit more precise. To invoke a function on an argument, they need to both have the same lifetime
constraint applied, which in practice means lowering to their intersection.
The result of the invocation is then this same lifetime.
For example,
if we apply a function of type l ! FnOnce(A) -> B
to an argument of type m ! A
, we will get
a value of type l * m ! B
.
Being semistatic basically tells us how much of the environment
a return value is dependent on. A non-semistatic type like a closure must be assumed (in this case accurately)
to be capturing and depending on the entire environment it is given. Thus, it is impossible
to construct a non-semistatic value without being constrained to the lifetimes of its inputs, which may themselves
be semistatic with known lifetimes, but may also be non-semistatics with arbitrary lifetimes.
This is why trying to hide a lifetime within a type constructor doesn’t really work;
all values of the type that ever get constructed will still end up with a lifetime constraint
on the outside, either one it is asserted to outlive or all the lifetimes of whatever environment was used to construct it.
If storing the negative return type of a function as a closure, then this means the closure is lifetime constrained to all inputs passed to that function. For example, in
fn f(a : A) -> FnOnce(B) -> C
{
|b| g(a, b)
}
let a : 'l ! A = ...;
let g : 'l ! FnOnce(B) -> C = f(a);
g
must be constrainted to lifetime 'l
because it contains a
sharing the same constraint.
An arbitrary closure type cannot be semistatic,
but because we know these are the only inputs, we can explicitly assert that the closure is semistatic
by writing its type as FnOnce(B) -> C + 'l
.
let g : 'l ! (FnOnce(B) -> C + 'l) = f(a);
Writing 'l
twice is a bit unwieldy, so let’s assume that at least let expressions can infer
their lifetime from the expression being assigned.
let g : FnOnce(B) -> C + 'l = f(a);
Returning other non-semistatic types looks similar to returning a closure type; you will
be constrained to the lifetimes of whatever inputs were passed to the function.
For them too it sometimes makes sense to explicitly mark instances as being semistatic with T + 'l
—
but keep in mind that unless T
already outlives 'l
then this is implemented by a closure that returns T
.
Within the function, arguments are assumed to last the lifetime of the invocation, up to and including the constrained
return value, but not any longer than that.
In general, this means we do not usually need to put lifetime constraints on function arguments, and thus rarely do we need
lifetime parameters in functions at all. For example,
FnOnce(Return<T>) -> noreturn
written as is already disallows Return<T>
from escaping.
For this reason, I would not expect this system to ever need inference of lifetime parameters.
Negative types may not be semistatic, but their continuations as positive types will either be themselves
semistatic or be restricted in practice to being constructed from semistatic inputs.
We can understand why by looking at returning a negative type T
as returning
FnOnce(T::Cont) -> noreturn
. If need-be we could do this transformation automatically,
but in current calling conventions it is sort of implicit. The main thing this tells us, though,
is that negative types are strongly tied to noreturn
. The reason this is relevant is that if T::Cont
was not semistatic, then for most 'l ! T::Cont
, we would be forced to lower the function to 'l
and
then obtain 'l ! noreturn
. Right now, that is a dead end! noreturn
with a lifetime cannot be executed,
because the lifetime means that there may still undisposed variables (even if there actually isn’t and the
lifetime is extraneous, we will not allow that usage as it is inconsistent with our other lifetime rules).
As I mentioned, it is basically impossible to construct a non-semistatic value without some sort of lifetime,
unless it is done entirely from static inputs. Right now that means we cannot even use semistatic inputs,
but later on we will discuss functionality that allows us to know when it is safe to ignore certain known lifetimes,
even on noreturn
.
It thus appears that even when positive and negative types are syntactically unified, semistatic types remain an artifact of the distinction. Specifically, semistatic types seem to be a subset of positive types. Those positive types that are not semistatic are still valid argument types, but like closures they lack the ability to escape their environment. This creates a problem for their continuations, for the same reason as above; as long as the environment exists, we cannot call a continuation with only the tools we have now, as we have no way to ensure that the environment will eventually get cleaned up.
There is another way to look at this connection, from the point of view of constructions and eliminations. We said before that constructing a negative type is an asynchronous operation, meaning that its order does not matter as no information is lost by executing it. However, once lifetimes come into play there are suddenly order constraints. Once we apply the construction operation, we are immediately stuck with the lifetimes of all input variables. A negative type construction with a less strict lifetime than one of its input variables can only be so if we first eliminated that variable to the point where its original lifetime was no longer relevant — meaning we decomposed it into semistatic values. Similarly, when eliminating a positive type, the lifetimes of any available variables and the order they are destructured in is relevant to the lifetime of the result. In contrast, for the synchronous operations of constructing a positive type or eliminating a negative type, we have no choices; the lifetimes involved in the operation are preserved. Because we cannot eliminate the lifetime of a negative value without eliminating the value and thus losing information, it is impossible to take an arbitrary negative value of unknown lifetime and destructure and reconstruct it in such a way that only leaves a known lifetime. On the other hand, an arbitrary positive value of unknown lifetime can be destructured into values of the same lifetimes used to construct the value, so as long as these are known lifetimes we can reconstruct the positive value with only that lifetime constraint. Thus, right now the only positive types that would not be semistatic are actually closures, a.k.a. converted negative types. Being semistatic is thus in some sense a strong form of being positive.
One of the places that positive and negative types come up is in a proof technique called focusing.
As far as I understand it, focusing restricts the space of expressions one needs to case on
by forbidding spurious elim(construct(x))
and construct(elim(x))
combinations.
The way it does this is by structuring expressions so that
once a synchronous operation begins on a particular variable to be focused, you must continue to use synchronous operations
on that same variable or fields produced/consumed by it
until you hit an expression converting between a positive and negative type — then you begin
using asynchronous operations again. I am struck by how similar the positive case is to the effect of placing variables
into a particular relative order while requiring the result to have a specific lifetime.
We cannot break the order until those variables have been turned into semistatics, and we cannot construct the result too early
or else the resulting lifetime will be too strict. I wonder if a similar situation exists for the negative case. Still, I am no expert
and cannot make definitive statements on if there is a relationship here.
As a curiousity, we can define a negative counterpart of a lifetime constraint.
type 'l ? T = FnOnce('l ! T::Cont) -> noreturn
If this was built in like 'l ! T
, we might be able to use this as a sort of constrained continuation-passing style
automatically generated by a compiler from ordinary-looking syntax. For example, 'static ? T
is a value of T
but requires that its continuation is static. There could be uses for such a thing, if for example we want to invisibly fork
the continuation onto another thread.
We expect this constraint to have opposite properties to 'l ! T
:
Extra continuation lifetime constraints can always be removed; that is, we always have
fn extract<'m>(self : 'm ? Self) -> Self;
Continuation lifetimess distribute over choice and coroutines. If a choice or coroutine is continuation-lifetime-constrained, then it can still be destructured, but all of its fields will then have that same constraint added. If constructing a choice or coroutine from fields with the same continuation lifetime, then we can move the continuation lifetime constraint to the outside.
From these properties, then it is possible to show that 'l ? FnOnce(A) -> B
is equivalent to
FnOnce('l ! A) -> 'l ? B