{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreicyp464dewwjoigejobt3v7oadc532qtl775sjh4ue3knubjtfqla",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mk67jilr7qk2"
  },
  "path": "/t/pure-borrow-linear-haskell-meets-rust-style-borrowing/13975#post_1",
  "publishedAt": "2026-04-23T12:48:17.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "[2604.15290] Pure Borrow: Linear Haskell Meets Rust-Style Borrowing",
    "GitHub - SoftwareFoundationGroupAtKyotoU/pure-borrow: Pure Borrow: Linear Haskell Meets Rust-Style Borrowing · GitHub",
    "Pure Borrow: Linear Haskell Meets Rust-Style Borrowing (PLDI 2026 - PLDI Research Papers) - PLDI 2026",
    "RustHorn: CHC-based Verification for Rust Programs",
    "Experience Report: Linear Haskell enables Pure, Parallel, and In-place Fast Fourier Transformation",
    "Show and Tell",
    "Linearly Quantified Types paper",
    "Arnaud’s articles on Linear Constraints",
    "Linear constraints proposal",
    "github.com/SoftwareFoundationGroupAtKyotoU/pure-borrow",
    "src/Data/Vector/Mutable/Linear/Borrow.hs",
    "98634b264",
    "show original",
    "src/Control/Monad/Borrow/Pure/Internal.hs",
    "fb11ce913",
    "src/Control/Monad/Borrow/Pure.hs",
    "github.com/ghc-proposals/ghc-proposals",
    "Linear constraints proposal (#621)",
    "aspiwack",
    "+1737\n-0",
    "…",
    "github.com",
    "GitHub - konn/tamagoh",
    "@α",
    "@_",
    "@-XImpredicativeTypes"
  ],
  "textContent": "**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!\n\nWe are really pleased to announce the acceptance of our work, _Pure Borrow_ , at PLDI 2026\n\n  * Paper (Extended Version): [2604.15290] Pure Borrow: Linear Haskell Meets Rust-Style Borrowing\n  * Implementation: GitHub - SoftwareFoundationGroupAtKyotoU/pure-borrow: Pure Borrow: Linear Haskell Meets Rust-Style Borrowing · GitHub\n  * PLDI Program: Pure Borrow: Linear Haskell Meets Rust-Style Borrowing (PLDI 2026 - PLDI Research Papers) - PLDI 2026\n\n\n\nThis is joint work of Yusuke Matsushita, the first author of “RustHorn: CHC-based Verification for Rust Programs”, and I.\nI am mainly in charge of the implementation and Yusuke-san does the theoretical works.\n\n## Background\n\nLinear 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`.\nIn 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.\nThe guarantee of the uniqueness of the owner, or absence of alias, typically should allow a pure and deterministic _parallel_ computation.\nThis intuition once lead me to the exploration around the pure and parallel divide-and-conquer algorithm on arrays:\n\nExperience Report: Linear Haskell enables Pure, Parallel, and In-place Fast Fourier Transformation Show and Tell\n\n> 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…\n\nMeanwhile, Yusuke started Pure Borrow project and just stumbled upon my article above.\nHe reached out to me and we started to work together\n\n## What’s New in Pure Borrow?\n\nIn Pure Borrow, we bring the notion of Rust-style _borrows_ into the Linear Haskell realm.\n\nTo see the flavour, we give a simple parallel quicksort implementation in Pure Borrow:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Data/Vector/Mutable/Linear/Borrow.hs\n\n98634b264\n\n\n\n\n\n\n        273. qsort ::\n\n\n        274.   forall a α β.\n\n\n        275.   (Ord a, Copyable a, α >= β) =>\n\n\n        276.   {- | Cost for using parallelism. Halved after each recursive call,\n\n\n        277.   and stops parallelizing when it reaches 1.\n\n\n        278.   -}\n\n\n        279.   Word ->\n\n\n        280.   Mut α (Vector a) %1 ->\n\n\n        281.   BO β ()\n\n\n        282. qsort = go\n\n\n        283.   where\n\n\n        284.     go :: Word -> Mut α (Vector a) %1 -> BO β ()\n\n\n        285.     go budget v = case size v of\n\n\n        286.       (Ur 0, v) -> Control.pure $ consume v\n\n\n        287.       (Ur 1, v) -> Control.pure $ consume v\n\n\n        288.       (Ur n, v) -> Control.do\n\n\n        289.         let i = n `quot` 2\n\n\n        290.         (Ur pivot, v) <- copyAtMut i v\n\n\n        291.         (lo, hi) <- divide pivot v 0 n\n\n\n        292.         let b' = budget `quot` 2\n\n\n        293.         Control.void $ parIf (b' NonLinear.> 0) (go b' lo) (go b' hi)\n\n\n\n\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Data/Vector/Mutable/Linear/Borrow.hs\n\n98634b264\n\n\n\n\n\n\n        295. parIf :: Bool %1 -> BO α a %1 -> BO α b %1 -> BO α (a, b)\n\n\n        296. {-# INLINE parIf #-}\n\n\n        297. parIf p = if p then parBO else Control.liftA2 (,)\n\n\n        298.\n\n        299. divide ::\n\n\n        300.   (Ord a, Copyable a, α >= β) =>\n\n\n        301.   a ->\n\n\n        302.   Mut α (Vector a) %1 ->\n\n\n        303.   Int ->\n\n\n        304.   Int ->\n\n\n        305.   BO β (Mut α (Vector a), Mut α (Vector a))\n\n\n        306. divide pivot = partUp\n\n\n        307.   where\n\n\n        308.     partUp v l u\n\n\n        309.       | l < u = Control.do\n\n\n        310.           (Ur e, v) <- copyAtMut l v\n\n\n        311.           if e < pivot\n\n\n        312.             then partUp v (l + 1) u\n\n\n        313.             else partDown v l (u - 1)\n\n\n        314.       | otherwise = Control.pure $ splitAt l v\n\n\n\n\n\nThis file has been truncated. show original\n\n`BO α` is the monad that plays the central role in Pure Borrow.\nIt 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.\n\nNote 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.\nThis is safe and pure, thanks to Pure Borrow’s support of disjoint division of borrows.\n\n`Mut α x` is the _mutable borrow_ of a resource of type `x` - in particular, it is always bound and consumed linearly.\nIndeed, it is a special case of more general ‘Borrow’ type:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Control/Monad/Borrow/Pure/Internal.hs\n\nfb11ce913\n\n\n\n\n\n\n        226. -- | Mutable borrower, which is affine and can update the data.\n\n\n        227. type Mut :: Lifetime -> Type -> Type\n\n\n        228. type Mut α = Borrow 'Mut α\n\n\n\n\n\nThere is one more borrow type: `Share`:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Control/Monad/Borrow/Pure/Internal.hs\n\nfb11ce913\n\n\n\n\n\n\n        269. -- | Shared borrower, which is unrestricted but usually can only read from the data.\n\n\n        270. type Share :: Lifetime -> Type -> Type\n\n\n        271. type Share α = Borrow 'Share α\n\n\n\n\n\nSo, what’s the difference between mutable and shared borrows?\nFirst, both borrows a resource from its unique `Lend`er:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Control/Monad/Borrow/Pure/Internal.hs\n\nfb11ce913\n\n\n\n\n\n\n        294. -- | Lender, which can retrieve the lifetime at the lifetime @α@.\n\n\n        295. type Lend :: Lifetime -> Type -> Type\n\n\n        296. type Lend α = Alias ('Lend α)\n\n\n\n\n\nA `Mut α a` retains the _exclusive_ permission to mutate the borrowed resource of type `a` during the lifetime `α`.\nTogether with `Lend α a`, it can be introduced by `borrow`ing a bare resource:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Control/Monad/Borrow/Pure/Internal.hs\n\nfb11ce913\n\n\n\n\n\n\n        301. -- | Borrow a resource linearly and obtain the mutable borrow to it and 'Lend' witness to 'reclaim the resource to lend at the 'End' of the lifetime.\n\n\n        302. borrow :: forall α a. a %1 -> Linearly %1 -> (Mut α a, Lend α a)\n\n\n\n\n\nNote that they are bound linearly, making sure there is only one `Mut α`.\n\nOn 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`.\nThe primal introduction rule of `Share α a` is `share`ing it:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Control/Monad/Borrow/Pure/Internal.hs\n\nfb11ce913\n\n\n\n\n\n\n        311. -- | Shares a mutable borrow, invalidating the original one.\n\n\n        312. share :: Borrow k α a %1 -> Ur (Share α a)\n\n\n\n\n\nNote 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:\n\n\n    data Ur a where Ur :: a %'Many -> Ur a\n\n\nAs `share` consumes `Mut α a` linearly, it assumes there is no `Mut α a` left after the `shar`ing.\nIn this way, Pure Borrow allows both localized pure destructive updates and multiply-aliased shared read access to the resources.\n\nFurther, both types of borrow can be divided into pieces.\nOne such example is `splitAt` function used in the quicksort example above:\n\n\n    splitAt ::\n      Int %1 ->\n      Borrow bk α (Vector a) %1 ->\n      (Borrow bk α (Vector a), Borrow bk α (Vector a))\n\n\nSome 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:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Control/Monad/Borrow/Pure/Internal.hs\n\nfb11ce913\n\n\n\n\n\n\n        484. class Copyable a where\n\n\n        485.   copy :: Share α a %1 -> a\n\n\n\n\n\nWe also have a variant for random access to arrays:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Data/Vector/Mutable/Linear/Borrow.hs\n\nfb11ce913\n\n\n\n\n\n\n        259. copyAt :: (Copyable a, α >= β) => Int -> Share α (Vector a) -> BO β (Ur a)\n\n\n        260. copyAt i v = Control.do Ur s <- move Control.<$> get i v; Control.pure $ Ur $ copy s\n\n\n\n\n\nWhich is implemented in terms of `get` on an array and `copy`:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Data/Vector/Mutable/Linear/Borrow.hs\n\nfb11ce913\n\n\n\n\n\n\n        182. get ::\n\n\n        183.   (HasCallStack, α >= β) =>\n\n\n        184.   Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)\n\n\n\n\n\nBut, both `copyAt` and `copy` are expecting `Share α a` as its argument.\nHow can we apply it to `Mut α a` things?\nHere, the concept of sublifetime comes into a play, as in the implementation of `copyAtMut`:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Data/Vector/Mutable/Linear/Borrow.hs\n\nfb11ce913\n\n\n\n\n\n\n        262. copyAtMut :: forall a α β. (Copyable a, α >= β) => Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))\n\n\n        263. copyAtMut i v = upcast $ sharing @_ @α v $ copyAt i\n\n\n\n\n\nWhere, `sharing` combinator delimits the ephemeral sublifetime and share the given mutable borrow:\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Control/Monad/Borrow/Pure.hs\n\nfb11ce913\n\n\n\n\n\n\n        257. {- | Executes an operation on 'Share'd borrow in sub lifetime.\n\n\n        258. You may need @-XImpredicativeTypes@ extension to use this function.\n\n\n        259.\n\n        260. See also: '(<$~)', 'sharing'', and 'sharing_'.\n\n\n        261. -}\n\n\n        262. sharing ::\n\n\n        263.   forall α α' a r.\n\n\n        264.   Mut α a %1 ->\n\n\n        265.   (forall β. Share (β /\\ α) a -> BO (β /\\ α') r) %1 ->\n\n\n        266.   BO α' (r, Mut α a)\n\n\n\n\n\nIt is implemented in terms of `share` and `reborrow` (and `reborrow` in terms of more low-level primitives):\n\ngithub.com/SoftwareFoundationGroupAtKyotoU/pure-borrow\n\n#### src/Control/Monad/Borrow/Pure.hs\n\nfb11ce913\n\n\n\n\n\n\n        307. reborrowing ::\n\n\n        308.   Mut α a %1 ->\n\n\n        309.   (forall β. Mut (β /\\ α) a %1 -> BO (β /\\ α') r) %1 ->\n\n\n        310.   BO α' (r, Mut α a)\n\n\n\n\n\nAside from the quicksort example, here is a simple example demonstrating a mixed use of mutable and shared borrows:\n\n\n    example :: (Int, Int, Int, [Int])\n    example = linearly \\lin -> DataFlow.do\n      (lin, lin') <- dup lin\n      vec <- fromList [0, 1, 2] lin\n      runBO lin' \\ @α -> Control.do\n        let !(mvec, lend) = borrowLinearOnly vec\n        mvec <- modify 0 (+ 3) mvec\n        ((i0, i2), mvec) <- sharing mvec \\svec -> Control.do -- (*)\n          Ur i0 <- copyAt 0 svec\n          Ur i2 <- copyAt 2 svec\n          Control.pure (i0, i2)\n        mvec <- modify 2 (+ 5) mvec -- (a)\n        mvec <- modify 0 (* 4) mvec -- (b)\n        let !(Ur svec) = share mvec\n        Ur n <- copyAt 0 svec\n        pureAfter (i0, i2, n, unur $ toList (reclaim @α lend))\n\n\nThis 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.\nThis evaluates to `(3, 2, 12, [12, 1, 7])` as expected.\n\n> **Something is going wrong with GHCi…**\n>  Although the Pure Borrow programs work fine after the _compilation_ , we are observing that some vector programs with Pure Borrow (involving `copyAt` especially) segfaults when _interpreted_ inside GHCi and HLS Eval Plugin.\n>  We are working on this problem, so please be patient and please compile your Pure Borrow program to check the output meanwhile.\n\nThe `sharing` in the line `(*)` delimits the sublifetime, and share the contents of `mvec` temporarily for that lifetime.\nFurther 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 `svec`s and can call multiple times and read it for multiple times.\nAfter the sublifetime ends, the original `mvec` is returned and the process proceeds.\nNote that `svec` is bound nonlinearly, we do not need to return the value or consuming it explicitly.\n\nWe 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:\n\n\n        mvec <- reborrowing_ mvec \\mvec -> Control.do\n          let !(mvec1, mvec2) = LV.splitAt 2 mvec\n          consume Control.<$>\n            LV.modify 0 (+ 5) mvec2 `parBO` LV.modify 0 (* 4) mvec1\n\n\nThis time, the mutable borrow `mvec` is reborrowed into the sublifetime, then divided into two pieces.\nWe then modify each pieces _in parallel_ using `parBO` combinator, and discard the returned mutable borrows by calling `consume` combinator on the returned value.\nIn this way, we can discard the mutable borrows amidst in the sublifetime without worrying about leaking.\n\n## Shout out for Linear Constraints\n\nOur 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.\nManually threading them is somewhat cumbersome - and we are really missing for Linear Constraints to ease such handle token management!\n\ngithub.com/ghc-proposals/ghc-proposals\n\n####  Linear constraints proposal (#621)\n\n`master` ← `tweag:linear-constraints`\n\nopened 01:03PM - 21 Nov 23 UTC\n\n\n\n            aspiwack\n          \n\n\n+1737\n-0\n\n\nAdds 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.\n\nIndeed, the permission tokens cover all three types of (non-)linear constraints being proposed:\n\n  1. `End α` is a (nonlinear) constraint, which can just be expressed as an ordinary typeclass.\n  2. `Linearly` is a _duplicable_ linear constraint, which is one of the motivating examples of original Linear Constraints.\n  3. `Now α` is a _non-duplicable_ linear constraint.\n\n\n\nIndeed, `End α` is already made a typeclass in our actual implementation (we didn’t do so in the paper to avoid complication).\nThen, why not for `Linearly` and `Now α`? In this sense, we think our Pure Borrow can be yet another motivating application of Linear Constraints.\nAlso, it must be interesting to pursue the possibility to combine Pure Borrow and the permission model a la Linear Constraints paper.\n\nIf you feel the same, please  to the Linear Constraints proposal above!\n\n## Conclusions\n\nThe paper and implementation also comes with a more sophisticated work-stealing-based quicksort example.\nI’m also re-implementing e-graphs algorithms using Pure Borrow in the repository below:\n\ngithub.com\n\n### GitHub - konn/tamagoh\n\nContribute to konn/tamagoh development by creating an account on GitHub.\n\nAlthough `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.\n\nThe latter half of the paper discusses the theoretical foundation, and sketches the proof of the type safety, purity and leak-freedom of Pure Borrow.\nAlthough it is not spelled out rigorously, we believe our work bring new insights into this area.\n\nIf curious, please read our paper and implementation. Happy Linear Haskelling, and perhaps see you guys in Boulder!",
  "title": "Pure Borrow: Linear Haskell Meets Rust-Style Borrowing"
}