Dilated

Exclusion Typing

The structural rules of lifetimes

I have been developing an implementation of references for my type system, drawing from Rust’s lifetimes. This post is a quick description of the design I’m running with at the moment, and relies on concepts from Rust about lifetimes and mutable references themselves - for anyone who wants to learn more about those I’d recommend the Rustonomicon, possibly Oxide an approachable subset of rust described in typing rules, and RustBelt is still relevant as a very thorough description of rust’s borrow checker - in many ways, my system behaves as the type theory of the logic used in rustbelt.

I had a few goals here:

That last paragraph in particular uses type theory terminology that might be new to some readers. I’d like to share a more theory-focused writeup soon, but this post is focused on how programs are written with these exclusion types.

I’ve encountered exciting answers to all of these points, so let’s have a look at the system!

We’ll begin with a nice classic example

fn swizzle<'l>(list: &'l mut Vec<u32>) {
    let v = &list[list.len() - 1];
    list.push(4);
    print(*v);
}

A function’s body gets permission to use its parameters as locals, so we set up the typing context:

named l: _, local list: &l mut Vec<u32>, perm_list: exl(?list, l), live l

We also have this extra property in the context: live l. In rust, lifetime parameters on functions are always live. This is explicitly tracked in our typing context because we need to be able to shrink the liveness requirement for expressions that touch less of the mutable environment.

The other new binding is the permission to access the list local: exl(?list, l). This is live, because it depends on the live permission l, and by passing this permission around we can build expressions that use the list.

Now lets go through the lines of the function and see how they change the context:

Line Statement perm_list perm_list₁ shr_pl v perm_list₂
1 
let v = &list[list.len() - 1];
 
exl(?list, l)
2 
list.push(4);
 
0 _
 
exl(?list, l)
 
shr(?list, perm_list₁)
 
&perm_list₁ u32
3 
print(*v);
 
0 _
 
0 _
 
shr(?list, perm_list₁)
 
&perm_list₁ u32
 
exl(?list, l)

The variables are listed out horizontally, and their state in the context is in the cells of each row. For example, the v variable is introduced on line 1 and becomes visible in line 2’s context with the &pl1 u32 type.

The first thing that this should highlight is that permission types in the context can change. That is to say, they’re flow typed and their types depend on the control flow of which operations have led to the current expression. This is the critical element that the type checker uses to see the conflict here: Line 2 consumes the perm_list1: exl(?list, l) to push to the list. It restores the exl(?list, l) of course, reborrowing the permission to use in the push method, but we’ve already broken the dependency of the reference that was made on line 1. Now, when we go to use the &pl1 u32 on line 3, we’ll find that the permission is damaged.

Understanding this pattern is the core intuition of the system - this would likely be a sufficient explanation for tutorial documentation to get users started in the language. Of course, for implementers it leaves many questions.

.. see more here later <3