Recently there has been some discussion about interprocedural borrowing conflicts in rust. This is something I’ve been fighting with a lot, especially while working on my SAT solver varisat. Around the time Niko Matsakis published his blog post about this, I realized that the existing workarounds I’ve been using in varisat have become a maintenance nightmare. Making simple changes to the code required lots of changes in the boilerplate needed to thread various references to the places where they’re needed.
While I didn’t think that a new language feature to solve this would be something I’d be willing to wait for, I decided to sit down and figure out how such a language feature would have to look like. I knew that I wanted something that allows for partial borrows across function calls. I also prefer this to work with annotations instead of global inference. While trying to come up with a coherent design that fits neatly into the existing type and trait system, I realized that most of what I wanted can be realized in stable rust today.
Luckily some time ago I came across the frunk crate. From there I learned a trick that I’d call inference driven metaprogramming. Rust requires trait implementations to be unambiguously non-overlapping. The rules for this just consider the implementing type, not any bounds. The trick I’ve learned from frunk is to add an additional type parameter to the trait that would otherwise have overlapping implementations. That type parameter is only used to disambiguate the implementations. As long as there is only one implementation, but this time considering bounds, rust’s powerful type inference will infer that extra type parameter. An example would be frunk’s Plucker trait, where the Index type parameter selects between the otherwise overlapping instances.
Equipped with this, I was able to implement type-level borrow checking logic. Today I’ve released a first version of this. The documentation contains a small tutorial. I also documented the type-level borrow checking logic, as the involved types and traits will appear in error messages. While I tried to optimize for readable error messages, I think every trait and type that could be part of one should be documented.
Using the library looks like this (see the tutorial for an explanation):
use partial_ref::*;
part!(pub Neighbors: Vec<Vec<usize>>);
part!(pub Colors: Vec<usize>);
part!(pub Weights: Vec<f32>);
#[derive(PartialRefTarget, Default)]
pub struct Graph {
#[part = "Neighbors"]
pub neighbors: Vec<Vec<usize>>,
#[part = "Colors"]
pub colors: Vec<usize>,
#[part = "Weights"]
pub weights: Vec<f32>,
}
let mut g = Graph::default();
let mut g_ref = g.into_partial_ref_mut();
g_ref.part_mut(Colors).extend(&[0, 1, 0]);
g_ref.part_mut(Weights).extend(&[0.25, 0.5, 0.75]);
g_ref.part_mut(Neighbors).push(vec![1, 2]);
g_ref.part_mut(Neighbors).push(vec![0, 2]);
g_ref.part_mut(Neighbors).push(vec![0, 1]);
pub fn add_color_to_weight(
mut g: partial!(Graph, mut Weights, Colors),
index: usize,
) {
g.part_mut(Weights)[index] += g.part(Colors)[index] as f32;
}
let (neighbors, mut g_ref) = g_ref.split_part_mut(Neighbors);
let (colors, mut g_ref) = g_ref.split_part(Colors);
for (edges, &color) in neighbors.iter_mut().zip(colors.iter()) {
edges.retain(|&neighbor| colors[neighbor] != color);
for &neighbor in edges.iter() {
add_color_to_weight(g_ref.borrow(), neighbor);
}
}
I have a bunch of additional features planned, but the next thing I want to do is to refactor my SAT solver to use this library.
I also hope that this library can be used to experiment with partial borrowing to gather experience for a possible future language extension.
