TL;DR You can now use Rust-style mutable and shared borrows in Linear Haskell, within ST-like linear monad, BO, with pure, type-safe, and leak-freedom support of mutation and concurrency! It comes with flexible feature of multiple aliasing of shared borrows, delimiting lifetime regions, etc!
We are really pleased to announce the acceptance of our work, Pure Borrow, at PLDI 2026
This is joint work of Yusuke Matsushita, the first author of “RustHorn: CHC-based Verification for Rust Programs”, and I.
I am mainly in charge of the implementation and Yusuke-san does the theoretical works.
Background
Linear Haskell, i.e. today’s GHC with LinearTypes extension enabled, introduces the new arrow type a %1 -> b, which reads "If the application is consumed exactly once, then so is the argument of type a.
In particular, it ensures that there is exactly one owner of the resource bound by the function, and this allows us fine-grained resource management and do destructive updates purely.
The guarantee of the uniqueness of the owner, or absence of alias, typically should allow a pure and deterministic parallel computation.
This intuition once lead me to the exploration around the pure and parallel divide-and-conquer algorithm on arrays:
Motivation
Since I have read the Linearly Quantified Types paper and Arnaud’s articles on Linear Constraints, I’ve been very excited about how we will be able to use linear constraints to formulate borrowing subslices of arrays within Linear Haskell.
Linear Constraint is not available in GHC today, as the Linear constraints proposal by Arnaud has just been discussed (I :+1:ed a lot ):
Although it is not available in the current GHC, we should still be able to simulate linear constrain…
Meanwhile, Yusuke started Pure Borrow project and just stumbled upon my article above.
He reached out to me and we started to work together
What’s New in Pure Borrow?
In Pure Borrow, we bring the notion of Rust-style borrows into the Linear Haskell realm.
To see the flavour, we give a simple parallel quicksort implementation in Pure Borrow:
273. qsort ::
274. forall a α β.
275. (Ord a, Copyable a, α >= β) =>
276. {- | Cost for using parallelism. Halved after each recursive call,
277. and stops parallelizing when it reaches 1.
278. -}
279. Word ->
280. Mut α (Vector a) %1 ->
281. BO β ()
282. qsort = go
283. where
284. go :: Word -> Mut α (Vector a) %1 -> BO β ()
285. go budget v = case size v of
286. (Ur 0, v) -> Control.pure $ consume v
287. (Ur 1, v) -> Control.pure $ consume v
288. (Ur n, v) -> Control.do
289. let i = n `quot` 2
290. (Ur pivot, v) <- copyAtMut i v
291. (lo, hi) <- divide pivot v 0 n
292. let b' = budget `quot` 2
293. Control.void $ parIf (b' NonLinear.> 0) (go b' lo) (go b' hi)
295. parIf :: Bool %1 -> BO α a %1 -> BO α b %1 -> BO α (a, b)
296. {-# INLINE parIf #-}
297. parIf p = if p then parBO else Control.liftA2 (,)
298. - divide ::
- (Ord a, Copyable a, α >= β) =>
- a ->
- Mut α (Vector a) %1 ->
- Int ->
- Int ->
- BO β (Mut α (Vector a), Mut α (Vector a))
- divide pivot = partUp
- where
- partUp v l u
- | l < u = Control.do
- (Ur e, v) <- copyAtMut l v
- if e < pivot
- then partUp v (l + 1) u
- else partDown v l (u - 1)
- | otherwise = Control.pure $ splitAt l v
This file has been truncated. show original
BO α is the monad that plays the central role in Pure Borrow.
It is a linear-variant of the ST-monad, with each parameter α corresponds to the lifetime where the resources are borrowed for. It can also be viewed as a linear generalization of monadic regions, but for pure computation.
Note that parIf is a simple combinator to run the given two computations in parallel with parBO primtive when the condition is met, and runs sequentially otherwise.
This is safe and pure, thanks to Pure Borrow’s support of disjoint division of borrows.
Mut α x is the mutable borrow of a resource of type x - in particular, it is always bound and consumed linearly.
Indeed, it is a special case of more general ‘Borrow’ type:
There is one more borrow type: Share:
So, what’s the difference between mutable and shared borrows?
First, both borrows a resource from its unique Lender:
A Mut α a retains the exclusive permission to mutate the borrowed resource of type a during the lifetime α.
Together with Lend α a, it can be introduced by borrowing a bare resource:
Note that they are bound linearly, making sure there is only one Mut α.
On the other hand, Share α a can be aliased nonrestrictedly, i.e. they can be bound for any number of times, in the absence of Mut α a.
The primal introduction rule of Share α a is shareing it:
Note that Ur a is defined as follows, which means that value wrapped inside Ur can be used for as many times as possible (i.e. nonlinearly) after pattern matching on it:
data Ur a where Ur :: a %'Many -> Ur a
As share consumes Mut α a linearly, it assumes there is no Mut α a left after the sharing.
In this way, Pure Borrow allows both localized pure destructive updates and multiply-aliased shared read access to the resources.
Further, both types of borrow can be divided into pieces.
One such example is splitAt function used in the quicksort example above:
splitAt ::
Int %1 ->
Borrow bk α (Vector a) %1 ->
(Borrow bk α (Vector a), Borrow bk α (Vector a))
Some immutable types (e.g. primitive types such as Int or Bool, and the recursive type with those elements like Maybe Char or [Either Int (Bool, String)], etc.) can be copied into the direct value:
We also have a variant for random access to arrays:
Which is implemented in terms of get on an array and copy:
But, both copyAt and copy are expecting Share α a as its argument.
How can we apply it to Mut α a things?
Here, the concept of sublifetime comes into a play, as in the implementation of copyAtMut:
Where, sharing combinator delimits the ephemeral sublifetime and share the given mutable borrow:
257. {- | Executes an operation on 'Share'd borrow in sub lifetime.
258. You may need @-XImpredicativeTypes@ extension to use this function.
259. - See also: '(<$~)', 'sharing'', and 'sharing_'.
- -}
- sharing ::
- forall α α' a r.
- Mut α a %1 ->
- (forall β. Share (β /\ α) a -> BO (β /\ α') r) %1 ->
- BO α' (r, Mut α a)
It is implemented in terms of share and reborrow (and reborrow in terms of more low-level primitives):
Aside from the quicksort example, here is a simple example demonstrating a mixed use of mutable and shared borrows:
example :: (Int, Int, Int, [Int])
example = linearly \lin -> DataFlow.do
(lin, lin') <- dup lin
vec <- fromList [0, 1, 2] lin
runBO lin' \ @α -> Control.do
let !(mvec, lend) = borrowLinearOnly vec
mvec <- modify 0 (+ 3) mvec
((i0, i2), mvec) <- sharing mvec \svec -> Control.do -- (*)
Ur i0 <- copyAt 0 svec
Ur i2 <- copyAt 2 svec
Control.pure (i0, i2)
mvec <- modify 2 (+ 5) mvec -- (a)
mvec <- modify 0 (* 4) mvec -- (b)
let !(Ur svec) = share mvec
Ur n <- copyAt 0 svec
pureAfter (i0, i2, n, unur $ toList (reclaim @α lend))
This just allocates a mutable array with elements [0, 1, 2], multiply the first element, inspect first and third intermediate values, modify the third and first again, then retrieve the final value of the first value.
This evaluates to (3, 2, 12, [12, 1, 7]) as expected.
Something is going wrong with GHCi…
Although the Pure Borrow programs work fine after the compilation, we are observing that some vector programs with Pure Borrow (involvingcopyAtespecially) segfaults when interpreted inside GHCi and HLS Eval Plugin.
We are working on this problem, so please be patient and please compile your Pure Borrow program to check the output meanwhile.
The sharing in the line (*) delimits the sublifetime, and share the contents of mvec temporarily for that lifetime.
Further note that, although we thread through mutable share mvec manually (i.e. pass and given back by each function call on mvec), we don’t have to thread through shared borrow svecs and can call multiple times and read it for multiple times.
After the sublifetime ends, the original mvec is returned and the process proceeds.
Note that svec is bound nonlinearly, we do not need to return the value or consuming it explicitly.
We can go further. Now that mutation in (a) and (b) are on the disjoint parts, we can do it parallelly, by replacing lines (a) and (b) as follows:
mvec <- reborrowing_ mvec \mvec -> Control.do
let !(mvec1, mvec2) = LV.splitAt 2 mvec
consume Control.<$>
LV.modify 0 (+ 5) mvec2 `parBO` LV.modify 0 (* 4) mvec1
This time, the mutable borrow mvec is reborrowed into the sublifetime, then divided into two pieces.
We then modify each pieces in parallel using parBO combinator, and discard the returned mutable borrows by calling consume combinator on the returned value.
In this way, we can discard the mutable borrows amidst in the sublifetime without worrying about leaking.
Shout out for Linear Constraints
Our API makes extensive use of many permission tokens; we need Linearly token to ensure the safety of allocation, End α token to run the finalization after the lifetime ends, and, even though it doesn’t manifest in the high-level APIs, we need the unique Now α linear token for each lifetime α to ensure the uniqueness of the lifetime.
Manually threading them is somewhat cumbersome - and we are really missing for Linear Constraints to ease such handle token management!
master ← tweag:linear-constraints
opened 01:03PM - 21 Nov 23 UTC
Adds a linear fat arrow `%1 \=>` this is meant to greatly improve the ergonomics …of some of the APIs using linear types (it tends to apply to APIs based on typestate or related to mutation).
[Rendered](https://github.com/tweag/ghc-proposals/blob/linear-constraints/proposals/0621-linear-constraints.rst).
There are quite a bit of interactions to consider, let me know if I forgot (or misrepresent!) anything. The alternatives section is rather large, with variants in the design space that may be worth exploring. Don't hesitate to peruse and argue from one variant or other.
Indeed, the permission tokens cover all three types of (non-)linear constraints being proposed:
End αis a (nonlinear) constraint, which can just be expressed as an ordinary typeclass.Linearlyis a duplicable linear constraint, which is one of the motivating examples of original Linear Constraints.Now αis a non-duplicable linear constraint.
Indeed, End α is already made a typeclass in our actual implementation (we didn’t do so in the paper to avoid complication).
Then, why not for Linearly and Now α? In this sense, we think our Pure Borrow can be yet another motivating application of Linear Constraints.
Also, it must be interesting to pursue the possibility to combine Pure Borrow and the permission model a la Linear Constraints paper.
If you feel the same, please to the Linear Constraints proposal above!
Conclusions
The paper and implementation also comes with a more sophisticated work-stealing-based quicksort example.
I’m also re-implementing e-graphs algorithms using Pure Borrow in the repository below:
Contribute to konn/tamagoh development by creating an account on GitHub.
Although tamagoh is not so performant yet, it contains much more involved use cases of Pure Borrow, so you can grasp the taste of Pure Borrow. It also contains experiments around new interfaces for more involvd borrow division and effectful cloning.
The latter half of the paper discusses the theoretical foundation, and sketches the proof of the type safety, purity and leak-freedom of Pure Borrow.
Although it is not spelled out rigorously, we believe our work bring new insights into this area.
If curious, please read our paper and implementation. Happy Linear Haskelling, and perhaps see you guys in Boulder!