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 
- Paper (Extended Version): [2604.15290] Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
- Implementation: GitHub - SoftwareFoundationGroupAtKyotoU/pure-borrow: Pure Borrow: Linear Haskell Meets Rust-Style Borrowing · GitHub
- PLDI Program: Pure Borrow: Linear Haskell Meets Rust-Style Borrowing (PLDI 2026 - PLDI Research Papers) - 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:
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:
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:
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.
Use GHC 9.12.3 or higher when using REPL (EDITED)
If you want to use REPL to evaluate the above code, please use GHC 9.12.3 - GHC 9.10.3 and 9.12.2 contains a bug that results in segfaults.
(Once we considered the behaviour is our correctness bug, but @romes kindly pointing it out it was the bug in GHCi <9.12.2 and he fixed it in 9.12.3 onward. Thank you @romes!)
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!
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:
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!
