Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
This work addresses the challenge of integrating non-local borrowing from Rust into a purely functional language like Haskell, offering a new approach for safe, parallel mutation in a pure setting.
Pure Borrow introduces Rust-style borrowing into Linear Haskell, enabling safe parallel state mutation with affine mutable references inside pure computation, while preserving purity, lazy evaluation, first-class polymorphism, and leak freedom. The framework is implemented as a library and demonstrated with a parallel computing case study.
A promising approach to unifying functional and imperative programming paradigms is to localize mutation using linear or affine types. Haskell, a purely functional language, was recently extended with linear types by Bernardy et al., in the name of Linear Haskell. However, it remained unknown whether such a pure language could safely support non-local borrowing in the style of Rust, where each borrower can be freely split and dropped without direct communication of ownership back to the lender. We answer this question affirmatively with Pure Borrow, a novel framework that realizes Rust-style borrowing in Linear Haskell with purity. Notably, it features parallel state mutation with affine mutable references inside pure computation, unlike the IO and ST monads and existing Linear Haskell APIs. It also enjoys purity, lazy evaluation, first-class polymorphism and leak freedom, unlike Rust. We implement Pure Borrow simply as a library in Linear Haskell and demonstrate its power with a case study in parallel computing. We formalize the core of Pure Borrow and build a metatheory that works toward establishing safety, leak freedom and confluence, with a new, history-based model of borrowing.