Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
summary
Pure Borrow implements Rust-style borrowing as a Linear Haskell library that runs on GHC, exposing a BO monad for lifetime-restricted mutation, borrow/split/reclaim APIs, and a parBO primitive for parallel access. The authors build a parallel in-place parallel quicksort that outperforms a naive sequential version, and they formalize a history-based model to justify reclaiming ownership without borrower-to-lender communication. Implementation and reusable artifacts are available, and the metatheory is promising but some proofs remain work in progress.
AI-written summary · about
chapters (11)
- 0:00Pure Borrow project intro
- 1:49Haskell vs Rust paradigms
- 2:56Pure Borrow overview
- 4:21Linear Haskell mutation
- 7:15Rust borrowing in Haskell
- 9:23BO monad for lifetimes
- 11:52Sharing and reborrowing
- 12:12Parallel quick sort case
- 14:05Metatheory and purity
- 16:13OCaml comparison and libraries
- 16:58Summary and Q&A
related talks
31mTowards a linear functional translation for borrowing
40mAgainst Borrowing: Own the forest, not the trees!
22mThe Rust Borrow Checker - A Deep Dive
53mThe Rust Borrow Checker - A Deep Dive
36mThe Rust Borrow Checker: A Deep Dive
31mAn Incremental Approach to the Semantics of Borrowing
26mThe first six years in the development of Polonius
50mRust's Borrow Checker Proven Correct!